Homotopy invariance of singular cohomology — UNCONDITIONAL

This file proves homotopy invariance for the library's singular cohomology functor singularCohomologyFunctor, unconditionally, for an arbitrary coefficient module M : ModuleCat R (and in particular for ZMod 2).

The argument has two parts.

• Dualization (algebraic). A chain homotopy between the singular chain maps of two continuous maps (at any coefficient module M : ModuleCat R) dualizes to equal pullbacks on singular cohomology Hⁿ(-; M). This is the cohomology analogue of the homology consumer singularHomologyMap_eq_of_singularChainHomotopy (HomotopyToChainHomotopy.lean) and needs no prism operator. It is singularCohomologyMap_eq_of_chainHomotopy.

• Prism (topological → chain homotopy). Turning a topological homotopy into that chain homotopy is exactly the prism operator. Pinned Mathlib has no such operator, but the library's backported algebraic prism together with its singular cylinder constructs it, at integer coefficients (singularChainHomotopyOfHomotopy) and — what we use here — at an arbitrary coefficient module (singularChainHomotopyOfHomotopyModule, Backports/PrismSimplicialHomotopy.lean). Hence the prism hypothesis SingularCohomologyPrism R M isolated below is a theorem (singularCohomologyPrism), and full homotopy invariance of cohomology is unconditional in every form downstream code needs (TopCat maps, the Homotopic relation, the C(X, Y) interface), with ZMod 2 specializations.

Logical shape

topological homotopy ──singularChainHomotopyOfHomotopyModule──▶ chain homotopy (coeff M)
 │
 homotopyOpFunctorMap │
 + Functor.mapHomotopy │
 + Homotopy.homologyMap_eq │
 ▼
 equal pullbacks on Hⁿ(-; M)

theorem SphereOddDegree.singularCohomologyMap_eq_of_chainHomotopy (R : Type) [CommRing R] (M : ModuleCat R) (n : ℕ) {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj M).map f) (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj M).map g)) : (singularCohomologyFunctor R M n).map f.op = (singularCohomologyFunctor R M n).map g.op

Unconditional dualization step. If the singular chain maps (with coefficients in M : ModuleCat R) induced by two continuous maps f, g : X ⟶ Y are chain-homotopic, then the induced pullbacks on the n-th singular cohomology Hⁿ(-; M) are equal.

This is the genuine cohomology consumer of a chain homotopy: it requires no prism operator.

def SphereOddDegree.SingularCohomologyPrism (R : Type) [CommRing R] (M : ModuleCat R) : Prop

The cohomology prism-operator hypothesis (coefficient-M form).

A SingularCohomologyPrism R M asserts that every topological homotopy between two TopCat maps gives rise to a chain homotopy of the induced singular chain maps with coefficients in M. This is exactly the classical prism operator at coefficient module M. It is no longer a hypothesis: it is discharged by singularCohomologyPrism below using the library's backported algebraic prism. The definition is kept for documentation and as a reusable interface.

Equations

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

theorem SphereOddDegree.singularCohomologyPrism (R : Type) [CommRing R] (M : ModuleCat R) : SingularCohomologyPrism R M

The cohomology prism operator, discharged (unconditional). For any coefficient module M : ModuleCat R, the prism hypothesis holds: a topological homotopy gives a chain homotopy of the singular chain maps with coefficients in M. Witnessed by singularChainHomotopyOfHomotopyModule.

theorem SphereOddDegree.singularCohomologyMap_eq_of_homotopy (R : Type) [CommRing R] (M : ModuleCat R) (n : ℕ) {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) : (singularCohomologyFunctor R M n).map f.op = (singularCohomologyFunctor R M n).map g.op

Homotopy invariance of cohomology (topological homotopy form), unconditional.

A topological homotopy between two TopCat maps f, g : X ⟶ Y induces equal pullbacks on the n-th singular cohomology Hⁿ(-; M).

theorem SphereOddDegree.singularCohomologyMap_eq_of_homotopic (R : Type) [CommRing R] (M : ModuleCat R) (n : ℕ) {X Y : TopCat} {f g : X ⟶ Y} (h : (TopCat.Hom.hom f).Homotopic (TopCat.Hom.hom g)) : (singularCohomologyFunctor R M n).map f.op = (singularCohomologyFunctor R M n).map g.op

Homotopy invariance of cohomology (Homotopic form), unconditional.

theorem SphereOddDegree.singularCohomologyMap_eq_of_homotopic_continuousMap (R : Type) [CommRing R] (M : ModuleCat R) (n : ℕ) {X Y : TopCat} {f g : C(↑X, ↑Y)} (h : f.Homotopic g) : (singularCohomologyFunctor R M n).map (TopCat.ofHom f).op = (singularCohomologyFunctor R M n).map (TopCat.ofHom g).op

Homotopy invariance of cohomology (C(X, Y) interface), unconditional.

ZMod 2 specializations

theorem SphereOddDegree.singularCohomologyZMod2_map_eq_of_chainHomotopy (n : ℕ) {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat (ZMod 2))).obj ↧(ZMod 2)).map f) (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat (ZMod 2))).obj ↧(ZMod 2)).map g)) : (singularCohomologyZMod2 n).map f.op = (singularCohomologyZMod2 n).map g.op

ZMod 2 cohomology consumer of a chain homotopy. If the ZMod 2-singular chain maps of f, g are chain-homotopic, the ZMod 2-cohomology pullbacks agree.

theorem SphereOddDegree.singularCohomologyZMod2_map_eq_of_homotopic (n : ℕ) {X Y : TopCat} {f g : X ⟶ Y} (h : (TopCat.Hom.hom f).Homotopic (TopCat.Hom.hom g)) : (singularCohomologyZMod2 n).map f.op = (singularCohomologyZMod2 n).map g.op

ZMod 2 homotopy invariance (Homotopic form), unconditional.

theorem SphereOddDegree.singularCohomologyZMod2_map_eq_of_homotopic_continuousMap (n : ℕ) {X Y : TopCat} {f g : C(↑X, ↑Y)} (h : f.Homotopic g) : (singularCohomologyZMod2 n).map (TopCat.ofHom f).op = (singularCohomologyZMod2 n).map (TopCat.ofHom g).op

ZMod 2 homotopy invariance (C(X, Y) interface), unconditional. Two homotopic continuous maps f, g : C(X, Y) induce equal pullbacks on the ZMod 2 singular cohomology.