Documentation

LeanPool.NandakumarRamanaRao.NRR.OddSphereDegree.RPnCohomologyRingModel

The algebraic target ring F₂[α] / (αⁿ⁺¹) of the RPⁿ mod-two cohomology computation #

The classical computation of the mod-two cohomology ring of real projective space is the ring isomorphism

H^*(RPⁿ; F₂) ≅ F₂[α] / (αⁿ⁺¹), deg α = 1.

This file builds the right-hand side — the algebraic model — as a genuine, formalized Lean object together with the structural facts the final theorem consumes, namely (on the model side):

Here the model ring is the genuine quotient polynomial ring

RPnCohomologyRingModel n := (ZMod 2)[X] ⧸ (X^(n+1)),

and modelAlpha n is the residue class of X (the model of the degree-one generator α). ** The bridge H^*(RPⁿ; F₂) ≅ RPnCohomologyRingModel n remains genuinely open (it needs singular cohomology with a cup product that descends to a graded ring, the degree-one universal coefficient class α, and the cellular/inductive nonvanishing input — none of which exist in pinned Mathlib; see

These model facts are nonetheless the precise consequences requested for the final theorem (αⁿ ≠ 0, αⁿ is the top class, αⁿ⁺¹ = 0): under the ring isomorphism, they transport to H^*(RPⁿ; F₂).

source
noncomputable def SphereOddDegree.RPnCohomologyRingModel (n : ℕ) :
Type

The algebraic model F₂[α] / (αⁿ⁺¹) of the mod-two cohomology ring of RPⁿ, realized as the genuine quotient polynomial ring (ZMod 2)[X] ⧸ (X^(n+1)).

This is the right-hand side of the classical isomorphism H^*(RPⁿ; F₂) ≅ F₂[α]/(αⁿ⁺¹). The isomorphism itself to topological cohomology is not asserted here (it remains open); only the model and its internal structure are built.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable instance SphereOddDegree.instCommRingRPnCohomologyRingModel (n : ℕ) :
    CommRing (RPnCohomologyRingModel n)
    Equations
    source
    @[instance_reducible]
    noncomputable instance SphereOddDegree.instAlgebraZModOfNatNatRPnCohomologyRingModel (n : ℕ) :
    Algebra (ZMod 2) (RPnCohomologyRingModel n)
    Equations
    source
    noncomputable def SphereOddDegree.modelAlpha (n : ℕ) :
    RPnCohomologyRingModel n

    The model of the degree-one generator α: the residue class of the indeterminate X in RPnCohomologyRingModel n = (ZMod 2)[X] ⧸ (X^(n+1)).

    Equations
    Instances For
      source
      theorem SphereOddDegree.modelAlpha_pow_eq_zero_iff (n k : ℕ) :
      modelAlpha n ^ k = 0 ↔ n + 1 ≤ k

      Power-vanishing characterization. In the model ring F₂[α]/(αⁿ⁺¹), the power αᵏ vanishes exactly when k reaches the truncation bound, i.e. αᵏ = 0 ↔ n + 1 ≤ k. Equivalently, αᵏ ≠ 0 for all k ≤ n and αᵏ = 0 for all k ≥ n + 1.

      source
      @[simp]
      theorem SphereOddDegree.modelAlpha_pow_succ_eq_zero (n : ℕ) :
      modelAlpha n ^ (n + 1) = 0

      The truncation relation. αⁿ⁺¹ = 0 in the model ring — this is the defining relation of F₂[α]/(αⁿ⁺¹).

      source
      theorem SphereOddDegree.modelAlpha_pow_ne_zero (n k : ℕ) (hk : k ≤ n) :
      modelAlpha n ^ k ≠ 0

      Sub-truncation nonvanishing. αᵏ ≠ 0 for every k ≤ n: every power strictly below the truncation bound is nonzero in the model ring.

      source
      theorem SphereOddDegree.modelAlpha_pow_top_ne_zero (n : ℕ) :
      modelAlpha n ^ n ≠ 0

      The top power is nonzero. αⁿ ≠ 0 in the model ring — the model-side form of "αⁿ ≠ 0", i.e. the top class survives.

      source
      theorem SphereOddDegree.modelAlpha_isNilpotent (n : ℕ) :
      IsNilpotent (modelAlpha n)

      α is nilpotent in the model ring (with αⁿ⁺¹ = 0).

      source
      theorem SphereOddDegree.modelAlpha_finrank (n : ℕ) :
      Module.finrank (ZMod 2) (RPnCohomologyRingModel n) = n + 1

      Total dimension. The model ring F₂[α]/(αⁿ⁺¹) is a free F₂-module of rank n + 1, matching Σₖ dim_{F₂} Hᵏ(RPⁿ; F₂) = n + 1 (one class in each degree 0, 1, …, n).