Homotopy invariance of simplicial homology

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.

The invariance of singular homology (of topological spaces) is obtained in the file Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvarianceTopCat.lean.

noncomputable def CategoryTheory.SimplicialObject.Homotopy.sSetChainComplexMap {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 (SSet.chainComplexMap f R) (SSet.chainComplexMap g R)

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.chainComplexMap for the variant using SSet.Homotopy as an assumption.

Equations

• H.sSetChainComplexMap R = (H.whiskerRight (CategoryTheory.Limits.sigmaConst.obj R)).toChainHomotopy

@[deprecated CategoryTheory.SimplicialObject.Homotopy.sSetChainComplexMap (since := "2026-04-05")]

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 (SSet.chainComplexMap f R) (SSet.chainComplexMap g R)

Alias of CategoryTheory.SimplicialObject.Homotopy.sSetChainComplexMap.

---

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.chainComplexMap for the variant using SSet.Homotopy as an assumption.

Equations

• @CategoryTheory.SimplicialObject.Homotopy.singularChainComplexFunctorObjMap = @CategoryTheory.SimplicialObject.Homotopy.sSetChainComplexMap

@[deprecated CategoryTheory.SimplicialObject.Homotopy.sSetChainComplexMap (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 (SSet.chainComplexMap f R) (SSet.chainComplexMap g R)

Alias of CategoryTheory.SimplicialObject.Homotopy.sSetChainComplexMap.

---

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.chainComplexMap for the variant using SSet.Homotopy as an assumption.

Equations

• @singularChainComplexFunctor_mapHomotopy_of_simplicialHomotopy = @CategoryTheory.SimplicialObject.Homotopy.sSetChainComplexMap

theorem CategoryTheory.SimplicialObject.Homotopy.congr_sSetHomologyMap {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 : ℕ) : SSet.homologyMap f R n = SSet.homologyMap g R 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 for the variant using SSet.Homotopy as an assumption.

@[deprecated CategoryTheory.SimplicialObject.Homotopy.congr_sSetHomologyMap (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 : ℕ) : SSet.homologyMap f R n = SSet.homologyMap g R n

Alias of CategoryTheory.SimplicialObject.Homotopy.congr_sSetHomologyMap.

---

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 for the variant using SSet.Homotopy as an assumption.

@[deprecated CategoryTheory.SimplicialObject.Homotopy.congr_sSetHomologyMap (since := "2026-04-05")]

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 : ℕ) : SSet.homologyMap f R n = SSet.homologyMap g R n

Alias of CategoryTheory.SimplicialObject.Homotopy.congr_sSetHomologyMap.

---

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 for the variant using SSet.Homotopy as an assumption.

noncomputable def SSet.Homotopy.chainComplexMap {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 (SSet.chainComplexMap f R) (SSet.chainComplexMap g R)

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.

Equations

• H.chainComplexMap R = H.toSimplicialObjectHomotopy.sSetChainComplexMap R

@[deprecated SSet.Homotopy.chainComplexMap (since := "2026-04-05")]

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 (SSet.chainComplexMap f R) (SSet.chainComplexMap g R)

Alias of SSet.Homotopy.chainComplexMap.

---

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.

Equations

• @SSet.Homotopy.singularChainComplexFunctorObjMap = @SSet.Homotopy.chainComplexMap

theorem SSet.Homotopy.congr_homologyMap {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 : ℕ) : SSet.homologyMap f R n = SSet.homologyMap g R n

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

@[deprecated SSet.Homotopy.congr_homologyMap (since := "2026-04-05")]

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 : ℕ) : SSet.homologyMap f R n = SSet.homologyMap g R n

Alias of SSet.Homotopy.congr_homologyMap.

---

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