Singular homology of contractible spaces

A contractible space has the singular homology of a point: its homology vanishes in every positive degree, and its reduced homology vanishes in every degree. Consequently, the reduced connecting morphism of a pair is an isomorphism whenever its ambient space is contractible. For TauCeti.diskBoundaryPair n, this identifies the relative homology of a disk modulo its boundary with the reduced homology of the boundary sphere.

Coefficients are an object R of an abelian category with coproducts, as everywhere in relative singular homology.

The results follow Hatcher, Algebraic Topology, Section 2.1: the vanishing of reduced homology for contractible spaces after Corollary 2.11 and Example 2.23 for the disk and its boundary sphere.

theorem TauCeti.isZero_singularHomologyFunctor_of_contractibleSpace {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) (X : TopCat) [ContractibleSpace ↑X] {n : ℕ} (hn : n ≠ 0) : CategoryTheory.Limits.IsZero (((AlgebraicTopology.singularHomologyFunctor C n).obj R).obj X)

The positive-degree singular homology of a contractible space vanishes. The identity of a contractible space is homotopic to a map factoring through a point, whose positive-degree homology vanishes.

theorem TauCeti.isZero_reducedSingularHomologyFunctor_of_contractibleSpace {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] (X : TopCat) [ContractibleSpace ↑X] (n : ℕ) : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor R n).obj X)

The reduced singular homology of a contractible space vanishes in every degree.

instance TopPair.isIso_reducedSingularHomologyδ_of_contractibleSpace {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : TopPair) (R : A) [ContractibleSpace ↑fst] (k : ℕ) : CategoryTheory.IsIso (P.reducedSingularHomologyδ R k)

The reduced connecting morphism of a pair with contractible ambient space is an isomorphism in every degree.