The alternating constant complex

Given an object X : C and endomorphisms φ, ψ : X ⟶ X such that φ ∘ ψ = ψ ∘ φ = 0, this file defines the periodic chain and cochain complexes ... ⟶ X --φ--> X --ψ--> X --φ--> X --ψ--> 0 and 0 ⟶ X --ψ--> X --φ--> X --ψ--> X --φ--> ... (or more generally for any complex shape c on ℕ where c.Rel i j implies i and j have different parity). We calculate the homology of these periodic complexes.

In particular, we show ... ⟶ X --𝟙--> X --0--> X --𝟙--> X --0--> X ⟶ 0 is homotopy equivalent to the single complex where X is in degree 0.

theorem ComplexShape.up_nat_odd_add {i j : ℕ} (h : (up ℕ).Rel i j) : Odd (i + j)

theorem ComplexShape.down_nat_odd_add {i j : ℕ} (h : (down ℕ).Rel i j) : Odd (i + j)

noncomputable def HomologicalComplex.alternatingConst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) : HomologicalComplex C c

Let c : ComplexShape ℕ be such that i j : ℕ have opposite parity if they are related by c. Let φ, ψ : A ⟶ A be such that φ ∘ ψ = ψ ∘ φ = 0. This is a complex of shape c whose objects are all A. For all i, j related by c, dᵢⱼ = φ when i is even, and dᵢⱼ = ψ when i is odd.

Equations

• HomologicalComplex.alternatingConst A hOdd hEven hc = { X := fun (n : ℕ) => A, d := fun (i j : ℕ) => if hij : c.Rel i j then if hi : Even i then φ else ψ else 0, shape := ⋯, d_comp_d' := ⋯ }

@[simp]

theorem HomologicalComplex.alternatingConst_X {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) (n : ℕ) : (alternatingConst A hOdd hEven hc).X n = A

@[simp]

theorem HomologicalComplex.alternatingConst_d {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) (i j : ℕ) : (alternatingConst A hOdd hEven hc).d i j = if c.Rel i j then if Even i then φ else ψ else 0

noncomputable def HomologicalComplex.alternatingConstScIsoEven {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) {i j k : ℕ} (hij : c.Rel i j) (hjk : c.Rel j k) (h : Even j) : (alternatingConst A hOdd hEven hc).sc' i j k ≅ { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven }

The i, j, kth short complex associated to the alternating constant complex on φ, ψ : A ⟶ A is A --ψ--> A --φ--> A when i ~ j, j ~ k and j is even.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HomologicalComplex.alternatingConstScIsoOdd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) {i j k : ℕ} (hij : c.Rel i j) (hjk : c.Rel j k) (h : Odd j) : (alternatingConst A hOdd hEven hc).sc' i j k ≅ { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd }

The i, j, kth short complex associated to the alternating constant complex on φ, ψ : A ⟶ A is A --φ--> A --ψ--> A when i ~ j, j ~ k and j is even.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HomologicalComplex.alternatingConst_iCycles_even_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Even j) : CategoryTheory.CategoryStruct.comp ((alternatingConst A hOdd hEven hc).iCycles j) φ = 0

@[simp]

theorem HomologicalComplex.alternatingConst_iCycles_even_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Even j) {Z : C} (h✝ : A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((alternatingConst A hOdd hEven hc).iCycles j) (CategoryTheory.CategoryStruct.comp φ h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem HomologicalComplex.alternatingConst_iCycles_even_comp_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Even j) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : CategoryTheory.ToType ((alternatingConst A hOdd hEven hc).cycles j)) : (CategoryTheory.ConcreteCategory.hom φ) ((CategoryTheory.ConcreteCategory.hom ((alternatingConst A hOdd hEven hc).iCycles j)) x) = (CategoryTheory.ConcreteCategory.hom 0) x

@[simp]

theorem HomologicalComplex.alternatingConst_iCycles_odd_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Odd j) : CategoryTheory.CategoryStruct.comp ((alternatingConst A hOdd hEven hc).iCycles j) ψ = 0

@[simp]

theorem HomologicalComplex.alternatingConst_iCycles_odd_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Odd j) {Z : C} (h✝ : A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((alternatingConst A hOdd hEven hc).iCycles j) (CategoryTheory.CategoryStruct.comp ψ h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem HomologicalComplex.alternatingConst_iCycles_odd_comp_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Odd j) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : CategoryTheory.ToType ((alternatingConst A hOdd hEven hc).cycles j)) : (CategoryTheory.ConcreteCategory.hom ψ) ((CategoryTheory.ConcreteCategory.hom ((alternatingConst A hOdd hEven hc).iCycles j)) x) = (CategoryTheory.ConcreteCategory.hom 0) x

noncomputable def HomologicalComplex.alternatingConstHomologyIsoEven {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Even j) : (alternatingConst A hOdd hEven hc).homology j ≅ { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven }.homology

The jth homology of the alternating constant complex on φ, ψ : A ⟶ A is the homology of A --ψ--> A --φ--> A when prev(j) ~ j, j ~ next(j) and j is even.

Equations

• HomologicalComplex.alternatingConstHomologyIsoEven A hOdd hEven hc hpj hnj h = CategoryTheory.ShortComplex.homologyMapIso (HomologicalComplex.alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)

noncomputable def HomologicalComplex.alternatingConstHomologyIsoOdd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [DecidableRel c.Rel] (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : ℕ} (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Odd j) : (alternatingConst A hOdd hEven hc).homology j ≅ { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd }.homology

The jth homology of the alternating constant complex on φ, ψ : A ⟶ A is the homology of A --φ--> A --ψ--> A when prev(j) ~ j, j ~ next(j) and j is odd.

Equations

• HomologicalComplex.alternatingConstHomologyIsoOdd A hOdd hEven hc hpj hnj h = CategoryTheory.ShortComplex.homologyMapIso (HomologicalComplex.alternatingConstScIsoOdd A hOdd hEven hc hpj hnj h)

noncomputable def ChainComplex.alternatingConst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor C (ChainComplex C ℕ)

The chain complex X ←0- X ←𝟙- X ←0- X ←𝟙- X ⋯. It is exact away from 0 and has homology X at 0.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ChainComplex.alternatingConst_map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (x✝ : ℕ) : (alternatingConst.map f).f x✝ = f

@[simp]

theorem ChainComplex.alternatingConst_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : alternatingConst.obj X = HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯

noncomputable def ChainComplex.alternatingConstHomologyDataEvenNEZero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (n : ℕ) (hn : Even n) (h₀ : n ≠ 0) : (HomologicalComplex.sc (alternatingConst.obj X) n).HomologyData

The n-th homology of the alternating constant complex is zero for non-zero even n.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ChainComplex.alternatingConstHomologyDataOdd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (n : ℕ) (hn : Odd n) : (HomologicalComplex.sc (alternatingConst.obj X) n).HomologyData

The n-th homology of the alternating constant complex is zero for odd n.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ChainComplex.alternatingConstHomologyDataZero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (n : ℕ) (hn : n = 0) : (HomologicalComplex.sc (alternatingConst.obj X) n).HomologyData

The n-th homology of the alternating constant complex is X for n = 0.

Equations

• ChainComplex.alternatingConstHomologyDataZero X n hn = CategoryTheory.ShortComplex.HomologyData.ofZeros (HomologicalComplex.sc (ChainComplex.alternatingConst.obj X) n) ⋯ ⋯

instance ChainComplex.instHasHomologyNatObjAlternatingConst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (n : ℕ) : HomologicalComplex.HasHomology (alternatingConst.obj X) n

theorem ChainComplex.alternatingConst_exactAt {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (n : ℕ) (hn : n ≠ 0) : HomologicalComplex.ExactAt (alternatingConst.obj X) n

The n-th homology of the alternating constant complex is X for n ≠ 0.

noncomputable def ChainComplex.alternatingConstHomologyZero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : C) : HomologicalComplex.homology (alternatingConst.obj X) 0 ≅ X

The n-th homology of the alternating constant complex is X for n = 0.

Equations

• ChainComplex.alternatingConstHomologyZero X = (ChainComplex.alternatingConstHomologyDataZero X 0 ChainComplex.alternatingConstHomologyZero._proof_1).left.homologyIso

noncomputable def AlgebraicTopology.alternatingFaceMapComplexConst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : (CategoryTheory.Functor.const SimplexCategoryᵒᵖ).comp (alternatingFaceMapComplex C) ≅ ChainComplex.alternatingConst

The alternating face complex of the constant complex is the alternating constant complex.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ChainComplex.alternatingConstHomotopyEquiv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : C) : HomotopyEquiv (alternatingConst.obj X) ((single₀ C).obj X)

alternatingConst.obj X is homotopy equivalent to the chain complex (single₀ C).obj X.

Equations

• One or more equations did not get rendered due to their size.