Homotopy invariance of singular homology

In this file, we show that for any homotopy H : TopCat.Homotopy f g between two morphisms f : X ⟶ Y and g : X ⟶ Y in TopCat, the corresponding morphisms on the singular chain complexes are homotopic, and in particular the induced morphisms on singular homology are equal.

The proof proceeds by observing that this result is a particular case of the homotopy invariance of the homology of simplicial sets (see the file Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvariance.lean), applied to the morphisms TopCat.toSSet.map f and TopCat.toSSet.map g between the singular simplicial sets of X and Y. That the homotopy H induces a homotopy between these morphisms of simplicial sets is the definition TopCat.Homotopy.toSSet which appeared in the file Mathlib/Topology/Homotopy/TopCat/ToSSet.lean.

This result was first formalized in Lean 3 in 2022 by Brendan Seamus Murphy (with a different proof).

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

Two homotopic morphisms in TopCat induce homotopic morphisms on the singular chain complexes with coefficients in R (e.g. R := ℤ considered as an object of the category of abelian groups).

Equations

• H.singularChainComplexFunctorObjMap R = H.toSSet.singularChainComplexFunctorObjMap R

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

Two homotopic morphisms in TopCat induce equal morphisms on the singular homology with coefficients in R (e.g. R := ℤ considered as an object of the category of abelian groups).