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.SSet.singularChainComplexFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive 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 := ℤ.

Equations

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

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

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

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

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.SSet.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 SSet C).obj (SSet.stdSimplex.obj (SimplexCategory.mk n))

The adjunction Hom(Cⁿ(-, X), F) ≃ Hom(X, F(Δ[n])) for X : C and F : SSet ⥤ 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 (SimplexCategory.mk 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 : ((SimplexCategory.toTop.{w}.comp TopCat.toSSet).obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk n))) => R) ((SSet.stdSimplexToTop.app (SimplexCategory.mk n)).app (Opposite.op (SimplexCategory.mk n)) (SSet.stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.id (SimplexCategory.mk 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 (SimplexCategory.mk n))) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : (TopCat.toSSet.obj X).obj (Opposite.op (SimplexCategory.mk n))) => ((CategoryTheory.evaluation TopCat C).obj (SimplexCategory.toTop.{w}.obj (SimplexCategory.mk 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.