Kummer-depth filtration comparisons #
The Kummer kernel, square-depth parity, graded squaring, and class-graded comparison.
See GQ2.DeepCount for the paper-facing overview, source citations, and deviations.
The Kummer kernel (converse of kummerClassK_eq_zero_of_sq): a unit of k with
vanishing Kummer class is a square in k. B¹(G_k, 𝔽₂) = 0 because the coefficient action
is trivial (δ⁰m = g•m − m = 0), so class-zero forces the COCYCLE to vanish pointwise:
G_k fixes sqrtCl a, hence sqrtCl a ∈ ℚ̄₂^{G_k} = k by the Galois correspondence.
Mid units give mid classes — the ≤-mirror of kummerClassK_mem_deepClasses.
Witnesses: A := a, β := sqrtCl A, b := (A − 1)/2.
Stage e of the Kummer depth filtration is exactly the mid classes — the ≤-mirror
of coe_kummerDepth_deep. Forward: ‖a − 1‖ ≤ ‖π‖^e = ‖2‖ is mid; backward: a mid class is
kummerClassK of a unit with ‖a − 1‖ ≤ ‖2‖ (midClass_eq_kummerClassK), and mid IS
depth-e on the nose (no discreteness upgrade).
The square-depth parity core #
w² − 1 = (w − 1)(w + 1) with w + 1 = (w − 1) + 2: by the ultrametric, either
‖w − 1‖ > ‖2‖ and ‖w² − 1‖ = ‖w − 1‖² (an EVEN π-power), or ‖w² − 1‖ ≤ ‖4‖
(past depth 2e). Consequence: no square sits at an odd depth < 2e — the injectivity
half of the odd-level class-gr fullness.
The discreteness step-down (extracted from coe_kummerDepth_deep): a k-rational
element strictly below depth i is at depth i + 1.
The square-depth dichotomy: ‖w² − 1‖ = ‖w − 1‖² or ‖w² − 1‖ ≤ ‖4‖.
No square at an odd depth < 2e: if w² is within ‖π‖^j of 1 for ODD
j ≤ 2e − 1, it is within ‖π‖^{j+1} (the depth skips the odd level). Even case of the
dichotomy: an even power cannot land at exactly an odd level (discreteness step-down on
w − 1); ≤ ‖4‖-case: ‖4‖ = ‖π‖^{2e} ≤ ‖π‖^{j+1}.
The graded squaring U_i/U_{i+1} → U_{2i}/U_{2i+1} and the even-level collapse #
Squaring doubles depth for i ≤ e (w² − 1 = (w−1)(w+1), ‖w+1‖ ≤ max(‖w−1‖, ‖2‖)).
The induced map of graded pieces is INJECTIVE for i < e (the square-parity dichotomy +
discreteness), and both grs have 2^f elements (B13 card_gr), so it is SURJECTIVE — every
even-depth unit is a square times something deeper. Consequence
(kummerDepth_even_collapse): the class-level filtration COLLAPSES at even levels
0 < 2i < 2e.
The strengthened square-depth dichotomy, retaining the base-side bound in the degenerate
branch: either ‖w − 1‖ ≤ ‖2‖ (the unit is mid-or-deeper) or ‖w² − 1‖ = ‖w − 1‖².
Squaring doubles depth: u ∈ U_i ⟹ u² ∈ U_{2i} for i ≤ e.
Squaring sends U_{i+1} into U_{2i+1} (i ≤ e) — the well-definedness of the
graded squaring.
A unit whose square is one level deeper than double is itself one level deeper
(i + 1 ≤ e): the kernel-triviality core of the graded squaring, via the strengthened
dichotomy + the discreteness step-down.
The squaring homomorphism U_i →* U_{2i} on the subtype groups (i ≤ e).
Equations
- GQ2.sqHom k π hπle he hie = { toFun := fun (u : ↥(GQ2.depthUnits k π i)) => ⟨↑u ^ 2, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The graded squaring U_i/U_{i+1} →* U_{2i}/U_{2i+1} (i ≤ e).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Injectivity of the graded squaring for i + 1 ≤ e.
Surjectivity of the graded squaring for 1 ≤ i, i + 1 ≤ e: injective + both grs
have 2^f elements (B13 card_gr, passed as hypotheses).
The even-level collapse (0 < 2i < 2e): the class-level Kummer filtration does not
move at even levels — every even-depth unit is a square times a one-deeper unit, and squares
have trivial class.
The class-graded comparison map and the odd-level count #
classGrMap : U_j/U_{j+1} → Dc_j/Dc_{j+1}, [u] ↦ [[u]] — always surjective (depth-j
classes are classes of depth-j units by definition), and INJECTIVE at odd j < 2e:
a unit whose class drops a level is b·w² with b one deeper and w² a square in U_j
(the Kummer kernel), and squares skip odd levels (norm_sq_sub_one_le_succ_of_odd), so the
unit itself is one deeper. Consequences: #(Dc_j/Dc_{j+1}) ≤ 2^f always, = 2^f at odd
j < 2e, and = 1 at even 0 < j < 2e (increment 2's collapse).
The comparison map from the unit-graded piece to the class-graded piece.
Equations
- GQ2.classGrMap k π j q = Quotient.liftOn' q (fun (u : ↥(GQ2.depthUnits k π j)) => ↑⟨GQ2.kummerClassK k ↑u, ⋯⟩) ⋯
Instances For
Computation rule (definitional).
classGrMap is surjective (depth-j classes are classes of depth-j units).
classGrMap is injective at odd j ≤ 2e − 1 — the odd-level fullness core.
The odd-level class-gr count: #(Dc_j/Dc_{j+1}) = 2^f at odd j ≤ 2e − 1
(the comparison map is bijective).
The even-level class-gr count: #(Dc_{2i}/Dc_{2i+1}) = 1 for 0 < 2i < 2e
(increment 2's collapse makes the quotient a subsingleton).