Constructing the degree-one projective cohomology class

Uses the mod-two Kronecker equivalence to turn a linear functional on H₁(RPⁿ; F₂) into a class of H¹(RPⁿ; F₂) and proves naturality under descended odd sphere maps. The structure MonodromyFunctional n isolates the homology functional and its invariance property. The canonical instance used by the final proof is constructed later in RPnMonodromyFunctional.

noncomputable def SphereOddDegree.rpAlphaOfFunctional (n : ℕ) (g : ↑(homologyZMod2 (↧(RP n)) 1) →ₗ[ZMod 2] ZMod 2) : ↑(rpCohomology n 1)

The cohomology class α ∈ H¹(RPⁿ; F₂) produced from a ZMod 2-valued functional g on H₁(RPⁿ; F₂) via the surjectivity of the Kronecker classifier (kroneckerMap_surjective). It is a genuine element of rpCohomology n 1.

Equations

• SphereOddDegree.rpAlphaOfFunctional n g = Classical.choose ⋯

theorem SphereOddDegree.rpAlphaOfFunctional_spec (n : ℕ) (g : ↑(homologyZMod2 (↧(RP n)) 1) →ₗ[ZMod 2] ZMod 2) : (ModuleCat.Hom.hom (kroneckerMap (↧(RP n)) 1)) (rpAlphaOfFunctional n g) = g

Defining property: the Kronecker functional of rpAlphaOfFunctional n g is exactly g.

theorem SphereOddDegree.inducedOnRPPullback_rpAlphaOfFunctional (n : ℕ) (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (g : ↑(homologyZMod2 (↧(RP n)) 1) →ₗ[ZMod 2] ZMod 2) (hg : g ∘ₗ ModuleCat.Hom.hom (homologyPushZMod2 (TopCat.ofHom (inducedOnRP f hf)) 1) = g) : (ModuleCat.Hom.hom (inducedOnRPPullback f hf 1)) (rpAlphaOfFunctional n g) = rpAlphaOfFunctional n g

Conditional naturality. If a functional g : H₁(RPⁿ; F₂) → F₂ is invariant under the homology pushforward of a descended odd map fbar = inducedOnRP f hf (i.e. g ∘ fbar_* = g), then the pullback of the descended odd map fixes the corresponding cohomology class: fbar^*(rpAlphaOfFunctional n g) = rpAlphaOfFunctional n g.

The proof uses the universal coefficient theorem over F₂ in full: naturality (kroneckerMap_naturality_apply) transports the invariance of g to an equality of Kronecker functionals, and injectivity (kroneckerMap_injective) lifts it back to an equality of cohomology classes.

structure SphereOddDegree.MonodromyFunctional (n : ℕ) : Type

A mod-two functional on H₁(RPⁿ; F₂) together with invariance under the homology pushforward of every descended odd map. This is the interface used to construct the degree-one class; RPnMonodromyFunctional supplies the canonical instance.

• g : ↑(homologyZMod2 (↧(RP n)) 1) →ₗ[ZMod 2] ZMod 2

  The ZMod 2-valued functional on H₁(RPⁿ; F₂).

• invariant (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) : self.g ∘ₗ ModuleCat.Hom.hom (homologyPushZMod2 (TopCat.ofHom (inducedOnRP f hf)) 1) = self.g

  Invariance under the homology pushforward of every descended odd map.

noncomputable def SphereOddDegree.rpAlpha (n : ℕ) (m : MonodromyFunctional n) : ↑(rpCohomology n 1)

The canonical degree-one class α ∈ H¹(RPⁿ; F₂) associated to the canonical double cover, built from the monodromy functional m. It is a genuine element of rpCohomology n 1.

Equations

• SphereOddDegree.rpAlpha n m = SphereOddDegree.rpAlphaOfFunctional n m.g

theorem SphereOddDegree.rpAlpha_def (n : ℕ) (m : MonodromyFunctional n) : rpAlpha n m = rpAlphaOfFunctional n m.g

rpAlpha n m is the class produced by the universal coefficient surjection from the monodromy functional m.g.

theorem SphereOddDegree.rpAlpha_kroneckerMap (n : ℕ) (m : MonodromyFunctional n) : (ModuleCat.Hom.hom (kroneckerMap (↧(RP n)) 1)) (rpAlpha n m) = m.g

The defining property of rpAlpha: its Kronecker functional is the monodromy functional m.g.

theorem SphereOddDegree.inducedOnRPPullback_rpAlpha (n : ℕ) (m : MonodromyFunctional n) (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) : (ModuleCat.Hom.hom (inducedOnRPPullback f hf 1)) (rpAlpha n m) = rpAlpha n m

Descended odd maps preserve rpAlpha — unconditionally (given the monodromy functional m). For every odd self-map f of Sⁿ with descent fbar = inducedOnRP f hf,

(inducedOnRPPullback f hf 1) (rpAlpha n m) = rpAlpha n m,

i.e. fbar^*(α) = α. This is exactly the action hypothesis the final-assembly theorems take as input; here it is proved.