Homotopy invariance of relative simplicial homology

A homotopy between morphisms of a pair of simplicial sets, that is, an SSetPair.Homotopy, induces a chain homotopy between the maps of relative chain complexes, so that homotopic morphisms of pairs induce the same map on relative simplicial homology, and morphisms of pairs that are inverse to each other up to homotopy induce isomorphisms.

The relative chain complex is the degreewise cokernel of the inclusion of the chains of the subcomplex, and the chain homotopy is obtained from Homotopy.descCokernel. The input is the compatibility of the chain homotopies of Mathlib's absolute homotopy invariance (Mathlib/AlgebraicTopology/SimplicialSet/Homology/HomotopyInvariance.lean, F. Odermatt, J. Riou), which comes from the commutative square of simplicial homotopies.

theorem SSet.Homotopy.chainComplexMap_hom_comm {X Y X' Y' : SSet} {f g : X ⟶ Y} {f' g' : X' ⟶ Y'} {u : X ⟶ X'} {v : Y ⟶ Y'} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (H : Homotopy f g) (H' : Homotopy f' g') (hu : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight u (stdSimplex.obj { len := 1 })) H'.h = CategoryTheory.CategoryStruct.comp H.h v) (R : C) (p q : ℕ) : CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap u R).f p) ((H'.chainComplexMap R).hom p q) = CategoryTheory.CategoryStruct.comp ((H.chainComplexMap R).hom p q) ((SSet.chainComplexMap v R).f q)

The chain homotopies induced by simplicial homotopies which fit into a commutative square are compatible with the chain maps induced by that square.

theorem SSetPair.Homotopy.chainComplexMap_condition {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : SSetPair} {f g : P ⟶ P'} (H : Homotopy f g) (R : C) (i j : ℕ) : CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap P.hom R).f i) (CategoryTheory.CategoryStruct.comp ((H.right.chainComplexMap R).hom i j) ((P'.chainComplexπ R).f j)) = 0

The chain homotopy on the total complexes carries the chains of the subcomplex into the kernel of the quotient map onto relative chains.

noncomputable def SSetPair.Homotopy.chainComplexMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : SSetPair} {f g : P ⟶ P'} (H : Homotopy f g) (R : C) : _root_.Homotopy (SSetPair.chainComplexMap f R) (SSetPair.chainComplexMap g R)

A homotopy of morphisms of pairs of simplicial sets induces a chain homotopy between the induced morphisms of relative chain complexes.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSetPair.Homotopy.chainComplexMap_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : SSetPair} {f g : P ⟶ P'} (H : Homotopy f g) (R : C) (p q : ℕ) : CategoryTheory.CategoryStruct.comp ((P.chainComplexπ R).f p) ((H.chainComplexMap R).hom p q) = CategoryTheory.CategoryStruct.comp ((H.right.chainComplexMap R).hom p q) ((P'.chainComplexπ R).f q)

@[simp]

theorem SSetPair.Homotopy.chainComplexMap_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : SSetPair} {f g : P ⟶ P'} (H : Homotopy f g) (R : C) (p q : ℕ) {Z : C} (h : (P'.chainComplex R).X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((P.chainComplexπ R).f p) (CategoryTheory.CategoryStruct.comp ((H.chainComplexMap R).hom p q) h) = CategoryTheory.CategoryStruct.comp ((H.right.chainComplexMap R).hom p q) (CategoryTheory.CategoryStruct.comp ((P'.chainComplexπ R).f q) h)

theorem SSetPair.Homotopy.congr_homologyMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : SSetPair} {f g : P ⟶ P'} (H : Homotopy f g) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : SSetPair.homologyMap f R n = SSetPair.homologyMap g R n

Homotopic morphisms of pairs of simplicial sets induce the same morphism on relative simplicial homology.

theorem SSetPair.isIso_homologyMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {P P' : SSetPair} (f : P ⟶ P') (f' : P' ⟶ P) (H : Homotopy (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.id P)) (H' : Homotopy (CategoryTheory.CategoryStruct.comp f' f) (CategoryTheory.CategoryStruct.id P')) (R : C) (n : ℕ) : CategoryTheory.IsIso (SSetPair.homologyMap f R n)

Morphisms of pairs of simplicial sets which are inverse to each other up to homotopy induce isomorphisms on relative simplicial homology.