Homotopy invariance of singular homology (simplicial step)

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

First, in the case where the homotopy between two morphisms of simplicial sets f : X ⟶ Y and g : X ⟶ Y is given as combinatorial simplicial homotopy (SimplicialObject.Homotopy), i.e. as family of morphisms X _⦋n⦌ ⟶ Y _⦋n + 1⦌, we use the fact that we still have a similar kind of homotopy between the corresponding morphisms on the simplicial objects in C that are obtained after applying the "free object" functor sigmaConst.obj R : Type _ ⥤ C degreewise, and that a combinatoral homotopy of simplicial objects in a preadditive category induces a homotopy on the alternating face map complexes (see SimplicialObject.Homotopy.toChainHomotopy, which is defined in the file Mathlib/AlgebraicTopology/SimplicialObject/ChainHomotopy.lean).

Secondly, in the case where the homotopy between f and g is given by a usual homotopy of morphisms of simplicial sets (SSet.Homotopy), i.e. by a morphism h : X ⊗ Δ[1] ⟶ Y, we apply the construction above to the combinatorial simplicial homotopy that is deduced from h by using the definition SSet.Homotopy.toSimplicialObjectHomotopy from the file Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean.

noncomputable def CategoryTheory.SimplicialObject.Homotopy.singularChainComplexFunctorObjMap {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasCoproducts C] {X Y : SSet} {f g : X ⟶ Y} (H : Homotopy f g) (R : C) : _root_.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. The assumption is in SimplicialObject.Homotopy, see also SSet.Homotopy.singularChainComplexFunctorObjMap for the variant using SSet.Homotopy as an assumption.

@[deprecated CategoryTheory.SimplicialObject.Homotopy.singularChainComplexFunctorObjMap (since := "2026-03-24")]

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

Alias of CategoryTheory.SimplicialObject.Homotopy.singularChainComplexFunctorObjMap.

---

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. The assumption is in SimplicialObject.Homotopy, see also SSet.Homotopy.singularChainComplexFunctorObjMap for the variant using SSet.Homotopy as an assumption.

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

Simplicially homotopic maps of simplicial sets induce the same map on homology of the singular chain complex (with coefficients in R). The assumption is in SimplicialObject.Homotopy, see also SSet.Homotopy.congr_homologyMap_singularChainComplexFunctor for the variant using SSet.Homotopy as an assumption.

@[deprecated CategoryTheory.SimplicialObject.Homotopy.congr_homologyMap_singularChainComplexFunctor (since := "2026-03-24")]

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

Alias of CategoryTheory.SimplicialObject.Homotopy.congr_homologyMap_singularChainComplexFunctor.

---

Simplicially homotopic maps of simplicial sets induce the same map on homology of the singular chain complex (with coefficients in R). The assumption is in SimplicialObject.Homotopy, see also SSet.Homotopy.congr_homologyMap_singularChainComplexFunctor for the variant using SSet.Homotopy as an assumption.

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

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

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

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