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 : ι) :
The composition of C.d i i' ≫ f i' i if there is some i' coming after i,
and 0 otherwise.
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 : ι) :
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.
@[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') :
@[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 : ι) :
@[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 : ι) :
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 : ι) :
The composition of f j j' ≫ D.d j' j if there is some j' coming before j,
and 0 otherwise.
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 : ι) :
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.
@[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 : ι) :
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) :
@[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 : ι) :
@[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 : ι) :
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) :
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) :
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) :
@[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)
- hom : Π (i j : ι), C.X i ⟶ D.X j
- zero' : (∀ (i j : ι), ¬c.rel j i → self.hom i j = 0) . "obviously"
- comm : (∀ (i : ι), f.f i = ⇑(d_next i) self.hom + ⇑(prev_d i) self.hom + g.f i) . "obviously'"
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 : ι) :
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} :
f is homotopic to g iff f - g is homotopic to 0.
@[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) :
homotopy f g
Equal chain maps are homotopic.
@[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) :
homotopy f f
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 : ι) :
@[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) :
homotopy g f
f is homotopic to g iff g is homotopic to f.
@[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 e g
homotopy is a transitive relation.
@[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 : ι) :
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₂) :
the sum of two homotopies is a homotopy between the sum of the respective morphisms.
@[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 : ι) :
@[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 : ι) :
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 is closed under composition (on the right)
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 is closed under composition (on the left)
@[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 : ι) :
@[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 : ι) :
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 is closed under composition
Equations
- h₁.comp h₂ = (h₁.comp_right f₂).trans (h₂.comp_left g₁)
@[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 : ι) :
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) :
a variant of homotopy.comp_right useful for dealing with homotopy equivalences.
Equations
- h.comp_right_id g = (h.comp_right g).trans (homotopy.of_eq _)
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) :
a variant of homotopy.comp_left useful for dealing with homotopy equivalences.
Equations
- h.comp_left_id g = (h.comp_left g).trans (homotopy.of_eq _)
@[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 : ι) :
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.
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
- homotopy.null_homotopic_map' h = homotopy.null_homotopic_map (λ (i j : ι), dite (c.rel j i) (h i j) (λ (_x : ¬c.rel j i), 0))
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) :
homotopy.null_homotopic_map hom ≫ g = 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}
[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) :
f ≫ homotopy.null_homotopic_map hom = 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}
[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.
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.X i ⟶ D.X j) :
(G.map_homological_complex c).map (homotopy.null_homotopic_map hom) = 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}
[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) :
homotopy (homotopy.null_homotopic_map hom) 0
Tautological construction of the homotopy to zero for maps constructed by
null_homotopic_map, at least when we have the zero' condition.
@[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 : ι) :
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
- homotopy.null_homotopy' h = homotopy.null_homotopy (λ (i j : ι), dite (c.rel j i) (h i j) (λ (_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 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) :
@[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)) :
@[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) :
(homotopy.null_homotopic_map hom).f k₀ = 0
@[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.null_homotopic_map' h).f k₀ = 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}
[category_theory.category V]
[category_theory.preadditive V]
{P Q : chain_complex V ℕ}
(f : Π (i j : ℕ), P.X i ⟶ Q.X j)
(j : ℕ) :
@[simp]
theorem
homotopy.d_next_zero_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) :
@[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 : ℕ) :
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
- homotopy.mk_inductive_aux₁ e zero comm_zero one comm_one succ (n + 2) = ⟨(homotopy.mk_inductive_aux₁ e zero comm_zero one comm_one succ n.succ).snd.fst, ⟨(succ (n + 1) (homotopy.mk_inductive_aux₁ e zero comm_zero one comm_one succ n.succ)).fst, _⟩⟩
- homotopy.mk_inductive_aux₁ e zero comm_zero one comm_one succ 1 = ⟨one, ⟨(succ 0 ⟨zero, ⟨one, comm_one⟩⟩).fst, _⟩⟩
- homotopy.mk_inductive_aux₁ e zero comm_zero one comm_one succ 0 = ⟨zero, ⟨one, comm_one⟩⟩
@[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 : ℕ) :
Σ' (f : homological_complex.X_next P n ⟶ Q.X n) (f' : P.X n ⟶ homological_complex.X_prev Q n), e.f n = homological_complex.d_from P n ≫ f + f' ≫ homological_complex.d_to Q n
An auxiliary construction for mk_inductive.
Equations
- homotopy.mk_inductive_aux₂ e zero 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) := homotopy.mk_inductive_aux₁ e zero comm_zero one comm_one succ n in ⟨(homological_complex.X_next_iso P _).hom ≫ I.fst, ⟨I.snd.fst ≫ (homological_complex.X_prev_iso Q _).inv, _⟩⟩
- homotopy.mk_inductive_aux₂ e zero comm_zero one comm_one succ 0 = ⟨0, ⟨zero ≫ (homological_complex.X_prev_iso Q homotopy.mk_inductive_aux₂._main._proof_1).inv, _⟩⟩
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)) :
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.
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 : ℕ) :
@[simp]
theorem
homotopy.prev_d_zero_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) :
@[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 : ℕ) :
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
- homotopy.mk_coinductive_aux₁ e zero comm_zero one comm_one succ (n + 2) = ⟨(homotopy.mk_coinductive_aux₁ e zero comm_zero one comm_one succ n.succ).snd.fst, ⟨(succ (n + 1) (homotopy.mk_coinductive_aux₁ e zero comm_zero one comm_one succ n.succ)).fst, _⟩⟩
- homotopy.mk_coinductive_aux₁ e zero comm_zero one comm_one succ 1 = ⟨one, ⟨(succ 0 ⟨zero, ⟨one, comm_one⟩⟩).fst, _⟩⟩
- homotopy.mk_coinductive_aux₁ e zero comm_zero one comm_one succ 0 = ⟨zero, ⟨one, comm_one⟩⟩
@[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 : ℕ) :
Σ' (f : P.X n ⟶ homological_complex.X_prev Q n) (f' : homological_complex.X_next P n ⟶ Q.X n), e.f n = f ≫ homological_complex.d_to Q n + homological_complex.d_from P n ≫ f'
An auxiliary construction for mk_inductive.
Equations
- homotopy.mk_coinductive_aux₂ e zero 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' := homotopy.mk_coinductive_aux₁ e zero comm_zero one comm_one succ n in ⟨I.fst ≫ (homological_complex.X_prev_iso Q _).inv, ⟨(homological_complex.X_next_iso P _).hom ≫ I.snd.fst, _⟩⟩
- homotopy.mk_coinductive_aux₂ e zero comm_zero one comm_one succ 0 = ⟨0, ⟨(homological_complex.X_next_iso P homotopy.mk_coinductive_aux₂._main._proof_1).hom ≫ zero, _⟩⟩
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'') :
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.
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)
- hom : C ⟶ D
- inv : D ⟶ C
- homotopy_hom_inv_id : homotopy (self.hom ≫ self.inv) (𝟙 C)
- homotopy_inv_hom_id : homotopy (self.inv ≫ self.hom) (𝟙 D)
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
- homotopy_equiv.has_sizeof_inst
- homotopy_equiv.inhabited
@[refl]
def
homotopy_equiv.refl
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{c : complex_shape ι}
(C : homological_complex V c) :
homotopy_equiv C C
Any complex is homotopy equivalent to itself.
Equations
- homotopy_equiv.refl C = {hom := 𝟙 C, inv := 𝟙 C, homotopy_hom_inv_id := _.mpr (homotopy.refl (𝟙 C)), homotopy_inv_hom_id := _.mpr (homotopy.refl (𝟙 C))}
@[protected, instance]
def
homotopy_equiv.inhabited
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{c : complex_shape ι}
{C : homological_complex V c} :
inhabited (homotopy_equiv C C)
Equations
@[symm]
def
homotopy_equiv.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 : homotopy_equiv C D) :
homotopy_equiv D C
Being homotopy equivalent is a symmetric relation.
Equations
- f.symm = {hom := f.inv, inv := f.hom, homotopy_hom_inv_id := f.homotopy_inv_hom_id, homotopy_inv_hom_id := f.homotopy_hom_inv_id}
@[trans]
def
homotopy_equiv.trans
{ι : 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 : homotopy_equiv C D)
(g : homotopy_equiv D E) :
homotopy_equiv C E
Homotopy equivalence is a transitive relation.
Equations
- f.trans g = {hom := f.hom ≫ g.hom, inv := g.inv ≫ f.inv, homotopy_hom_inv_id := _.mpr (_.mp (((g.homotopy_hom_inv_id.comp_right_id f.inv).comp_left f.hom).trans f.homotopy_hom_inv_id)), homotopy_inv_hom_id := _.mpr (_.mp (((f.homotopy_inv_hom_id.comp_right_id g.hom).comp_left g.inv).trans g.homotopy_inv_hom_id))}
def
homotopy_equiv.of_iso
{ι : 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) :
homotopy_equiv C D
An isomorphism of complexes induces a homotopy equivalence.
Equations
- homotopy_equiv.of_iso f = {hom := f.hom, inv := f.inv, homotopy_hom_inv_id := homotopy.of_eq _, homotopy_inv_hom_id := homotopy.of_eq _}
theorem
homology_map_eq_of_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}
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
(h : homotopy f g)
(i : ι) :
(homology_functor V c i).map f = (homology_functor V 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}
[category_theory.category V]
[category_theory.preadditive V]
{c : complex_shape ι}
{C D : homological_complex V c}
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
(f : homotopy_equiv C D)
(i : ι) :
(homology_functor V c i).obj C ≅ (homology_functor V c i).obj D
Homotopy equivalent complexes have isomorphic homologies.
Equations
- homology_obj_iso_of_homotopy_equiv f i = {hom := (homology_functor V c i).map f.hom, inv := (homology_functor V c i).map f.inv, hom_inv_id' := _, inv_hom_id' := _}
@[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)
def
category_theory.functor.map_homotopy
{ι : 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) :
homotopy ((F.map_homological_complex c).map f) ((F.map_homological_complex c).map g)
An additive functor takes homotopies to homotopies.
def
category_theory.functor.map_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}
{W : Type u_2}
[category_theory.category W]
[category_theory.preadditive W]
(F : V ⥤ W)
[F.additive]
(h : homotopy_equiv C D) :
homotopy_equiv ((F.map_homological_complex c).obj C) ((F.map_homological_complex c).obj D)
An additive functor preserves homotopy equivalences.
Equations
- F.map_homotopy_equiv h = {hom := (F.map_homological_complex c).map h.hom, inv := (F.map_homological_complex c).map h.inv, homotopy_hom_inv_id := _.mpr (_.mpr (F.map_homotopy h.homotopy_hom_inv_id)), homotopy_inv_hom_id := _.mpr (_.mpr (F.map_homotopy h.homotopy_inv_hom_id))}
@[simp]
theorem
category_theory.functor.map_homotopy_equiv_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]
(h : homotopy_equiv C D) :
(F.map_homotopy_equiv h).hom = (F.map_homological_complex c).map h.hom
@[simp]
theorem
category_theory.functor.map_homotopy_equiv_homotopy_hom_inv_id
{ι : 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]
(h : homotopy_equiv C D) :
(F.map_homotopy_equiv h).homotopy_hom_inv_id = _.mpr (_.mpr (F.map_homotopy h.homotopy_hom_inv_id))
@[simp]
theorem
category_theory.functor.map_homotopy_equiv_inv
{ι : 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]
(h : homotopy_equiv C D) :
(F.map_homotopy_equiv h).inv = (F.map_homological_complex c).map h.inv
@[simp]
theorem
category_theory.functor.map_homotopy_equiv_homotopy_inv_hom_id
{ι : 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]
(h : homotopy_equiv C D) :
(F.map_homotopy_equiv h).homotopy_inv_hom_id = _.mpr (_.mpr (F.map_homotopy h.homotopy_inv_hom_id))