# mathlib3documentation

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} {c : complex_shape ι} {C D : 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} {c : complex_shape ι} {C D : 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} {c : complex_shape ι} {C D : c} (f : Π (i j : ι), C.X i D.X j) (i : ι) :
theorem d_next_eq {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : 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} {c : complex_shape ι} {C D E : 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} {c : complex_shape ι} {C D E : 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} {c : complex_shape ι} {C D : 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} {c : complex_shape ι} {C D : 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} {c : complex_shape ι} {C D : 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} {c : complex_shape ι} {C D : 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} {c : complex_shape ι} {C D E : 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} {c : complex_shape ι} {C D E : 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} (C D : ) (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} (C D : ) (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 : c} {f g : C D} (x y : g) :
x = y x.hom = y.hom
@[nolint, ext]
structure homotopy {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : 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 : c} {f g : C D} (x y : g) (h : x.hom = y.hom) :
x = y
theorem homotopy.zero {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} {f g : C D} (self : g) (i j : ι) :
¬c.rel j i self.hom i j = 0
def homotopy.equiv_sub_zero {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} {f g : C D} :
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} {c : complex_shape ι} {C D : c} {f g : C D} (h : f = g) (i j : ι) :
.hom i j = 0 i j
def homotopy.of_eq {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} {f g : C D} (h : f = g) :
g

Equal chain maps are homotopic.

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

Every chain map is homotopic to itself.

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

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

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

homotopy is a transitive relation.

Equations
@[simp]
theorem homotopy.trans_hom {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} {e f g : C D} (h : f) (k : g) (i j : ι) :
(h.trans k).hom i j = (h.hom + k.hom) i j
def homotopy.add {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : 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} {c : complex_shape ι} {C D : 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} {c : complex_shape ι} {C D E : c} {e f : C D} (h : 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} {c : complex_shape ι} {C D E : c} {e f : C D} (h : 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} {c : complex_shape ι} {C D E : c} {f g : D E} (h : 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} {c : complex_shape ι} {C D E : c} {f g : D E} (h : 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} {c : complex_shape ι} {C₁ C₂ C₃ : 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} {c : complex_shape ι} {C₁ C₂ C₃ : 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} {c : complex_shape ι} {C D : c} {f : C C} (h : (𝟙 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} {c : complex_shape ι} {C D : c} {f : C C} (h : (𝟙 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} {c : complex_shape ι} {C D : c} {f : D D} (h : (𝟙 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} {c : complex_shape ι} {C D : c} {f : D D} (h : (𝟙 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} {c : complex_shape ι} {C D : 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} {c : complex_shape ι} {C D : 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} {c : complex_shape ι} {C D E : c} (hom : Π (i j : ι), C.X i D.X j) (g : D E) :
= homotopy.null_homotopic_map (λ (i j : ι), hom i j g.f j)

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} {c : complex_shape ι} {C D E : c} (hom : Π (i j : ι), c.rel j i (C.X i D.X j)) (g : D E) :
= 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} {c : complex_shape ι} {C D E : c} (f : C D) (hom : Π (i j : ι), D.X i E.X j) :
= homotopy.null_homotopic_map (λ (i j : ι), f.f i hom i 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} {c : complex_shape ι} {C D E : c} (f : C D) (hom : Π (i j : ι), c.rel j i (D.X i E.X j)) :
= 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.

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

Compatibility of `null_homotopic_map` with the application of additive functors

theorem homotopy.map_null_homotopic_map' {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} {W : Type u_2} (G : V W) [G.additive] (hom : Π (i j : ι), c.rel j i (C.X i D.X j)) :
= 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} {c : complex_shape ι} {C D : c} (hom : Π (i j : ι), C.X i D.X j) (zero' : (i j : ι), ¬c.rel j i hom i j = 0) (i j : ι) :
zero').hom i j = hom i j
def homotopy.null_homotopy {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : 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} {c : complex_shape ι} {C D : c} (h : Π (i j : ι), c.rel j i (C.X i D.X j)) (i j : ι) :
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} {c : complex_shape ι} {C D : 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} {c : complex_shape ι} {C D : c} {k₂ k₁ k₀ : ι} (r₂₁ : c.rel k₂ k₁) (r₁₀ : c.rel k₁ k₀) (hom : Π (i j : ι), C.X i D.X j) :
.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} {c : complex_shape ι} {C D : 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)) :
= 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} {c : complex_shape ι} {C D : c} {k₁ k₀ : ι} (r₁₀ : c.rel k₁ k₀) (hk₀ : (l : ι), ¬c.rel k₀ l) (hom : Π (i j : ι), C.X i D.X j) :
.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} {c : complex_shape ι} {C D : 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)) :
= 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} {c : complex_shape ι} {C D : c} {k₁ k₀ : ι} (r₁₀ : c.rel k₁ k₀) (hk₁ : (l : ι), ¬c.rel l k₁) (hom : Π (i j : ι), C.X i D.X j) :
.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} {c : complex_shape ι} {C D : 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)) :
= C.d k₁ k₀ h k₀ k₁ r₁₀
@[simp]
theorem homotopy.null_homotopic_map_f_eq_zero {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} {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.null_homotopic_map'_f_eq_zero {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : 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)) :
= 0

`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} {P Q : } (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} {P Q : } (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]
theorem homotopy.d_next_zero_chain_complex {V : Type u} {P Q : } (f : Π (i j : ), P.X i Q.X j) :
(d_next 0) f = 0
@[simp, nolint]
def homotopy.mk_inductive_aux₁ {V : Type u} {P Q : } (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
• comm_zero one comm_one succ (n + 2) = zero comm_zero one comm_one succ n.succ).snd.fst, (succ (n + 1) zero comm_zero one comm_one succ n.succ)).fst, _⟩
• comm_zero one comm_one succ 1 = one, (succ 0 zero, one, comm_one⟩⟩).fst, _⟩
• comm_zero one comm_one succ 0 = zero, one, comm_one⟩
@[simp]
noncomputable def homotopy.mk_inductive_aux₂ {V : Type u} {P Q : } (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 : Q.X n) (f' : P.X n , e.f n = +

An auxiliary construction for `mk_inductive`.

Equations
• comm_zero one comm_one succ (n + 1) = let I : Σ' (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) := comm_zero one comm_one succ n in , I.snd.fst , _⟩
• comm_zero one comm_one succ 0 = 0, zero homotopy.mk_inductive_aux₂._main._proof_1).inv, _⟩
theorem homotopy.mk_inductive_aux₃ {V : Type u} {P Q : } (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) :
zero comm_zero one comm_one succ i).snd.fst = zero comm_zero one comm_one succ j).fst
noncomputable def homotopy.mk_inductive {V : Type u} {P Q : } (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)) :
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
• zero comm_zero one comm_one succ = {hom := λ (i j : ), dite (i + 1 = j) (λ (h : i + 1 = j), zero comm_zero one comm_one succ i).snd.fst (λ (h : ¬i + 1 = j), 0), zero' := _, comm := _}

`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} {P Q : } (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} {P Q : } (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]
theorem homotopy.prev_d_zero_cochain_complex {V : Type u} {P Q : } (f : Π (i j : ), P.X i Q.X j) :
(prev_d 0) f = 0
@[simp, nolint]
def homotopy.mk_coinductive_aux₁ {V : Type u} {P Q : } (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
• comm_zero one comm_one succ (n + 2) = zero comm_zero one comm_one succ n.succ).snd.fst, (succ (n + 1) zero comm_zero one comm_one succ n.succ)).fst, _⟩
• comm_zero one comm_one succ 1 = one, (succ 0 zero, one, comm_one⟩⟩).fst, _⟩
• comm_zero one comm_one succ 0 = zero, one, comm_one⟩
@[simp]
noncomputable def homotopy.mk_coinductive_aux₂ {V : Type u} {P Q : } (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 (f' : Q.X n), e.f n = +

An auxiliary construction for `mk_inductive`.

Equations
• comm_zero one comm_one succ (n + 1) = let I : Σ' (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' := comm_zero one comm_one succ n in , I.snd.fst, _⟩
• comm_zero one comm_one succ 0 = 0, homotopy.mk_coinductive_aux₂._main._proof_1).hom zero, _⟩
theorem homotopy.mk_coinductive_aux₃ {V : Type u} {P Q : } (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) :
zero comm_zero one comm_one succ i).snd.fst = zero comm_zero one comm_one succ j).fst
noncomputable def homotopy.mk_coinductive {V : Type u} {P Q : } (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'') :
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
• zero comm_zero one comm_one succ = {hom := λ (i j : ), dite (j + 1 = i) (λ (h : j + 1 = i), zero comm_zero one comm_one succ j).snd.fst) (λ (h : ¬j + 1 = i), 0), zero' := _, comm := _}
structure homotopy_equiv {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C D : 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]
def homotopy_equiv.refl {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) :

Any complex is homotopy equivalent to itself.

Equations
@[protected, instance]
def homotopy_equiv.inhabited {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C : c} :
Equations
@[symm]
def homotopy_equiv.symm {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (f : D) :

Being homotopy equivalent is a symmetric relation.

Equations
@[trans]
def homotopy_equiv.trans {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D E : c} (f : D) (g : E) :

Homotopy equivalence is a transitive relation.

Equations
def homotopy_equiv.of_iso {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (f : C D) :

An isomorphism of complexes induces a homotopy equivalence.

Equations
theorem homology_map_eq_of_homotopy {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} {f g : C D} (h : g) (i : ι) :
c i).map f = c i).map g

Homotopic maps induce the same map on homology.

noncomputable def homology_obj_iso_of_homotopy_equiv {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (f : D) (i : ι) :
c i).obj C c i).obj D

Homotopy equivalent complexes have isomorphic homologies.

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

An additive functor takes homotopies to homotopies.

Equations
def category_theory.functor.map_homotopy_equiv {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} {W : Type u_2} (F : V W) [F.additive] (h : D) :

An additive functor preserves homotopy equivalences.

Equations
@[simp]
theorem category_theory.functor.map_homotopy_equiv_hom {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} {W : Type u_2} (F : V W) [F.additive] (h : D) :
@[simp]
theorem category_theory.functor.map_homotopy_equiv_homotopy_hom_inv_id {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} {W : Type u_2} (F : V W) [F.additive] (h : D) :
= _.mpr (_.mpr
@[simp]
theorem category_theory.functor.map_homotopy_equiv_inv {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} {W : Type u_2} (F : V W) [F.additive] (h : D) :
@[simp]
theorem category_theory.functor.map_homotopy_equiv_homotopy_inv_hom_id {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} {W : Type u_2} (F : V W) [F.additive] (h : D) :
= _.mpr (_.mpr