Singular cohomology functor (dualization of the singular chain complex)

This file builds a functorial singular cohomology theory by dualizing Mathlib's singular chain complex functor.

Pinned Mathlib (v4.28.0, commit 8f9d9cff6bd728b17a24e163c9402775d9e6a365) has no packaged singular cohomology theory (no singularCohomologyFunctor, no named Hⁿ(X; M), no cup product, no universal coefficient theorem). It does, however, provide every building block needed to construct singular cohomology with coefficients in a module by dualizing the existing singular chain complex:

• AlgebraicTopology.singularChainComplexFunctor — the singular chains C_•(X), covariantly functorial in X;
• HomologicalComplex.opFunctor / Functor.op — make the construction contravariant in X (so the pullback f^* comes for free, structurally);
• CategoryTheory.linearYoneda — the dualizing Hom(-, M) into R-modules;
• Functor.mapHomologicalComplex — apply the dualizer objectwise;
• HomologicalComplex.homologyFunctor — take n-th (co)homology.

Construction

For a commutative ring R and a coefficient module M : ModuleCat R, the singular cochain complex functor is the composite

singularCochainComplexFunctor R M
 : TopCatᵒᵖ ⥤ CochainComplex (ModuleCat R) ℕ
 := ((singularChainComplexFunctor (ModuleCat R)).obj M).op
 ⋙ HomologicalComplex.opFunctor _ _
 ⋙ ((linearYoneda R (ModuleCat R)).obj M).mapHomologicalComplex _

and the singular cohomology functor in degree n is

singularCohomologyFunctor R M n
 : TopCatᵒᵖ ⥤ ModuleCat R
 := singularCochainComplexFunctor R M ⋙ HomologicalComplex.homologyFunctor _ _ n.

The codomain is recorded as CochainComplex (ModuleCat R) ℕ rather than HomologicalComplex (ModuleCat R) (ComplexShape.down ℕ).symm; these are definitionally equal since (ComplexShape.down ℕ).symm = ComplexShape.up ℕ by rfl, so no shape-isomorphism lemma is needed.

Conventions

• Coefficients. M : ModuleCat R is the coefficient module; the coefficient ring is R. The relevant downstream case is R = ZMod 2, for which the abbreviation singularCohomologyZMod2 fixes M = ModuleCat.of (ZMod 2) (ZMod 2).
• Contravariance. The functor is contravariant in the space: a continuous map f : X → Y becomes a TopCat morphism TopCat.ofHom f : X ⟶ Y, whose opposite (TopCat.ofHom f).op : Opposite.op Y ⟶ Opposite.op X is sent by the functor to the pullback f^* : Hⁿ(Y; M) → Hⁿ(X; M).
• Functoriality. Identities and composites are preserved (singularCohomologyFunctor_map_id, singularCohomologyFunctor_map_comp), and equal morphisms induce equal pullbacks (singularCohomologyFunctor_map_congr). These are the generic CategoryTheory.Functor laws on the composite.

Scope

This is the construction layer only (the analogue of PR-coh1a in the design inventories). It does not include homotopy invariance, the universal coefficient theorem, any cohomology computation, or the cup product; those remain downstream work.

noncomputable def SphereOddDegree.singularCochainComplexFunctor (R : Type) [CommRing R] (M : ModuleCat R) : CategoryTheory.Functor TopCatᵒᵖ (CochainComplex (ModuleCat R) ℕ)

The singular cochain complex functor with coefficients in a module M : ModuleCat R, obtained by dualizing the singular chain complex functor.

It sends a space X (as an object of TopCatᵒᵖ) to the cochain complex Hom(C_•(X), M) and is contravariant in X: a continuous map induces a cochain map in the opposite direction. The codomain CochainComplex (ModuleCat R) ℕ is definitionally HomologicalComplex (ModuleCat R) (ComplexShape.down ℕ).symm, since (ComplexShape.down ℕ).symm = ComplexShape.up ℕ.

Equations

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

noncomputable def SphereOddDegree.singularCohomologyFunctor (R : Type) [CommRing R] (M : ModuleCat R) (n : ℕ) : CategoryTheory.Functor TopCatᵒᵖ (ModuleCat R)

The n-th singular cohomology functor Hⁿ(-; M) : TopCatᵒᵖ ⥤ ModuleCat R with coefficients in a module M : ModuleCat R, obtained by taking n-th homology of the singular cochain complex Hom(C_•(X), M).

Contravariance in the space is structural: a continuous map f induces the pullback f^* : Hⁿ(Y; M) → Hⁿ(X; M) via the functor's action on (TopCat.ofHom f).op.

Equations

• SphereOddDegree.singularCohomologyFunctor R M n = (SphereOddDegree.singularCochainComplexFunctor R M).comp (HomologicalComplex.homologyFunctor (ModuleCat R) (ComplexShape.up ℕ) n)

theorem SphereOddDegree.singularCohomologyFunctor_map_id (R : Type) [CommRing R] (M : ModuleCat R) (n : ℕ) (X : TopCatᵒᵖ) : (singularCohomologyFunctor R M n).map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id ((singularCohomologyFunctor R M n).obj X)

Functoriality: the singular cohomology functor preserves identities.

theorem SphereOddDegree.singularCohomologyFunctor_map_comp (R : Type) [CommRing R] (M : ModuleCat R) (n : ℕ) {X Y Z : TopCatᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) : (singularCohomologyFunctor R M n).map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((singularCohomologyFunctor R M n).map f) ((singularCohomologyFunctor R M n).map g)

Functoriality: the singular cohomology functor preserves composition. Note that, being contravariant in the space, this reverses the order of the induced pullbacks at the level of TopCat.

theorem SphereOddDegree.singularCohomologyFunctor_map_congr (R : Type) [CommRing R] (M : ModuleCat R) (n : ℕ) {X Y : TopCatᵒᵖ} {f g : X ⟶ Y} (h : f = g) : (singularCohomologyFunctor R M n).map f = (singularCohomologyFunctor R M n).map g

Congruence: equal morphisms induce equal maps on singular cohomology.

theorem SphereOddDegree.singularCochainComplexFunctor_map_id (R : Type) [CommRing R] (M : ModuleCat R) (X : TopCatᵒᵖ) : (singularCochainComplexFunctor R M).map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id ((singularCochainComplexFunctor R M).obj X)

Functoriality: the singular cochain complex functor preserves identities.

theorem SphereOddDegree.singularCochainComplexFunctor_map_comp (R : Type) [CommRing R] (M : ModuleCat R) {X Y Z : TopCatᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) : (singularCochainComplexFunctor R M).map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((singularCochainComplexFunctor R M).map f) ((singularCochainComplexFunctor R M).map g)

Functoriality: the singular cochain complex functor preserves composition.

@[reducible, inline]

noncomputable abbrev SphereOddDegree.singularCohomologyZMod2 (n : ℕ) : CategoryTheory.Functor TopCatᵒᵖ (ModuleCat (ZMod 2))

The n-th singular cohomology functor with ZMod 2 coefficients, Hⁿ(-; ZMod 2) : TopCatᵒᵖ ⥤ ModuleCat (ZMod 2). This is the coefficient target needed for the downstream odd-degree / real projective space work.

Equations

• SphereOddDegree.singularCohomologyZMod2 n = SphereOddDegree.singularCohomologyFunctor (ZMod 2) (↧(ZMod 2)) n

@[reducible, inline]

noncomputable abbrev SphereOddDegree.singularCochainComplexZMod2 : CategoryTheory.Functor TopCatᵒᵖ (CochainComplex (ModuleCat (ZMod 2)) ℕ)

The singular cochain complex functor with ZMod 2 coefficients.

Equations

• SphereOddDegree.singularCochainComplexZMod2 = SphereOddDegree.singularCochainComplexFunctor (ZMod 2) ↧(ZMod 2)