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.

noncomputable 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.

Equations

• AlgebraicTopology.singularChainComplexFunctor C = (SSet.chainComplexFunctor C).comp ((CategoryTheory.Functor.whiskeringLeft TopCat SSet (ChainComplex C ℕ)).obj TopCat.toSSet)

instance AlgebraicTopology.instAdditiveFunctorTopCatChainComplexNatSingularChainComplexFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : (singularChainComplexFunctor C).Additive

instance AlgebraicTopology.instPreservesMonomorphismsTopCatChainComplexNatObjFunctorSingularChainComplexFunctorOfHasPullbacks (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasPullbacks C] {X : C} : ((singularChainComplexFunctor C).obj X).PreservesMonomorphisms

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

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

Equations

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

noncomputable def AlgebraicTopology.singularChainComplexFunctorAdjunction (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (n : ℕ) : (CategoryTheory.Functor.postcompose₂.obj (HomologicalComplex.eval C (ComplexShape.down ℕ) n)).obj (singularChainComplexFunctor C) ⊣ (CategoryTheory.evaluation TopCat C).obj (SimplexCategory.toTop.{w}.obj { len := n })

The adjunction Hom(Cⁿ(-, X), F) ≃ Hom(X, F(Δ[n])) for X : C and F : Top ⥤ C.

Equations

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

theorem AlgebraicTopology.singularChainComplexFunctorAdjunction_unit_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (n : ℕ) (R : C) : (singularChainComplexFunctorAdjunction C n).unit.app R = CategoryTheory.Limits.Sigma.ι (fun (x : (fun (X : Type w) => X) (((SimplexCategory.toTop.{w}.comp TopCat.toSSet).obj { len := n }).obj (Opposite.op { len := n }))) => R) ((CategoryTheory.ConcreteCategory.hom ((SSet.stdSimplexToTop.app { len := n }).app (Opposite.op { len := n }))) (SSet.stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.id { len := n })))

theorem AlgebraicTopology.ι_singularChainComplexFunctorAdjunction_counit_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (n : ℕ) (F : CategoryTheory.Functor TopCat C) (X : TopCat) (i : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) => ((CategoryTheory.evaluation TopCat C).obj (SimplexCategory.toTop.{w}.obj { len := n })).obj F) i) (((singularChainComplexFunctorAdjunction C n).counit.app F).app X) = F.map i.down

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.

Equations

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

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] (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] (n : ℕ) (R : C) (X : TopCat) [TotallyDisconnectedSpace ↑X] [CategoryTheory.CategoryWithHomology C] (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] (R : C) (X : TopCat) [TotallyDisconnectedSpace ↑X] [CategoryTheory.CategoryWithHomology C] : ((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.

Equations

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