Relative singular homology of totally disconnected pairs

For a pair whose ambient space is totally disconnected, relative singular homology vanishes in positive degrees. The map on zeroth homology induced by the subspace inclusion is injective: when the subspace is nonempty, its singular simplicial set is a retract of the ambient singular simplicial set; the empty case follows from its zero homology. Together with the existing exact sequence of a pair, this isolates the degree-zero quotient as the only nonzero relative homology.

The computation uses Andrew Yang's calculation of singular homology of totally disconnected spaces in Mathlib, Joël Riou's dimension bound for simplicial-set homology there, and the relative singular-homology exact sequence. See Eilenberg--Steenrod, Foundations of Algebraic Topology, Chapters I--III.

noncomputable def TopPair.splitMonoSingularHomologyMapOfTotallyDisconnectedSpace (P : TopPair) [TotallyDisconnectedSpace ↑fst] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (n : ℕ) : CategoryTheory.SplitMono (SSet.homologyMap (TopCat.toSSet.map map) R n)

The homology map of a subspace inclusion into a totally disconnected space is a split monomorphism.

Equations

• One or more equations did not get rendered due to their size.

theorem TopPair.mono_singularHomologyMap_zero_of_totallyDisconnectedSpace (P : TopPair) [TotallyDisconnectedSpace ↑fst] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) : CategoryTheory.Mono (SSet.homologyMap (TopCat.toSSet.map map) R 0)

Inclusion of a subspace of a totally disconnected space is injective on zeroth singular homology.

theorem TopPair.isZero_singularHomology_of_totallyDisconnectedSpace (P : TopPair) [TotallyDisconnectedSpace ↑fst] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {n : ℕ} (hn : n ≠ 0) : CategoryTheory.Limits.IsZero (P.singularHomology R n)

Relative singular homology of a totally disconnected pair vanishes in positive degree.