The Kummer depth filtration on H¹(G_k, 𝔽₂)

The image of the unit filtration U^{(j)}(k) (GQ2/UnitFiltration.lean) under the Kummer class map, as a decreasing chain of additive subgroups of H¹(G_k, 𝔽₂) — the filtration whose graded Hom-counts (the deep-part proof's engine) produce DeepKummerData.card_fam/card_deepFam for the Lemma-6.17 dimension clause.

• kummerDepth k π j — classes kummerClassK k a of depth-j units; an AddSubgroup by the banked Kummer-class algebra (kummerClassK_mul/_one, 2-torsion of H¹);
• kummerDepth_antitone — decreasing in j;
• kummerDepth_eq_bot — the filtration dies at j = 2e + 1 (U^{(2e+1)} ⊆ (k^×)² — the Local Square Theorem sq_of_near_one + kummerClassK_sq), the endpoint for the the deep-part proof iteration;
• kummerClassK_mem_deepClasses / coe_kummerDepth_deep — stage e + 1 is the deep classes: (kummerDepth k π (e+1) : Set _) = LocalKummer.deepClasses k.fixingSubgroup. (In particular deepClasses is an additive subgroup — the form the Lemma 6.17 vanishing proof's orbit analysis and the card_deepFam count consume.)

The B13 inputs — the uniformizer π ∈ k, ‖2‖ = ‖π‖^e, ‖π‖ < 1, and value-group discreteness hπ_max — enter only as hypotheses (the consumer pulls them from the GQ2.dyadicUnitFiltration bundle), so this file is axiom-free.

def GQ2.kummerDepth (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (π : AlgebraicClosure ℚ_[2]) (j : ℕ) : AddSubgroup (ContCoh.H1 (↥k.fixingSubgroup) (ZMod 2))

The depth-j Kummer classes: images under kummerClassK of the depth-j units U^{(j)}(k). An additive subgroup by the Kummer-class algebra ([ab] = [a] + [b], [1] = 0, and H¹(G_k, 𝔽₂) is 2-torsion so negation is the identity).

Equations

• GQ2.kummerDepth k π j = { carrier := {ξ : GQ2.ContCoh.H1 (↥k.fixingSubgroup) (ZMod 2) | ∃ a ∈ GQ2.depthUnits k π j, GQ2.kummerClassK k a = ξ}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem GQ2.mem_kummerDepth_iff (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (π : AlgebraicClosure ℚ_[2]) {j : ℕ} {ξ : ContCoh.H1 (↥k.fixingSubgroup) (ZMod 2)} : ξ ∈ kummerDepth k π j ↔ ∃ a ∈ depthUnits k π j, kummerClassK k a = ξ

Membership in kummerDepth unfolded.

theorem GQ2.kummerDepth_antitone (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (π : AlgebraicClosure ℚ_[2]) (hπ1 : ‖π‖ ≤ 1) {i j : ℕ} (hij : i ≤ j) : kummerDepth k π j ≤ kummerDepth k π i

The Kummer depth filtration is decreasing.

theorem GQ2.kummerClassK_eq_zero_of_sq (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (a : (↥k)ˣ) (w : ↥k) (hw : w ^ 2 = ↑a) : kummerClassK k a = 0

Squares have trivial Kummer class (unit-of-a-square form): if (a : ↥k) = w ^ 2 then [a] = 0 — package the root as a unit and apply kummerClassK_mul_self-style algebra.

theorem GQ2.kummerDepth_eq_bot (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (π : AlgebraicClosure ℚ_[2]) [FiniteDimensional ℚ_[2] ↥k] (hπ0 : π ≠ 0) (hπ1 : ‖π‖ < 1) {e : ℕ} (he : ‖2‖ = ‖π‖ ^ e) {j : ℕ} (hj : 2 * e + 1 ≤ j) : kummerDepth k π j = ⊥

The filtration endpoint (U^{(2e+1)} ⊆ (k^×)², the Local Square Theorem): past depth 2e every Kummer class dies. The the deep-part proof iteration terminates here (card_equivHoms_of_subsingleton).

theorem GQ2.kummerClassK_mem_deepClasses (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (a : (↥k)ˣ) (ha : ‖↑↑a - 1‖ < ‖2‖) : kummerClassK k a ∈ LocalKummer.deepClasses k.fixingSubgroup

Deep units give deep classes (the converse of LocalKummer.deepClass_eq_kummerClassK): the Kummer class of a unit with ‖a − 1‖ < ‖2‖ lies in deepClasses. Witnesses: A := a, β := sqrtCl A, b := (A − 1)/2.

theorem GQ2.coe_kummerDepth_deep (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (π : AlgebraicClosure ℚ_[2]) [FiniteDimensional ℚ_[2] ↥k] (hπk : π ∈ k) (hπ0 : π ≠ 0) (hπ1 : ‖π‖ < 1) (hπmax : ∀ x ∈ k, ‖x‖ < 1 → ‖x‖ ≤ ‖π‖) {e : ℕ} (he_pos : 1 ≤ e) (he : ‖2‖ = ‖π‖ ^ e) : ↑(kummerDepth k π (e + 1)) = LocalKummer.deepClasses k.fixingSubgroup

Stage e + 1 of the Kummer depth filtration is exactly the deep classes — given the B13 bundle data (uniformizer π ∈ k, discreteness hπ_max, ‖2‖ = ‖π‖^e). Forward: ‖a − 1‖ ≤ ‖π‖^{e+1} < ‖π‖^e = ‖2‖ is deep; backward: a deep class is kummerClassK of a unit with ‖a − 1‖ < ‖2‖ (deepClass_eq_kummerClassK), and discreteness upgrades the strict bound to ≤ ‖π‖^{e+1}. In particular deepClasses is an additive subgroup.