Pullback on singular cohomology of the descended odd map

This file connects the library's two finished layers — the genuine singular cohomology functor of SingularCohomology.lean and the genuine odd-map descent / double-cover API of RealProjectiveSpace.lean — into honest, formalized statements about the pullback action of the descended odd map on the real mod-2 singular cohomology of real projective space.

Everything here is a real mathematical object:

• rpCohomology n k and sphereCohomology n k are the actual k-th singular cohomology ModuleCat (ZMod 2)-objects of RP n and S^n, obtained by applying the constructed functor singularCohomologyZMod2 k to the genuine TopCat objects TopCat.of (RP n) and TopCat.of (Sphere n);
• inducedOnRPPullback f hf k, projPullback n k, and spherePullback f k are the actual pullback ModuleCat (ZMod 2)-morphisms induced by the descended odd map inducedOnRP f hf, the double cover proj n, and an odd map f, respectively. They are the functor's action on the opposite of the corresponding TopCat morphisms; their naturality is structural.

The degree-1 generator α ∈ H¹(RPⁿ; F₂), its powers αⁿ, the cup product, and the top-class / degree comparison remain genuinely absent (they need the universal coefficient theorem, the Alexander–Whitney cup product, and the transfer/Gysin comparison — implemented by the project modules listed below).

What is proved here

• inducedOnRPPullback_id — the pullback of the descended identity is the identity on H^k(RP n; F₂) (functoriality at the identity).
• inducedOnRPPullback_comp — contravariant functoriality of the descended pullback: (g ∘ f)bar^* = gbar^* ≫ fbar^* (note the reversal).
• inducedOnRP_pullback_naturality — the naturality square of the double cover:

fbar^* ≫ proj^* = proj^* ≫ f^* on H^k(RP n; F₂) ⟶ H^k(S^n; F₂)

This is the cohomological form of the commuting square inducedOnRP_comp_proj (fbar ∘ proj = proj ∘ f); it is exactly the square used by the top-class / degree comparison (C3b).

• proj_pullback_antipodal — the nontrivial deck transformation (the antipodal map) acts trivially on the image of proj^*: proj^* ≫ antipodal^* = proj^*.
• inducedOnRPPullback_antipodal — the descended antipodal pullback is the identity (a corollary of inducedOnRP_antipodal and inducedOnRPPullback_id).

These are the functorial pullback / double-cover-compatibility / descended-map naturality facts independent of the cup-product ring computation.

noncomputable def SphereOddDegree.rpCohomology (n k : ℕ) : ModuleCat (ZMod 2)

The k-th singular cohomology of RP n with ZMod 2 coefficients, as an object of ModuleCat (ZMod 2). This is a genuine object: the constructed functor singularCohomologyZMod2 k applied to the genuine space TopCat.of (RP n).

Equations

• SphereOddDegree.rpCohomology n k = (SphereOddDegree.singularCohomologyZMod2 k).obj (Opposite.op ↧(SphereOddDegree.RP n))

noncomputable def SphereOddDegree.sphereCohomology (n k : ℕ) : ModuleCat (ZMod 2)

The k-th singular cohomology of S^n with ZMod 2 coefficients, as an object of ModuleCat (ZMod 2).

Equations

• SphereOddDegree.sphereCohomology n k = (SphereOddDegree.singularCohomologyZMod2 k).obj (Opposite.op ↧(SphereOddDegree.Sphere n))

noncomputable def SphereOddDegree.inducedOnRPPullback {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (k : ℕ) : rpCohomology n k ⟶ rpCohomology n k

The pullback fbar^* : H^k(RP n; F₂) → H^k(RP n; F₂) of the descended odd map fbar = inducedOnRP f hf. This is the functor's action on the opposite of the TopCat morphism TopCat.ofHom (inducedOnRP f hf); naturality is structural.

Equations

• SphereOddDegree.inducedOnRPPullback f hf k = (SphereOddDegree.singularCohomologyZMod2 k).map (TopCat.ofHom (SphereOddDegree.inducedOnRP f hf)).op

noncomputable def SphereOddDegree.projPullback (n k : ℕ) : rpCohomology n k ⟶ sphereCohomology n k

The pullback proj^* : H^k(RP n; F₂) → H^k(S^n; F₂) of the double cover proj n : S^n → RP n.

Equations

• SphereOddDegree.projPullback n k = (SphereOddDegree.singularCohomologyZMod2 k).map (TopCat.ofHom (SphereOddDegree.proj n)).op

noncomputable def SphereOddDegree.spherePullback {n : ℕ} (f : C(Sphere n, Sphere n)) (k : ℕ) : sphereCohomology n k ⟶ sphereCohomology n k

The pullback f^* : H^k(S^n; F₂) → H^k(S^n; F₂) of a self-map f of the sphere.

Equations

• SphereOddDegree.spherePullback f k = (SphereOddDegree.singularCohomologyZMod2 k).map (TopCat.ofHom f).op

theorem SphereOddDegree.inducedOnRPPullback_id (n k : ℕ) : inducedOnRPPullback (ContinuousMap.id (Sphere n)) ⋯ k = CategoryTheory.CategoryStruct.id (rpCohomology n k)

Functoriality at the identity: the pullback of the descended identity map is the identity on H^k(RP n; F₂).

theorem SphereOddDegree.inducedOnRPPullback_comp {n : ℕ} (f g : C(Sphere n, Sphere n)) (hf : IsOddMap f) (hg : IsOddMap g) (k : ℕ) : inducedOnRPPullback (g.comp f) ⋯ k = CategoryTheory.CategoryStruct.comp (inducedOnRPPullback g hg k) (inducedOnRPPullback f hf k)

Contravariant functoriality of the descended pullback: the pullback of the descent of g ∘ f is gbar^* followed by fbar^* (the order is reversed, since cohomology is contravariant).

theorem SphereOddDegree.inducedOnRP_pullback_naturality {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (k : ℕ) : CategoryTheory.CategoryStruct.comp (inducedOnRPPullback f hf k) (projPullback n k) = CategoryTheory.CategoryStruct.comp (projPullback n k) (spherePullback f k)

Naturality square of the double cover. For an odd map f with descent fbar = inducedOnRP f hf, the cohomology pullbacks fit into the commuting square

fbar^* ≫ proj^* = proj^* ≫ f^* : H^k(RP n; F₂) ⟶ H^k(S^n; F₂).

This is the cohomological image of the point-set commuting square inducedOnRP_comp_proj (fbar ∘ proj = proj ∘ f). It is exactly the square the top-class / degree comparison evaluates on the top class.

theorem SphereOddDegree.proj_pullback_antipodal {n : ℕ} (k : ℕ) : CategoryTheory.CategoryStruct.comp (projPullback n k) (spherePullback (antipodal n) k) = projPullback n k

The nontrivial deck transformation (the antipodal map) acts trivially on the image of proj^*: proj^* ≫ antipodal^* = proj^*. This is the cohomological form of proj_comp_antipodal (proj n ∘ antipodal n = proj n).

theorem SphereOddDegree.inducedOnRPPullback_antipodal (n k : ℕ) : inducedOnRPPullback (antipodal n) ⋯ k = CategoryTheory.CategoryStruct.id (rpCohomology n k)

The pullback of the descended antipodal map is the identity on H^k(RP n; F₂), since the antipodal map descends to the identity on RP n (inducedOnRP_antipodal).

theorem SphereOddDegree.spherePullback_eq_of_homotopic {n : ℕ} {f g : C(Sphere n, Sphere n)} (h : f.Homotopic g) (k : ℕ) : spherePullback f k = spherePullback g k

Homotopy invariance on the sphere (unconditional). Homotopic self-maps f, g of S^n induce equal pullbacks f^* = g^* on the mod-2 cohomology H^k(S^n; F₂).

This specializes singularCohomologyMap_eq_of_homotopic_continuousMap to the sphere pullback spherePullback; it is the cohomological input the top-class / degree comparison will use to replace a sphere self-map by any homotopic representative.

theorem SphereOddDegree.inducedOnRPPullback_eq_of_homotopic {n : ℕ} {f g : C(Sphere n, Sphere n)} (hf : IsOddMap f) (hg : IsOddMap g) (h : (inducedOnRP f hf).Homotopic (inducedOnRP g hg)) (k : ℕ) : inducedOnRPPullback f hf k = inducedOnRPPullback g hg k

Homotopy invariance for descended maps on RP n (unconditional). If two odd self-maps f, g of S^n descend to homotopic self-maps of RP n, their pullbacks on H^k(RP n; F₂) agree.

The hypothesis is phrased on the descended maps inducedOnRP f hf and inducedOnRP g hg (their Homotopicness on RP n), since a homotopy on the sphere need not be odd and hence need not descend on its own.

theorem SphereOddDegree.inducedOnRP_cochainPow_fixed {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (φ : singularCochainGroup (ZMod 2) (↧(RP n)) 1) (hφ : cochainPullback (TopCat.ofHom (inducedOnRP f hf)) 1 φ = φ) (k : ℕ) : cochainPullback (TopCat.ofHom (inducedOnRP f hf)) k (cochainPow φ k) = cochainPow φ k

Cochain-level fixed-point powers for the descended odd map on RP n. If a degree-one mod-2 cochain φ on RP n is fixed by the cochain pullback of the descended odd map fbar = inducedOnRP f hf (i.e. fbar^* φ = φ), then so are all its cup powers: fbar^*(φⁿ) = φⁿ.

This is the cochain-level form of the final-theorem target fbar^*(α)=α ⟹ fbar^*(αⁿ)=αⁿ for the descended odd map, specialized to the ZMod 2 coefficients of the RP n computation. The cohomology-level version is inducedOnRP_cohPullback_cupPow_fixed below (the cup product now descends to cohomology, see CohomologyCupProduct.lean); the degree-1 class α ∈ H¹(RPⁿ; F₂) itself remains gated on the universal coefficient theorem, so no unsupported α is introduced.

theorem SphereOddDegree.inducedOnRPPullback_eq_cohPullback {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (k : ℕ) : inducedOnRPPullback f hf k = cohPullback (TopCat.ofHom (inducedOnRP f hf)) k

The descended-odd-map pullback on H^k(RP n; F₂) is the cohomology pullback of the descended map fbar = inducedOnRP f hf.

theorem SphereOddDegree.inducedOnRP_cohPullback_cupPow_fixed {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (a : ↑(cohomologyZMod2 (↧(RP n)) 1)) (ha : (ModuleCat.Hom.hom (cohPullback (TopCat.ofHom (inducedOnRP f hf)) 1)) a = a) (k : ℕ) : (ModuleCat.Hom.hom (cohPullback (TopCat.ofHom (inducedOnRP f hf)) k)) (cupPowZMod2 a k) = cupPowZMod2 a k

Cohomology-level fixed-point powers for the descended odd map on RP n. If a degree-one mod-2 cohomology class a ∈ H¹(RP n; F₂) is fixed by the pullback of the descended odd map fbar = inducedOnRP f hf (i.e. fbar^* a = a), then so are all its cup powers: fbar^*(aⁿ) = aⁿ.

This is the cohomology-level implication fbar^*(α)=α ⟹ fbar^*(αⁿ)=αⁿ, using the ZMod 2 cup product cupZMod2 and its powers cupPowZMod2 from CohomologyCupProduct.lean.

theorem SphereOddDegree.inducedOnRPPullback_cup {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (p q : ℕ) (a : ↑(rpCohomology n p)) (b : ↑(rpCohomology n q)) : (ModuleCat.Hom.hom (inducedOnRPPullback f hf (p + q))) (cupZMod2 a b) = cupZMod2 ((ModuleCat.Hom.hom (inducedOnRPPullback f hf p)) a) ((ModuleCat.Hom.hom (inducedOnRPPullback f hf q)) b)

Cohomology-level cup naturality for the descended odd map on RP n. The descended-odd-map pullback is multiplicative for the ZMod 2 cohomology cup product: fbar^*(a ⌣ b) = fbar^* a ⌣ fbar^* b for fbar = inducedOnRP f hf.

This is the RP n-specialized form of cohPullback_cupZMod2, stated directly in terms of inducedOnRPPullback (which is cohPullback (TopCat.ofHom (inducedOnRP f hf)) by inducedOnRPPullback_eq_cohPullback).

theorem SphereOddDegree.inducedOnRPPullback_pow {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (a : ↑(rpCohomology n 1)) (k : ℕ) : (ModuleCat.Hom.hom (inducedOnRPPullback f hf k)) (cupPowZMod2 a k) = cupPowZMod2 ((ModuleCat.Hom.hom (inducedOnRPPullback f hf 1)) a) k

Cohomology-level cup-power naturality for the descended odd map on RP n. fbar^*(aⁿ) = (fbar^* a)ⁿ for a degree-one class a ∈ H¹(RP n; F₂) and the descended odd map fbar = inducedOnRP f hf.

This is the RP n-specialized form of cohPullback_cupPowZMod2, stated directly in terms of inducedOnRPPullback. Together with a fixed-point hypothesis fbar^* a = a it yields inducedOnRP_cohPullback_cupPow_fixed.