mathlib3 documentation

algebra.homology.homotopy

Chain homotopies #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

noncomputable def d_next {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (i : ι) :
(Π (i j : ι), C.X i D.X j) →+ (C.X i D.X i)

The composition of C.d i i' ≫ f i' i if there is some i' coming after i, and 0 otherwise.

Equations
noncomputable def from_next {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (i : ι) :
(Π (i j : ι), C.X i D.X j) →+ (C.X_next i D.X i)

f i' i if i' comes after i, and 0 if there's no such i'. Hopefully there won't be much need for this, except in d_next_eq_d_from_from_next to see that d_next factors through C.d_from i.

Equations
@[simp]
theorem d_next_eq_d_from_from_next {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (f : Π (i j : ι), C.X i D.X j) (i : ι) :
theorem d_next_eq {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (f : Π (i j : ι), C.X i D.X j) {i i' : ι} (w : c.rel i i') :
(d_next i) f = C.d i i' f i' i
@[simp]
theorem d_next_comp_left {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D E : homological_complex V c} (f : C D) (g : Π (i j : ι), D.X i E.X j) (i : ι) :
(d_next i) (λ (i j : ι), f.f i g i j) = f.f i (d_next i) g
@[simp]
theorem d_next_comp_right {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D E : homological_complex V c} (f : Π (i j : ι), C.X i D.X j) (g : D E) (i : ι) :
(d_next i) (λ (i j : ι), f i j g.f j) = (d_next i) f g.f i
noncomputable def prev_d {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (j : ι) :
(Π (i j : ι), C.X i D.X j) →+ (C.X j D.X j)

The composition of f j j' ≫ D.d j' j if there is some j' coming before j, and 0 otherwise.

Equations
noncomputable def to_prev {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (j : ι) :
(Π (i j : ι), C.X i D.X j) →+ (C.X j D.X_prev j)

f j j' if j' comes after j, and 0 if there's no such j'. Hopefully there won't be much need for this, except in d_next_eq_d_from_from_next to see that d_next factors through C.d_from i.

Equations
@[simp]
theorem prev_d_eq_to_prev_d_to {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (f : Π (i j : ι), C.X i D.X j) (j : ι) :
(prev_d j) f = (to_prev j) f D.d_to j
theorem prev_d_eq {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (f : Π (i j : ι), C.X i D.X j) {j j' : ι} (w : c.rel j' j) :
(prev_d j) f = f j j' D.d j' j
@[simp]
theorem prev_d_comp_left {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D E : homological_complex V c} (f : C D) (g : Π (i j : ι), D.X i E.X j) (j : ι) :
(prev_d j) (λ (i j : ι), f.f i g i j) = f.f j (prev_d j) g
@[simp]
theorem prev_d_comp_right {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D E : homological_complex V c} (f : Π (i j : ι), C.X i D.X j) (g : D E) (j : ι) :
(prev_d j) (λ (i j : ι), f i j g.f j) = (prev_d j) f g.f j
theorem d_next_nat {V : Type u} [category_theory.category V] [category_theory.preadditive V] (C D : chain_complex V ) (i : ) (f : Π (i j : ), C.X i D.X j) :
(d_next i) f = C.d i (i - 1) f (i - 1) i
theorem prev_d_nat {V : Type u} [category_theory.category V] [category_theory.preadditive V] (C D : cochain_complex V ) (i : ) (f : Π (i j : ), C.X i D.X j) :
(prev_d i) f = f i (i - 1) D.d (i - 1) i
theorem homotopy.ext_iff {ι : Type u_1} {V : Type u} {_inst_1 : category_theory.category V} {_inst_2 : category_theory.preadditive V} {c : complex_shape ι} {C D : homological_complex V c} {f g : C D} (x y : homotopy f g) :
x = y x.hom = y.hom
@[nolint, ext]
structure homotopy {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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.

Instances for homotopy
  • homotopy.has_sizeof_inst
theorem homotopy.ext {ι : Type u_1} {V : Type u} {_inst_1 : category_theory.category V} {_inst_2 : category_theory.preadditive V} {c : complex_shape ι} {C D : homological_complex V c} {f g : C D} (x y : homotopy f g) (h : x.hom = y.hom) :
x = y
theorem homotopy.zero {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} {f g : C D} (self : homotopy f g) (i j : ι) :
¬c.rel j i self.hom i j = 0
def homotopy.equiv_sub_zero {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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
@[simp]
theorem homotopy.of_eq_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} {f g : C D} (h : f = g) (i j : ι) :
(homotopy.of_eq h).hom i j = 0 i j
def homotopy.of_eq {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} {f g : C D} (h : f = g) :

Equal chain maps are homotopic.

Equations
@[simp]
theorem homotopy.refl_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (f : C D) (i j : ι) :
(homotopy.refl f).hom i j = 0
@[refl]
def homotopy.refl {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (f : C D) :

Every chain map is homotopic to itself.

Equations
@[simp]
theorem homotopy.symm_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} {f g : C D} (h : homotopy f g) (i j : ι) :
h.symm.hom i j = (-h.hom) i j
@[symm]
def homotopy.symm {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} {f g : C D} (h : homotopy f g) :

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

Equations
@[trans]
def homotopy.trans {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} {e f g : C D} (h : homotopy e f) (k : homotopy f g) :

homotopy is a transitive relation.

Equations
@[simp]
theorem homotopy.trans_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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 + k.hom) i j
def homotopy.add {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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
@[simp]
theorem homotopy.add_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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 + h₂.hom) i j
@[simp]
theorem homotopy.comp_right_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D E : homological_complex V c} {e f : C D} (h : homotopy e f) (g : D E) (i j : ι) :
(h.comp_right g).hom i j = h.hom i j g.f j
def homotopy.comp_right {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D E : homological_complex V c} {e f : C D} (h : homotopy e f) (g : D E) :
homotopy (e g) (f g)

homotopy is closed under composition (on the right)

Equations
def homotopy.comp_left {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D E : homological_complex V c} {f g : D E} (h : homotopy f g) (e : C D) :
homotopy (e f) (e g)

homotopy is closed under composition (on the left)

Equations
@[simp]
theorem homotopy.comp_left_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D E : homological_complex V c} {f g : D E} (h : homotopy f g) (e : C D) (i j : ι) :
(h.comp_left e).hom i j = e.f i h.hom i j
@[simp]
theorem homotopy.comp_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C₁ C₂ C₃ : homological_complex 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 = h₁.hom i j f₂.f j + g₁.f i h₂.hom i j
def homotopy.comp {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C₁ C₂ C₃ : homological_complex V c} {f₁ g₁ : C₁ C₂} {f₂ g₂ : C₂ C₃} (h₁ : homotopy f₁ g₁) (h₂ : homotopy f₂ g₂) :
homotopy (f₁ f₂) (g₁ g₂)

homotopy is closed under composition

Equations
@[simp]
theorem homotopy.comp_right_id_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} {f : C C} (h : homotopy f (𝟙 C)) (g : C D) (i j : ι) :
(h.comp_right_id g).hom i j = h.hom i j g.f j
def homotopy.comp_right_id {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} {f : C C} (h : homotopy f (𝟙 C)) (g : C D) :
homotopy (f g) g

a variant of homotopy.comp_right useful for dealing with homotopy equivalences.

Equations
def homotopy.comp_left_id {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} {f : D D} (h : homotopy f (𝟙 D)) (g : C D) :
homotopy (g f) g

a variant of homotopy.comp_left useful for dealing with homotopy equivalences.

Equations
@[simp]
theorem homotopy.comp_left_id_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} {f : D D} (h : homotopy f (𝟙 D)) (g : C D) (i j : ι) :
(h.comp_left_id g).hom i j = 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.

noncomputable def homotopy.null_homotopic_map {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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
noncomputable def homotopy.null_homotopic_map' {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (h : Π (i j : ι), c.rel j i (C.X i D.X j)) :
C D

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

Equations
theorem homotopy.null_homotopic_map_comp {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D E : homological_complex V c} (hom : Π (i j : ι), C.X i D.X j) (g : D E) :

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

theorem homotopy.null_homotopic_map'_comp {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D E : homological_complex V c} (hom : Π (i j : ι), c.rel j i (C.X i D.X j)) (g : D E) :
homotopy.null_homotopic_map' hom g = homotopy.null_homotopic_map' (λ (i j : ι) (hij : c.rel j i), hom i j hij g.f j)

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

theorem homotopy.comp_null_homotopic_map {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D E : homological_complex V c} (f : C D) (hom : Π (i j : ι), D.X i E.X j) :

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

theorem homotopy.comp_null_homotopic_map' {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D E : homological_complex V c} (f : C D) (hom : Π (i j : ι), c.rel j i (D.X i E.X j)) :
f homotopy.null_homotopic_map' hom = homotopy.null_homotopic_map' (λ (i j : ι) (hij : c.rel j i), f.f i hom i j hij)

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

Compatibility of null_homotopic_map with the application of additive functors

theorem homotopy.map_null_homotopic_map' {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (G : V W) [G.additive] (hom : Π (i j : ι), c.rel j i (C.X i D.X j)) :
(G.map_homological_complex c).map (homotopy.null_homotopic_map' hom) = homotopy.null_homotopic_map' (λ (i j : ι) (hij : c.rel j i), G.map (hom i j hij))

Compatibility of null_homotopic_map' with the application of additive functors

@[simp]
theorem homotopy.null_homotopy_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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.null_homotopy hom zero').hom i j = hom i j
def homotopy.null_homotopy {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (hom : Π (i j : ι), C.X i D.X j) (zero' : (i j : ι), ¬c.rel j i hom i j = 0) :

Tautological construction of the homotopy to zero for maps constructed by null_homotopic_map, at least when we have the zero' condition.

Equations
@[simp]
theorem homotopy.null_homotopy'_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (h : Π (i j : ι), c.rel j i (C.X i D.X j)) (i j : ι) :
(homotopy.null_homotopy' h).hom i j = dite (c.rel j i) (h i j) (λ (_x : ¬c.rel j i), 0)
noncomputable def homotopy.null_homotopy' {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (h : Π (i j : ι), c.rel j i (C.X i D.X j)) :

Homotopy to zero for maps constructed with null_homotopic_map'

Equations

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

@[simp]
theorem homotopy.null_homotopic_map_f {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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.null_homotopic_map hom).f k₁ = C.d k₁ k₀ hom k₀ k₁ + hom k₁ k₂ D.d k₂ k₁
@[simp]
theorem homotopy.null_homotopic_map'_f {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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.null_homotopic_map' h).f k₁ = C.d k₁ k₀ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ D.d k₂ k₁
@[simp]
theorem homotopy.null_homotopic_map_f_of_not_rel_left {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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.null_homotopic_map hom).f k₀ = hom k₀ k₁ D.d k₁ k₀
@[simp]
theorem homotopy.null_homotopic_map'_f_of_not_rel_left {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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.null_homotopic_map' h).f k₀ = h k₀ k₁ r₁₀ D.d k₁ k₀
@[simp]
theorem homotopy.null_homotopic_map_f_of_not_rel_right {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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.null_homotopic_map hom).f k₁ = C.d k₁ k₀ hom k₀ k₁
@[simp]
theorem homotopy.null_homotopic_map'_f_of_not_rel_right {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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.null_homotopic_map' h).f k₁ = C.d k₁ k₀ h k₀ k₁ r₁₀
@[simp]
theorem homotopy.null_homotopic_map_f_eq_zero {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} {k₀ : ι} (hk₀ : (l : ι), ¬c.rel k₀ l) (hk₀' : (l : ι), ¬c.rel l k₀) (hom : Π (i j : ι), C.X i D.X j) :
@[simp]
theorem homotopy.null_homotopic_map'_f_eq_zero {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex 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.mk_inductive 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.equiv_sub_zero can provide the general case.

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

@[simp]
theorem homotopy.prev_d_chain_complex {V : Type u} [category_theory.category V] [category_theory.preadditive V] {P Q : chain_complex V } (f : Π (i j : ), P.X i Q.X j) (j : ) :
(prev_d j) f = f j (j + 1) Q.d (j + 1) j
@[simp]
theorem homotopy.d_next_succ_chain_complex {V : Type u} [category_theory.category V] [category_theory.preadditive V] {P Q : chain_complex V } (f : Π (i j : ), P.X i Q.X j) (i : ) :
(d_next (i + 1)) f = P.d (i + 1) i f i (i + 1)
@[simp]
@[simp, nolint]
def homotopy.mk_inductive_aux₁ {V : Type u} [category_theory.category V] [category_theory.preadditive V] {P Q : chain_complex V } (e : P Q) (zero : P.X 0 Q.X 1) (comm_zero : e.f 0 = zero Q.d 1 0) (one : P.X 1 Q.X 2) (comm_one : e.f 1 = P.d 1 0 zero + 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) = P.d (n + 1) n f + f' Q.d (n + 2) (n + 1)), Σ' (f'' : P.X (n + 2) Q.X (n + 3)), e.f (n + 2) = P.d (n + 2) (n + 1) p.snd.fst + 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) = P.d (n + 1) n f + f' Q.d (n + 2) (n + 1)

An auxiliary construction for mk_inductive.

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 mk_inductive.

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 X_next and X_prev, which we do in mk_inductive_aux₂.

Equations
@[simp]
noncomputable def homotopy.mk_inductive_aux₂ {V : Type u} [category_theory.category V] [category_theory.preadditive V] {P Q : chain_complex V } (e : P Q) (zero : P.X 0 Q.X 1) (comm_zero : e.f 0 = zero Q.d 1 0) (one : P.X 1 Q.X 2) (comm_one : e.f 1 = P.d 1 0 zero + 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) = P.d (n + 1) n f + f' Q.d (n + 2) (n + 1)), Σ' (f'' : P.X (n + 2) Q.X (n + 3)), e.f (n + 2) = P.d (n + 2) (n + 1) p.snd.fst + f'' Q.d (n + 3) (n + 2)) (n : ) :

An auxiliary construction for mk_inductive.

Equations
theorem homotopy.mk_inductive_aux₃ {V : Type u} [category_theory.category V] [category_theory.preadditive V] {P Q : chain_complex V } (e : P Q) (zero : P.X 0 Q.X 1) (comm_zero : e.f 0 = zero Q.d 1 0) (one : P.X 1 Q.X 2) (comm_one : e.f 1 = P.d 1 0 zero + 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) = P.d (n + 1) n f + f' Q.d (n + 2) (n + 1)), Σ' (f'' : P.X (n + 2) Q.X (n + 3)), e.f (n + 2) = P.d (n + 2) (n + 1) p.snd.fst + f'' Q.d (n + 3) (n + 2)) (i j : ) (h : i + 1 = j) :
(homotopy.mk_inductive_aux₂ e zero comm_zero one comm_one succ i).snd.fst (homological_complex.X_prev_iso Q h).hom = (homological_complex.X_next_iso P h).inv (homotopy.mk_inductive_aux₂ e zero comm_zero one comm_one succ j).fst
noncomputable def homotopy.mk_inductive {V : Type u} [category_theory.category V] [category_theory.preadditive V] {P Q : chain_complex V } (e : P Q) (zero : P.X 0 Q.X 1) (comm_zero : e.f 0 = zero Q.d 1 0) (one : P.X 1 Q.X 2) (comm_one : e.f 1 = P.d 1 0 zero + 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) = P.d (n + 1) n f + f' Q.d (n + 2) (n + 1)), Σ' (f'' : P.X (n + 2) Q.X (n + 3)), e.f (n + 2) = P.d (n + 2) (n + 1) p.snd.fst + 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

homotopy.mk_coinductive 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.d_next_cochain_complex {V : Type u} [category_theory.category V] [category_theory.preadditive V] {P Q : cochain_complex V } (f : Π (i j : ), P.X i Q.X j) (j : ) :
(d_next j) f = P.d j (j + 1) f (j + 1) j
@[simp]
theorem homotopy.prev_d_succ_cochain_complex {V : Type u} [category_theory.category V] [category_theory.preadditive V] {P Q : cochain_complex V } (f : Π (i j : ), P.X i Q.X j) (i : ) :
(prev_d (i + 1)) f = f (i + 1) i Q.d i (i + 1)
@[simp]
@[simp, nolint]
def homotopy.mk_coinductive_aux₁ {V : Type u} [category_theory.category V] [category_theory.preadditive V] {P Q : cochain_complex V } (e : P Q) (zero : P.X 1 Q.X 0) (comm_zero : e.f 0 = P.d 0 1 zero) (one : P.X 2 Q.X 1) (comm_one : e.f 1 = zero Q.d 0 1 + 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) = f Q.d n (n + 1) + P.d (n + 1) (n + 2) f'), Σ' (f'' : P.X (n + 3) Q.X (n + 2)), e.f (n + 2) = p.snd.fst Q.d (n + 1) (n + 2) + 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) = f Q.d n (n + 1) + P.d (n + 1) (n + 2) f'

An auxiliary construction for mk_coinductive.

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 mk_coinductive.

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 X_next and X_prev, which we do in mk_inductive_aux₂.

Equations
@[simp]
noncomputable def homotopy.mk_coinductive_aux₂ {V : Type u} [category_theory.category V] [category_theory.preadditive V] {P Q : cochain_complex V } (e : P Q) (zero : P.X 1 Q.X 0) (comm_zero : e.f 0 = P.d 0 1 zero) (one : P.X 2 Q.X 1) (comm_one : e.f 1 = zero Q.d 0 1 + 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) = f Q.d n (n + 1) + P.d (n + 1) (n + 2) f'), Σ' (f'' : P.X (n + 3) Q.X (n + 2)), e.f (n + 2) = p.snd.fst Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) f'') (n : ) :

An auxiliary construction for mk_inductive.

Equations
theorem homotopy.mk_coinductive_aux₃ {V : Type u} [category_theory.category V] [category_theory.preadditive V] {P Q : cochain_complex V } (e : P Q) (zero : P.X 1 Q.X 0) (comm_zero : e.f 0 = P.d 0 1 zero) (one : P.X 2 Q.X 1) (comm_one : e.f 1 = zero Q.d 0 1 + 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) = f Q.d n (n + 1) + P.d (n + 1) (n + 2) f'), Σ' (f'' : P.X (n + 3) Q.X (n + 2)), e.f (n + 2) = p.snd.fst Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) f'') (i j : ) (h : i + 1 = j) :
(homological_complex.X_next_iso P h).inv (homotopy.mk_coinductive_aux₂ e zero comm_zero one comm_one succ i).snd.fst = (homotopy.mk_coinductive_aux₂ e zero comm_zero one comm_one succ j).fst (homological_complex.X_prev_iso Q h).hom
noncomputable def homotopy.mk_coinductive {V : Type u} [category_theory.category V] [category_theory.preadditive V] {P Q : cochain_complex V } (e : P Q) (zero : P.X 1 Q.X 0) (comm_zero : e.f 0 = P.d 0 1 zero) (one : P.X 2 Q.X 1) (comm_one : e.f 1 = zero Q.d 0 1 + 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) = f Q.d n (n + 1) + P.d (n + 1) (n + 2) f'), Σ' (f'' : P.X (n + 3) Q.X (n + 2)), e.f (n + 2) = p.snd.fst Q.d (n + 1) (n + 2) + 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
structure homotopy_equiv {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} (C D : homological_complex 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.

Instances for homotopy_equiv
@[refl]

Any complex is homotopy equivalent to itself.

Equations
@[symm]

Being homotopy equivalent is a symmetric relation.

Equations
@[trans]

Homotopy equivalence is a transitive relation.

Equations

An isomorphism of complexes induces a homotopy equivalence.

Equations
@[simp]
theorem category_theory.functor.map_homotopy_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (F : V W) [F.additive] {f g : C D} (h : homotopy f g) (i j : ι) :
(F.map_homotopy h).hom i j = F.map (h.hom i j)

An additive functor takes homotopies to homotopies.

Equations