Singular homology in degree 0

The main definition in this file is TopCat.singularHomology₀Iso which is an isomorphism ((singularHomologyFunctor C 0).obj R).obj X ≅ ∐ (fun (_ : ZerothHomotopy X) ↦ R) for any X : TopCat.

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

The singular homology of a topological space X with coefficients in R identifies with the coproduct of copies of R indexed by ZerothHomotopy X.

Equations

• X.singularHomology₀Iso R = (TopCat.toSSet.obj X).homology₀Iso R ≪≫ (CategoryTheory.Limits.sigmaConst.obj R).mapIso TopCat.zerothHomotopyEquiv.toIso.symm

noncomputable def TopCat.singularHomology₀ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (X : TopCat) (R : C) : ((AlgebraicTopology.singularHomologyFunctor C 0).obj R).obj X ⟶ R

The augmentation map ((singularHomologyFunctor C 0).obj R).obj X ⟶ R.

Equations

• X.singularHomology₀ε R = (TopCat.toSSet.obj X).homology₀ε R

@[simp]

theorem TopCat.singularHomology₀Iso_sigma_desc_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (X : TopCat) (R : C) : CategoryTheory.CategoryStruct.comp (X.singularHomology₀Iso R).hom (CategoryTheory.Limits.Sigma.desc fun (x : ZerothHomotopy ↑X) => CategoryTheory.CategoryStruct.id R) = X.singularHomology₀ε R

@[simp]

theorem TopCat.singularHomology₀Iso_sigma_desc_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (X : TopCat) (R : C) {Z : C} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.singularHomology₀Iso R).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc fun (x : ZerothHomotopy ↑X) => CategoryTheory.CategoryStruct.id R) h) = CategoryTheory.CategoryStruct.comp (X.singularHomology₀ε R) h

instance TopCat.instIsIsoSingularHomology₀εOfPathConnectedSpaceCarrier {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (X : TopCat) (R : C) [PathConnectedSpace ↑X] : CategoryTheory.IsIso (X.singularHomology₀ε R)