Documentation

TauCeti.AlgebraicTopology.Singular.Point

The singular chains of a point #

The singular chain complex of a one-point space X, with coefficients in an object R of a preadditive category, is chain homotopy equivalent to R placed in degree zero (TauCeti.pointSingularChainHomotopyEquiv). The forward map is the augmentation, which sends the unique singular vertex to the identity of R, and the inverse includes R as the summand of that vertex.

Unlike the vanishing of positive-degree homology, a chain homotopy equivalence survives any additive functor. Applying Hom(-, M) to it computes the singular cohomology of a point with arbitrary coefficients (TauCeti.pointSingularCochainHomotopyEquiv), without projectivity or injectivity assumptions.

A point is totally disconnected, so Mathlib identifies its singular chains with the alternating constant complex on the coefficients summed over the point (AlgebraicTopology.singularChainComplexFunctorIsoOfTotallyDisconnectedSpace), and that complex contracts onto its degree-zero term (ChainComplex.alternatingConstHomotopyEquiv, from the extra degeneracy SimplicialObject.Augmented.ExtraDegeneracy.const). The construction of the contraction, and of its cochain counterpart, follows the unmerged Tau Ceti pull request https://github.com/TauCetiProject/TauCeti/pull/20882.

Main declarations #

References #

source
noncomputable def TauCeti.pointSingularChainHomotopyEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (R : C) (X : TopCat) [Unique ↑X] :
HomotopyEquiv ((TopCat.toSSet.obj X).chainComplex R) ((ChainComplex.single₀ C).obj R)

The singular chains of a point contract onto the coefficients. For a one-point space X, the singular chain complex with coefficients in R is chain homotopy equivalent to R in degree zero. The forward map is the augmentation and the inverse is the inclusion of the unique vertex.

Instances For
    source
    @[simp]
    theorem TauCeti.ιChainComplex_pointSingularChainHomotopyEquiv_hom_f_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (R : C) (X : TopCat) [Unique ↑X] (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := 0 })) :
    CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) ((pointSingularChainHomotopyEquiv R X).hom.f 0) = (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 R).inv

    The augmentation sends the summand of the unique singular vertex of a point identically to the coefficients.

    source
    theorem TauCeti.ιChainComplex_pointSingularChainHomotopyEquiv_hom_f_zero_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (R : C) (X : TopCat) [Unique ↑X] (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := 0 })) {Z : C} (h : ((ChainComplex.single₀ C).obj R).X 0 ⟶ Z) :
    CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) (CategoryTheory.CategoryStruct.comp ((pointSingularChainHomotopyEquiv R X).hom.f 0) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 R).inv h

    The augmentation sends the summand of the unique singular vertex of a point identically to the coefficients.

    source
    instance TauCeti.isIso_pointSingularChainHomotopyEquiv_hom_f_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (R : C) (X : TopCat) [Unique ↑X] :
    CategoryTheory.IsIso ((pointSingularChainHomotopyEquiv R X).hom.f 0)

    In degree zero, the augmentation of the singular chains of a point is an isomorphism.

    source
    theorem TauCeti.pointSingularChainHomotopyEquiv_inv_f_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (R : C) (X : TopCat) [Unique ↑X] (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := 0 })) :
    (pointSingularChainHomotopyEquiv R X).inv.f 0 = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 R).hom ((TopCat.toSSet.obj X).ιChainComplex σ)

    The inverse of the contraction of the singular chains of a point includes the coefficients as the summand of the unique singular vertex.

    source
    theorem TauCeti.pointSingularChainHomotopyEquiv_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (R : C) (X : TopCat) [Unique ↑X] {S : C} (f : R ⟶ S) :
    CategoryTheory.CategoryStruct.comp (((SSet.chainComplexFunctor C).map f).app (TopCat.toSSet.obj X)) (pointSingularChainHomotopyEquiv S X).hom = CategoryTheory.CategoryStruct.comp (pointSingularChainHomotopyEquiv R X).hom ((ChainComplex.single₀ C).map f)

    The augmentation of the singular chains of a point is natural in the coefficients.

    source
    theorem TauCeti.pointSingularChainHomotopyEquiv_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (R : C) (X : TopCat) [Unique ↑X] {S : C} (f : R ⟶ S) {Z : ChainComplex C ℕ} (h : (ChainComplex.single₀ C).obj S ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (((SSet.chainComplexFunctor C).map f).app (TopCat.toSSet.obj X)) (CategoryTheory.CategoryStruct.comp (pointSingularChainHomotopyEquiv S X).hom h) = CategoryTheory.CategoryStruct.comp (pointSingularChainHomotopyEquiv R X).hom (CategoryTheory.CategoryStruct.comp ((ChainComplex.single₀ C).map f) h)

    The augmentation of the singular chains of a point is natural in the coefficients.