Projective top-class and model power API

Defines the top cohomology abbreviations and the truncated-polynomial model top class modelAlpha n ^ n. It proves the model-side nonvanishing and nilpotence lemmas used by the comparison layer and records the pullback induced by a descended odd sphere map. Later modules identify the actual projective cohomology generator and its powers with this model.

1. Top-degree target abbreviations

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

The top mod-two cohomology Hⁿ(RPⁿ; F₂) of real projective n-space, the target group of the top class αⁿ. A genuine object: rpCohomology n n.

Equations

• SphereOddDegree.rpTopCohomology n = SphereOddDegree.rpCohomology n n

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

The top mod-two cohomology Hⁿ(Sⁿ; F₂) of the n-sphere.

Equations

• SphereOddDegree.sphereTopCohomology n = SphereOddDegree.sphereCohomology n n

theorem SphereOddDegree.rpTopCohomology_eq (n : ℕ) : rpTopCohomology n = rpCohomology n n

theorem SphereOddDegree.sphereTopCohomology_eq (n : ℕ) : sphereTopCohomology n = sphereCohomology n n

noncomputable def SphereOddDegree.rpTopPullback {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) : rpTopCohomology n ⟶ rpTopCohomology n

The top-degree pullback fbar^* : Hⁿ(RPⁿ; F₂) → Hⁿ(RPⁿ; F₂) of the descended odd map fbar = inducedOnRP f hf. This is the endomorphism whose triviality (= id) on the nonzero top class αⁿ would yield degree f ≡ 1 mod 2 in the final theorem.

Equations

• SphereOddDegree.rpTopPullback f hf = SphereOddDegree.inducedOnRPPullback f hf n

@[simp]

theorem SphereOddDegree.rpTopPullback_id (n : ℕ) : rpTopPullback (ContinuousMap.id (Sphere n)) ⋯ = CategoryTheory.CategoryStruct.id (rpTopCohomology n)

@[simp]

theorem SphereOddDegree.rpTopPullback_antipodal (n : ℕ) : rpTopPullback (antipodal n) ⋯ = CategoryTheory.CategoryStruct.id (rpTopCohomology n)

The descended antipodal map acts as the identity on the top cohomology.

2. The model top class

instance SphereOddDegree.instNontrivialRPnCohomologyRingModel (n : ℕ) : Nontrivial (RPnCohomologyRingModel n)

The model ring F₂[α]/(αⁿ⁺¹) is nontrivial (it has the nonzero element αⁿ).

noncomputable def SphereOddDegree.modelTopClass (n : ℕ) : RPnCohomologyRingModel n

The model top class αⁿ ∈ F₂[α]/(αⁿ⁺¹) — the model-side avatar of the top class of Hⁿ(RPⁿ; F₂).

Equations

• SphereOddDegree.modelTopClass n = SphereOddDegree.modelAlpha n ^ n

theorem SphereOddDegree.modelTopClass_eq (n : ℕ) : modelTopClass n = modelAlpha n ^ n

theorem SphereOddDegree.modelTopClass_ne_zero (n : ℕ) : modelTopClass n ≠ 0

The model top class is nonzero — the model-side form of αⁿ ≠ 0.

theorem SphereOddDegree.modelAlpha_mul_modelTopClass (n : ℕ) : modelAlpha n * modelTopClass n = 0

The generator annihilates the top class: α · αⁿ = αⁿ⁺¹ = 0.

3. Cup-power notation

def SphereOddDegree.«term_^⌣_» : Lean.TrailingParserDescr

Notation φ ^⌣ n for the n-th cochain cup power cochainPow φ n of a degree-one cochain.

Equations

• SphereOddDegree.«term_^⌣_» = Lean.ParserDescr.trailingNode `SphereOddDegree.«term_^⌣_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^⌣ ") (Lean.ParserDescr.cat `term 76))

4. Conditional nonvanishing interfaces

These are the honest interfaces the full computation plugs into. None of them assert nonvanishing in Hⁿ(RPⁿ; F₂) unconditionally; each derives it from a hypothesised ring map or isomorphism matching the algebraic model. When an isomorphism H^*(RPⁿ; F₂) ≅ F₂[α]/(αⁿ⁺¹) is supplied, these yield αⁿ ≠ 0 and the truncation αᵏ = 0 ↔ n+1 ≤ k verbatim.

theorem SphereOddDegree.pow_ne_zero_of_ringHom_modelAlpha {R : Type u_1} [CommRing R] {n : ℕ} (Φ : R →+* RPnCohomologyRingModel n) {a : R} (ha : Φ a = modelAlpha n) {k : ℕ} (hk : k ≤ n) : a ^ k ≠ 0

Conditional sub-truncation nonvanishing. If a ring homomorphism Φ from a commutative ring R to the model F₂[α]/(αⁿ⁺¹) carries a : R to the model generator modelAlpha n, then aᵏ ≠ 0 for every k ≤ n. (No injectivity of Φ is needed: the image Φ(aᵏ) = αᵏ is already nonzero.)

theorem SphereOddDegree.pow_top_ne_zero_of_ringHom_modelAlpha {R : Type u_1} [CommRing R] {n : ℕ} (Φ : R →+* RPnCohomologyRingModel n) {a : R} (ha : Φ a = modelAlpha n) : a ^ n ≠ 0

Conditional top-power nonvanishing — the conditional αⁿ ≠ 0. If a ring homomorphism carries a to modelAlpha n, then aⁿ ≠ 0.

theorem SphereOddDegree.pow_eq_zero_iff_of_ringEquiv {R : Type u_1} [CommRing R] {n : ℕ} (e : R ≃+* RPnCohomologyRingModel n) {a : R} (ha : e a = modelAlpha n) (k : ℕ) : a ^ k = 0 ↔ n + 1 ≤ k

Conditional power-vanishing characterization. If a ring isomorphism carries a to modelAlpha n, then aᵏ = 0 ↔ n+1 ≤ k: exactly the powers below the truncation bound are nonzero.

theorem SphereOddDegree.pow_succ_eq_zero_of_ringEquiv {R : Type u_1} [CommRing R] {n : ℕ} (e : R ≃+* RPnCohomologyRingModel n) {a : R} (ha : e a = modelAlpha n) : a ^ (n + 1) = 0

Conditional truncation relation. If a ring isomorphism carries a to modelAlpha n, then aⁿ⁺¹ = 0.

theorem SphereOddDegree.pow_top_ne_zero_of_ringEquiv {R : Type u_1} [CommRing R] {n : ℕ} (e : R ≃+* RPnCohomologyRingModel n) {a : R} (ha : e a = modelAlpha n) : a ^ n ≠ 0

Conditional top-power nonvanishing, isomorphism form.

5. Low-dimensional cases (model side)

@[simp]

theorem SphereOddDegree.modelAlpha_zero_eq_zero : modelAlpha 0 = 0

For RP⁰ the generator itself is zero: modelAlpha 0 = 0 (the model ring is F₂[α]/(α) ≅ F₂).

@[simp]

theorem SphereOddDegree.modelTopClass_zero : modelTopClass 0 = 1

For RP⁰ the top class is the unit: α⁰ = 1, and it is nonzero — the genuine H⁰ top class on the model side.

theorem SphereOddDegree.modelTopClass_zero_ne_zero : modelTopClass 0 ≠ 0

theorem SphereOddDegree.modelAlpha_one_ne_zero : modelAlpha 1 ≠ 0

For RP¹ the generator is nonzero: α ≠ 0.

@[simp]

theorem SphereOddDegree.modelTopClass_one : modelTopClass 1 = modelAlpha 1

For RP¹ the top class is α itself.

theorem SphereOddDegree.modelAlpha_one_sq_eq_zero : modelAlpha 1 ^ 2 = 0

For RP¹ the square of the generator vanishes: α² = 0.