The structural deep-count theorem

The final assembly of the arithmetic, filtration, and duality inputs.

See GQ2.DeepCount for the paper-facing overview, source citations, and deviations.

The finale: hduality

The instantiation of the abstract engine card_equivHoms_deep_eq_quot at M := H¹(ker ρ, 𝔽₂) (conjModule), U := V^∨ (dualModule), Deep := deepClassesSubgroup, E := midClassesSubgroup, B := pairingK — every input a named, verified producer; the conclusion is EXACTLY the hduality hypothesis of the f6 capstone card_deepPart_sq_of_duality (and hence of f8's lemma_6_17_dim_of_hduality).

theorem GQ2.hduality_of_data {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [DistribMulAction C V] [Finite V] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) [Finite (ContCoh.H1 (↥ρ.ker) (ZMod 2))] (hsimple : ∀ (S : AddSubgroup (V →+ ZMod 2)), (∀ (h : C), ∀ w ∈ S, SMul.smul h w ∈ S) → S = ⊥ ∨ S = ⊤) (hnt : Nontrivial (V →+ ZMod 2)) {Nreg : ℕ} (ι : (V →+ ZMod 2) →+ Fin Nreg → C → ZMod 2) (r : (Fin Nreg → C → ZMod 2) →+ V →+ ZMod 2) (hι : ∀ (h : C) (φ : V →+ ZMod 2) (n : Fin Nreg) (x : C), ι (SMul.smul h φ) n x = ι φ n (h⁻¹ * x)) (hr : ∀ (h : C) (F : Fin Nreg → C → ZMod 2), (r fun (n : Fin Nreg) (x : C) => F n (h⁻¹ * x)) = SMul.smul h (r F)) (hri : ∀ (φ : V →+ ZMod 2), r (ι φ) = φ) (eU : (V →+ ZMod 2) ≃+ ((V →+ ZMod 2) →+ ZMod 2)) (heU : ∀ (c : C) (φ : V →+ ZMod 2), eU (SMul.smul c φ) = SMul.smul c (eU φ)) (t₀ : C) (ht₀U : ∃ (φ : V →+ ZMod 2), SMul.smul t₀ φ ≠ φ) (g₀ : AbsGalQ2) (hg₀ : ρ g₀ = t₀) (hg₀rt : IsResidueTrivial ρ.ker g₀) (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥k] (htriv : ∀ (g : ↥k.fixingSubgroup) (m : ZMod 2), g • m = m) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (π : AlgebraicClosure ℚ_[2]) (hπk : π ∈ k) (hπ0 : π ≠ 0) (hπ1 : ‖π‖ < 1) (hπmax : ∀ x ∈ k, ‖x‖ < 1 → ‖x‖ ≤ ‖π‖) {e : ℕ} (he : ‖2‖ = ‖π‖ ^ e) (he_pos : 1 ≤ e) {f : ℕ} (hf_pos : 1 ≤ f) (hcard_zero : Nat.card (↥(normUnits k) ⧸ (depthUnits k π 1).subgroupOf (normUnits k)) = 2 ^ f - 1) (hcard_gr : ∀ (i : ℕ), 1 ≤ i → Nat.card (↥(depthUnits k π i) ⧸ (depthUnits k π (i + 1)).subgroupOf (depthUnits k π i)) = 2 ^ f) : Nat.card ↥(equivHoms C (V →+ ZMod 2) ↥(deepClassesSubgroup ρ.ker)) = Nat.card ↥(equivHoms C (V →+ ZMod 2) (ContCoh.H1 (↥ρ.ker) (ZMod 2) ⧸ deepClassesSubgroup ρ.ker))

hduality — the deep-part proof's result. Inputs: the V^∨ regular-summand package (f8's Lemma-6.11 output at dualModule: hsimple/hnt/ι/r/hι/hr/hri), the self-duality eU/heU (§H's dualSelfDual(_equivariant) given the 6.17 invariant form), the dualized inertia ht₀U (§H's exists_dualModule_smul_ne given hram), a residue-trivial lift g₀ of t₀ (tame inertia; the f8 arithmetic), and the B13 bundle data for the splitting field k with the pointwise kernel identification hker.