§3 statements: the tame and maximal pro-2 quotients #
Faithful Lean statements of the paper's §3 interior nodes — Prop. 3.2,
Lemmas 3.5, 3.7, Prop. 3.8, and Prop. 1.1 — phrased against the foundational APIs.
The companion
design note docs/section3-extraction.md maps every statement to its paper display and
records the absorption and deviation decisions summarized here:
- Lemma 3.4 is absorbed by the axiom layer: its abstract-isomorphism clause is subsumed by
the marked B3c interface (
absGalQ2_maxProTwo_presentationis not used as a separate B4 axiom), and its orientation-value clause is also part of B3c (DyadicOrientation, route (ii)), and its classification-membership clause ("D₀is the standard rank-3,q = 2Demushkin group") is deliberately-unformalized Labute content per the standing B3b decision (the Demushkin classification and orientation interface). No additional statement is introduced for it. - Lemma 3.6 is absorbed: it is axiom B8 (
peripheralCyclotomicAction) verbatim — the peripheral-action interface bundle is exactly Lemma 3.6's group-theoretic conclusion. - Lemma 3.5's
(ν_ur, χ_D)rows of eq. (13) and the abelianized relationā²s̄⁴ = 1are already proved (bundle-parametrized) inGQ2/Reciprocity.lean:nu_ur_recip_neg4/nu_ur_recip_uniformizer/nu_ur_recip_neg3,chiCyc_recip_neg4/chiCyc_recip_neg3,abelianized_relator. What remains here: the marked pro-2-abelianization identification, the Hilbert-symbol square-class ledger, and the injectivity of the pair(ν_ur, χ_D). - Prop. 3.2's local side rests on axiom B10 (
GQ2.tameQuotient): the classical tame-quotient description ofG_{ℚ₂}(NSW (7.5.3), Iwasawa) is not derivable from the 2-centric step-1 census. The bundle and citation discussion live inGQ2/TameQuotient.lean; what remains a theorem here is Lemma 3.3's maximality (themaximalfieldprop_3_2_localadds on top of the axiom'sTameQuotientData).
Conventions: x ^ g = g⁻¹xg (conjP), [x,y] = x⁻¹y⁻¹xy (commP), reciprocity/ν_ur
normalizations as in the LocalReciprocity convention table (GQ2/Reciprocity.lean).
Topology on the topological abelianization #
GQ2.topAbelianization (the Demushkin classification) registered only the Group instance; the statements below
compare topological abelianizations, so we register its canonical quotient topology. These
are the (unique) canonical instances, named explicitly to avoid auto-name collisions.
The quotient topology on G^{ab} = G ⧸ closure ⁅G,G⁆.
Equations
- GQ2.SectionThree.instTopologicalSpaceTopAbelianization G = { IsOpen := GQ2.SectionThree.instTopologicalSpaceTopAbelianization._aux_1 G, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }
G^{ab} is a topological group.
The abelianization projection G →* G^{ab} (cf. GQ2.toAb for G = G_{ℚ₂}).
Equations
- GQ2.SectionThree.abMk = { toFun := QuotientGroup.mk, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Pro-2 abelianization infrastructure for D₀ #
The instances and coordinate machinery that Lemmas 3.5/3.7/3.8 and Prop. 1.1 consume: the
profinite-group instances on G^{ab} (so ZtwoPowering's zpowZtwo applies), the pro-2-ness of
D₀^{ab}, and the coordinate surjection D0ab_coord: every element of D₀^{ab} is
Ā^a S̄^s Ȳ^y (topological generation of {Ā, S̄, Ȳ} pushed through
F₃ ↠ D0Full ↠ D₀ ↠ D₀^{ab}, with the range a closed subgroup).
G^{ab} is commutative.
Equations
- GQ2.SectionThree.instCommGroupTopAb = { toGroup := inferInstance, mul_comm := ⋯ }
Instances For
IsProP p passes along a continuous surjection.
topAbelianization D0 is pro-2 (image of the pro-2 group D0 under abMk).
zpowZtwo helper lemmas #
Powering a square-trivial element: g ^ a = g ^ (a mod 2).
In a commutative pro-2 group, ℤ₂-powering distributes over the base.
ℤ₂-powering in Multiplicative ℤ₂ is multiplication of exponents.
x ^ (0 : ℤ₂) = 1.
Φ : ℤ₂³ → D0^ab and its surjectivity #
The coordinate hom Φ(a,s,y) = Ā^a · S̄^s · Ȳ^y on D0^{ab}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Coordinate surjectivity of D0^{ab}: every element is Ā^a S̄^s Ȳ^y.
The finite-quotient tame group T_tame (paper §3, first display) #
T_tame = ⟨σ, τ | τ^σ = τ²⟩_prof is GQ2.Ttame with marked generators
tameSigma/tameTau (the boundary-frame design layer, GQ2/BoundaryFrame.lean; the tame relation
τ^σ = τ² is proved as GQ2.tame_relation in GQ2/TameQuotient.lean).
GQ2/Tame.lean (Lemma 3.1, fully proved) describes its finite quotients.
The marked generators of Γ_A and its wild subgroup W_A (paper §2.1/§3) #
W_A is the closed normal subgroup of Γ_A generated by the images of x₀, x₁ (paper
§2.1, after eq. (7)). Deduplicated with the admissible-limit proof (GQ2/AdmissibleLimit.lean): wildPart
is definitionally GQ2.wildCore (the generator spellings agree up to rfl), so the admissible-limit proof's
limit theorems transfer verbatim — in particular isProP_wildPart below is
isProP_wildCore, the pro-2 clause of eq. (7) in the limit.
The image of σ in Γ_A.
Equations
Instances For
The image of τ in Γ_A.
Equations
Instances For
The image of x₀ in Γ_A.
Equations
Instances For
The image of x₁ in Γ_A.
Equations
Instances For
W_A (paper §2.1): the closed normal subgroup of Γ_A generated by x₀, x₁ —
definitionally GQ2.wildCore (the admissible-limit proof), under the Subgroup GammaA spelling of this layer.
(normalClosure {gammaX0, gammaX1}-based unfoldings still hold by rfl;
see wildPart_eq_closure.)
Equations
Instances For
W_A is pro-2 — the pro-2 clause of eq. (7) holds in the limit. This is the admissible-limit proof's
isProP_wildCore (GQ2/AdmissibleLimit.lean), re-exported under the §3 name; it is the
input Prop. 3.2's Γ_A side needs for "W_A is the wild part".
Proposition 3.2 — the common tame quotient #
Paper: "There are canonical isomorphisms Γ_A/W_A ≅ T_tame ≅ G_{ℚ₂}/W_F, where W_F is
wild inertia." Split into the two sides; "canonical" is realized as (i) generator-pinning
on the Γ_A side and (ii) uniqueness-by-maximality of the wild subgroup on the local side
(the residual choice of local isomorphism is count-invisible downstream — design note §3.2).
Prop. 3.2, local side + Lemma 3.3's characterization, bundled. Extends the B10
bundle TameQuotientData (GQ2/TameQuotient.lean: W closed normal pro-2 with
G_{ℚ₂}/W ≅ T_tame — the paper's wild inertia, encoded intrinsically since Mathlib has no
ramification theory; deviation, flagged there) by Lemma 3.3's maximality, which pins
W uniquely (the "canonical" of Prop. 3.2 on the local side). Maximality is deliberately
not part of axiom B10 — it is the paper's own proved content.
W_Fis the maximal closed normal pro-2 subgroup — Lemma 3.3'sO₂(G_{ℚ₂}) = W_F.
Instances For
Equation (11) — the marked decomposition of B = D₀^{ab} #
Paper (9)–(11): B = D₀^{ab} = ⟨Ā, S̄, Ȳ | 2Ā + 4S̄ = 0⟩_{ℤ₂} = C₂·t ⊕ ℤ₂·S̄ ⊕ ℤ₂·Ȳ with
t = Ā + 2S̄. Bundled so that Lemmas 3.7/3.8 can be phrased against a fixed coordinate
system (house bundle style, cf. LocalReciprocity). In coordinates (t, S̄, Ȳ), note
Ā ↦ (1, −2, 0) (forced: Ā = t − 2S̄).
Equation (11), bundled: a continuous isomorphism B = D₀^{ab} ≅ ℤ/2 × ℤ₂ × ℤ₂
sending t̄ = A·S², S̄, Ȳ to the standard basis.
- e : topAbelianization ↑D0.toProfinite.toTop ≃ₜ* Multiplicative (ZMod 2 × ℤ_[2] × ℤ_[2])
The coordinate isomorphism
B ≅ C₂ ⊕ ℤ₂ ⊕ ℤ₂of (11). The torsion coordinate:
t = Ā + 2S̄ ↦ (1,0,0).S̄ ↦ (0,1,0).Ȳ ↦ (0,0,1).
Instances For
Universal property of D₀ (local replica of AnabelianBridge.d0Lift) #
AnabelianBridge.d0Lift is exactly this, but that file imports SectionThree, so we replicate
it here to build the coordinate homs τ, σ, γ out of D₀^ab.
Universal property of D₀: a triple in a pro-2 group satisfying the Demushkin relation
classifies a continuous hom D₀ → H.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Multiplicative (ZMod 2) is pro-2 (a finite 2-group).
A continuous hom from D₀ to an abelian group factors through D₀^{ab}.
Equations
- GQ2.SectionThree.abLift g = GQ2.quotientLift (commutator ↑GQ2.D0.toProfinite.toTop).topologicalClosure g ⋯
Instances For
Source-generic abLift: descend a continuous hom G → H (H abelian, T2) through abMk.
Equations
- GQ2.SectionThree.abLiftG g = GQ2.quotientLift (commutator G).topologicalClosure g ⋯
Instances For
The three coordinate homs σ (S-coord), γ (Y-coord), τ (t-coord) #
The S̄-coordinate hom σ : D₀^ab → ℤ₂, with Ā ↦ −2, S̄ ↦ 1, Ȳ ↦ 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Ȳ-coordinate hom γ : D₀^ab → ℤ₂, with Ā ↦ 0, S̄ ↦ 0, Ȳ ↦ 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The t̄-coordinate hom τ : D₀^ab → ZMod 2, with Ā ↦ 1, S̄ ↦ 0, Ȳ ↦ 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The combined coordinate hom φ = (τ, σ, γ) #
The combined coordinate map φ : D₀^ab → ZMod 2 × ℤ₂ × ℤ₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Coordinate computations on Ā^a S̄^s Ȳ^y #
φ is injective #
t̄ = Ā · S̄² is 2-torsion.
φ is surjective #
The ZMod 2 powering hits every class: (ofAdd 1)^(c.val) = ofAdd c.
Assembly #
The coordinate isomorphism φ : D₀^ab ≃ₜ* ZMod 2 × ℤ₂ × ℤ₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lemma 3.5 — marked abelianization, orientation, and initial form #
The (ν_ur, χ_D)-rows of eq. (13) and ā²s̄⁴ = 1 are proved in GQ2/Reciprocity.lean
(see the module docstring above). The three remaining clauses:
−4 ∈ ℚ₂ˣ — the class ā = rec(−4) of Lemma 3.5. (Public counterpart of the private
uNeg4 in GQ2/Reciprocity.lean.)
Equations
- GQ2.SectionThree.unitNeg4 = Units.mk0 (-4) GQ2.SectionThree.unitNeg4._proof_1
Instances For
−3 ∈ ℚ₂ˣ — the class ȳ = rec(−3) of Lemma 3.5.
Equations
- GQ2.SectionThree.unitNeg3 = Units.mk0 (-3) GQ2.SectionThree.unitNeg3._proof_1
Instances For
Marked-abelianization clause #
The descent markedPi, the marked hom markedHom
(Ā,S̄,Ȳ ↦ rec(−4), rec(1/2), rec(−3), relation verified), and the generator matching are
std-3. Bijectivity of markedHom — that the three reciprocity classes coordinatize
(G_ℚ₂(2))^ab — uses B5.
Arithmetic input for markedHom_bijective's surjectivity #
Finite-2-group Frattini (sq_generate), Hensel square roots (hensel_sq), and the square-class
generation of ℚ₂ˣ by {−4, 2, −3} (units_gen). None of these use the Galois-theoretic
section variables.
If every element of a finite 2-group Q is s·t² with s ∈ S, then S = ⊤. (Squares lie in
every index-2 subgroup, so a coatom M ≥ S would swallow all of Q.)
Hensel square roots: a 2-adic unit ≡ 1 (mod 8) is a square.
toZModPow 3 detects divisibility by 8 in ℤ₂.
-3 as a 2-adic unit.
Equations
Instances For
A norm-1 element of ℚ₂ˣ comes from a ℤ₂-unit.
Mod-8 square decomposition of ℤ₂ˣ: every 2-adic unit is s·w² with s ∈ {1,−1,−3,3}.
ℚ₂ˣ = ⟨−4, 2, −3⟩ · (ℚ₂ˣ)²: every unit of ℚ₂ is s·t² with s in the subgroup
generated by {−4, 2, −3}. (Valuation split x = 2ⁿ·u + mod-8 square classes of ℤ₂ˣ.)
Lemma 3.5, injectivity clause: the pair (ν_ur, χ_D) : B → ℤ₂ × ℤ₂ˣ is injective.
Stated intrinsically on B = D₀^{ab}: any continuous pair with the eq. (13) rows on the
marked generator classes separates points. (The rows pin ν, χ on a dense subgroup, hence
everywhere, so this is the paper's clause.) Proof the Lemmas 3.4–3.5 proof — from b_decomposition
plus v₂(η − 1) = 2 (η = (−3)⁻¹ topologically generates 1 + 4ℤ₂).
(G_ℚ₂(2))^ab is pro-2 (image of the pro-2 G_ℚ₂(2) under abMk).
The descent π : G_ℚ₂^ab → (G_ℚ₂(2))^ab of abMk ∘ maxProPMk through toAb. Abelian
target ⇒ all lifts of a class agree (markedPi_toAb).
Equations
- GQ2.SectionThree.markedPi = QuotientGroup.lift GQ2.commClosure (GQ2.SectionThree.abMk.comp (GQ2.maxProPMk 2 GQ2.AbsGalQ2).toMonoidHom) ⋯
Instances For
The marked hom D₀^ab → (G_ℚ₂(2))^ab, Ā,S̄,Ȳ ↦ rec(−4), rec(1/2), rec(−3). Well-defined:
rec(−4)²·rec(1/2)⁴ = rec((−4)²·2⁻⁴) = rec(1) = 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ν̃ : (G_ℚ₂(2))^ab → ℤ₂, the descent of the unramified coordinate ν_ur.
Equations
Instances For
χ̃ : (G_ℚ₂(2))^ab → ℤ₂ˣ, the descent of the cyclotomic character (via the max-pro-2 UP).
Equations
- GQ2.SectionThree.chiT x✝ = GQ2.SectionThree.abLiftG ((GQ2.maxProPHomEquiv GQ2.isProP_two_unitsPadicInt).symm { toMonoidHom := GQ2.chiCyc, continuous_toFun := GQ2.continuous_chiCyc })
Instances For
markedHom is injective — the two coordinate descents (ν̃, χ̃) compose with markedHom
to the six generator values of the already-proved lemma_3_5_injective.
markedHom is surjective — markedPi ∘ rec is dense, ℚ₂ˣ = ⟨−4,2,−3⟩·(ℚ₂ˣ)²
(units_gen), and a finite-2-group Frattini argument (sq_generate) makes the three rec-classes
generate every finite quotient of (G_ℚ₂(2))^ab; so their closed span is everything.
The marked abelianization is bijective (Lemma 3.5's last clause). Injective via the two
coordinate descents + lemma_3_5_injective; surjective via density of markedPi ∘ rec and the
square-class generation units_gen. Std-3 + B5 — no census cost (B5 as bundled suffices).
Lemma 3.5, marked-abelianization clause: the pro-2 abelianization of D = G_{ℚ₂}(2)
is identified with B = D₀^{ab} by Ā ↦ ā = rec(−4), S̄ ↦ s̄ = rec(2)⁻¹ = rec(1/2),
Ȳ ↦ ȳ = rec(−3). The rec-classes live in G^{ab} (R.recip); the matching is quantified
over lifts g ∈ G_{ℚ₂} (all lifts agree via markedPi, an abelian descent). The proof uses
markedHom_bijective and B5.
Lemma 3.5, Hilbert-symbol ledger (the "initial form" clause in symbol vocabulary):
on the square-class basis (−1, 2, −3) of Lemma 3.5, the dyadic Hilbert symbol takes the
values (−1,−1)₂ = −1, (2,−3)₂ = −1, and +1 on every other (unordered) pair. In the
dual basis (α, β, γ) of H¹(D, 𝔽₂) this is exactly the quadratic initial form
α² + βγ + γβ — the degree-two initial form of r₀ = A²S⁴[S,Y] (design note §3.5 for the
dictionary; the Kummer-cocycle cup reading enters at §6). The proof consists of six evaluations
of hilbertSymbol_dyadic.
Lemma 3.7 and Proposition 3.8 — lifting automorphisms of (B, χ₀) #
Phrased against a BDecomposition coordinate system. A continuous group isomorphism of
pro-2 abelian groups is automatically ℤ₂-linear, so the coordinate transcriptions below
are exactly the paper's ℤ₂-module statements (design note §3.7–3.8).
Proposition 1.1 — the marked dyadic Demushkin normalization #
Paper: "There exist topological generators a, s, y of D = G_{ℚ₂}(2) with
D ≅ ⟨a,s,y | a²s⁴[s,y] = 1⟩_{pro-2} and ν_ur(a,s,y) = (−2,1,0)." The generators-plus-
presentation clause is packaged as a continuous isomorphism e : G_{ℚ₂}(2) ≅ D₀ (then
a = e⁻¹(A), s = e⁻¹(S), y = e⁻¹(Y) topologically generate and satisfy the relation, by
transport of d0_relation); the ν_ur-row is read through arbitrary lifts to G_{ℚ₂}, as
in the orientation interface full-group readings (chiCyc_eq_neg_one_of_lift_A).
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- eq. (13) = ⟦eq-localmarkingorientation⟧
- eq. (7) = ⟦eq-candidateinverse⟧
- Lemma 3.1 = ⟦lem-tamefinite⟧
- Lemma 3.3 = ⟦lem-o2tame⟧
- Lemma 3.4 = ⟦lem-standardorientation⟧
- Lemma 3.5 = ⟦lem-markedinitialform⟧
- Lemma 3.6 = ⟦lem-peripheralpower⟧ (= lemma 3.7 in current tex)
- Lemma 3.7 = ⟦lem-squarerootHNN⟧ (= lemma 3.8 in current tex)
- Proposition 1.1 = ⟦prop-markedDem⟧
- Prop 3.2 = ⟦prop-tamequotient⟧
- Prop 3.8 = ⟦prop-orientationlift⟧ (= proposition 3.9 in current tex)