Documentation

LeanPool.NandakumarRamanaRao.NRR.OddSphereDegree.RPnCohomologyRingBridge

Bridge from RP singular cohomology to the truncated polynomial model #

Defines explicit interfaces for maps from the actual mod-two cohomology of RP n to the model F₂[α]/(αⁿ⁺¹) and derives nonvanishing and truncation consequences for cup powers. This module is an intermediate model-comparison API; the final unconditional odd-degree proof uses the direct cohomology-dimension-vanishing route.

source
structure SphereOddDegree.RPnCohomologyToModelHom (n : ℕ) :
Type

The model-side half of the RPⁿ mod-two cohomology ring isomorphism: a graded ring homomorphism from the actual singular cohomology of RPⁿ to the algebraic model F₂[α]/(αⁿ⁺¹), carrying a chosen degree-one class to the model generator modelAlpha n.

This is the honest, explicit, single hypothesis to which the top-class nonvanishing αⁿ ≠ 0 in Hⁿ(RPⁿ; F₂) is reduced. Concretely it bundles:

  • a ZMod 2-linear map toFun k : Hᵏ(RPⁿ; F₂) → F₂[α]/(αⁿ⁺¹) in every degree;
  • multiplicativity across degrees for the cup product (toFun (p+q) (a ⌣ b) = toFun p a · toFun q b);
  • unitality (toFun 0 1 = 1);
  • a chosen degree-one class alpha ∈ H¹(RPⁿ; F₂) with toFun 1 alpha = modelAlpha n.

Such a homomorphism is exactly what the classical ring isomorphism supplies on the model side.

Instances For
    source
    theorem SphereOddDegree.RPnCohomologyToModelHom.map_cupPow {n : ℕ} (Φ : RPnCohomologyToModelHom n) (k : ℕ) :
    (Φ.toFun k) (cupPowZMod2 Φ.alpha k) = modelAlpha n ^ k

    The bridge sends the k-th cup power of the chosen class α to modelAlpha n ^ k. This is the computation that transports the model nonvanishing facts to the actual cohomology.

    source
    theorem SphereOddDegree.rpAlpha_power_ne_zero {n : ℕ} (Φ : RPnCohomologyToModelHom n) {k : ℕ} (hk : k ≤ n) :
    cupPowZMod2 Φ.alpha k ≠ 0

    Conditional sub-truncation nonvanishing, in the actual cohomology. Given the bridge Φ, the k-th cup power of α is nonzero in the genuine Hᵏ(RPⁿ; F₂) for every k ≤ n.

    source
    theorem SphereOddDegree.rpAlpha_power_top_ne_zero {n : ℕ} (Φ : RPnCohomologyToModelHom n) :
    cupPowZMod2 Φ.alpha n ≠ 0

    Conditional top-class nonvanishing, in the actual cohomology — the load-bearing αⁿ ≠ 0 in the genuine Hⁿ(RPⁿ; F₂).

    source
    structure SphereOddDegree.RPnCohomologyRingModelEmbedding (n : ℕ) extends SphereOddDegree.RPnCohomologyToModelHom n :
    Type

    The full model-side ring embedding of the actual RPⁿ mod-two cohomology: a graded ring homomorphism to the model (RPnCohomologyToModelHom n) that is, in addition, injective in every degree. This is the genuine "ring-equivalence hypothesis" the design asks to reduce to: an injective graded ring map to the model carrying α to modelAlpha n is exactly the model-side data of the isomorphism H^*(RPⁿ; F₂) ≅ F₂[α]/(αⁿ⁺¹), and it pins down the relation αⁿ⁺¹ = 0 as well as the nonvanishing.

    Instances For
      source
      theorem SphereOddDegree.rpAlpha_power_succ_eq_zero {n : ℕ} (e : RPnCohomologyRingModelEmbedding n) :
      cupPowZMod2 e.alpha (n + 1) = 0

      Conditional truncation relation, in the actual cohomology. Given the injective bridge, αⁿ⁺¹ = 0 in the genuine Hⁿ⁺¹(RPⁿ; F₂).

      source
      theorem SphereOddDegree.rpAlpha_power_eq_zero_iff {n : ℕ} (e : RPnCohomologyRingModelEmbedding n) (k : ℕ) :
      cupPowZMod2 e.alpha k = 0 ↔ n + 1 ≤ k

      Conditional full power-vanishing characterization, in the actual cohomology. Given the injective bridge, the cup power αᵏ vanishes in Hᵏ(RPⁿ; F₂) exactly at and beyond the truncation bound: αᵏ = 0 ↔ n+1 ≤ k.

      source
      theorem SphereOddDegree.rpAlpha_power_top_fixed_ne_zero {n : ℕ} (Φ : RPnCohomologyToModelHom n) (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (ha : (ModuleCat.Hom.hom (inducedOnRPPullback f hf 1)) Φ.alpha = Φ.alpha) :
      (ModuleCat.Hom.hom (inducedOnRPPullback f hf n)) (cupPowZMod2 Φ.alpha n) = cupPowZMod2 Φ.alpha n ∧ cupPowZMod2 Φ.alpha n ≠ 0

      Conditional final-theorem package, in the actual cohomology. Given the bridge Φ and a degree-one class α = Φ.alpha fixed by the pullback of a descended odd self-map fbar = inducedOnRP f hf, the top cup power αⁿ ∈ Hⁿ(RPⁿ; F₂) is simultaneously fixed by fbar^* and nonzero. This is exactly the shape consumed by the final odd-degree comparison: fbar^*(α) = α forces fbar^*(αⁿ) = αⁿ, while αⁿ ≠ 0 makes that identity nontrivial.