Local Kummer theory for the deep half #
Infrastructure for SectionSix.lemma_6_17_dim — the deep-half dimension count
#X₊² = #H¹(ℚ₂, V) for ramified V — via the paper's filtration route (Route B of
docs/orchestration/p15f1-scoping.md): under the Kummer identification
H¹(ℚ₂, V) ≅ Hom_{H_V}(V^∨, M_K) (M_K = K^×/K^{×2}, K the tame splitting field),
the multiplicity d j of V^∨ at filtration depth j satisfies d j = d (2e − j)
(graded duality, self-duality of V through the invariant form q) and d e = 0
(Lemma 6.10, middle layer unramified), so the deep tail Σ_{j>e} d j is exactly half the
total — no H¹-pairing is involved.
Layers #
- Layer 1 (this file, bottom): the counting core — pure
Finsetarithmetic turning the four count facts (htotal,hdeep,hpair,hmid) into thelemma_6_17_dimgoal. Std-3, no axioms, no design risk. - Layer 2 (below): the
DeepKummerDatabundle records the filtration multiplicities, inflation and extension inputs, graded self-duality, middle vanishing, and the two family counts. The resulting dimension theorem is parametric in this data; downstream modules construct the required inputs from the proved Kummer and duality interfaces.
Layer 1: the halving arithmetic #
Duality-paired sums halve. If the multiplicities d on depths 0, …, 2e satisfy
the duality symmetry d j = d (2e − j) and the middle multiplicity vanishes, then the total
is twice the deep tail Σ_{e < j ≤ 2e} d j. (The tail is indexed as Ico (e+1) (2e+1).)
Layer 2a: the scalar restriction map and the deep classes #
The identification H¹(ℚ₂, V) ≅ Hom_{H_V}(V^∨, M_K) is built from the scalar restriction
map phiRes ρ x φ = [n ↦ φ((Quotient.out x) n)] ∈ H¹(N, 𝔽₂), N = ker ρ. Everything is
stated ambiently over G_ℚ₂: no G/N-quotient types and no K^×/K^{×2}-carrier appear.
H¹(N, 𝔽₂) itself plays the role of M_K (the L1 Kummer leaf will identify them), the
H_V-equivariance conditions are phrased through conjugation inside G_ℚ₂, and the two
cohomological inputs produced later from Lemma 6.11 projectivity (InflationVanishes,
extension of equivariant homs) are plain ambient statements about cocycles.
Since the N-action on both V (as N = ker ρ) and 𝔽₂ is trivial, B¹ vanishes on both
sides of the restriction: H¹(N, 𝔽₂)-classes are just continuous homs (h1ofFun_eq_zero_iff)
and restriction is representative-independent at the raw-cocycle level (phiRes_of_rep).
𝔽₂-functionals separate points on an elementary finite 2-group. (Local copy of
GQ2.FoxH.elemDual_separates from GQ2/Devissage.lean, duplicated to keep this file's build
decoupled from the FoxHeisenberg import chain — a the Prop. 5.15 proof hot file.)
Over a subgroup N ≤ G_ℚ₂ the coefficient action on 𝔽₂ is trivial, so B¹(N, 𝔽₂) = 0:
a raw cocycle's class vanishes iff the cocycle is the zero function. (N is bound as
Subgroup AbsGalQ2 — the phiRes-side instance flavor — so that rw matches at use
sites; the defeq Kummer.GaloisGroup ℚ_[2]-flavor of deepClasses casts at use sites.)
The scalar restriction map Θ: the φ-coordinate of the restriction of a class
x ∈ H¹(ℚ₂, V) to N = ker ρ — the class of n ↦ φ((Quotient.out x) n) in H¹(N, 𝔽₂).
deepPart ρ is definitionally {x | ∀ φ, phiRes ρ x φ ∈ deepClasses} (mem_deepPart_iff).
Equations
- GQ2.LocalKummer.phiRes ρ x φ = GQ2.H1ofFun ↥ρ.ker fun (n : ↥ρ.ker) => φ (↑(Quotient.out x) ↑n)
Instances For
Unfolding rule for phiRes (a rw-safe alternative to unfold, which delta-exposes the
H1-quotient in type arguments).
Representative independence of the scalar restriction: any Z¹-representative of x
computes phiRes ρ x φ (representatives differ by a coboundary, and coboundaries vanish
pointwise on ker ρ).
phiRes is additive in the class.
phiRes is additive in the functional.
The deep classes in H¹(N, 𝔽₂) and the deepPart bridge #
The deep Kummer classes in H¹(N, 𝔽₂): classes of restricted Kummer cocycles of deep
units (the image of U_{e+1}(K) ⊂ K^×/K^{×2} under the Kummer identification, stated without
the identification). deepPart ρ is exactly the set of classes all of whose scalar
restrictions land here (mem_deepPart_iff).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The deepPart bridge (P4, definitional half): membership in the deep half is exactly
"every scalar restriction is a deep Kummer class".
Depth-to-norm bridge: a deep unit (the IsDeepUnit idiom A = 1 + 2b, ‖b‖ < 1)
satisfies the ‖A − 1‖ < ‖2‖ hypothesis shape of the Tier-5 eq.-(94) orthogonality leaves
(GQ2.normForm_of_deep / GQ2.cup_deep_* in GQ2/HilbertLedger.lean) — the consumer-side
glue for discharging f1's isotropy hiso and f2's orbit vanishing once the monomial
expansion lands.
Bridge deepClasses → kummerClassK: over a finite intermediate field k, a deep
Kummer class in H¹(G_k, 𝔽₂) is the Kummer class of a genuine deep unit a ∈ kˣ
(‖a − 1‖ < ‖2‖, i.e. a ∈ U_{e+1}(k)). The k.fixingSubgroup-fixed deep unit A lands in
k by the Galois correspondence (InfiniteGalois.fixedField_fixingSubgroup); its Kummer
cocycle matches kummerClassK's canonical-root cocycle up to a sign (kummerCocycleFun_neg).
This is the consumer glue turning the Tier-5 (94) orthogonality (GQ2.cup_deep_deep, over
kummerClassK) into the deepClasses-vocabulary orthogonality the monomial expansion needs.
Eq.-(94) orthogonality in deepClasses vocabulary (the shared f1-isotropy /
f2-orbit-vanishing leaf, over a finite intermediate field k): two deep Kummer classes in
H¹(G_k, 𝔽₂) cup to zero. Bridges deepClasses to the Tier-5 GQ2.cup_deep_deep via
deepClass_eq_kummerClassK. std-3 ∪ {B11a}.
Injectivity of the scalar restriction from the inflation input #
The ambient inflation-vanishing input (to be produced from Lemma 6.11 projectivity
via H¹(H_V, V) = 0, stated with no G/N-quotient types): every continuous cocycle that
vanishes pointwise on N = ker ρ is a coboundary. A cocycle vanishing on N factors
through G/N ≅ H_V, so this is precisely inflation-H¹-vanishing.
Equations
- GQ2.LocalKummer.InflationVanishes ρ = ∀ (b : ↥(GQ2.ContCoh.Z1 GQ2.AbsGalQ2 V)), (∀ (n : ↥ρ.ker), ↑b ↑n = 0) → ∃ (w₀ : V), ∀ (g : GQ2.AbsGalQ2), ↑b g = g • w₀ - w₀
Instances For
All scalar restrictions of x vanish iff the canonical representative vanishes pointwise
on N = ker ρ (functionals separate points; B¹(N, 𝔽₂) = 0).
Injectivity of the scalar restriction package from the inflation input: two classes
with equal scalar restrictions are equal. (With InflationVanishes discharged by Lemma 6.11
projectivity, this is the injectivity half of H¹(ℚ₂,V) ≅ Hom_{H_V}(V^∨, M_K).)
Discharging InflationVanishes — the coprime-averaging proof #
InflationVanishes (= H¹(H_V, V) = 0 content) is not a projectivity fact: the paper
proves it (proof of (78), p. 25) by coprime-order averaging over the odd tame inertia
I ◁ H_V plus V^I = 0. The argument here is Hochschild–Serre-free: a cocycle b vanishing
on N = ker ρ (whose kernel acts trivially on V, hρ) descends to a cocycle
b̄ : C → V on the finite image C; averaging over I (odd order ⟹ |I|·x = x in the
2-torsion V) makes b̄ cohomologous to a cocycle killed on I; and the two-way evaluation
b̄(ic) = b̄(c·(c⁻¹ic)) forces the residue into V^I = 0.
Stated parametrically over (I, |I| odd, V^I = 0) — the tame-arithmetic verification of
those (odd inertia, ramified-simple fixed-point-freeness) is supplied at the DeepKummerData
instantiation.
The image of tame inertia has odd order. For any hom c : T_tame →* C into a finite
group, orderOf (c τ) is odd: applying c to the tame relation τ^σ = τ² shows c τ is
conjugate to (c τ)², so orderOf (c τ) = orderOf ((c τ)²) = orderOf (c τ) / gcd(·, 2), which
forces the order odd. Supplies Odd (Nat.card ↥⟨c τ⟩) for the inertia subgroup at the
inflationVanishes_of_oddNormal instantiation.
The image of tame inertia is normal. If c : T_tame →* C (into a finite group) has
c σ, c τ generating C, then ⟨c τ⟩ = zpowers(c τ) is normal: conjugation by c σ sends
c τ to (c τ)² (the tame relation), and zpowers((c τ)²) = zpowers(c τ) since c τ has odd
order — so c σ and c τ both normalize zpowers(c τ), hence so does all of C. Supplies
the I.Normal hypothesis of inflationVanishes_of_oddNormal. (The generation hypothesis
hgen is the profinite fact im c = closure{c σ, c τ}, discharged at instantiation from the
surjectivity of the classifying map.)
The I-fixed submodule vanishes (V^I = 0) for a normal subgroup I ◁ C acting
nontrivially on the simple module V: V^I is a C-submodule (by normality), and it is not
all of V (some i ∈ I moves some vector), so simplicity forces V^I = ⊥. This produces
the hVI hypothesis of inflationVanishes_of_oddNormal for a ramified simple module.
InflationVanishes from an odd normal subgroup with no fixed vectors (the
coprime-averaging discharge, parametric): if ρ : G_ℚ₂ ↠ C with C acting on the 2-torsion
V through ρ, and C has a normal subgroup I of odd order with V^I = 0, then every
cocycle vanishing on ker ρ is a coboundary.
InflationVanishes for a ramified simple tame module — the four-brick assembly.
Takes the classifying data ρ (surjective) with lower map c : T_tame →* C, the ramified
simple hypotheses, and the tame-generation fact hgen; discharges InflationVanishes by
instantiating inflationVanishes_of_oddNormal at the inertia subgroup I = ⟨c τ⟩, whose three
hypotheses are supplied by tameInertia_normal (normal), odd_orderOf_tameInertia (odd order),
and fixedByNormal_eq_bot (V^I = 0, from hram). The only inputs beyond lemma_6_17_dim's
own are the two profinite facts hsurj (im ρ = C) and hgen (C = ⟨c σ, c τ⟩).
Conjugation equivariance and the admissible-family identification #
The H_V-module structure on H¹(N, 𝔽₂) is the conjugation action, defined ambiently for
every g : G_ℚ₂ (it factors through G/N since inner-N conjugation composed with the
trivial coefficient action is homotopic to the identity — not needed here). A scalar
restriction family φ ↦ phiRes ρ x φ is additive and conjugation-equivariant
(phiRes_conj, from the cocycle identity b(g⁻¹ng) = g⁻¹ • b(n) on N = ker ρ); the
extension input (to be produced from Lemma 6.11 projectivity via H²(H_V, V) = 0)
asserts every such family arises. Together with phiRes_injective this identifies
H¹(ℚ₂, V) with the admissible families, carrying deepPart onto the families valued in
deepClasses — the counting interface consumed by the Layer-2b filtration bundle.
Conjugation carries N = ker ρ into itself.
The conjugation self-map of N = ker ρ, n ↦ g⁻¹ n g, as a continuous map.
Equations
- GQ2.LocalKummer.conjMap ρ g n = ⟨g⁻¹ * ↑n * g, ⋯⟩
Instances For
Conjugation-precomposition preserves Z¹(N, 𝔽₂) (the coefficient action is trivial, so
cocycles are continuous homs and conjugation is a continuous endomorphism).
The conjugation action of g ∈ G_ℚ₂ on H¹(N, 𝔽₂), [f] ↦ [n ↦ f(g⁻¹ n g)].
Equations
- GQ2.LocalKummer.conjAct ρ g ξ = GQ2.H1ofFun ↥ρ.ker fun (n : ↥ρ.ker) => ↑(Quotient.out ξ) (GQ2.LocalKummer.conjMap ρ g n)
Instances For
Computation rule for conjAct on the class of an explicit cocycle.
conjAct is additive.
conjAct is a left action (contravariant conjMap composition): conjAct (g·h)
= conjAct g ∘ conjAct h.
Inner conjugation is trivial on H¹(N): for m ∈ N, conjAct ρ m = id (the cocycle
is a hom on N, so f(m⁻¹ n m) = f n in characteristic 2).
conjAct depends only on ρ g: two elements with the same image act identically
(their ratio lies in N, and inner conjugation is trivial).
The C-module (H_V-module) structure on H¹(N, 𝔽₂) via conjugation: c • ξ is the
G_ℚ₂-conjugation conjAct ρ g ξ for any lift g of c (well-defined by conjAct_ker, as
conjugation descends through ρ). The action axioms are the conjAct algebra. Provided as a
def (not a global instance); consumers letI it — ρ is surjective in the ramified §6.3
setup (hc : Surjective c + B.tameF_surjective). This is the acting-group structure that
identifies AdmissibleFam with the equivariant Homs equivHoms C V^∨ (H¹(N, 𝔽₂)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conjugation identity for cocycles on the kernel: for a cocycle b and
n ∈ N = ker ρ (so that conjugates of n act trivially on V),
b(g⁻¹ n g) = g⁻¹ • b(n).
Equivariance of the scalar restriction family:
g · (phiRes x φ) = phiRes x (φ ∘ (g⁻¹ • ·)).
The admissible families and the counting identification #
An admissible family: an additive, conjugation-equivariant assignment of
H¹(N, 𝔽₂)-classes to 𝔽₂-functionals on V — the ambient encoding of
Hom_{H_V}(V^∨, M_K) (under the L1 Kummer leaf, H¹(N, 𝔽₂) ≅ M_K).
- fam : (V →+ ZMod 2) → ContCoh.H1 (↥ρ.ker) (ZMod 2)
The underlying assignment
V^∨ → H¹(N, 𝔽₂). Additivity in the functional.
- equiv' (g : AbsGalQ2) (φ : V →+ ZMod 2) : conjAct ρ g (self.fam φ) = self.fam (φ.comp (DistribSMul.toAddMonoidHom V g⁻¹))
Conjugation equivariance.
Instances For
The scalar restriction family of a class, as an AdmissibleFam.
Equations
- GQ2.LocalKummer.toFam ρ hρ x = { fam := GQ2.LocalKummer.phiRes ρ x, add' := ⋯, equiv' := ⋯ }
Instances For
The extension input (to be produced from Lemma 6.11 projectivity via
H²(H_V, V) = 0; ambient statement, no G/N-quotients): every admissible family is the
scalar restriction family of some class.
Equations
- GQ2.LocalKummer.FamiliesExtend ρ = ∀ (ξ : GQ2.LocalKummer.AdmissibleFam ρ), ∃ (x : GQ2.ContCoh.H1 GQ2.AbsGalQ2 V), ∀ (φ : V →+ ZMod 2), GQ2.LocalKummer.phiRes ρ x φ = ξ.fam φ
Instances For
The identification: given the two deferred cohomological inputs, toFam is an
equivalence H¹(ℚ₂, V) ≃ AdmissibleFam.
Equations
- GQ2.LocalKummer.h1EquivFam hρ hV2 hinf hext = Equiv.ofBijective (GQ2.LocalKummer.toFam ρ hρ) ⋯
Instances For
Count H¹ by families (modulo the deferred inputs).
Count the deep half by deep-valued families (modulo the deferred inputs): the
identification carries X₊ onto the admissible families valued in the deep classes.
Layer 2b: the DeepKummerData bundle and the parametric dimension theorem #
Following the B6/TateDuality pattern, DeepKummerData bundles exactly the paper-content and
literature-leaf outputs that the filtration count produces, so that lemma_6_17_dim is proved
parametrically over it (std-3) and only the instantiation remains. Its fields:
- the filtration depth bound
e(= v_K(2)) and theV^∨-isotypic multiplicitiesd j; - the two deferred cohomological inputs
hinf/hext(theH¹/H²(H_V, V) vanishing that Lemma 6.11 projectivity supplies); - the self-duality symmetry
hpair(d j = d (2e−j), fromV ≅ V^∨through the invariant formq+ graded Hilbert duality) and the middle vanishinghmid(d e = 0, Lemma 6.10 + ramifiedness); and - the two family counts (
#{admissible families} = 2^{Σ_{j≤2e} d j}and#{deep families} = 2^{Σ_{j>e} d j}, the exact-Hom_{H_V}(V^∨, −)computation over the unit filtration ofM_K).
None of these fields is declared as an axiom; the theorem below is parametric in the bundled mathematical inputs.
The bundled local-Kummer count data for a ramified simple module, from which the deep-half
dimension clause follows parametrically (Route B of docs/orchestration/p15f1-scoping.md).
- e : ℕ
The filtration depth bound
e = v_K(2). - d : ℕ → ℕ
The
V^∨-isotypic multiplicity ofM_Kat depthj. - hinf : InflationVanishes ρ
Inflation vanishing (
H¹(H_V, V) = 0from Lemma 6.11 projectivity). - hext : FamiliesExtend ρ
Extension surjectivity (
H²(H_V, V) = 0from Lemma 6.11 projectivity). Graded self-duality:
V ≅ V^∨(via the invariant formq) plus Hilbert duality of the depth-jand depth-(2e−j)graded pieces give equal multiplicities.Middle vanishing (Lemma 6.10): the unpaired middle depth
j = ecarries no ramified copy ofV.- card_fam : Nat.card (AdmissibleFam ρ) = 2 ^ (Finset.range (2 * self.e + 1)).sum self.d
Total count:
#{admissible families} = 2^{Σ_{j ≤ 2e} d j}(exactHom_{H_V}(V^∨, −)over the full unit filtration ofM_K). - card_deepFam : Nat.card { ξ : AdmissibleFam ρ // ∀ (φ : V →+ ZMod 2), ξ.fam φ ∈ deepClasses ρ.ker } = 2 ^ (Finset.Ico (self.e + 1) (2 * self.e + 1)).sum self.d
Deep count:
#{deep families} = 2^{Σ_{e < j ≤ 2e} d j}(the same computation over the deep tailU_{e+1}).
Instances For
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- Lemma 6.10 = ⟦lem-middlelayer⟧
- Lemma 6.11 = ⟦lem-faithfulprojective⟧