prop_6_18_unramified via the Hermitian-line model #
The unramified case of Proposition 6.18 (eq. (115)): for a simple faithful 𝔽₂[C]-module V
of cardinality 2^{2m} at an unramified marking (c tameTau acts trivially), the base
determinant form Q⁰_loc has the negative Gauss sign:
#(Q⁰_loc)⁻¹(0) = 2^{2m−1} − 2^{m−1}.
Unlike the ramified case (which routes through Lemma 6.17's self-perpendicularity + vanishing,
GQ2.DeepPart.card_Q0loc_zero_eq_of_dim_of_vanish, hardwired to the + sign), the unramified
minus-type count comes from the Hermitian-line model: V is identified with a finite field
F = 𝔽_{2^{2m}} (Schur, C cyclic hence 𝔽₂[C]-image a field), H¹(G_{ℚ₂}, V) ≅ F as an
F-line, and Q⁰_loc transports to a nonsingular norm-one-invariant quadratic form on F,
whose zero-count is 2^{2m−1} − 2^{m−1} by the model-free algebraic core
GQ2.DeepPart.card_normOne_invariant_form_zero.
This file lives downstream of DeepPart (which supplies Q0loc, the Euler collapse, the
Hermitian count, and nonsingular_Q0loc), so — following the Lemma 6.14 proof / 6.18-ramified pattern — the
statement is moved out of SectionSix.lean (a pointer comment is left there); the fully
qualified name stays GQ2.SectionSix.prop_6_18_unramified is preserved by re-export.
Coefficient functoriality of mapCoeff1 (general — belongs in the cohomology library) #
mapCoeff1 is functorial in the coefficient map: it sends id to id and f ∘ g to
mapCoeff1 f ∘ mapCoeff1 g. These descend the corresponding cochain-level facts about Z1comap
through the H¹ quotient (QuotientAddGroup.map_mk'). Needed to promote the coefficient action
of an abelian C on V to a C-action on H¹.
Step 1 of the unramified model: the acting group C is cyclic, generated by
c tameSigma. Faithfulness (hfaith) upgrades the trivial action hunram to the trivial
element c tameTau = 1, then tame topological generation (SectionThree.gen_ttame_quotient)
collapses the two generators to one. (Verbatim the hgen step of prop_6_9_unramified.)
Commutativity of a cyclic C (generated by t): every element is a power of t.
The coefficient endomorphism of H¹(G_ℚ₂, V) attached to c : C (for a ρ-factored
action with C commutative): c • · is a G_ℚ₂-equivariant additive endo of V —
equivariance is commutativity of C with the ρ-factored action — so it acts on H¹ via
mapCoeff1.
Equations
- GQ2.UnramifiedModel.cCoeff ρ hρ hCcomm c = GQ2.ContCoh.mapCoeff1 (DistribSMul.toAddMonoidHom V c) ⋯ ⋯
Instances For
The coefficient action of a commutative C on H¹(G_ℚ₂, V) (brick toward
arf(Q0loc)=1): the DistribMulAction axioms for cCoeff descend from mapCoeff1
functoriality (mapCoeff1_id/mapCoeff1_comp).
Equations
- GQ2.UnramifiedModel.cActionH1 ρ hρ hCcomm = { smul := fun (c : C) => ⇑(GQ2.UnramifiedModel.cCoeff ρ hρ hCcomm c), mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }
Instances For
The Schur transfer (brick (c)): for a cyclic C = ⟨T⟩ acting faithfully and simply on a
finite nontrivial V, the coefficient action cCoeff on H¹(G_ℚ₂, V) is again faithful and
simple, provided #H¹ = #V.
Route: F := 𝔽₂⟨σ⟩ ⊆ End(V) (σ = the T-action) is a finite domain — kernels of its nonzero
elements are C-stable, so trivial by simplicity, and injective ⟹ bijective on finite V —
hence a field by little Wedderburn (Finite.isDomain_to_isField; no commutativity needed as
input). The orbit map F → V, f ↦ f v₀ at any v₀ ≠ 0 is injective with C-stable range,
so bijective by simplicity: #F = #V. mapCoeff1 transfers F multiplicatively/additively to
End(H¹), where units of F stay pointwise-invertible; the orbit map F → H¹ at any
0 ≠ x₀ ∈ S for a C-stable S is injective with range inside S, so
#S ≥ #F = #V = #H¹ forces S = ⊤.
Brick (d2), the explicit datum coboundary: for g₀ : C (abelian C), the graph pullback
along the g₀-comapped datum differs from the original by the 2-coboundary of the continuous
1-cochain γ ↦ m_{g₀}(b γ). Pointwise this is m_quad (turning f(g₀v, g₀w) − f(v,w) into the
∂(m_{g₀})-term) plus the two m_mul expansions of m_{g₀·ργ} = m_{ργ·g₀} and the 1-cocycle
identity for b. This is the specific instance of Lemma 6.4 datum-independence that the
unramified Prop 6.18 needs.
Proposition 6.18, eq. (115), unramified case: negative Gauss sign,
#(Q⁰_loc)⁻¹(0) = 2^{2m−1} − 2^{m−1}.
Proved via the Hermitian-line model (see the file docstring): identify V with 𝔽_{2^{2m}},
transport Q⁰_loc to a norm-one-invariant nonsingular form, and count zeros with
card_normOne_invariant_form_zero. [the §§6–7 statement; proof the deep-part proof, Ax: B6, B7.]
Signature note: the hypothesis hc : Function.Surjective ⇑c (as in
prop_6_18_ramified).
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- eq. (115) = ⟦eq-localzeros⟧
- Lemma 6.17 = ⟦lem-shapirodet⟧
- Lemma 6.4 = ⟦lem-detnormalizationindependence⟧
- Proposition 6.18 = ⟦prop-localzero⟧