B13-1 + B13-2 — the topology layer and the uniformizer #
This file proves the B13-1 + B13-2 components of dyadicUnitFiltration.
B13-1 (topology). The compact unit ball O = {‖x‖ ≤ 1} of a finite extension k/ℚ₂ (a
bundled OpenAddSubgroup off IsUltrametricDist.closedBall_openAddSubgroup), the finite quotient
O/2O (dyadicIndex k := #(O/2O)), and the uniformizer pigeonhole exists_pow_sub_dyadic:
among x⁰, …, x^M two are congruent mod the radius-‖2‖ ball.
B13-2 (uniformizer). norm_two_lt_one (‖2‖ < 1, via the spectral norm extending the base
2-adic norm — 2 is a non-unit); the gap lemma uniform_gap (‖x‖^M ≤ ‖2‖ for ‖x‖ < 1, by
factoring xⁱ(1 − xʲ⁻ⁱ)); the uniformizer exists_uniformizer (a norm-maximal π with
‖π‖ < 1, attained on the compact ball {‖y‖^M ≤ ‖2‖} via IsCompact.exists_isMaxOn); the
ramification index exists_ramificationIndex (‖2‖ = ‖π‖^e exactly, e ≥ 1, via
Nat.find + the 2/π^e-unit argument); and their package exists_uniformizer_data in the
ℚ̄₂-vocabulary the DyadicUnitFiltration structure consumes.
The residue field O/𝔪 and the graded counts are B13-3/B13-4 (UnitFiltrationCounts.lean).
‖2‖ < 1 in ℚ̄₂: the spectral norm extends the 2-adic norm on the base, and ‖2‖ = 2⁻¹
there — 2 is a non-unit. The whole uniformizer theory rests on this.
The closed unit ball O = {x ∈ k : ‖x‖ ≤ 1} of k, as a bundled open additive subgroup
(the ball is clopen in the ultrametric topology).
Equations
- GQ2.unitBall k = IsUltrametricDist.closedBall_openAddSubgroup (↥k) GQ2.unitBall._proof_3
Instances For
The radius-‖2‖ ball 2O = {x ∈ k : ‖x‖ ≤ ‖2‖}, as a bundled open additive subgroup.
Equations
- GQ2.dyadicBall k = IsUltrametricDist.closedBall_openAddSubgroup (↥k) GQ2.dyadicBall._proof_2
Instances For
The ℚ₂-value ‖(2 : ↥k)‖ is ‖(2 : ℚ̄₂)‖ (the norm on ↥k restricts ℚ̄₂'s).
Powers of a norm-≤ 1 element stay in the unit ball.
The ramification index e with ‖2‖ = ‖π‖^e for any uniformizer-like π (norm < 1,
norm-maximal below 1, with ‖2‖ ≤ ‖π‖). e is least with ‖π‖^{e+1} < ‖2‖; the exactness
‖2‖ = ‖π‖^e comes from applying the max property to 2/π^e. (Norm algebra only — no
finite-dimensionality needed.)
The unit ball is compact: a closed ball in the proper space ↥k (finite-dimensional over the
locally compact ℚ₂).
The quotient O/2O is finite: 2O is an open subgroup of the compact group O.
The index M = #(O/2O) — the length of the pigeonhole and the exponent of the value-group
gap.
Equations
- GQ2.dyadicIndex k = Nat.card (↥↑(GQ2.unitBall k) ⧸ (↑(GQ2.dyadicBall k)).addSubgroupOf ↑(GQ2.unitBall k))
Instances For
The uniformizer pigeonhole. For ‖x‖ ≤ 1, two of the powers x⁰, …, x^M
(M = dyadicIndex)
are congruent modulo the radius-‖2‖ ball: ‖xⁱ − xʲ‖ ≤ ‖2‖ with i < j ≤ M.
The value-group gap (B13-2): for ‖x‖ < 1, ‖x‖^M ≤ ‖2‖ (M = dyadicIndex). Factor the
pigeonhole difference xⁱ − xʲ = xⁱ(1 − xʲ⁻ⁱ): ‖1 − xʲ⁻ⁱ‖ = 1 (ultrametric, ‖x‖ < 1), so
‖x‖ⁱ ≤ ‖2‖, and ‖x‖^M ≤ ‖x‖ⁱ since i ≤ M.
The uniformizer (B13-2): a nonzero π with ‖π‖ < 1 that is norm-maximal below 1.
Attained as the norm-maximizer on the compact ball {‖y‖^M ≤ ‖2‖} (which, by uniform_gap,
contains every element of norm < 1).
The uniformizer + ramification data (B13-2's result for the B13-5 capstone), in the
ℚ̄₂-vocabulary of the DyadicUnitFiltration structure: a π ∈ k, π ≠ 0, ‖π‖ < 1,
norm-maximal below 1, together with e ≥ 1 and ‖2‖ = ‖π‖^e.