mathlib documentation

algebra.homology.homotopy

Chain homotopies #

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

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
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} [category_theory.limits.has_zero_object V] (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
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} [category_theory.limits.has_zero_object V] (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
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
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} [category_theory.limits.has_zero_object V] (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
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} [category_theory.limits.has_zero_object V] (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 to_prev'_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.

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 iself.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
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
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
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
@[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

homotopy.mk_inductive allows us to build a homotopy 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]
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) :
(d_next 0) f = 0
@[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]
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)) [category_theory.limits.has_zero_object V] (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)) [category_theory.limits.has_zero_object V] (i : ) :
(homotopy.mk_inductive_aux₂ e zero comm_zero one comm_one succ i).snd.fst (homological_complex.X_prev_iso Q rfl).hom = (homological_complex.X_next_iso P rfl).inv (homotopy.mk_inductive_aux₂ e zero comm_zero one comm_one succ (i + 1)).fst
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)) [category_theory.limits.has_zero_object V] :

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

Any complex is homotopy equivalent to itself.

Equations
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) :

Being homotopy equivalent is a symmetric relation.

Equations
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 equivalence is a transitive relation.

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