Singular cohomology of a point

The singular cochains of a one-point space X, with coefficients Hom(-, M) applied to singular chains with coefficients in R, are cochain homotopy equivalent to the module Hom(R, M) placed in degree zero (TauCeti.pointSingularCochainHomotopyEquiv). This is the contravariant image of the chain contraction TauCeti.pointSingularChainHomotopyEquiv, so it holds for arbitrary coefficients: positive-degree singular cohomology of a point vanishes (TauCeti.isZero_singularCohomology_point) without any projectivity, injectivity or hereditary-ring hypothesis, as a universal coefficient argument would need. In degree zero the comparison evaluates a cocycle on the unique singular vertex (TauCeti.singularCohomologyPointZeroIso), and it sends the class of a constant cocycle, such as the unit of the cup product, to its value.

Consequently a nullhomotopic map, which factors through a point up to homotopy, induces zero on positive-degree singular cohomology (TopCat.singularCohomologyMap_eq_zero_of_nullhomotopic), and positive-degree singular cohomology of a contractible space vanishes (TauCeti.isZero_singularCohomology_of_contractibleSpace). For the open sets of a categorical cover in the sense of Lusternik and Schnirelmann, whose inclusions are nullhomotopic, this says that every positive-degree class restricts to zero on each open of the cover, so comes from the cohomology relative to that open (TopPair.epi_singularCohomologyπ_of_nullhomotopic), which is the input to the cup-length lower bound for the Lusternik–Schnirelmann category.

Main declarations

• TauCeti.pointSingularCochainHomotopyEquiv: the cochain homotopy equivalence between the singular cochains of a point and Hom(R, M) in degree zero, and TauCeti.pointSingularCochainHomotopyEquiv_hom_f_zero_apply, its formula in degree zero.
• TauCeti.isZero_singularCohomology_point: Hⁿ(pt; M) = 0 for n ≠ 0.
• TauCeti.singularCohomologyPointZeroIso: H⁰(pt; M) ≅ Hom(R, M), by evaluation on the unique vertex (TauCeti.singularCohomologyPointZeroIso_hom_homologyπ_apply), with inverse sending e to the class of the constant cocycle (TauCeti.singularCohomologyPointZeroIso_inv_apply). It is natural in both coefficients (TauCeti.singularCohomologyPointZeroIso_hom_naturality_right and TauCeti.singularCohomologyPointZeroIso_hom_naturality_left).
• TopCat.singularCohomologyMap_eq_zero_of_nullhomotopic and TauCeti.isZero_singularCohomology_of_contractibleSpace.
• TopPair.epi_singularCohomologyπ_of_nullhomotopic: if the inclusion A ⟶ X is nullhomotopic, every positive-degree class of X comes from Hⁿ(X, A).
• TauCeti.isZero_singularCohomology_of_isEmpty: the singular cohomology of the empty space vanishes.

The cochain contraction follows the unmerged Tau Ceti pull request https://github.com/TauCetiProject/TauCeti/pull/20882.

References

• A. Hatcher, Algebraic Topology, Sections 3.1 and 3.2.
• O. Cornea, G. Lupton, J. Oprea, D. Tanré, Lusternik–Schnirelmann Category, Mathematical Surveys and Monographs 103, AMS, 2003, Section 1.5, for the cup-length bound.

noncomputable def TauCeti.pointSingularCochainHomotopyEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [Unique ↑X] : HomotopyEquiv (TopCat.singularCochainComplex R k M X) ((CochainComplex.single₀ (ModuleCat k)).obj ↧(R ⟶ M))

The singular cochains of a point contract onto Hom(R, M) in degree zero. For a one-point space X, the singular cochain complex Hom(C(X; R), M) is cochain homotopy equivalent to the module Hom(R, M) placed in degree zero. The forward map evaluates a zero-cochain on the unique singular vertex.

theorem TauCeti.pointSingularCochainHomotopyEquiv_hom_f_zero_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [Unique ↑X] (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := 0 })) (a : ((TopCat.toSSet.obj X).chainComplex R).X 0 ⟶ M) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 ↧(R ⟶ M)).hom) ((CategoryTheory.ConcreteCategory.hom ((pointSingularCochainHomotopyEquiv R k M X).hom.f 0)) a) = CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) a

In degree zero, the contraction of the singular cochains of a point evaluates a cochain on the unique singular vertex.

theorem TauCeti.isZero_singularCohomology_point {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [Unique ↑X] {n : ℕ} (hn : n ≠ 0) : CategoryTheory.Limits.IsZero (TopCat.singularCohomology R k M X n)

The positive-degree singular cohomology of a point vanishes, for arbitrary coefficients.

noncomputable def TauCeti.singularCohomologyPointZeroIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [Unique ↑X] : TopCat.singularCohomology R k M X 0 ≅ ↧(R ⟶ M)

The degree-zero singular cohomology of a point is the module Hom(R, M). The class of a cocycle is sent to its value on the unique singular vertex (TauCeti.singularCohomologyPointZeroIso_hom_homologyπ_apply).

theorem TauCeti.homologyπ_singularCohomologyPointZeroIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [Unique ↑X] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (TopCat.singularCochainComplex R k M X) 0) (singularCohomologyPointZeroIso R k M X).hom = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (TopCat.singularCochainComplex R k M X) 0) (CategoryTheory.CategoryStruct.comp ((pointSingularCochainHomotopyEquiv R k M X).hom.f 0) (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 ↧(R ⟶ M)).hom)

The comparison of the degree-zero singular cohomology of a point with Hom(R, M) is induced by the contraction of the singular cochains.

theorem TauCeti.homologyπ_singularCohomologyPointZeroIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [Unique ↑X] {Z : ModuleCat k} (h : ↧(R ⟶ M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (TopCat.singularCochainComplex R k M X) 0) (CategoryTheory.CategoryStruct.comp (singularCohomologyPointZeroIso R k M X).hom h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (TopCat.singularCochainComplex R k M X) 0) (CategoryTheory.CategoryStruct.comp ((pointSingularCochainHomotopyEquiv R k M X).hom.f 0) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 ↧(R ⟶ M)).hom h))

The comparison of the degree-zero singular cohomology of a point with Hom(R, M) is induced by the contraction of the singular cochains.

theorem TauCeti.singularCohomologyPointZeroIso_hom_homologyπ_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [Unique ↑X] (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := 0 })) (a : ↑(HomologicalComplex.cycles (TopCat.singularCochainComplex R k M X) 0)) : (CategoryTheory.ConcreteCategory.hom (singularCohomologyPointZeroIso R k M X).hom) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopCat.singularCochainComplex R k M X) 0)) a) = CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (TopCat.singularCochainComplex R k M X) 0)) a)

The comparison of the degree-zero singular cohomology of a point with Hom(R, M) sends the class of a zero-cocycle to its value on the unique singular vertex.

@[simp]

theorem TauCeti.singularCohomologyPointZeroIso_hom_constSingularCocycle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [Unique ↑X] (e : R ⟶ M) : (CategoryTheory.ConcreteCategory.hom (singularCohomologyPointZeroIso R k M X).hom) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopCat.singularCochainComplex R k M X) 0)) (X.constSingularCocycle k e)) = e

The class of the constant zero-cocycle with value e : R ⟶ M, for instance the unit of the cup product, corresponds to e in the degree-zero singular cohomology of a point.

@[simp]

theorem TauCeti.singularCohomologyPointZeroIso_inv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [Unique ↑X] (e : R ⟶ M) : (CategoryTheory.ConcreteCategory.hom (singularCohomologyPointZeroIso R k M X).inv) e = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopCat.singularCochainComplex R k M X) 0)) (X.constSingularCocycle k e)

The inverse comparison sends e : R ⟶ M to the class of the constant zero-cocycle with value e in the degree-zero singular cohomology of a point.

theorem TauCeti.singularCohomologyPointZeroIso_hom_naturality_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [Unique ↑X] {M' : C} (g : M ⟶ M') : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((TopCat.toSSet.obj X).chainComplex R) g) 0) (singularCohomologyPointZeroIso R k M' X).hom = CategoryTheory.CategoryStruct.comp (singularCohomologyPointZeroIso R k M X).hom (ModuleCat.ofHom (CategoryTheory.Linear.rightComp k R g))

The comparison of the degree-zero singular cohomology of a point with Hom(R, M) is natural in the target coefficients: postcomposing cochains with g : M ⟶ M' corresponds to postcomposition with g on Hom(R, M).

theorem TauCeti.singularCohomologyPointZeroIso_hom_naturality_right_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [Unique ↑X] {M' : C} (g : M ⟶ M') {Z : ModuleCat k} (h : ↧(R ⟶ M') ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k ((TopCat.toSSet.obj X).chainComplex R) g) 0) (CategoryTheory.CategoryStruct.comp (singularCohomologyPointZeroIso R k M' X).hom h) = CategoryTheory.CategoryStruct.comp (singularCohomologyPointZeroIso R k M X).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (CategoryTheory.Linear.rightComp k R g)) h)

The comparison of the degree-zero singular cohomology of a point with Hom(R, M) is natural in the target coefficients: postcomposing cochains with g : M ⟶ M' corresponds to postcomposition with g on Hom(R, M).

theorem TauCeti.singularCohomologyPointZeroIso_hom_naturality_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [Unique ↑X] {R' : C} (f : R' ⟶ R) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((ChainComplex.linearYonedaFunctor k M).map (((SSet.chainComplexFunctor C).map f).app (TopCat.toSSet.obj X)).op) 0) (singularCohomologyPointZeroIso R' k M X).hom = CategoryTheory.CategoryStruct.comp (singularCohomologyPointZeroIso R k M X).hom (ModuleCat.ofHom (CategoryTheory.Linear.leftComp k M f))

The comparison of the degree-zero singular cohomology of a point with Hom(R, M) is natural in the source coefficients: precomposing cochains with the chain map induced by f : R' ⟶ R corresponds to precomposition with f on Hom(R, M).

theorem TauCeti.singularCohomologyPointZeroIso_hom_naturality_left_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [Unique ↑X] {R' : C} (f : R' ⟶ R) {Z : ModuleCat k} (h : ↧(R' ⟶ M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((ChainComplex.linearYonedaFunctor k M).map (((SSet.chainComplexFunctor C).map f).app (TopCat.toSSet.obj X)).op) 0) (singularCohomologyPointZeroIso R' k M X).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (singularCohomologyPointZeroIso R k M X).hom (ModuleCat.ofHom (CategoryTheory.Linear.leftComp k M f))) h

The comparison of the degree-zero singular cohomology of a point with Hom(R, M) is natural in the source coefficients: precomposing cochains with the chain map induced by f : R' ⟶ R corresponds to precomposition with f on Hom(R, M).

theorem TopCat.singularCohomologyMap_eq_zero_of_nullhomotopic {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {X Y : TopCat} {f : X ⟶ Y} (hf : (Hom.hom f).Nullhomotopic) {n : ℕ} (hn : n ≠ 0) : TopCat.singularCohomologyMap f n = 0

A nullhomotopic map induces zero on positive-degree singular cohomology: up to homotopy it factors through a point, whose positive-degree cohomology vanishes.

theorem TopPair.epi_singularCohomologyπ_of_nullhomotopic {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} (P : TopPair) (hP : (TopCat.Hom.hom map).Nullhomotopic) {n : ℕ} (hn : n ≠ 0) : CategoryTheory.Epi (P.singularCohomologyπ R k M n)

Positive-degree classes lift relative to a nullhomotopic subspace. If the inclusion A ⟶ X of a pair (X, A) is nullhomotopic, then in positive degrees the map Hⁿ(X, A) ⟶ Hⁿ(X) is an epimorphism: by exactness of the long exact sequence of the pair, since the restriction Hⁿ(X) ⟶ Hⁿ(A) vanishes.

theorem TauCeti.isZero_singularCohomology_of_contractibleSpace {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [ContractibleSpace ↑X] {n : ℕ} (hn : n ≠ 0) : CategoryTheory.Limits.IsZero (TopCat.singularCohomology R k M X n)

The positive-degree singular cohomology of a contractible space vanishes, for arbitrary coefficients.

theorem TauCeti.isZero_singularCohomology_of_isEmpty {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (X : TopCat) [IsEmpty ↑X] (n : ℕ) : CategoryTheory.Limits.IsZero (TopCat.singularCohomology R k M X n)

The singular cohomology of the empty space vanishes in every degree, for arbitrary coefficients: there are no singular simplices, so the singular cochain complex is zero.