Conditional odd-map cohomological comparison #
Assembles the reusable implication from explicit RP cohomology generator, cup-power,
transfer/naturality, and mod-two degree data to odd integer degree. These conditional interfaces
are used by later assembly modules; the stable public theorem is the unconditional endpoint in
SphereOddDegree.Final.
1. Element-level double-cover naturality (genuine) #
Element-level naturality square of the double cover at degree k.
Applying the morphism identity inducedOnRP_pullback_naturality to a cohomology
class a ∈ Hᵏ(RPⁿ; F₂) gives
proj^*(fbar^* a) = f^*(proj^* a) in Hᵏ(Sⁿ; F₂).
f^* fixes the pulled-back top class. If the descended odd map fbar
fixes a top class a ∈ Hⁿ(RPⁿ; F₂) (fbar^* a = a), then the sphere self-map
f fixes its image proj^* a ∈ Hⁿ(Sⁿ; F₂) under the double-cover pullback:
f^*(proj^* a) = proj^* a.
This is the genuine, unconditional cohomological core of the comparison: it is
the push of fbar^*(αⁿ) = αⁿ across the double-cover naturality square.
2. Conditional top-class / degree comparison #
Conditional mod-2 degree comparison from the top class.
Given a top class a ∈ Hⁿ(RPⁿ; F₂) that is fixed by the descended odd map
(fbar^* a = a) and whose double-cover image proj^* a is a nonzero element of
Hⁿ(Sⁿ; F₂), the only remaining input is the top-class / degree comparison
hcmp: that f^* fixing the nonzero sphere top class forces
degree f ≡ 1 (mod 2). Under that input the mod-2 degree is 1.
The genuine work — pushing fbar^* a = a to f^*(proj^* a) = proj^* a via the
double-cover naturality square — is done by spherePullback_fixes_projPullback;
hcmp then consumes that fact.
Conditional oddness of the degree from the top class. The Odd phrasing
of oddMap_degree_mod_two_eq_one_of_top_class_comparison, obtained through the
parity bridge degreeOfIso_intCast_zmodTwo_eq_one_iff_odd.
3. Conditional final theorem from the full cohomological chain #
Conditional final odd-map degree theorem from the full cohomological chain. This is the assembled conditional version of
f odd ⇒ Odd (degree f),
with the cohomological inputs as explicit hypotheses. Concretely:
alpha— the degree-one classα ∈ H¹(RPⁿ; F₂);alphaPow— the top classαⁿ ∈ Hⁿ(RPⁿ; F₂);hα_fixed—fbar^*(α) = α, the action of the descended odd map onα;hpow— pullback preserves powers,fbar^*(α)=α ⇒ fbar^*(αⁿ)=αⁿ;hne—proj^* αⁿ ≠ 0, the nonvanishing of the top class on the sphere;hcmp— the top-class / degree comparison.
The internal step fbar^*(αⁿ)=αⁿ ⇒ f^*(proj^* αⁿ)=proj^* αⁿ follows from
spherePullback_fixes_projPullback, and the parity bridge yields the final oddness statement.
3b. Conditional final theorem from the single ring-bridge hypothesis #
Conditional final odd-map degree theorem from the single ring-bridge
hypothesis. This is the same conclusion as
oddMap_degree_odd_of_cohomological_inputs, but with the four separate RPⁿ-side
inputs (alpha, alphaPow, hpow, and the RPⁿ-level nonvanishing αⁿ ≠ 0)
replaced by the single model-side ring-bridge hypothesis
Φ : RPnCohomologyToModelHom n (RPnCohomologyRingBridge.lean).
Given the bridge Φ:
- the degree-one class is
α := Φ.alpha ∈ H¹(RPⁿ; F₂); - the top class is its
n-th cup powerαⁿ := cupPowZMod2 Φ.alpha n ∈ Hⁿ(RPⁿ; F₂); - the step
fbar^*(α) = α ⇒ fbar^*(αⁿ) = αⁿis discharged automatically by the proved cohomology-level cup-power naturality (rpAlpha_power_top_fixed_ne_zero), andαⁿ ≠ 0is supplied by the bridge as well, so neither needs to be assumed separately.
The only remaining inputs are the genuinely sphere and degree side ones: the action
hypothesis hα_fixed (fbar^*(α) = α, gated on the degree-one UCT identifying
α), the sphere nonvanishing hne, and the top-class/degree comparison hcmp.
Thus the RPⁿ top-class story is reduced to the one explicit input Φ.
3c. The single required input, packaged as one named comparison #
Everything above keeps the genuine topological coefficient-reduction / top-class
comparison as a per-call hypothesis hcmp. We now isolate it once and for all as a
single named predicate ModTwoTopClassComparison e, uniform over all sphere
self-maps and all nonzero top F₂-classes. The final odd-map theorem then
follows from this one input together with the proved unconditional ingredients
(the double-cover naturality core spherePullback_fixes_projPullback and the
parity bridge degreeOfIso_intCast_zmodTwo_eq_one_iff_odd), with no extra
parity assumptions. This is the exact form of the required input.
The mod-two top-class / degree comparison. This interface packages the
coefficient-reduction statement consumed by the conditional assembly. Relative to a chosen
identification
e : SphereTopHomologyIso n (which fixes the integer degree degreeOfIso e), it
asserts: whenever a self-map f of Sⁿ fixes a nonzero top class
c ∈ Hⁿ(Sⁿ; F₂) (f^* c = c, c ≠ 0), its integer degree is odd mod 2
((degree f : ZMod 2) = 1).
It states that the action on a nonzero top mod-two cohomology class determines the parity of the integer degree. Downstream coefficient-reduction modules construct this comparison.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reduction of the comparison to the top F₂-homology scalar action #
The comparison ModTwoTopClassComparison e is here reduced — fully formalized,
using only the library's proved universal-coefficient machinery over F₂
(kroneckerMap_naturality_apply and kroneckerMap_injective) — to the single,
precise statement that the F₂ pushforward on the top homology Hₙ(Sⁿ; F₂) acts
as the scalar (degree f mod 2). This isolates the exact homological scalar statement from which
the comparison
follows.
The top F₂-homology scalar action. Relative to a chosen integral
identification e : SphereTopHomologyIso n, this asserts that the F₂ homology
pushforward f_* : Hₙ(Sⁿ; F₂) → Hₙ(Sⁿ; F₂) of every self-map f acts as the
scalar (degreeOfIso e f : ZMod 2).
Mathematically this is the conjunction of (i) Hₙ(Sⁿ; F₂) being one-dimensional
over F₂ (so f_* is a scalar) and (ii) that scalar being the mod-2 reduction
of the integer degree (coefficient-change compatibility Hₙ(-;ℤ)⊗F₂ → Hₙ(-;F₂)).
Downstream sphere-homology and coefficient-reduction modules prove this scalar
action for the canonical orientation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The comparison follows from the top F₂-homology scalar action. This is a
proved, formalized reduction: it derives ModTwoTopClassComparison e from
ModTwoTopHomologyScalar e using only the library's proved F₂ universal
coefficient theorem (the Kronecker classifier's naturality and injectivity).
Given a self-map f fixing a nonzero top class c ∈ Hⁿ(Sⁿ; F₂), the Kronecker
functional ψ = ⟨c, ·⟩ is nonzero (injectivity) and f_*-invariant (naturality
plus f^* c = c); the scalar hypothesis turns invariance into ψ z = d · ψ z
for d = degree f mod 2, and since some ψ z = 1 in F₂ we get d = 1.
Final odd-map degree theorem from the single packaged comparison. Given
the one named input ModTwoTopClassComparison e, every odd self-map f of Sⁿ
that (via a fixed nonzero RPⁿ top class a) fixes the nonzero sphere top class
has odd integer degree. The proof uses only the proved unconditional core
spherePullback_fixes_projPullback and the proved parity bridge — there is no
extra parity assumption, exactly as required by the acceptance criterion.
Final odd-map degree theorem from the single comparison + the single ring
bridge. Combines the two reductions: the RPⁿ top-class story is reduced to one
ring bridge Φ : RPnCohomologyToModelHom n, and the sphere/degree story to the
one comparison ModTwoTopClassComparison e. The only remaining sphere-side
hypotheses are the genuine action input hα_fixed (fbar^*(α) = α) and the
sphere nonvanishing hne; all parity reasoning is discharged.
3d. conditional near-final assembly: three named blockers, no vacuous hypothesis #
The theorems in §3b/§3c route the sphere-side nonvanishing through projPullback
(proj^*). That route is degenerate: for n ≥ 1 one has proj^* α = 0 in
H¹(RPⁿ; F₂), hence proj^*(αⁿ) = 0, so the hypothesis proj^* (αⁿ) ≠ 0 is
unsatisfiable and the genuine comparison really proceeds through the double-cover
transfer, not proj^*. The assembly below avoids that degenerate route
entirely: it depends on exactly three honest named blockers and no vacuous or
redundant hypothesis.
Odd self-maps fix a nonzero top F₂-class. This packages the genuine
content of the RPⁿ / double-cover descent half of the argument: every odd
self-map f of Sⁿ fixes some nonzero class c ∈ Hⁿ(Sⁿ; F₂)
(f^* c = c, c ≠ 0).
Mathematically this holds because f descends to fbar : RPⁿ → RPⁿ, which acts
as the identity on the one-dimensional top group Hⁿ(RPⁿ; F₂) = ⟨αⁿ⟩ (the unique
nonzero element is fixed by any ring map), and the double-cover transfer
homomorphism transports this to the nonzero sphere top class. This property is packaged as an
explicit named input corresponding to the F₂ transfer/Gysin
sequence of the double cover Sⁿ → RPⁿ. It is
not the degenerate proj^* route (proj^*(αⁿ) = 0 for n ≥ 1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conditional near-final odd-map degree theorem.
f odd ⇒ Odd (degree f),
assembled from exactly the three remaining named topological blockers — and with
no vacuous or redundant hypothesis (in particular it does not route through
the degenerate proj^* avatar, for which proj^*(αⁿ) = 0 when n ≥ 1):
e : SphereTopHomologyIso n— the integral top-homology identificationHₙ(Sⁿ; ℤ) ≅ ℤthat pins the integer degreedegreeOfIso e; blocker branch sphere top homology (SphereTopHomologyReduction.lean);hcmp : ModTwoTopClassComparison e— a self-map fixing a nonzero topF₂-class has odd integer degree; blocker branch mod-two degree comparison (theF₂-coefficient transfer/reduction,ModTwoDegreeComparison.lean);htop : OddMapFixesTopClass n— an odd self-map fixes a nonzero topF₂-class; blocker branch RPⁿ / double-cover descent (the descended map acts trivially onHⁿ(RPⁿ; F₂), transported by the transfer).
Every other ingredient is the library's proved, unconditional machinery: the
parity bridge degreeOfIso_intCast_zmodTwo_eq_one_iff_odd. The oddness
hypothesis hf is used genuinely (it feeds htop to produce the fixed nonzero
top class). Supplying genuine terms for e, hcmp, htop specializes this to
the unconditional final theorem with no change of proof.
3e. Discharging the fbar^*(α) = α hypothesis via the constructed rpAlpha #
The theorems in §3–§3d keep the action of the descended odd map on the degree-one
class as an explicit hypothesis hα_fixed : fbar^*(α) = α. Using the genuine
class rpAlpha n m (ConstructRPAlpha.lean) built from a monodromy functional
m : MonodromyFunctional n (the degree-one homology functional interface), this
hypothesis is proved by inducedOnRPPullback_rpAlpha,
and — via the cohomology-level cup-power naturality — so is its consequence on the
top power. The theorems below are the §3/§3c assemblies with the hα_fixed
hypothesis removed.
§3 assembly with fbar^*(α) = α discharged. Same conclusion as
oddMap_degree_odd_of_cohomological_inputs, but with the action hypothesis
hα_fixed removed: it is supplied by inducedOnRPPullback_rpAlpha for the genuine
class α := rpAlpha n m. The only RPⁿ-side datum now needed is the monodromy
functional m (the degree-one Hurewicz input).
Top-class assembly with both fbar^*(α) = α and the power step discharged.
Taking the top class to be the n-th cup power (rpAlpha n m)ⁿ, both the action
hypothesis fbar^*(α) = α (via inducedOnRPPullback_rpAlpha) and its power
consequence fbar^*(αⁿ) = αⁿ (via inducedOnRP_cohPullback_cupPow_fixed) are
proved. The only remaining inputs are the genuine sphere/degree-side ones
(e, hne, hcmp) and the single monodromy functional m.
4. Sanity specializations (genuine) #
Sanity check: for the identity map every top class is fixed, so the
naturality core fires trivially — f^* fixes proj^* of any top class.
Sanity check: for the antipodal map (which descends to the identity on
RPⁿ) every top class is fixed, so (antipodal)^* fixes proj^* of any top
class.