Homotopy invariance of singular homology (simplicial step)

This file proves that simplicially homotopic morphisms of simplicial sets induce the same maps on singular homology (with coefficients in an object of a preadditive category with coproducts).

noncomputable def singularChainComplexFunctor_mapHomotopy_of_simplicialHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) {X Y : SSet} (f g : X ⟶ Y) (H : CategoryTheory.SimplicialObject.Homotopy f g) : Homotopy (((AlgebraicTopology.SSet.singularChainComplexFunctor C).obj R).map f) (((AlgebraicTopology.SSet.singularChainComplexFunctor C).obj R).map g)

If f and g are simplicially homotopic maps of simplicial sets, then they induce chain-homotopic maps on the singular chain complexes with coefficients in R.

Equations

• singularChainComplexFunctor_mapHomotopy_of_simplicialHomotopy R f g H = (H.whiskerRight (CategoryTheory.Limits.sigmaConst.obj R)).toChainHomotopy

theorem singularChainComplexFunctor_map_homology_eq_of_simplicialHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) {X Y : SSet} (f g : X ⟶ Y) [CategoryTheory.CategoryWithHomology C] (H : CategoryTheory.SimplicialObject.Homotopy f g) (n : ℕ) : (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n).map (((AlgebraicTopology.SSet.singularChainComplexFunctor C).obj R).map f) = (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n).map (((AlgebraicTopology.SSet.singularChainComplexFunctor C).obj R).map g)

Simplicially homotopic maps of simplicial sets induce the same map on homology of the singular chain complex (with coefficients in R).