# 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} {c : } {C : } {D : } (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
Instances For
def fromNext {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (i : ι) :
((i j : ι) → C.X i D.X j) →+ (C.xNext i D.X i)

f (c.next i) i.

Equations
Instances For
@[simp]
theorem dNext_eq_dFrom_fromNext {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : (i j : ι) → C.X i D.X j) (i : ι) :
() f = CategoryTheory.CategoryStruct.comp (C.dFrom i) (() f)
theorem dNext_eq {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : (i j : ι) → C.X i D.X j) {i : ι} {i' : ι} (w : c.Rel i i') :
() f = CategoryTheory.CategoryStruct.comp (C.d i i') (f i' i)
theorem dNext_eq_zero {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : (i j : ι) → C.X i D.X j) (i : ι) (hi : ¬c.Rel i (c.next i)) :
() f = 0
@[simp]
theorem dNext_comp_left {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } (f : C D) (g : (i j : ι) → D.X i E.X j) (i : ι) :
(() fun (i j : ι) => CategoryTheory.CategoryStruct.comp (f.f i) (g i j)) = CategoryTheory.CategoryStruct.comp (f.f i) (() g)
@[simp]
theorem dNext_comp_right {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } (f : (i j : ι) → C.X i D.X j) (g : D E) (i : ι) :
(() fun (i j : ι) => CategoryTheory.CategoryStruct.comp (f i j) (g.f j)) = CategoryTheory.CategoryStruct.comp (() f) (g.f i)
def prevD {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (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
Instances For
theorem prevD_eq_zero {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : (i j : ι) → C.X i D.X j) (i : ι) (hi : ¬c.Rel (c.prev i) i) :
() f = 0
def toPrev {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (j : ι) :
((i j : ι) → C.X i D.X j) →+ (C.X j D.xPrev j)

f j (c.prev j).

Equations
Instances For
@[simp]
theorem prevD_eq_toPrev_dTo {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : (i j : ι) → C.X i D.X j) (j : ι) :
theorem prevD_eq {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : (i j : ι) → C.X i D.X j) {j : ι} {j' : ι} (w : c.Rel j' j) :
() f = CategoryTheory.CategoryStruct.comp (f j j') (D.d j' j)
@[simp]
theorem prevD_comp_left {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } (f : C D) (g : (i j : ι) → D.X i E.X j) (j : ι) :
(() fun (i j : ι) => CategoryTheory.CategoryStruct.comp (f.f i) (g i j)) = CategoryTheory.CategoryStruct.comp (f.f j) (() g)
@[simp]
theorem prevD_comp_right {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } (f : (i j : ι) → C.X i D.X j) (g : D E) (j : ι) :
(() fun (i j : ι) => CategoryTheory.CategoryStruct.comp (f i j) (g.f j)) = CategoryTheory.CategoryStruct.comp (() f) (g.f j)
theorem dNext_nat {V : Type u} (C : ) (D : ) (i : ) (f : (i j : ) → C.X i D.X j) :
() f = CategoryTheory.CategoryStruct.comp (C.d i (i - 1)) (f (i - 1) i)
theorem prevD_nat {V : Type u} (C : ) (D : ) (i : ) (f : (i j : ) → C.X i D.X j) :
() f = CategoryTheory.CategoryStruct.comp (f i (i - 1)) (D.d (i - 1) i)
theorem Homotopy.ext_iff {ι : Type u_1} {V : Type u} :
∀ {inst : } {inst_1 : } {c : } {C D : } {f g : C D} (x y : Homotopy f g), x = y x.hom = y.hom
theorem Homotopy.ext {ι : Type u_1} {V : Type u} :
∀ {inst : } {inst_1 : } {c : } {C D : } {f g : C D} (x y : Homotopy f g), x.hom = y.homx = y
structure Homotopy {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : C D) (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 iself.hom i j = 0
• comm : ∀ (i : ι), f.f i = () self.hom + () self.hom + g.f i
Instances For
theorem Homotopy.zero {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : C D} {g : C D} (self : Homotopy f g) (i : ι) (j : ι) :
¬c.Rel j iself.hom i j = 0
theorem Homotopy.comm {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : C D} {g : C D} (self : Homotopy f g) (i : ι) :
f.f i = () self.hom + () self.hom + g.f i
def Homotopy.equivSubZero {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : C D} {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.
Instances For
@[simp]
theorem Homotopy.ofEq_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : C D} {g : C D} (h : f = g) (i : ι) (j : ι) :
().hom i j = 0 i j
def Homotopy.ofEq {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : C D} {g : C D} (h : f = g) :

Equal chain maps are homotopic.

Equations
• = { hom := 0, zero := , comm := }
Instances For
@[simp]
theorem Homotopy.refl_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : C D) (i : ι) (j : ι) :
().hom i j = 0
def Homotopy.refl {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : C D) :

Every chain map is homotopic to itself.

Equations
Instances For
@[simp]
theorem Homotopy.symm_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : C D} {g : C D} (h : Homotopy f g) (i : ι) (j : ι) :
h.symm.hom i j = -h.hom i j
def Homotopy.symm {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : C D} {g : C D} (h : Homotopy f g) :

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

Equations
• h.symm = { hom := -h.hom, zero := , comm := }
Instances For
@[simp]
theorem Homotopy.trans_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {e : C D} {f : C D} {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.trans {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {e : C D} {f : C D} {g : C D} (h : Homotopy e f) (k : Homotopy f g) :

homotopy is a transitive relation.

Equations
• h.trans k = { hom := h.hom + k.hom, zero := , comm := }
Instances For
@[simp]
theorem Homotopy.add_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f₁ : C D} {g₁ : C D} {f₂ : C D} {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.add {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f₁ : C D} {g₁ : C D} {f₂ : C D} {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 := }
Instances For
@[simp]
theorem Homotopy.smul_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : C D} {g : C D} {R : Type u_2} [] [] (h : Homotopy f g) (a : R) (i : ι) (j : ι) :
(h.smul a).hom i j = a h.hom i j
def Homotopy.smul {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : C D} {g : C D} {R : Type u_2} [] [] (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 := }
Instances For
@[simp]
theorem Homotopy.compRight_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } {e : C D} {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.compRight {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } {e : C D} {f : C D} (h : Homotopy e f) (g : D E) :

homotopy is closed under composition (on the right)

Equations
Instances For
@[simp]
theorem Homotopy.compLeft_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } {f : D E} {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.compLeft {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } {f : D E} {g : D E} (h : Homotopy f g) (e : C D) :

homotopy is closed under composition (on the left)

Equations
Instances For
@[simp]
theorem Homotopy.comp_hom {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } {C₃ : } {f₁ : C₁ C₂} {g₁ : C₁ C₂} {f₂ : C₂ C₃} {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.comp {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } {C₃ : } {f₁ : C₁ C₂} {g₁ : C₁ C₂} {f₂ : C₂ C₃} {g₂ : C₂ C₃} (h₁ : Homotopy f₁ g₁) (h₂ : Homotopy f₂ g₂) :

homotopy is closed under composition

Equations
• h₁.comp h₂ = (h₁.compRight f₂).trans (h₂.compLeft g₁)
Instances For
@[simp]
theorem Homotopy.compRightId_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : C C} (h : ) (g : C D) (i : ι) (j : ι) :
(h.compRightId g).hom i j = CategoryTheory.CategoryStruct.comp (h.hom i j) (g.f j)
def Homotopy.compRightId {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : C C} (h : ) (g : C D) :

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

Equations
• h.compRightId g = (h.compRight g).trans ()
Instances For
@[simp]
theorem Homotopy.compLeftId_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : D D} (h : ) (g : C D) (i : ι) (j : ι) :
(h.compLeftId g).hom i j = CategoryTheory.CategoryStruct.comp (g.f i) (h.hom i j)
def Homotopy.compLeftId {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : D D} (h : ) (g : C D) :

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

Equations
• h.compLeftId g = (h.compLeft g).trans ()
Instances For

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} {c : } {C : } {D : } (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
• = { f := fun (i : ι) => () hom + () hom, comm' := }
Instances For
def Homotopy.nullHomotopicMap' {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (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
Instances For
theorem Homotopy.nullHomotopicMap_comp {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } (hom : (i j : ι) → C.X i D.X j) (g : D E) :

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

theorem Homotopy.nullHomotopicMap'_comp {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } (hom : (i j : ι) → c.Rel j i(C.X i D.X j)) (g : D E) :
= 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} {c : } {C : } {D : } {E : } (f : C D) (hom : (i j : ι) → D.X i E.X j) :

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

theorem Homotopy.comp_nullHomotopicMap' {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } (f : C D) (hom : (i j : ι) → c.Rel j i(D.X i E.X j)) :
= 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} {c : } {C : } {D : } {W : Type u_2} [] (G : ) [G.Additive] (hom : (i j : ι) → C.X i D.X j) :
(G.mapHomologicalComplex c).map = 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} {c : } {C : } {D : } {W : Type u_2} [] (G : ) [G.Additive] (hom : (i j : ι) → c.Rel j i(C.X i D.X j)) :
(G.mapHomologicalComplex c).map = 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

@[simp]
theorem Homotopy.nullHomotopy_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (hom : (i j : ι) → C.X i D.X j) (zero : ∀ (i j : ι), ¬c.Rel j ihom i j = 0) (i : ι) (j : ι) :
(Homotopy.nullHomotopy hom zero).hom i j = hom i j
def Homotopy.nullHomotopy {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (hom : (i j : ι) → C.X i D.X j) (zero : ∀ (i j : ι), ¬c.Rel j ihom i j = 0) :

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

Equations
Instances For
@[simp]
theorem Homotopy.nullHomotopy'_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (h : (i j : ι) → c.Rel j i(C.X i D.X j)) (i : ι) (j : ι) :
.hom i j = dite (c.Rel j i) (h i j) fun (x : ¬c.Rel j i) => 0
def Homotopy.nullHomotopy' {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (h : (i j : ι) → c.Rel j i(C.X i D.X j)) :

Homotopy to zero for maps constructed with nullHomotopicMap'

Equations
Instances For

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} {c : } {C : } {D : } {k₂ : ι} {k₁ : ι} {k₀ : ι} (r₂₁ : c.Rel k₂ k₁) (r₁₀ : c.Rel k₁ k₀) (hom : (i j : ι) → C.X i D.X j) :
.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} {c : } {C : } {D : } {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)) :
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} {c : } {C : } {D : } {k₁ : ι} {k₀ : ι} (r₁₀ : c.Rel k₁ k₀) (hk₀ : ∀ (l : ι), ¬c.Rel k₀ l) (hom : (i j : ι) → C.X i D.X j) :
.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} {c : } {C : } {D : } {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)) :
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} {c : } {C : } {D : } {k₁ : ι} {k₀ : ι} (r₁₀ : c.Rel k₁ k₀) (hk₁ : ∀ (l : ι), ¬c.Rel l k₁) (hom : (i j : ι) → C.X i D.X j) :
.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} {c : } {C : } {D : } {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)) :
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} {c : } {C : } {D : } {k₀ : ι} (hk₀ : ∀ (l : ι), ¬c.Rel k₀ l) (hk₀' : ∀ (l : ι), ¬c.Rel l k₀) (hom : (i j : ι) → C.X i D.X j) :
.f k₀ = 0
@[simp]
theorem Homotopy.nullHomotopicMap'_f_eq_zero {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {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)) :
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} {P : } {Q : } (f : (i j : ) → P.X i Q.X j) (j : ) :
() f = CategoryTheory.CategoryStruct.comp (f j (j + 1)) (Q.d (j + 1) j)
@[simp]
theorem Homotopy.dNext_succ_chainComplex {V : Type u} {P : } {Q : } (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} {P : } {Q : } (f : (i j : ) → P.X i Q.X j) :
() f = 0
def Homotopy.mkInductiveAux₁ {V : Type u} {P : } {Q : } (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,
Instances For
def Homotopy.mkInductiveAux₂ {V : Type u} {P : } {Q : } (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 : Q.X n) ×' (f' : P.X n ) ×' e.f n =

An auxiliary construction for mkInductive.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Homotopy.mkInductiveAux₂_zero {V : Type u} {P : } {Q : } (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, ,
@[simp]
theorem Homotopy.mkInductiveAux₂_add_one {V : Type u} {P : } {Q : } (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 I.snd.fst .inv,
theorem Homotopy.mkInductiveAux₃ {V : Type u} {P : } {Q : } (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 .hom = CategoryTheory.CategoryStruct.comp .inv (Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ j).fst
def Homotopy.mkInductive {V : Type u} {P : } {Q : } (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))) :

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.
Instances For

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} {P : } {Q : } (f : (i j : ) → P.X i Q.X j) (j : ) :
() f = CategoryTheory.CategoryStruct.comp (P.d j (j + 1)) (f (j + 1) j)
@[simp]
theorem Homotopy.prevD_succ_cochainComplex {V : Type u} {P : } {Q : } (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} {P : } {Q : } (f : (i j : ) → P.X i Q.X j) :
() f = 0
def Homotopy.mkCoinductiveAux₁ {V : Type u} {P : } {Q : } (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
Instances For
def Homotopy.mkCoinductiveAux₂ {V : Type u} {P : } {Q : } (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 ) ×' (f' : Q.X n) ×' e.f n =

An auxiliary construction for mkInductive.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Homotopy.mkCoinductiveAux₂_zero {V : Type u} {P : } {Q : } (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, ,
@[simp]
theorem Homotopy.mkCoinductiveAux₂_add_one {V : Type u} {P : } {Q : } (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 .hom I.snd.fst,
theorem Homotopy.mkCoinductiveAux₃ {V : Type u} {P : } {Q : } (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 .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 .hom
def Homotopy.mkCoinductive {V : Type u} {P : } {Q : } (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'') :

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.
Instances For
structure HomotopyEquiv {ι : Type u_1} {V : Type u} {c : } (C : ) (D : ) :
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.

Instances For
def HomologicalComplex.homotopyEquivalences {ι : Type u_1} (V : Type u) (c : ) :

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

Equations
• = ∃ (e : ), e.hom = f
Instances For
def HomotopyEquiv.refl {ι : Type u_1} {V : Type u} {c : } (C : ) :

Any complex is homotopy equivalent to itself.

Equations
• = { hom := , inv := , homotopyHomInvId := , homotopyInvHomId := }
Instances For
instance HomotopyEquiv.instInhabited {ι : Type u_1} {V : Type u} {c : } {C : } :
Equations
• HomotopyEquiv.instInhabited = { default := }
def HomotopyEquiv.symm {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : ) :

Being homotopy equivalent is a symmetric relation.

Equations
• f.symm = { hom := f.inv, inv := f.hom, homotopyHomInvId := f.homotopyInvHomId, homotopyInvHomId := f.homotopyHomInvId }
Instances For
def HomotopyEquiv.trans {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } (f : ) (g : ) :

Homotopy equivalence is a transitive relation.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def HomotopyEquiv.ofIso {ι : Type u_2} {V : Type u} {c : } {C : } {D : } (f : C D) :

An isomorphism of complexes induces a homotopy equivalence.

Equations
• = { hom := f.hom, inv := f.inv, homotopyHomInvId := , homotopyInvHomId := }
Instances For
@[simp]
theorem CategoryTheory.Functor.mapHomotopy_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {W : Type u_2} [] (F : ) [F.Additive] {f : C D} {g : C D} (h : Homotopy f g) (i : ι) (j : ι) :
(F.mapHomotopy h).hom i j = F.map (h.hom i j)
def CategoryTheory.Functor.mapHomotopy {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {W : Type u_2} [] (F : ) [F.Additive] {f : C D} {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 := }
Instances For
@[simp]
theorem CategoryTheory.Functor.mapHomotopyEquiv_inv {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {W : Type u_2} [] (F : ) [F.Additive] (h : ) :
(F.mapHomotopyEquiv h).inv = (F.mapHomologicalComplex c).map h.inv
@[simp]
theorem CategoryTheory.Functor.mapHomotopyEquiv_hom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {W : Type u_2} [] (F : ) [F.Additive] (h : ) :
(F.mapHomotopyEquiv h).hom = (F.mapHomologicalComplex c).map h.hom
@[simp]
theorem CategoryTheory.Functor.mapHomotopyEquiv_homotopyHomInvId {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {W : Type u_2} [] (F : ) [F.Additive] (h : ) :
(F.mapHomotopyEquiv h).homotopyHomInvId = .mpr (.mpr (F.mapHomotopy h.homotopyHomInvId))
@[simp]
theorem CategoryTheory.Functor.mapHomotopyEquiv_homotopyInvHomId {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {W : Type u_2} [] (F : ) [F.Additive] (h : ) :
(F.mapHomotopyEquiv h).homotopyInvHomId = .mpr (.mpr (F.mapHomotopy h.homotopyInvHomId))
def CategoryTheory.Functor.mapHomotopyEquiv {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {W : Type u_2} [] (F : ) [F.Additive] (h : ) :
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.
Instances For
noncomputable def Homotopy.toShortComplex {C : Type u_2} [] {ι : Type u_4} {c : } [DecidableRel c.Rel] {K : } {L : } {f : K L} {g : K L} (ho : Homotopy f g) (i : ι) :

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.
Instances For
theorem Homotopy.homologyMap_eq {C : Type u_2} [] {ι : Type u_4} {c : } [DecidableRel c.Rel] {K : } {L : } {f : K L} {g : K L} (ho : Homotopy f g) (i : ι) [K.HasHomology i] [L.HasHomology i] :
noncomputable def HomotopyEquiv.toHomologyIso {C : Type u_2} [] {ι : Type u_4} {c : } [DecidableRel c.Rel] {K : } {L : } (h : ) (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 := , inv := , hom_inv_id := , inv_hom_id := }
Instances For