The Q⁰_loc quadratic structure (§6.3, eq. (93)) #
Q⁰_loc is a quadratic map on H¹(G_ℚ₂, V) whose polar form is the cup product of the polar
pairing (through ι_F): at the cochain level,
gp(b₁+b₂) − gp(b₁) − gp(b₂) − (b₂ ∪_B b₁) = δ¹(g ↦ f(b₁ g, b₂ g)),
by four instances of the factor-set cocycle identity and f_polar — no bilinearity of f
needed. Class level via RepIndependence.repIndep (Lemma 6.4). This layer also proves the
nonsingularity of Q⁰_loc, that the deep half X₊ is an additive subgroup, and the dim clause
feeding Prop 6.18 (ramified).
This file is part of the GQ2.DeepPart split (the deep-part proof); see GQ2/DeepPart.lean for the overview.
The (93) cochain identity: the graph pullback is quadratic in the cocycle, with the
cup cocycle of the polar pairing (swapped slots) as cross-term, up to the explicit coboundary
δ¹(g ↦ f(b₁ g, b₂ g)).
Q⁰_loc unfolded (definitional).
The polar pairing is G_ℚ₂-equivariant for a Galois-invariant q (𝔽₂ acts trivially).
Eq. (93), class level: Q⁰_loc(x+y) = Q⁰_loc(x) + Q⁰_loc(y) + ι_F(y ∪_B x).
The polar form of Q⁰_loc is the (swapped) polar-pairing cup through ι_F —
eq. (93) in polar form.
Q⁰_loc is a quadratic map on H¹(G_ℚ₂, V) (eq. (93)): normalized with biadditive
polar form.
Nonsingularity of Q⁰_loc (B6 perfect11 via the polar μ₂-dual) #
SectionSix's 𝔽₂ → μ₂ bridge is (definitionally) the DeepPart one.
The μ₂-valued polar self-duality v ↦ (w ↦ bridge(B(v,w))) — definitionally
postPairing of the polar pairing with the bridge, viewed into the μ₂-dual.
Equations
Instances For
Equivariance of the polar μ₂-dual map.
#Hom(V, μ₂) = #V for exp-2 V.
The polar μ₂-dual map is bijective (nonsingularity + counting).
mapCoeff1 of an equivariant additive bijection is injective (coboundaries pull back
along the inverse).
Cup coefficient naturality at the polar pairing: pushing the 𝔽₂-valued polar cup along
the μ₂-bridge is the μ₂-evaluation cup against the polar μ₂-dual class (definitional at
representatives).
Q⁰_loc is nonsingular (§6.3): its polar form is a perfect pairing on H¹(G_ℚ₂, V),
via B6's perfect11 clause through the polar μ₂-self-duality.
The deep half X₊ is a subgroup #
0 ∈ X₊ (witness A = β = 1; the zero class restricts to 0 on ker ρ since coboundaries die
there) and X₊ + X₊ ⊆ X₊ (witness products: deep units are closed under multiplication, Kummer
cocycles are multiplicative on ker ρ-fixed squares, and out(x+y) = out x + out y up to a
coboundary that dies on ker ρ).
H¹ of an exponent-2 module has exponent 2.
A Z¹-cocycle whose class vanishes dies pointwise on ker ρ (the coboundary
g ↦ g•w₀ − w₀ is trivial there since the action factors through ρ).
The restricted Kummer cocycle of an N-fixed square is a hom on N (sign bookkeeping via
two_values_of_fixed).
The restricted Kummer cocycle of an N-fixed square lies in Z¹(N, 𝔽₂).
The φ-coordinate of a cocycle restricted to ker ρ lies in Z¹(ker ρ, 𝔽₂) (the action
is trivial there).
H1ofFun is additive on actual cocycles.
The deep half X₊ is an additive subgroup of H¹(G_ℚ₂, V).
Equations
- GQ2.DeepPart.deepPartSubgroup ρ hρ hV2 = { carrier := GQ2.SectionSix.deepPart ρ, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
The dim clause and Prop 6.18 (ramified), reduced to the two Kummer cores #
Prop 6.18 (eq. (115), ramified) from Lemma 6.17: given the dim clause (hdim,
#X₊² = #H¹) and the vanishing clause (hvanish, Q⁰_loc|X₊ = 0), the zero-count of
Q⁰_loc is 2^{2m−1} + 2^{m−1} — the positive Gauss sign, via the Lagrangian Arf package
(arf_zero_of_card_sq) and the Euler-characteristic count. Ax: B6 (via D), B7.
The two-torsion subgroup of a 2^{2m}-order simple module is everything: V has
exponent 2 (additive Cauchy + simplicity).