Singular homology

In this file, we define the singular chain complex and singular homology of a topological space. We also calculate the homology of a totally disconnected space as an example.

def AlgebraicTopology.SSet.singularChainComplexFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] : CategoryTheory.Functor C (CategoryTheory.Functor SSet (ChainComplex C ℕ))

The singular chain complex associated to a simplicial set, with coefficients in X : C. One can recover the ordinary singular chain complex when C := Ab and X := ℤ.

def AlgebraicTopology.singularChainComplexFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor C (CategoryTheory.Functor TopCat (ChainComplex C ℕ))

The singular chain complex functor with coefficients in C.

def AlgebraicTopology.singularHomologyFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (n : ℕ) : CategoryTheory.Functor C (CategoryTheory.Functor TopCat C)

The n-th singular homology functor with coefficients in C.

noncomputable def AlgebraicTopology.singularChainComplexFunctorIsoOfTotallyDisconnectedSpace (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (X : TopCat) [TotallyDisconnectedSpace ↑X] : ((singularChainComplexFunctor C).obj R).obj X ≅ ChainComplex.alternatingConst.obj (∐ fun (x : ↑X) => R)

If X is totally disconnected, its singular chain complex is given by R[X] ←0- R[X] ←𝟙- R[X] ←0- R[X] ⋯, where R[X] is the coproduct of copies of R indexed by elements of X.

theorem AlgebraicTopology.singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (n : ℕ) (R : C) (X : TopCat) [TotallyDisconnectedSpace ↑X] [CategoryTheory.Limits.HasZeroObject C] (hn : n ≠ 0) : HomologicalComplex.ExactAt (((singularChainComplexFunctor C).obj R).obj X) n

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

noncomputable def AlgebraicTopology.singularHomologyFunctorZeroOfTotallyDisconnectedSpace (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) (X : TopCat) [TotallyDisconnectedSpace ↑X] : ((singularHomologyFunctor C 0).obj R).obj X ≅ ∐ fun (x : ↑X) => R

The zeroth singular homology of a totally disconnected space is the free R-module generated by elements of X.