Chain homotopies

We define chain homotopies, and prove that homotopic chain maps induce the same map on homology.

def dNext {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (i : ι) : ((i j : ι) → C.X i ⟶ D.X j) →+ (C.X i ⟶ D.X i)

The composition of C.d i (c.next i) ≫ f (c.next i) i.

Equations

• dNext i = AddMonoidHom.mk' (fun (f : (i j : ι) → C.X i ⟶ D.X j) => CategoryTheory.CategoryStruct.comp (C.d i (c.next i)) (f (c.next i) i)) ⋯

def fromNext {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (i : ι) : ((i j : ι) → C.X i ⟶ D.X j) →+ (C.xNext i ⟶ D.X i)

f (c.next i) i.

Equations

• fromNext i = AddMonoidHom.mk' (fun (f : (i j : ι) → C.X i ⟶ D.X j) => f (c.next i) i) ⋯

@[simp]

theorem dNext_eq_dFrom_fromNext {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) (i : ι) : (dNext i) f = CategoryTheory.CategoryStruct.comp (C.dFrom i) ((fromNext i) f)

theorem dNext_eq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) {i i' : ι} (w : c.Rel i i') : (dNext i) f = CategoryTheory.CategoryStruct.comp (C.d i i') (f i' i)

theorem dNext_eq_zero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) (i : ι) (hi : ¬c.Rel i (c.next i)) : (dNext i) f = 0

@[simp]

theorem dNext_comp_left {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : C ⟶ D) (g : (i j : ι) → D.X i ⟶ E.X j) (i : ι) : ((dNext i) fun (i j : ι) => CategoryTheory.CategoryStruct.comp (f.f i) (g i j)) = CategoryTheory.CategoryStruct.comp (f.f i) ((dNext i) g)

@[simp]

theorem dNext_comp_right {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) (g : D ⟶ E) (i : ι) : ((dNext i) fun (i j : ι) => CategoryTheory.CategoryStruct.comp (f i j) (g.f j)) = CategoryTheory.CategoryStruct.comp ((dNext i) f) (g.f i)

def prevD {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (j : ι) : ((i j : ι) → C.X i ⟶ D.X j) →+ (C.X j ⟶ D.X j)

The composition f j (c.prev j) ≫ D.d (c.prev j) j.

Equations

• prevD j = AddMonoidHom.mk' (fun (f : (i j : ι) → C.X i ⟶ D.X j) => CategoryTheory.CategoryStruct.comp (f j (c.prev j)) (D.d (c.prev j) j)) ⋯

theorem prevD_eq_zero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) (i : ι) (hi : ¬c.Rel (c.prev i) i) : (prevD i) f = 0

def toPrev {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (j : ι) : ((i j : ι) → C.X i ⟶ D.X j) →+ (C.X j ⟶ D.xPrev j)

f j (c.prev j).

Equations

• toPrev j = AddMonoidHom.mk' (fun (f : (i j : ι) → C.X i ⟶ D.X j) => f j (c.prev j)) ⋯

@[simp]

theorem prevD_eq_toPrev_dTo {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) (j : ι) : (prevD j) f = CategoryTheory.CategoryStruct.comp ((toPrev j) f) (D.dTo j)

theorem prevD_eq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) {j j' : ι} (w : c.Rel j' j) : (prevD j) f = CategoryTheory.CategoryStruct.comp (f j j') (D.d j' j)

@[simp]

theorem prevD_comp_left {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : C ⟶ D) (g : (i j : ι) → D.X i ⟶ E.X j) (j : ι) : ((prevD j) fun (i j : ι) => CategoryTheory.CategoryStruct.comp (f.f i) (g i j)) = CategoryTheory.CategoryStruct.comp (f.f j) ((prevD j) g)

@[simp]

theorem prevD_comp_right {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) (g : D ⟶ E) (j : ι) : ((prevD j) fun (i j : ι) => CategoryTheory.CategoryStruct.comp (f i j) (g.f j)) = CategoryTheory.CategoryStruct.comp ((prevD j) f) (g.f j)

theorem dNext_nat {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (C D : ChainComplex V ℕ) (i : ℕ) (f : (i j : ℕ) → C.X i ⟶ D.X j) : (dNext i) f = CategoryTheory.CategoryStruct.comp (C.d i (i - 1)) (f (i - 1) i)

theorem prevD_nat {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (C D : CochainComplex V ℕ) (i : ℕ) (f : (i j : ℕ) → C.X i ⟶ D.X j) : (prevD i) f = CategoryTheory.CategoryStruct.comp (f i (i - 1)) (D.d (i - 1) i)

structure Homotopy {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f g : C ⟶ D) : Type (max u_1 v)

A homotopy h between chain maps f and g consists of components h i j : C.X i ⟶ D.X j which are zero unless c.Rel j i, satisfying the homotopy condition.

• hom : (i j : ι) → C.X i ⟶ D.X j
• zero : ∀ (i j : ι), ¬c.Rel j i → self.hom i j = 0
• comm : ∀ (i : ι), f.f i = (dNext i) self.hom + (prevD i) self.hom + g.f i

theorem Homotopy.ext {ι : Type u_1} {V : Type u} {inst✝ : CategoryTheory.Category.{v, u} V} {inst✝¹ : CategoryTheory.Preadditive V} {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} {x y : Homotopy f g} (hom : x.hom = y.hom) : x = y

def Homotopy.equivSubZero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} : Homotopy f g ≃ Homotopy (f - g) 0

f is homotopic to g iff f - g is homotopic to 0.

Equations

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

def Homotopy.ofEq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (h : f = g) : Homotopy f g

Equal chain maps are homotopic.

Equations

• Homotopy.ofEq h = { hom := 0, zero := ⋯, comm := ⋯ }

@[simp]

theorem Homotopy.ofEq_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (h : f = g) (i j : ι) : (Homotopy.ofEq h).hom i j = 0 i j

def Homotopy.refl {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ⟶ D) : Homotopy f f

Every chain map is homotopic to itself.

Equations

• Homotopy.refl f = Homotopy.ofEq ⋯

@[simp]

theorem Homotopy.refl_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ⟶ D) (i j : ι) : (Homotopy.refl f).hom i j = 0

def Homotopy.symm {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (h : Homotopy f g) : Homotopy g f

f is homotopic to g iff g is homotopic to f.

Equations

• h.symm = { hom := -h.hom, zero := ⋯, comm := ⋯ }

@[simp]

theorem Homotopy.symm_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (h : Homotopy f g) (i j : ι) : h.symm.hom i j = -h.hom i j

def Homotopy.trans {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {e f g : C ⟶ D} (h : Homotopy e f) (k : Homotopy f g) : Homotopy e g

homotopy is a transitive relation.

Equations

• h.trans k = { hom := h.hom + k.hom, zero := ⋯, comm := ⋯ }

@[simp]

theorem Homotopy.trans_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {e f g : C ⟶ D} (h : Homotopy e f) (k : Homotopy f g) (i j : ι) : (h.trans k).hom i j = h.hom i j + k.hom i j

def Homotopy.add {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f₁ g₁ f₂ g₂ : C ⟶ D} (h₁ : Homotopy f₁ g₁) (h₂ : Homotopy f₂ g₂) : Homotopy (f₁ + f₂) (g₁ + g₂)

the sum of two homotopies is a homotopy between the sum of the respective morphisms.

Equations

• h₁.add h₂ = { hom := h₁.hom + h₂.hom, zero := ⋯, comm := ⋯ }

@[simp]

theorem Homotopy.add_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f₁ g₁ f₂ g₂ : C ⟶ D} (h₁ : Homotopy f₁ g₁) (h₂ : Homotopy f₂ g₂) (i j : ι) : (h₁.add h₂).hom i j = h₁.hom i j + h₂.hom i j

def Homotopy.smul {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} {R : Type u_2} [Semiring R] [CategoryTheory.Linear R V] (h : Homotopy f g) (a : R) : Homotopy (a • f) (a • g)

the scalar multiplication of an homotopy

Equations

• h.smul a = { hom := fun (i j : ι) => a • h.hom i j, zero := ⋯, comm := ⋯ }

@[simp]

theorem Homotopy.smul_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} {R : Type u_2} [Semiring R] [CategoryTheory.Linear R V] (h : Homotopy f g) (a : R) (i j : ι) : (h.smul a).hom i j = a • h.hom i j

def Homotopy.compRight {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomologicalComplex V c} {e f : C ⟶ D} (h : Homotopy e f) (g : D ⟶ E) : Homotopy (CategoryTheory.CategoryStruct.comp e g) (CategoryTheory.CategoryStruct.comp f g)

homotopy is closed under composition (on the right)

Equations

• h.compRight g = { hom := fun (i j : ι) => CategoryTheory.CategoryStruct.comp (h.hom i j) (g.f j), zero := ⋯, comm := ⋯ }

@[simp]

theorem Homotopy.compRight_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomologicalComplex V c} {e f : C ⟶ D} (h : Homotopy e f) (g : D ⟶ E) (i j : ι) : (h.compRight g).hom i j = CategoryTheory.CategoryStruct.comp (h.hom i j) (g.f j)

def Homotopy.compLeft {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomologicalComplex V c} {f g : D ⟶ E} (h : Homotopy f g) (e : C ⟶ D) : Homotopy (CategoryTheory.CategoryStruct.comp e f) (CategoryTheory.CategoryStruct.comp e g)

homotopy is closed under composition (on the left)

Equations

• h.compLeft e = { hom := fun (i j : ι) => CategoryTheory.CategoryStruct.comp (e.f i) (h.hom i j), zero := ⋯, comm := ⋯ }

@[simp]

theorem Homotopy.compLeft_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomologicalComplex V c} {f g : D ⟶ E} (h : Homotopy f g) (e : C ⟶ D) (i j : ι) : (h.compLeft e).hom i j = CategoryTheory.CategoryStruct.comp (e.f i) (h.hom i j)

def Homotopy.comp {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c} {f₁ g₁ : C₁ ⟶ C₂} {f₂ g₂ : C₂ ⟶ C₃} (h₁ : Homotopy f₁ g₁) (h₂ : Homotopy f₂ g₂) : Homotopy (CategoryTheory.CategoryStruct.comp f₁ f₂) (CategoryTheory.CategoryStruct.comp g₁ g₂)

homotopy is closed under composition

Equations

• h₁.comp h₂ = (h₁.compRight f₂).trans (h₂.compLeft g₁)

@[simp]

theorem Homotopy.comp_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c} {f₁ g₁ : C₁ ⟶ C₂} {f₂ g₂ : C₂ ⟶ C₃} (h₁ : Homotopy f₁ g₁) (h₂ : Homotopy f₂ g₂) (i j : ι) : (h₁.comp h₂).hom i j = CategoryTheory.CategoryStruct.comp (h₁.hom i j) (f₂.f j) + CategoryTheory.CategoryStruct.comp (g₁.f i) (h₂.hom i j)

def Homotopy.compRightId {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f : C ⟶ C} (h : Homotopy f (CategoryTheory.CategoryStruct.id C)) (g : C ⟶ D) : Homotopy (CategoryTheory.CategoryStruct.comp f g) g

a variant of Homotopy.compRight useful for dealing with homotopy equivalences.

Equations

• h.compRightId g = (h.compRight g).trans (Homotopy.ofEq ⋯)

@[simp]

theorem Homotopy.compRightId_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f : C ⟶ C} (h : Homotopy f (CategoryTheory.CategoryStruct.id C)) (g : C ⟶ D) (i j : ι) : (h.compRightId g).hom i j = CategoryTheory.CategoryStruct.comp (h.hom i j) (g.f j)

def Homotopy.compLeftId {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f : D ⟶ D} (h : Homotopy f (CategoryTheory.CategoryStruct.id D)) (g : C ⟶ D) : Homotopy (CategoryTheory.CategoryStruct.comp g f) g

a variant of Homotopy.compLeft useful for dealing with homotopy equivalences.

Equations

• h.compLeftId g = (h.compLeft g).trans (Homotopy.ofEq ⋯)

@[simp]

theorem Homotopy.compLeftId_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f : D ⟶ D} (h : Homotopy f (CategoryTheory.CategoryStruct.id D)) (g : C ⟶ D) (i j : ι) : (h.compLeftId g).hom i j = CategoryTheory.CategoryStruct.comp (g.f i) (h.hom i j)

Null homotopic maps can be constructed using the formula hd+dh. We show that these morphisms are homotopic to 0 and provide some convenient simplification lemmas that give a degreewise description of hd+dh, depending on whether we have two differentials going to and from a certain degree, only one, or none.

def Homotopy.nullHomotopicMap {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (hom : (i j : ι) → C.X i ⟶ D.X j) : C ⟶ D

The null homotopic map associated to a family hom of morphisms C_i ⟶ D_j. This is the same datum as for the field hom in the structure Homotopy. For this definition, we do not need the field zero of that structure as this definition uses only the maps C_i ⟶ C_j when c.Rel j i.

Equations

• Homotopy.nullHomotopicMap hom = { f := fun (i : ι) => (dNext i) hom + (prevD i) hom, comm' := ⋯ }

def Homotopy.nullHomotopicMap' {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) : C ⟶ D

Variant of nullHomotopicMap where the input consists only of the relevant maps C_i ⟶ D_j such that c.Rel j i.

Equations

• Homotopy.nullHomotopicMap' h = Homotopy.nullHomotopicMap fun (i j : ι) => dite (c.Rel j i) (h i j) fun (x : ¬c.Rel j i) => 0

theorem Homotopy.nullHomotopicMap_comp {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomologicalComplex V c} (hom : (i j : ι) → C.X i ⟶ D.X j) (g : D ⟶ E) : CategoryTheory.CategoryStruct.comp (Homotopy.nullHomotopicMap hom) g = Homotopy.nullHomotopicMap fun (i j : ι) => CategoryTheory.CategoryStruct.comp (hom i j) (g.f j)

Compatibility of nullHomotopicMap with the postcomposition by a morphism of complexes.

theorem Homotopy.nullHomotopicMap'_comp {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomologicalComplex V c} (hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) (g : D ⟶ E) : CategoryTheory.CategoryStruct.comp (Homotopy.nullHomotopicMap' hom) g = Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) => CategoryTheory.CategoryStruct.comp (hom i j hij) (g.f j)

Compatibility of nullHomotopicMap' with the postcomposition by a morphism of complexes.

theorem Homotopy.comp_nullHomotopicMap {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : C ⟶ D) (hom : (i j : ι) → D.X i ⟶ E.X j) : CategoryTheory.CategoryStruct.comp f (Homotopy.nullHomotopicMap hom) = Homotopy.nullHomotopicMap fun (i j : ι) => CategoryTheory.CategoryStruct.comp (f.f i) (hom i j)

Compatibility of nullHomotopicMap with the precomposition by a morphism of complexes.

theorem Homotopy.comp_nullHomotopicMap' {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : C ⟶ D) (hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)) : CategoryTheory.CategoryStruct.comp f (Homotopy.nullHomotopicMap' hom) = Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) => CategoryTheory.CategoryStruct.comp (f.f i) (hom i j hij)

Compatibility of nullHomotopicMap' with the precomposition by a morphism of complexes.

theorem Homotopy.map_nullHomotopicMap {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (G : CategoryTheory.Functor V W) [G.Additive] (hom : (i j : ι) → C.X i ⟶ D.X j) : (G.mapHomologicalComplex c).map (Homotopy.nullHomotopicMap hom) = Homotopy.nullHomotopicMap fun (i j : ι) => G.map (hom i j)

Compatibility of nullHomotopicMap with the application of additive functors

theorem Homotopy.map_nullHomotopicMap' {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (G : CategoryTheory.Functor V W) [G.Additive] (hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) : (G.mapHomologicalComplex c).map (Homotopy.nullHomotopicMap' hom) = Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) => G.map (hom i j hij)

Compatibility of nullHomotopicMap' with the application of additive functors

def Homotopy.nullHomotopy {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (hom : (i j : ι) → C.X i ⟶ D.X j) (zero : ∀ (i j : ι), ¬c.Rel j i → hom i j = 0) : Homotopy (Homotopy.nullHomotopicMap hom) 0

Tautological construction of the Homotopy to zero for maps constructed by nullHomotopicMap, at least when we have the zero condition.

Equations

• Homotopy.nullHomotopy hom zero = { hom := hom, zero := zero, comm := ⋯ }

@[simp]

theorem Homotopy.nullHomotopy_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (hom : (i j : ι) → C.X i ⟶ D.X j) (zero : ∀ (i j : ι), ¬c.Rel j i → hom i j = 0) (i j : ι) : (Homotopy.nullHomotopy hom zero).hom i j = hom i j

def Homotopy.nullHomotopy' {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) : Homotopy (Homotopy.nullHomotopicMap' h) 0

Homotopy to zero for maps constructed with nullHomotopicMap'

Equations

• Homotopy.nullHomotopy' h = Homotopy.nullHomotopy (fun (i j : ι) => dite (c.Rel j i) (h i j) fun (x : ¬c.Rel j i) => 0) ⋯

@[simp]

theorem Homotopy.nullHomotopy'_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) (i j : ι) : (Homotopy.nullHomotopy' h).hom i j = dite (c.Rel j i) (h i j) fun (x : ¬c.Rel j i) => 0

This lemma and the following ones can be used in order to compute the degreewise morphisms induced by the null homotopic maps constructed with nullHomotopicMap or nullHomotopicMap'

@[simp]

theorem Homotopy.nullHomotopicMap_f {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₂ k₁ k₀ : ι} (r₂₁ : c.Rel k₂ k₁) (r₁₀ : c.Rel k₁ k₀) (hom : (i j : ι) → C.X i ⟶ D.X j) : (Homotopy.nullHomotopicMap hom).f k₁ = CategoryTheory.CategoryStruct.comp (C.d k₁ k₀) (hom k₀ k₁) + CategoryTheory.CategoryStruct.comp (hom k₁ k₂) (D.d k₂ k₁)

@[simp]

theorem Homotopy.nullHomotopicMap'_f {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₂ k₁ k₀ : ι} (r₂₁ : c.Rel k₂ k₁) (r₁₀ : c.Rel k₁ k₀) (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) : (Homotopy.nullHomotopicMap' h).f k₁ = CategoryTheory.CategoryStruct.comp (C.d k₁ k₀) (h k₀ k₁ r₁₀) + CategoryTheory.CategoryStruct.comp (h k₁ k₂ r₂₁) (D.d k₂ k₁)

@[simp]

theorem Homotopy.nullHomotopicMap_f_of_not_rel_left {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₁ k₀ : ι} (r₁₀ : c.Rel k₁ k₀) (hk₀ : ∀ (l : ι), ¬c.Rel k₀ l) (hom : (i j : ι) → C.X i ⟶ D.X j) : (Homotopy.nullHomotopicMap hom).f k₀ = CategoryTheory.CategoryStruct.comp (hom k₀ k₁) (D.d k₁ k₀)

@[simp]

theorem Homotopy.nullHomotopicMap'_f_of_not_rel_left {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₁ k₀ : ι} (r₁₀ : c.Rel k₁ k₀) (hk₀ : ∀ (l : ι), ¬c.Rel k₀ l) (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) : (Homotopy.nullHomotopicMap' h).f k₀ = CategoryTheory.CategoryStruct.comp (h k₀ k₁ r₁₀) (D.d k₁ k₀)

@[simp]

theorem Homotopy.nullHomotopicMap_f_of_not_rel_right {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₁ k₀ : ι} (r₁₀ : c.Rel k₁ k₀) (hk₁ : ∀ (l : ι), ¬c.Rel l k₁) (hom : (i j : ι) → C.X i ⟶ D.X j) : (Homotopy.nullHomotopicMap hom).f k₁ = CategoryTheory.CategoryStruct.comp (C.d k₁ k₀) (hom k₀ k₁)

@[simp]

theorem Homotopy.nullHomotopicMap'_f_of_not_rel_right {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₁ k₀ : ι} (r₁₀ : c.Rel k₁ k₀) (hk₁ : ∀ (l : ι), ¬c.Rel l k₁) (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) : (Homotopy.nullHomotopicMap' h).f k₁ = CategoryTheory.CategoryStruct.comp (C.d k₁ k₀) (h k₀ k₁ r₁₀)

@[simp]

theorem Homotopy.nullHomotopicMap_f_eq_zero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₀ : ι} (hk₀ : ∀ (l : ι), ¬c.Rel k₀ l) (hk₀' : ∀ (l : ι), ¬c.Rel l k₀) (hom : (i j : ι) → C.X i ⟶ D.X j) : (Homotopy.nullHomotopicMap hom).f k₀ = 0

@[simp]

theorem Homotopy.nullHomotopicMap'_f_eq_zero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₀ : ι} (hk₀ : ∀ (l : ι), ¬c.Rel k₀ l) (hk₀' : ∀ (l : ι), ¬c.Rel l k₀) (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) : (Homotopy.nullHomotopicMap' h).f k₀ = 0

Homotopy.mkInductive allows us to build a homotopy of chain complexes inductively, so that as we construct each component, we have available the previous two components, and the fact that they satisfy the homotopy condition.

To simplify the situation, we only construct homotopies of the form Homotopy e 0. Homotopy.equivSubZero can provide the general case.

Notice however, that this construction does not have particularly good definitional properties: we have to insert eqToHom in several places. Hopefully this is okay in most applications, where we only need to have the existence of some homotopy.

@[simp]

theorem Homotopy.prevD_chainComplex {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : ChainComplex V ℕ} (f : (i j : ℕ) → P.X i ⟶ Q.X j) (j : ℕ) : (prevD j) f = CategoryTheory.CategoryStruct.comp (f j (j + 1)) (Q.d (j + 1) j)

@[simp]

theorem Homotopy.dNext_succ_chainComplex {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : ChainComplex V ℕ} (f : (i j : ℕ) → P.X i ⟶ Q.X j) (i : ℕ) : (dNext (i + 1)) f = CategoryTheory.CategoryStruct.comp (P.d (i + 1) i) (f i (i + 1))

@[simp]

theorem Homotopy.dNext_zero_chainComplex {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : ChainComplex V ℕ} (f : (i j : ℕ) → P.X i ⟶ Q.X j) : (dNext 0) f = 0

def Homotopy.mkInductiveAux₁ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1) (one : P.X 1 ⟶ Q.X 2) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1)) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X (n + 1)) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) → (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) (n : ℕ) : (f : P.X n ⟶ Q.X (n + 1)) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))

An auxiliary construction for mkInductive.

Here we build by induction a family of diagrams, but don't require at the type level that these successive diagrams actually agree. They do in fact agree, and we then capture that at the type level (i.e. by constructing a homotopy) in mkInductive.

At this stage, we don't check the homotopy condition in degree 0, because it "falls off the end", and is easier to treat using xNext and xPrev, which we do in mkInductiveAux₂.

Equations

• One or more equations did not get rendered due to their size.
• Homotopy.mkInductiveAux₁ e zero one comm_one succ 0 = ⟨zero, ⟨one, comm_one⟩⟩
• Homotopy.mkInductiveAux₁ e zero one comm_one succ 1 = ⟨one, ⟨(succ 0 ⟨zero, ⟨one, comm_one⟩⟩).fst, ⋯⟩⟩

def Homotopy.mkInductiveAux₂ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 ⟶ Q.X 2) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1)) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X (n + 1)) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) → (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) (n : ℕ) : (f : HomologicalComplex.xNext P n ⟶ Q.X n) ×' (f' : P.X n ⟶ HomologicalComplex.xPrev Q n) ×' e.f n = CategoryTheory.CategoryStruct.comp (HomologicalComplex.dFrom P n) f + CategoryTheory.CategoryStruct.comp f' (HomologicalComplex.dTo Q n)

An auxiliary construction for mkInductive.

Equations

• One or more equations did not get rendered due to their size.
• Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ 0 = ⟨0, ⟨CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.xPrevIso Q Homotopy.mkInductiveAux₂.proof_1).inv, ⋯⟩⟩

@[simp]

theorem Homotopy.mkInductiveAux₂_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 ⟶ Q.X 2) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1)) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X (n + 1)) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) → (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) : Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ 0 = ⟨0, ⟨CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.xPrevIso Q ⋯).inv, ⋯⟩⟩

@[simp]

theorem Homotopy.mkInductiveAux₂_add_one {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 ⟶ Q.X 2) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1)) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X (n + 1)) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) → (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) (n : ℕ) : Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ (n + 1) = let I := Homotopy.mkInductiveAux₁ e zero one comm_one succ n; ⟨CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P ⋯).hom I.fst, ⟨CategoryTheory.CategoryStruct.comp I.snd.fst (HomologicalComplex.xPrevIso Q ⋯).inv, ⋯⟩⟩

theorem Homotopy.mkInductiveAux₃ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 ⟶ Q.X 2) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1)) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X (n + 1)) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) → (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) (i j : ℕ) (h : i + 1 = j) : CategoryTheory.CategoryStruct.comp (Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst (HomologicalComplex.xPrevIso Q h).hom = CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P h).inv (Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ j).fst

def Homotopy.mkInductive {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 ⟶ Q.X 2) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1)) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X (n + 1)) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) → (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) : Homotopy e 0

A constructor for a Homotopy e 0, for e a chain map between ℕ-indexed chain complexes, working by induction.

You need to provide the components of the homotopy in degrees 0 and 1, show that these satisfy the homotopy condition, and then give a construction of each component, and the fact that it satisfies the homotopy condition, using as an inductive hypothesis the data and homotopy condition for the previous two components.

Equations

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

Homotopy.mkCoinductive allows us to build a homotopy of cochain complexes inductively, so that as we construct each component, we have available the previous two components, and the fact that they satisfy the homotopy condition.

@[simp]

theorem Homotopy.dNext_cochainComplex {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : CochainComplex V ℕ} (f : (i j : ℕ) → P.X i ⟶ Q.X j) (j : ℕ) : (dNext j) f = CategoryTheory.CategoryStruct.comp (P.d j (j + 1)) (f (j + 1) j)

@[simp]

theorem Homotopy.prevD_succ_cochainComplex {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : CochainComplex V ℕ} (f : (i j : ℕ) → P.X i ⟶ Q.X j) (i : ℕ) : (prevD (i + 1)) f = CategoryTheory.CategoryStruct.comp (f (i + 1) i) (Q.d i (i + 1))

@[simp]

theorem Homotopy.prevD_zero_cochainComplex {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : CochainComplex V ℕ} (f : (i j : ℕ) → P.X i ⟶ Q.X j) : (prevD 0) f = 0

def Homotopy.mkCoinductiveAux₁ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0) (one : P.X 2 ⟶ Q.X 1) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one) (succ : (n : ℕ) → (p : (f : P.X (n + 1) ⟶ Q.X n) ×' (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') → (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') (n : ℕ) : (f : P.X (n + 1) ⟶ Q.X n) ×' (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f'

An auxiliary construction for mkCoinductive.

Here we build by induction a family of diagrams, but don't require at the type level that these successive diagrams actually agree. They do in fact agree, and we then capture that at the type level (i.e. by constructing a homotopy) in mkCoinductive.

At this stage, we don't check the homotopy condition in degree 0, because it "falls off the end", and is easier to treat using xNext and xPrev, which we do in mkInductiveAux₂.

Equations

• One or more equations did not get rendered due to their size.
• Homotopy.mkCoinductiveAux₁ e zero one comm_one succ 0 = ⟨zero, ⟨one, comm_one⟩⟩
• Homotopy.mkCoinductiveAux₁ e zero one comm_one succ 1 = ⟨one, ⟨(succ 0 ⟨zero, ⟨one, comm_one⟩⟩).fst, ⋯⟩⟩

def Homotopy.mkCoinductiveAux₂ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 ⟶ Q.X 1) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one) (succ : (n : ℕ) → (p : (f : P.X (n + 1) ⟶ Q.X n) ×' (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') → (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') (n : ℕ) : (f : P.X n ⟶ HomologicalComplex.xPrev Q n) ×' (f' : HomologicalComplex.xNext P n ⟶ Q.X n) ×' e.f n = CategoryTheory.CategoryStruct.comp f (HomologicalComplex.dTo Q n) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.dFrom P n) f'

An auxiliary construction for mkInductive.

Equations

• One or more equations did not get rendered due to their size.
• Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0 = ⟨0, ⟨CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P Homotopy.mkCoinductiveAux₂.proof_1).hom zero, ⋯⟩⟩

@[simp]

theorem Homotopy.mkCoinductiveAux₂_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 ⟶ Q.X 1) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one) (succ : (n : ℕ) → (p : (f : P.X (n + 1) ⟶ Q.X n) ×' (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') → (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') : Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0 = ⟨0, ⟨CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P ⋯).hom zero, ⋯⟩⟩

@[simp]

theorem Homotopy.mkCoinductiveAux₂_add_one {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 ⟶ Q.X 1) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one) (succ : (n : ℕ) → (p : (f : P.X (n + 1) ⟶ Q.X n) ×' (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') → (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') (n : ℕ) : Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ (n + 1) = let I := Homotopy.mkCoinductiveAux₁ e zero one comm_one succ n; ⟨CategoryTheory.CategoryStruct.comp I.fst (HomologicalComplex.xPrevIso Q ⋯).inv, ⟨CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P ⋯).hom I.snd.fst, ⋯⟩⟩

theorem Homotopy.mkCoinductiveAux₃ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 ⟶ Q.X 1) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one) (succ : (n : ℕ) → (p : (f : P.X (n + 1) ⟶ Q.X n) ×' (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') → (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') (i j : ℕ) (h : i + 1 = j) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P h).inv (Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst = CategoryTheory.CategoryStruct.comp (Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst (HomologicalComplex.xPrevIso Q h).hom

def Homotopy.mkCoinductive {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 ⟶ Q.X 1) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one) (succ : (n : ℕ) → (p : (f : P.X (n + 1) ⟶ Q.X n) ×' (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') → (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') : Homotopy e 0

A constructor for a Homotopy e 0, for e a chain map between ℕ-indexed cochain complexes, working by induction.

You need to provide the components of the homotopy in degrees 0 and 1, show that these satisfy the homotopy condition, and then give a construction of each component, and the fact that it satisfies the homotopy condition, using as an inductive hypothesis the data and homotopy condition for the previous two components.

Equations

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

structure HomotopyEquiv {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (C D : HomologicalComplex V c) : Type (max u_1 v)

A homotopy equivalence between two chain complexes consists of a chain map each way, and homotopies from the compositions to the identity chain maps.

Note that this contains data; arguably it might be more useful for many applications if we truncated it to a Prop.

• hom : C ⟶ D
• inv : D ⟶ C
• homotopyHomInvId : Homotopy (CategoryTheory.CategoryStruct.comp self.hom self.inv) (CategoryTheory.CategoryStruct.id C)
• homotopyInvHomId : Homotopy (CategoryTheory.CategoryStruct.comp self.inv self.hom) (CategoryTheory.CategoryStruct.id D)

def HomologicalComplex.homotopyEquivalences {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : CategoryTheory.MorphismProperty (HomologicalComplex V c)

The morphism property on HomologicalComplex V c given by homotopy equivalences.

Equations

• HomologicalComplex.homotopyEquivalences V c f = ∃ (e : HomotopyEquiv X Y), e.hom = f

def HomotopyEquiv.refl {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (C : HomologicalComplex V c) : HomotopyEquiv C C

Any complex is homotopy equivalent to itself.

Equations

• HomotopyEquiv.refl C = { hom := CategoryTheory.CategoryStruct.id C, inv := CategoryTheory.CategoryStruct.id C, homotopyHomInvId := Homotopy.ofEq ⋯, homotopyInvHomId := Homotopy.ofEq ⋯ }

instance HomotopyEquiv.instInhabited {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} : Inhabited (HomotopyEquiv C C)

Equations

• HomotopyEquiv.instInhabited = { default := HomotopyEquiv.refl C }

def HomotopyEquiv.symm {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D) : HomotopyEquiv D C

Being homotopy equivalent is a symmetric relation.

Equations

• f.symm = { hom := f.inv, inv := f.hom, homotopyHomInvId := f.homotopyInvHomId, homotopyInvHomId := f.homotopyHomInvId }

def HomotopyEquiv.trans {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : HomotopyEquiv C D) (g : HomotopyEquiv D E) : HomotopyEquiv C E

Homotopy equivalence is a transitive relation.

Equations

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

def HomotopyEquiv.ofIso {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ≅ D) : HomotopyEquiv C D

An isomorphism of complexes induces a homotopy equivalence.

Equations

• HomotopyEquiv.ofIso f = { hom := f.hom, inv := f.inv, homotopyHomInvId := Homotopy.ofEq ⋯, homotopyInvHomId := Homotopy.ofEq ⋯ }

def CategoryTheory.Functor.mapHomotopy {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] {f g : C ⟶ D} (h : Homotopy f g) : Homotopy ((F.mapHomologicalComplex c).map f) ((F.mapHomologicalComplex c).map g)

An additive functor takes homotopies to homotopies.

Equations

• F.mapHomotopy h = { hom := fun (i j : ι) => F.map (h.hom i j), zero := ⋯, comm := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapHomotopy_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] {f g : C ⟶ D} (h : Homotopy f g) (i j : ι) : (F.mapHomotopy h).hom i j = F.map (h.hom i j)

def CategoryTheory.Functor.mapHomotopyEquiv {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (h : HomotopyEquiv C D) : HomotopyEquiv ((F.mapHomologicalComplex c).obj C) ((F.mapHomologicalComplex c).obj D)

An additive functor preserves homotopy equivalences.

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapHomotopyEquiv_homotopyHomInvId {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (h : HomotopyEquiv C D) : (F.mapHomotopyEquiv h).homotopyHomInvId = ⋯.mpr (⋯.mpr (F.mapHomotopy h.homotopyHomInvId))

@[simp]

theorem CategoryTheory.Functor.mapHomotopyEquiv_homotopyInvHomId {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (h : HomotopyEquiv C D) : (F.mapHomotopyEquiv h).homotopyInvHomId = ⋯.mpr (⋯.mpr (F.mapHomotopy h.homotopyInvHomId))

@[simp]

theorem CategoryTheory.Functor.mapHomotopyEquiv_inv {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (h : HomotopyEquiv C D) : (F.mapHomotopyEquiv h).inv = (F.mapHomologicalComplex c).map h.inv

@[simp]

theorem CategoryTheory.Functor.mapHomotopyEquiv_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (h : HomotopyEquiv C D) : (F.mapHomotopyEquiv h).hom = (F.mapHomologicalComplex c).map h.hom

noncomputable def Homotopy.toShortComplex {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] {ι : Type u_4} {c : ComplexShape ι} [DecidableRel c.Rel] {K L : HomologicalComplex C c} {f g : K ⟶ L} (ho : Homotopy f g) (i : ι) : CategoryTheory.ShortComplex.Homotopy ((HomologicalComplex.shortComplexFunctor C c i).map f) ((HomologicalComplex.shortComplexFunctor C c i).map g)

A homotopy between morphisms of homological complexes K ⟶ L induces a homotopy between morphisms of short complexes K.sc i ⟶ L.sc i.

Equations

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

theorem Homotopy.homologyMap_eq {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] {ι : Type u_4} {c : ComplexShape ι} [DecidableRel c.Rel] {K L : HomologicalComplex C c} {f g : K ⟶ L} (ho : Homotopy f g) (i : ι) [K.HasHomology i] [L.HasHomology i] : HomologicalComplex.homologyMap f i = HomologicalComplex.homologyMap g i

noncomputable def HomotopyEquiv.toHomologyIso {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] {ι : Type u_4} {c : ComplexShape ι} [DecidableRel c.Rel] {K L : HomologicalComplex C c} (h : HomotopyEquiv K L) (i : ι) [K.HasHomology i] [L.HasHomology i] : K.homology i ≅ L.homology i

The isomorphism in homology induced by an homotopy equivalence.

Equations

• h.toHomologyIso i = { hom := HomologicalComplex.homologyMap h.hom i, inv := HomologicalComplex.homologyMap h.inv i, hom_inv_id := ⋯, inv_hom_id := ⋯ }