Reduced singular homology

Reduced singular homology is the kernel of the augmentation in degree zero and ordinary singular homology in positive degrees. The inclusion into ordinary homology is natural and reduced homology is homotopy invariant. A chosen point splits zeroth homology as reduced homology plus the coefficient object; the splitting commutes with maps preserving that point.

Coefficients lie in a preadditive category with coproducts, homology and kernels. The splitting isomorphism additionally uses binary biproducts. No connectedness assumption is needed for the splitting; for a path-connected space the reduced homology object in degree zero vanishes, and for the empty space reduced homology vanishes in every degree.

In degree zero, a chosen point identifies reduced homology with the coproduct of copies of the coefficient object indexed by the path components other than that of the point (TauCeti.reducedSingularHomology₀Iso); the generator at the component of y is the class [y] - [x]. This is the kernel of the codiagonal of Mathlib's TopCat.singularHomology₀Iso.

This follows Hatcher, Algebraic Topology, Section 2.1, using Mathlib's singular homology and augmentation and ShortComplex.Splitting.isoBinaryBiproduct.

@[simp]

theorem TauCeti.singularHomologyMap_singularHomology₀ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) {X Y : TopCat} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor C 0).obj R).map f) (Y.singularHomology₀ε R) = X.singularHomology₀ε R

The augmentation of zeroth singular homology is natural in the space.

@[simp]

theorem TauCeti.singularHomologyMap_singularHomology₀ε_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) {X Y : TopCat} (f : X ⟶ Y) {Z : C} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor C 0).obj R).map f) (CategoryTheory.CategoryStruct.comp (Y.singularHomology₀ε R) h) = CategoryTheory.CategoryStruct.comp (X.singularHomology₀ε R) h

The augmentation of zeroth singular homology is natural in the space.

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

The class of a chosen point gives a section of the singular augmentation.

Equations

• TauCeti.singularHomology₀Section R x = TauCeti.SSet.ιHomology₀ R (TopCat.toSSetObj₀Equiv.symm x)

theorem TauCeti.singularHomology₀Section_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) {X : TopCat} (x : ↑X) : singularHomology₀Section R x = SSet.ιHomology₀ R (TopCat.toSSetObj₀Equiv.symm x)

@[simp]

theorem TauCeti.singularHomology₀Section_singularHomology₀ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) {X : TopCat} (x : ↑X) : CategoryTheory.CategoryStruct.comp (singularHomology₀Section R x) (X.singularHomology₀ε R) = CategoryTheory.CategoryStruct.id R

The class of a chosen point is a right inverse to the augmentation.

@[simp]

theorem TauCeti.singularHomology₀Section_singularHomology₀ε_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) {X : TopCat} (x : ↑X) {Z : C} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularHomology₀Section R x) (CategoryTheory.CategoryStruct.comp (X.singularHomology₀ε R) h) = h

The class of a chosen point is a right inverse to the augmentation.

@[simp]

theorem TauCeti.singularHomology₀Section_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) {X Y : TopCat} (f : X ⟶ Y) (x : ↑X) : CategoryTheory.CategoryStruct.comp (singularHomology₀Section R x) (((AlgebraicTopology.singularHomologyFunctor C 0).obj R).map f) = singularHomology₀Section R ((CategoryTheory.ConcreteCategory.hom f) x)

The section is natural in the chosen point under continuous maps.

@[simp]

theorem TauCeti.singularHomology₀Section_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) {X Y : TopCat} (f : X ⟶ Y) (x : ↑X) {Z : C} (h : ((AlgebraicTopology.singularHomologyFunctor C 0).obj R).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularHomology₀Section R x) (CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor C 0).obj R).map f) h) = CategoryTheory.CategoryStruct.comp (singularHomology₀Section R ((CategoryTheory.ConcreteCategory.hom f) x)) h

The section is natural in the chosen point under continuous maps.

@[simp]

theorem TauCeti.singularHomology₀Section_singularHomology₀Iso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) {X : TopCat} (x : ↑X) : CategoryTheory.CategoryStruct.comp (singularHomology₀Section R x) (X.singularHomology₀Iso R).hom = CategoryTheory.Limits.Sigma.ι (fun (x : ZerothHomotopy ↑X) => R) (ZerothHomotopy.mk x)

Mathlib's identification of zeroth homology with the coproduct over path components sends the class of a point to the coproduct inclusion indexed by its path component.

@[simp]

theorem TauCeti.singularHomology₀Section_singularHomology₀Iso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) {X : TopCat} (x : ↑X) {Z : C} (h : (∐ fun (x : ZerothHomotopy ↑X) => R) ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularHomology₀Section R x) (CategoryTheory.CategoryStruct.comp (X.singularHomology₀Iso R).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : ZerothHomotopy ↑X) => R) (ZerothHomotopy.mk x)) h

Mathlib's identification of zeroth homology with the coproduct over path components sends the class of a point to the coproduct inclusion indexed by its path component.

noncomputable def TauCeti.reducedSingularHomologyFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] : ℕ → CategoryTheory.Functor TopCat C

Reduced singular homology: the augmentation kernel in degree zero and ordinary singular homology in positive degrees.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.reducedSingularHomologyFunctor R n.succ = (AlgebraicTopology.singularHomologyFunctor C (n + 1)).obj R

@[simp]

theorem TauCeti.reducedSingularHomologyFunctor_zero_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] (X : TopCat) : (reducedSingularHomologyFunctor R 0).obj X = CategoryTheory.Limits.kernel (X.singularHomology₀ε R)

@[simp]

theorem TauCeti.reducedSingularHomologyFunctor_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] (n : ℕ) : reducedSingularHomologyFunctor R (n + 1) = (AlgebraicTopology.singularHomologyFunctor C (n + 1)).obj R

noncomputable def TauCeti.reducedSingularHomologyι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] (n : ℕ) : reducedSingularHomologyFunctor R n ⟶ (AlgebraicTopology.singularHomologyFunctor C n).obj R

The canonical inclusion from reduced to ordinary singular homology.

Equations

• TauCeti.reducedSingularHomologyι R 0 = { app := fun (X : TopCat) => CategoryTheory.Limits.kernel.ι (X.singularHomology₀ε R), naturality := ⋯ }
• TauCeti.reducedSingularHomologyι R n.succ = CategoryTheory.CategoryStruct.id (TauCeti.reducedSingularHomologyFunctor R (n + 1))

@[simp]

theorem TauCeti.reducedSingularHomologyι_zero_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] (X : TopCat) : (reducedSingularHomologyι R 0).app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.kernel.ι (X.singularHomology₀ε R))

@[simp]

theorem TauCeti.reducedSingularHomologyι_succ_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] (n : ℕ) (X : TopCat) : (reducedSingularHomologyι R (n + 1)).app X = CategoryTheory.eqToHom ⋯

instance TauCeti.instMonoAppTopCatReducedSingularHomologyι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] (n : ℕ) (X : TopCat) : CategoryTheory.Mono ((reducedSingularHomologyι R n).app X)

noncomputable def TauCeti.reducedSingularHomologySuccIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] (n : ℕ) : reducedSingularHomologyFunctor R (n + 1) ≅ (AlgebraicTopology.singularHomologyFunctor C (n + 1)).obj R

Reduced and ordinary singular homology agree naturally in positive degrees.

Equations

• TauCeti.reducedSingularHomologySuccIso R n = CategoryTheory.eqToIso ⋯

@[simp]

theorem TauCeti.reducedSingularHomologySuccIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] (n : ℕ) : (reducedSingularHomologySuccIso R n).hom = reducedSingularHomologyι R (n + 1)

theorem TauCeti.reducedSingularHomologyFunctor_map_eq_of_homotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] {X Y : TopCat} {f g : X ⟶ Y} (H : TopCat.Homotopy f g) (n : ℕ) : (reducedSingularHomologyFunctor R n).map f = (reducedSingularHomologyFunctor R n).map g

Homotopic continuous maps induce the same map on reduced singular homology.

noncomputable def ContinuousMap.HomotopyEquiv.reducedSingularHomologyIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] {X Y : Type w} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) (n : ℕ) : (TauCeti.reducedSingularHomologyFunctor R n).obj ↧X ≅ (TauCeti.reducedSingularHomologyFunctor R n).obj ↧Y

A homotopy equivalence induces an isomorphism on reduced singular homology in every degree, with inverse induced by the homotopy inverse.

Equations

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

@[simp]

theorem ContinuousMap.HomotopyEquiv.reducedSingularHomologyIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] {X Y : Type w} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) (n : ℕ) : (reducedSingularHomologyIso R e n).hom = (TauCeti.reducedSingularHomologyFunctor R n).map (TopCat.ofHom e.toFun)

@[simp]

theorem ContinuousMap.HomotopyEquiv.reducedSingularHomologyIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] {X Y : Type w} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) (n : ℕ) : (reducedSingularHomologyIso R e n).inv = (TauCeti.reducedSingularHomologyFunctor R n).map (TopCat.ofHom e.invFun)

theorem TauCeti.isZero_reducedSingularHomologyFunctor_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] (X : TopCat) [PathConnectedSpace ↑X] : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor R 0).obj X)

The reduced zeroth homology of a path-connected space is zero.

theorem TauCeti.isZero_reducedSingularHomologyFunctor_of_isEmpty {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] (X : TopCat) [IsEmpty ↑X] (n : ℕ) : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor R n).obj X)

The reduced singular homology of the empty space vanishes in every degree.

noncomputable def TauCeti.reducedSingularHomology₀Iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] {X : TopCat} (x : ↑X) : (reducedSingularHomologyFunctor R 0).obj X ≅ ∐ fun (x : { c : ZerothHomotopy ↑X // c ≠ ZerothHomotopy.mk x }) => R

Reduced homology in degree zero is free on the path components other than that of a basepoint. A point x identifies the reduced zeroth singular homology of X with the coproduct of copies of R indexed by the path components of X different from that of x. The generator at the component of y corresponds to the class [y] - [x] (TauCeti.ι_reducedSingularHomology₀Iso_inv_ι).

Equations

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

theorem TauCeti.ι_reducedSingularHomology₀Iso_inv_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] {X : TopCat} (x y : ↑X) (h : ZerothHomotopy.mk y ≠ ZerothHomotopy.mk x) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : { c : ZerothHomotopy ↑X // c ≠ ZerothHomotopy.mk x }) => R) ⟨ZerothHomotopy.mk y, h⟩) (CategoryTheory.CategoryStruct.comp (reducedSingularHomology₀Iso R x).inv ((reducedSingularHomologyι R 0).app X)) = singularHomology₀Section R y - singularHomology₀Section R x

The generator of TauCeti.reducedSingularHomology₀Iso at the path component of y is the class [y] - [x] in ordinary zeroth homology.

theorem TauCeti.ι_reducedSingularHomology₀Iso_inv_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] {X : TopCat} (x y : ↑X) (h : ZerothHomotopy.mk y ≠ ZerothHomotopy.mk x) {Z : C} (h✝ : ((AlgebraicTopology.singularHomologyFunctor C 0).obj R).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : { c : ZerothHomotopy ↑X // c ≠ ZerothHomotopy.mk x }) => R) ⟨ZerothHomotopy.mk y, h⟩) (CategoryTheory.CategoryStruct.comp (reducedSingularHomology₀Iso R x).inv (CategoryTheory.CategoryStruct.comp ((reducedSingularHomologyι R 0).app X) h✝)) = CategoryTheory.CategoryStruct.comp (singularHomology₀Section R y - singularHomology₀Section R x) h✝

The generator of TauCeti.reducedSingularHomology₀Iso at the path component of y is the class [y] - [x] in ordinary zeroth homology.

noncomputable def TauCeti.singularHomology₀SplitIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : TopCat} (x : ↑X) : ((AlgebraicTopology.singularHomologyFunctor C 0).obj R).obj X ≅ (reducedSingularHomologyFunctor R 0).obj X ⊞ R

A basepoint splits ordinary zeroth singular homology into its reduced part and one copy of the coefficient object.

Equations

• TauCeti.singularHomology₀SplitIso R x = (TauCeti.singularHomology₀Splitting✝ R x).isoBinaryBiproduct

@[simp]

theorem TauCeti.singularHomology₀SplitIso_hom_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : TopCat} (x : ↑X) : CategoryTheory.CategoryStruct.comp (singularHomology₀SplitIso R x).hom CategoryTheory.Limits.biprod.fst = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift (X.singularHomology₀ε R) (CategoryTheory.CategoryStruct.id (((AlgebraicTopology.singularHomologyFunctor C 0).obj R).obj X) - CategoryTheory.CategoryStruct.comp (X.singularHomology₀ε R) (singularHomology₀Section R x)) ⋯) (CategoryTheory.eqToHom ⋯)

The reduced projection subtracts the chosen point class weighted by the augmentation.

@[simp]

theorem TauCeti.singularHomology₀SplitIso_hom_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : TopCat} (x : ↑X) {Z : C} (h : (reducedSingularHomologyFunctor R 0).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularHomology₀SplitIso R x).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift (X.singularHomology₀ε R) (CategoryTheory.CategoryStruct.id (((AlgebraicTopology.singularHomologyFunctor C 0).obj R).obj X) - CategoryTheory.CategoryStruct.comp (X.singularHomology₀ε R) (singularHomology₀Section R x)) ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

The reduced projection subtracts the chosen point class weighted by the augmentation.

@[simp]

theorem TauCeti.singularHomology₀SplitIso_hom_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : TopCat} (x : ↑X) : CategoryTheory.CategoryStruct.comp (singularHomology₀SplitIso R x).hom CategoryTheory.Limits.biprod.snd = X.singularHomology₀ε R

The coefficient projection of the splitting is the augmentation.

@[simp]

theorem TauCeti.singularHomology₀SplitIso_hom_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : TopCat} (x : ↑X) {Z : C} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularHomology₀SplitIso R x).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (X.singularHomology₀ε R) h

The coefficient projection of the splitting is the augmentation.

@[simp]

theorem TauCeti.inl_singularHomology₀SplitIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : TopCat} (x : ↑X) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (singularHomology₀SplitIso R x).inv = (reducedSingularHomologyι R 0).app X

The reduced summand of the inverse splitting is the canonical reduced inclusion.

@[simp]

theorem TauCeti.inl_singularHomology₀SplitIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : TopCat} (x : ↑X) {Z : C} (h : ((AlgebraicTopology.singularHomologyFunctor C 0).obj R).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (singularHomology₀SplitIso R x).inv h) = CategoryTheory.CategoryStruct.comp ((reducedSingularHomologyι R 0).app X) h

The reduced summand of the inverse splitting is the canonical reduced inclusion.

@[simp]

theorem TauCeti.inr_singularHomology₀SplitIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : TopCat} (x : ↑X) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (singularHomology₀SplitIso R x).inv = singularHomology₀Section R x

The coefficient summand of the inverse splitting is the section at the chosen point.

@[simp]

theorem TauCeti.inr_singularHomology₀SplitIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : TopCat} (x : ↑X) {Z : C} (h : ((AlgebraicTopology.singularHomologyFunctor C 0).obj R).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (singularHomology₀SplitIso R x).inv h) = CategoryTheory.CategoryStruct.comp (singularHomology₀Section R x) h

The coefficient summand of the inverse splitting is the section at the chosen point.

theorem TauCeti.singularHomology₀SplitIso_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : TopCat} (f : X ⟶ Y) (x : ↑X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map ((reducedSingularHomologyFunctor R 0).map f) (CategoryTheory.CategoryStruct.id R)) (singularHomology₀SplitIso R ((CategoryTheory.ConcreteCategory.hom f) x)).inv = CategoryTheory.CategoryStruct.comp (singularHomology₀SplitIso R x).inv (((AlgebraicTopology.singularHomologyFunctor C 0).obj R).map f)

The splitting of zeroth homology is natural in pointed maps.

theorem TauCeti.singularHomology₀SplitIso_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (R : C) [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : TopCat} (f : X ⟶ Y) (x : ↑X) {Z : C} (h : ((AlgebraicTopology.singularHomologyFunctor C 0).obj R).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map ((reducedSingularHomologyFunctor R 0).map f) (CategoryTheory.CategoryStruct.id R)) (CategoryTheory.CategoryStruct.comp (singularHomology₀SplitIso R ((CategoryTheory.ConcreteCategory.hom f) x)).inv h) = CategoryTheory.CategoryStruct.comp (singularHomology₀SplitIso R x).inv (CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor C 0).obj R).map f) h)

The splitting of zeroth homology is natural in pointed maps.