The abstract Kummer presentation package #
For a degree-2 extension k ≤ L of intermediate fields of ℚ̄₂/ℚ_[2] and a deep element
A ∈ L (‖A − 1‖ < ‖2‖), produce the concrete Kummer presentation that
SectionSix.lemma_6_16 consumes (the paper's "write L = k(√d), a = u + v√d", §6.3):
- a generator
(d : (↥k)ˣ, δ : ℚ̄₂)withδ² = d,δ ∈ L, and the Galois identificationG_L = Stab(δ)insideG_k(fixingSubgroup_subgroupOf_eq_stabilizer); - coordinates
(u : (↥k)ˣ, v : ↥k)withA = u + v·δ— the constant coordinate is a unit becauseAis deep:u = 0forcesσA = −Afor the conjugationσ, whence‖2‖ = ‖(A−1) + (σA−1)‖ ≤ max(‖A−1‖, ‖σA−1‖) = ‖A−1‖ < ‖2‖(ultrametric +GQ2.norm_galois).
The exported statement exists_kummer_presentation matches lemma_6_16's hypothesis shapes
on the nose. Interface note: the deepness input is the norm inequality
‖A − 1‖ < ‖2‖ — the consumer converts IsDeepUnit via the
banked LocalKummer.norm_sub_one_lt_of_isDeepUnit; this keeps the file free of IsDeepUnit
and §6 imports.
The mathlib gap is fixingSubgroup_adjoin_simple: the fixing subgroup of a simple adjoin
F⟮δ⟯ is the stabilizer of δ — mathlib has the Galois connection le_iff_le but not this
equality. Everything else is assembled from IntermediateField
(extendScalars/adjoin/eq_of_le_of_finrank_le), the infinite Galois correspondence
(InfiniteGalois.fixedField_fixingSubgroup at ⊥, giving the conjugation σδ = −δ with no
power basis, no liftNormal, no minpoly identification — (σδ)² = δ² suffices), and
Submodule.mem_span_pair for the coordinates.
Paper: §6.3, around eq. (110). Axioms: ∅ (std-3 target).
The √-adjoin fixing-subgroup lemma (the mathlib gap) #
The √-adjoin generator lemma (not in mathlib): the fixing subgroup of a simple adjoin
F⟮δ⟯ is exactly the stabilizer of the generator. ⟹ is δ ∈ F⟮δ⟯; ⟸ runs the Galois
connection IntermediateField.le_iff_le on the cyclic subgroup zpowers σ.
The concrete tower ℚ_[2] ≤ k ≤ L ≤ ℚ̄₂ #
Membership in ⊥ : IntermediateField ↥k ℚ̄₂ is membership in k (the base-change of the
bottom element along the subtype algebra map).
Complete the square: a degree-2 extension of intermediate fields of ℚ̄₂/ℚ_[2] has a
square-root generator: δ ∈ L ∖ k with δ² = d ∈ kˣ and L = k⟮δ⟯. From a primitive
θ ∈ L ∖ k (degree 2 is prime) with monic quadratic minimal polynomial X² + aX + b, take
δ := θ + a/2, d := a²/4 − b.
Coordinates in the {1, δ} basis: every element of L = k⟮δ⟯ is u + v·δ with
u, v ∈ k (the span of the independent pair {1, δ} fills the 2-dimensional L by
finrank comparison; extract with Submodule.mem_span_pair).
The conjugation: some ↥k-automorphism of ℚ̄₂ negates δ. Since δ ∉ k, the
infinite Galois correspondence over ↥k (at ⊥, via fixingSubgroup_bot) produces a σ
moving δ; then (σδ)² = σ(δ²) = d = δ² forces σδ = −δ — no minimal polynomial needed.
Unit coordinate: if A = u + v·δ is deep (‖A − 1‖ < ‖2‖) then u ≠ 0 — otherwise
the conjugation gives σA = −A, so (A−1) + (σA−1) = −2 while both summands have norm
< ‖2‖ (Galois invariance GQ2.norm_galois + ultrametric inequality): contradiction.
Uniform in v (the v = 0 sub-case is A = 0, killed by the same norms).
The subgroupOf-packaged form of fixingSubgroup_adjoin_simple at the tower
ℚ_[2] ≤ k ≤ L ≤ ℚ̄₂: inside G_k, fixing L pointwise is stabilizing δ. Elements of
k.fixingSubgroup upgrade to ↥k-automorphisms along IntermediateField.fixingSubgroupEquiv
(same underlying function), L-membership transports along mem_extendScalars (Iff.rfl)
and hadj.
The exported package #
The abstract Kummer presentation package (the Lemma 6.17 vanishing proof, exported interface): a degree-2
extension k ≤ L inside ℚ̄₂/ℚ_[2] together with a deep element A ∈ L yields the full
generator-and-coordinates data of SectionSix.lemma_6_16: d, δ with δ² = d, δ ∈ L,
the fixing-subgroup/stabilizer identification, and A = u + v·δ with u a unit.
Consumer (the Lemma 6.17 vanishing proof) supplies hdeg from the index-2 hypothesis (fixing-index → degree
bridge) and hA1 from IsDeepUnit via LocalKummer.norm_sub_one_lt_of_isDeepUnit.
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- eq. (110) = ⟦eq-evensvanish⟧