The deep/quotient Hom-count duality

Produces the hduality input of the f6 capstone card_deepPart_sq_of_duality (GQ2/AdmissibleCount.lean):

#Hom_C(V^∨, deep) = #Hom_C(V^∨, H¹(N)/deep).

The minimal route (design note)

The paper (§6.3 p. 34) runs the full graded computation: eq. (93) square-class sizes, the per-level Hilbert duality U_i^⊥ = U_{2e−i+1} of eq. (94) pairing gr_j ≅ (gr_{2e−j})^∨, self-duality V ≅ V^∨ for equal multiplicities, and Lemma 6.10 killing the middle j = e. This file implements a strictly smaller route discovered at design time: with E := U_e-classes (norm-vocabulary ‖A−1‖ ≤ ‖2‖ — no uniformizer needed) and Deep := U_{e+1}-classes, the chain

#Hom(U, M/Deep) = #Hom(M/Deep, U) -- Hom-symmetry (§D) = #Hom(M/Deep, U^∨) -- U self-dual = #Hom(U, (M/Deep)^∨) -- currying (§C) = #Hom(U, Deep^⊥) -- nondegeneracy: ann(Deep) ≅ (M/Deep)^∨ (§E) = #Hom(U, Deep)·#Hom(U, Deep^⊥/Deep) -- f6 SES engine at Deep ≤ Deep^⊥ = #Hom(U, Deep) -- middle-kill (§B): Deep^⊥/Deep ⊆ E/Deep -- is inertia-trivial, U ramified simple

needs from the arithmetic side ONLY:

• (H2) nondegeneracy of one C-invariant pairing B on M = H¹(N,𝔽₂);
• (H3) isotropy Deep ≤ Deep^⊥ — banked (Tier-5 cup_deepClasses, std-3 ∪ {B11a});
• (H4) ONE sharp instance Deep^⊥ ≤ E — the ⊆-half of eq. (94) at i = e+1 (U_{e+1}^⊥ = U_e); NO other level of (94) is consumed;
• (H5) the middle twist — conjugates of the inertia generator act trivially on E/Deep (Lemma 6.10; the θ^e ≡ 1 twist is derivable norm-algebra per GQ2/UnitFiltration.lean).

No per-level graded (93) computation, no U_i^⊥ = U_{2e−i+1} beyond (H4), no new axiom in this file: (H2)/(H4)/(H5) enter as hypotheses, so the leaf decision (prove vs. cite Serre LF XIV §§1–3 / FV IV §5 Thm (5.2)) is deferred to the instantiation and needs user approval only there.

Contents

• §A — generic restricted/quotient DistribMulActions on a C-stable AddSubgroup (abstract twins of f6's conjModuleDeep/conjModuleQuot).
• §B — card_equivHoms_eq_one_of_conjSmulTrivial: if some t₀ : C acts nontrivially on the simple module U while every conjugate d t₀ d⁻¹ acts trivially on T, then #Hom_C(U, T) = 1 (homs factor through the inertia-coinvariants, which vanish).
• §C — the currying bijection #Hom_C(U, W^∨) = #Hom_C(W, U^∨) (duals via dualModule).
• §D — Hom-symmetry #Hom_C(U, W) = #Hom_C(W, U) for U simple, nontrivial, self-dual, with a regular-summand package (Lemma 6.11's output shape): strong induction on #W, splitting off U-copies via the banked equivariant_lift_of_regular_summand (epi side) and its dual (mono side). This is the precise module-theoretic content behind the paper's "self-duality gives equal multiplicities".
• §E — the perp layer: pairPerp, stability, perpEquivDualQuot (ann(S) ≅ (M/S)^∨).
• §F — the assembly card_equivHoms_deep_eq_quot (abstract hduality).

The main consumer is card_deepPart_sq_of_duality.

@[reducible]

def GQ2.stabSubAction {C : Type} [Group C] {M : Type} [AddCommGroup M] [DistribMulAction C M] (S : AddSubgroup M) (hS : ∀ (c : C), ∀ x ∈ S, c • x ∈ S) : DistribMulAction C ↥S

The restricted C-action on a C-stable additive subgroup (abstract twin of f6's conjModuleDeep). Provided as a @[reducible] def; consumers letI it.

Equations

• GQ2.stabSubAction S hS = { smul := fun (c : C) (x : ↥S) => ⟨c • ↑x, ⋯⟩, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

def GQ2.smulHom {C : Type} [Group C] {M : Type} [AddCommGroup M] [DistribMulAction C M] (c : C) : M →+ M

c • · as an additive endomorphism of M.

Equations

• GQ2.smulHom c = DistribSMul.toAddMonoidHom M c

noncomputable def GQ2.stabQuotHom {C : Type} [Group C] {M : Type} [AddCommGroup M] [DistribMulAction C M] (S : AddSubgroup M) (hS : ∀ (c : C), ∀ x ∈ S, c • x ∈ S) (c : C) : M ⧸ S →+ M ⧸ S

The descent of c • · to M ⧸ S for a C-stable S.

Equations

• GQ2.stabQuotHom S hS c = QuotientAddGroup.map S S (GQ2.smulHom c) ⋯

theorem GQ2.stabQuotHom_mk {C : Type} [Group C] {M : Type} [AddCommGroup M] [DistribMulAction C M] (S : AddSubgroup M) (hS : ∀ (c : C), ∀ x ∈ S, c • x ∈ S) (c : C) (a : M) : (stabQuotHom S hS c) ↑a = ↑(c • a)

Computation rule for stabQuotHom on a class.

@[reducible]

noncomputable def GQ2.stabQuotAction {C : Type} [Group C] {M : Type} [AddCommGroup M] [DistribMulAction C M] (S : AddSubgroup M) (hS : ∀ (c : C), ∀ x ∈ S, c • x ∈ S) : DistribMulAction C (M ⧸ S)

The induced C-action on M ⧸ S for a C-stable S (abstract twin of f6's conjModuleQuot). Provided as a @[reducible] def; consumers letI it.

Equations

• GQ2.stabQuotAction S hS = { smul := fun (c : C) (x : M ⧸ S) => (GQ2.stabQuotHom S hS c) x, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

theorem GQ2.card_equivHoms_eq_one_of_conjSmulTrivial {C : Type} [Group C] {U : Type} [AddCommGroup U] [DistribMulAction C U] {T : Type} [AddCommGroup T] [DistribMulAction C T] (hsimple : ∀ (W : AddSubgroup U), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (t₀ : C) (hU : ∃ (u : U), t₀ • u ≠ u) (hT : ∀ (d : C) (x : T), (d * t₀ * d⁻¹) • x = x) : Nat.card ↥(equivHoms C U T) = 1

The inertia-coinvariants kill (Lemma 6.10's consumer form): if some t₀ : C acts nontrivially on the simple module U while every conjugate d t₀ d⁻¹ acts trivially on T, then the only equivariant map U →+ T is zero — an equivariant map kills the (nonzero, C-stable, hence full) subgroup generated by {(d t₀ d⁻¹) • u − u}.

noncomputable def GQ2.equivHomsCurry {C : Type} [Group C] {U : Type} [AddCommGroup U] [DistribMulAction C U] {W : Type} [AddCommGroup W] [DistribMulAction C W] : ↥(equivHoms C U (W →+ ZMod 2)) ≃ ↥(equivHoms C W (U →+ ZMod 2))

The currying bijection: equivariant maps into the dual are equivariant pairings, read from either side — Hom_C(U, W^∨) ≃ Hom_C(W, U^∨) (both duals carrying dualModule). f ↦ AddMonoidHom.flip f.

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.card_equivHoms_curry {C : Type} [Group C] {U : Type} [AddCommGroup U] [DistribMulAction C U] {W : Type} [AddCommGroup W] [DistribMulAction C W] : Nat.card ↥(equivHoms C U (W →+ ZMod 2)) = Nat.card ↥(equivHoms C W (U →+ ZMod 2))

Cardinality form of the currying bijection.

noncomputable def GQ2.equivHomsProdTarget {C : Type} [Group C] {X A B : Type} [AddCommGroup X] [AddCommGroup A] [AddCommGroup B] [DistribMulAction C X] [DistribMulAction C A] [DistribMulAction C B] : ↥(equivHoms C X (A × B)) ≃ ↥(equivHoms C X A) × ↥(equivHoms C X B)

Equivariant maps into a product split componentwise.

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.card_equivHoms_prod_target {C : Type} [Group C] {X A B : Type} [AddCommGroup X] [AddCommGroup A] [AddCommGroup B] [DistribMulAction C X] [DistribMulAction C A] [DistribMulAction C B] : Nat.card ↥(equivHoms C X (A × B)) = Nat.card ↥(equivHoms C X A) * Nat.card ↥(equivHoms C X B)

#Hom_C(X, A × B) = #Hom_C(X, A) · #Hom_C(X, B).

noncomputable def GQ2.equivHomsProdSource {C : Type} [Group C] {X A B : Type} [AddCommGroup X] [AddCommGroup A] [AddCommGroup B] [DistribMulAction C X] [DistribMulAction C A] [DistribMulAction C B] : ↥(equivHoms C (A × B) X) ≃ ↥(equivHoms C A X) × ↥(equivHoms C B X)

Equivariant maps out of a product split componentwise.

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.card_equivHoms_prod_source {C : Type} [Group C] {X A B : Type} [AddCommGroup X] [AddCommGroup A] [AddCommGroup B] [DistribMulAction C X] [DistribMulAction C A] [DistribMulAction C B] : Nat.card ↥(equivHoms C (A × B) X) = Nat.card ↥(equivHoms C A X) * Nat.card ↥(equivHoms C B X)

#Hom_C(A × B, X) = #Hom_C(A, X) · #Hom_C(B, X).

theorem GQ2.card_equivHoms_congr_source {C : Type} [Group C] {X A B : Type} [AddCommGroup X] [AddCommGroup A] [AddCommGroup B] [DistribMulAction C X] [DistribMulAction C A] [DistribMulAction C B] (e : A ≃+ B) (he : ∀ (c : C) (a : A), e (c • a) = c • e a) : Nat.card ↥(equivHoms C B X) = Nat.card ↥(equivHoms C A X)

Source transport: the equivariant-Hom count is invariant under precomposition with an equivariant additive isomorphism (the source twin of f5's card_equivHoms_congr).

theorem GQ2.dualHom_surjective_of_injective {V : Type} [AddCommGroup V] {W : Type} [AddCommGroup W] [Finite V] [Finite W] (h2V : ∀ (v : V), v + v = 0) (h2W : ∀ (w : W), w + w = 0) (f : V →+ W) (hf : Function.Injective ⇑f) : Function.Surjective fun (ψ : W →+ ZMod 2) => ψ.comp f

Dual surjectivity of an injection over 𝔽₂: for finite 2-torsion groups, restriction of functionals along an injective additive map is surjective (every functional on the source extends). Via a linear left inverse over the field ZMod 2.

def GQ2.precompHom {A B : Type} [AddCommGroup A] [AddCommGroup B] (f : A →+ B) : (B →+ ZMod 2) →+ A →+ ZMod 2

Precomposition with f as an additive map between ZMod 2-duals.

Equations

• GQ2.precompHom f = { toFun := fun (ψ : B →+ ZMod 2) => ψ.comp f, map_zero' := ⋯, map_add' := ⋯ }

theorem GQ2.precompHom_equivariant {C : Type} [Group C] {A B : Type} [AddCommGroup A] [AddCommGroup B] [DistribMulAction C A] [DistribMulAction C B] (f : A →+ B) (hf : ∀ (c : C) (a : A), f (c • a) = c • f a) (c : C) (ψ : B →+ ZMod 2) : (precompHom f) (SMul.smul c ψ) = SMul.smul c ((precompHom f) ψ)

Equivariance of precompHom (both duals under dualModule).

def GQ2.evalDualHom {W : Type} [AddCommGroup W] : W →+ (W →+ ZMod 2) →+ ZMod 2

Evaluation into the ZMod 2 double dual, as an additive map.

Equations

• GQ2.evalDualHom = { toFun := fun (w : W) => { toFun := fun (φ : W →+ ZMod 2) => φ w, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def GQ2.evalDualEquiv {W : Type} [AddCommGroup W] [Finite W] (h2 : ∀ (w : W), w + w = 0) : W ≃+ ((W →+ ZMod 2) →+ ZMod 2)

The double-dual evaluation is an isomorphism for a finite 2-torsion group: injective by functional separation, bijective by the cardinality #W^∨∨ = #W^∨ = #W (card_addHom_zmod2 twice).

Equations

• GQ2.evalDualEquiv h2 = AddEquiv.ofBijective GQ2.evalDualHom ⋯

theorem GQ2.evalDualEquiv_equivariant {C : Type} [Group C] {W : Type} [AddCommGroup W] [Finite W] [DistribMulAction C W] (h2 : ∀ (w : W), w + w = 0) (c : C) (w : W) : (evalDualEquiv h2) (c • w) = SMul.smul c ((evalDualEquiv h2) w)

Equivariance of the double-dual evaluation (dualModule twice on the target).

noncomputable def GQ2.splitProdEquiv {U W : Type} [AddCommGroup U] [AddCommGroup W] (ι : U →+ W) (ρ : W →+ U) (hρι : ∀ (u : U), ρ (ι u) = u) : W ≃+ U × ↥ρ.ker

The complement isomorphism of a split pair: a retraction ρ of ι splits W as U × ker ρ.

Equations

• GQ2.splitProdEquiv ι ρ hρι = { toFun := fun (w : W) => (ρ w, ⟨w - ι (ρ w), ⋯⟩), invFun := fun (uk : U × ↥ρ.ker) => ι uk.1 + ↑uk.2, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

theorem GQ2.ker_stable {C : Type} [Group C] {U W : Type} [AddCommGroup U] [AddCommGroup W] [DistribMulAction C U] [DistribMulAction C W] (ρ : W →+ U) (hρeq : ∀ (c : C) (w : W), ρ (c • w) = c • ρ w) (c : C) (w : W) : w ∈ ρ.ker → c • w ∈ ρ.ker

The kernel of an equivariant map is C-stable.

theorem GQ2.splitProdEquiv_equivariant {C : Type} [Group C] {U W : Type} [AddCommGroup U] [AddCommGroup W] [DistribMulAction C U] [DistribMulAction C W] (ι : U →+ W) (ρ : W →+ U) (hρι : ∀ (u : U), ρ (ι u) = u) (hιeq : ∀ (c : C) (u : U), ι (c • u) = c • ι u) (hρeq : ∀ (c : C) (w : W), ρ (c • w) = c • ρ w) (c : C) (w : W) : (splitProdEquiv ι ρ hρι) (c • w) = c • (splitProdEquiv ι ρ hρι) w

Equivariance of the complement isomorphism (ker ρ under the restricted action).

theorem GQ2.exists_section_of_epi {C : Type} [Group C] {U W : Type} [AddCommGroup U] [AddCommGroup W] [DistribMulAction C U] [DistribMulAction C W] [Finite C] (h2U : ∀ (u : U), u + u = 0) (h2W : ∀ (w : W), w + w = 0) {N : ℕ} (ι : U →+ Fin N → C → ZMod 2) (r : (Fin N → C → ZMod 2) →+ U) (hι : ∀ (h : C) (v : U) (n : Fin N) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) (hr : ∀ (h : C) (F : Fin N → C → ZMod 2), (r fun (n : Fin N) (x : C) => F n (h⁻¹ * x)) = h • r F) (hri : ∀ (v : U), r (ι v) = v) (g : W →+ U) (hgeq : ∀ (c : C) (w : W), g (c • w) = c • g w) (hgsurj : Function.Surjective ⇑g) : ∃ (σ : U →+ W), (∀ (c : C) (u : U), σ (c • u) = c • σ u) ∧ ∀ (u : U), g (σ u) = u

The epi split — a surjective equivariant map onto the packaged module splits: the banked equivariant_lift_of_regular_summand lifts id.

theorem GQ2.exists_retraction_of_mono {C : Type} [Group C] {U W : Type} [AddCommGroup U] [AddCommGroup W] [DistribMulAction C U] [DistribMulAction C W] [Finite C] [Finite U] [Finite W] (h2U : ∀ (u : U), u + u = 0) (h2W : ∀ (w : W), w + w = 0) {N : ℕ} (ι : U →+ Fin N → C → ZMod 2) (r : (Fin N → C → ZMod 2) →+ U) (hι : ∀ (h : C) (v : U) (n : Fin N) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) (hr : ∀ (h : C) (F : Fin N → C → ZMod 2), (r fun (n : Fin N) (x : C) => F n (h⁻¹ * x)) = h • r F) (hri : ∀ (v : U), r (ι v) = v) (eU : U ≃+ (U →+ ZMod 2)) (heU : ∀ (c : C) (u : U), eU (c • u) = SMul.smul c (eU u)) (f : U →+ W) (hfeq : ∀ (c : C) (u : U), f (c • u) = c • f u) (hfinj : Function.Injective ⇑f) : ∃ (ρ : W →+ U), (∀ (c : C) (w : W), ρ (c • w) = c • ρ w) ∧ ∀ (u : U), ρ (f u) = u

The mono split — an injective equivariant map out of the packaged self-dual module admits an equivariant retraction: dualize (precompHom f is onto by 𝔽₂ functional extension), lift id on the dual side with the eU-transported package, and pull the section back through the double-dual evaluations.

theorem GQ2.card_equivHoms_comm {C : Type} [Group C] [Finite C] {U : Type} [AddCommGroup U] [DistribMulAction C U] [Finite U] {W : Type} [AddCommGroup W] [DistribMulAction C W] [Finite W] (h2U : ∀ (u : U), u + u = 0) (h2W : ∀ (w : W), w + w = 0) (hsimple : ∀ (S : AddSubgroup U), (∀ (h : C), ∀ w ∈ S, h • w ∈ S) → S = ⊥ ∨ S = ⊤) (hnt : Nontrivial U) {N : ℕ} (ι : U →+ Fin N → C → ZMod 2) (r : (Fin N → C → ZMod 2) →+ U) (hι : ∀ (h : C) (v : U) (n : Fin N) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) (hr : ∀ (h : C) (F : Fin N → C → ZMod 2), (r fun (n : Fin N) (x : C) => F n (h⁻¹ * x)) = h • r F) (hri : ∀ (v : U), r (ι v) = v) (eU : U ≃+ (U →+ ZMod 2)) (heU : ∀ (c : C) (u : U), eU (c • u) = SMul.smul c (eU u)) : Nat.card ↥(equivHoms C U W) = Nat.card ↥(equivHoms C W U)

Hom-symmetry (§D): for a simple, nontrivial, self-dual module U with a regular-summand package (Lemma 6.11's output shape), the equivariant-Hom counts are symmetric: #Hom_C(U, W) = #Hom_C(W, U) for every finite 2-torsion C-module W. This is the precise module-theoretic content behind the paper's "self-duality gives equal multiplicities" (§6.3 p. 34): the package makes U both projective and injective, so U-copies split off W on either side and the counts match block by block.

def GQ2.pairPerp {M : Type} [AddCommGroup M] (B : M →+ M →+ ZMod 2) (S : AddSubgroup M) : AddSubgroup M

The perp of a subgroup under a biadditive ZMod 2 pairing.

Equations

• GQ2.pairPerp B S = { carrier := {x : M | ∀ s ∈ S, (B x) s = 0}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem GQ2.mem_pairPerp_iff {M : Type} [AddCommGroup M] (B : M →+ M →+ ZMod 2) (S : AddSubgroup M) (x : M) : x ∈ pairPerp B S ↔ ∀ s ∈ S, (B x) s = 0

theorem GQ2.pairPerp_stable {C : Type} [Group C] {M : Type} [AddCommGroup M] [DistribMulAction C M] (B : M →+ M →+ ZMod 2) (hBinv : ∀ (c : C) (x y : M), (B (c • x)) (c • y) = (B x) y) (S : AddSubgroup M) (hS : ∀ (c : C), ∀ s ∈ S, c • s ∈ S) (c : C) (x : M) : x ∈ pairPerp B S → c • x ∈ pairPerp B S

The perp of a C-stable subgroup is C-stable when the pairing is invariant.

noncomputable def GQ2.perpEquivDualQuot {M : Type} [AddCommGroup M] (B : M →+ M →+ ZMod 2) [Finite M] (h2M : ∀ (m : M), m + m = 0) (hBnd : ∀ (x : M), (∀ (y : M), (B x) y = 0) → x = 0) (S : AddSubgroup M) : ↥(pairPerp B S) ≃+ (M ⧸ S →+ ZMod 2)

ann(S) ≅ (M/S)^∨: for a nondegenerate pairing on a finite 2-torsion module, the perp of S is additively isomorphic to the dual of M ⧸ S — x ↦ B x descended through mk. Surjectivity is the nondegeneracy count (φ_B : M ≃ M^∨ by injectivity + #M^∨ = #M).

Equations

• GQ2.perpEquivDualQuot B h2M hBnd S = AddEquiv.ofBijective { toFun := fun (x : ↥(GQ2.pairPerp B S)) => QuotientAddGroup.lift S (B ↑x) ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯

theorem GQ2.perpEquivDualQuot_mk {M : Type} [AddCommGroup M] (B : M →+ M →+ ZMod 2) [Finite M] (h2M : ∀ (m : M), m + m = 0) (hBnd : ∀ (x : M), (∀ (y : M), (B x) y = 0) → x = 0) (S : AddSubgroup M) (x : ↥(pairPerp B S)) (m : M) : ((perpEquivDualQuot B h2M hBnd S) x) ↑m = (B ↑x) m

Evaluation rule for perpEquivDualQuot on a class.

theorem GQ2.perpEquivDualQuot_equivariant {C : Type} [Group C] {M : Type} [AddCommGroup M] [DistribMulAction C M] (B : M →+ M →+ ZMod 2) [Finite M] (h2M : ∀ (m : M), m + m = 0) (hBnd : ∀ (x : M), (∀ (y : M), (B x) y = 0) → x = 0) (S : AddSubgroup M) (hBinv : ∀ (c : C) (x y : M), (B (c • x)) (c • y) = (B x) y) (hS : ∀ (c : C), ∀ s ∈ S, c • s ∈ S) [instQ : DistribMulAction C (M ⧸ S)] (hπ : ∀ (c : C) (m : M), ↑(c • m) = c • ↑m) (c : C) (x : ↥(pairPerp B S)) : (perpEquivDualQuot B h2M hBnd S) (c • x) = c • (perpEquivDualQuot B h2M hBnd S) x

Equivariance of perpEquivDualQuot: the perp carries the restricted action, the dual of the quotient the dualModule action over a compatible quotient action instQ.

theorem GQ2.card_pairPerp {M : Type} [AddCommGroup M] (B : M →+ M →+ ZMod 2) [Finite M] (h2M : ∀ (m : M), m + m = 0) (hBnd : ∀ (x : M), (∀ (y : M), (B x) y = 0) → x = 0) (S : AddSubgroup M) : Nat.card ↥(pairPerp B S) = Nat.card (M ⧸ S)

The perp count #S^⊥ = #(M ⧸ S): the nondegenerate-duality cardinality through perpEquivDualQuot and #(A^∨) = #A for elementary-2 A.

theorem GQ2.pairPerp_le_of_card_le {M : Type} [AddCommGroup M] (B : M →+ M →+ ZMod 2) [Finite M] (h2M : ∀ (m : M), m + m = 0) (hBnd : ∀ (x : M), (∀ (y : M), (B x) y = 0) → x = 0) {S E : AddSubgroup M} (hE : E ≤ pairPerp B S) (hcard : Nat.card (M ⧸ S) ≤ Nat.card ↥E) : pairPerp B S ≤ E

Sharpness from the easy inclusion + the cardinality balance: if E ≤ S^⊥ and #(M ⧸ S) ≤ #E, then S^⊥ ≤ E (the two are equal). This reduces (H4)'s hsharp to the structural count #(M ⧸ Deep) ≤ #E.

theorem GQ2.card_equivHoms_deep_eq_quot {C : Type} [Group C] [Finite C] {M : Type} [AddCommGroup M] [DistribMulAction C M] [Finite M] {U : Type} [AddCommGroup U] [DistribMulAction C U] [Finite U] (h2M : ∀ (m : M), m + m = 0) (h2U : ∀ (u : U), u + u = 0) (hsimple : ∀ (S : AddSubgroup U), (∀ (h : C), ∀ w ∈ S, h • w ∈ S) → S = ⊥ ∨ S = ⊤) (hnt : Nontrivial U) {N : ℕ} (ι : U →+ Fin N → C → ZMod 2) (r : (Fin N → C → ZMod 2) →+ U) (hι : ∀ (h : C) (v : U) (n : Fin N) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) (hr : ∀ (h : C) (F : Fin N → C → ZMod 2), (r fun (n : Fin N) (x : C) => F n (h⁻¹ * x)) = h • r F) (hri : ∀ (v : U), r (ι v) = v) (eU : U ≃+ (U →+ ZMod 2)) (heU : ∀ (c : C) (u : U), eU (c • u) = SMul.smul c (eU u)) (t₀ : C) (ht₀U : ∃ (u : U), t₀ • u ≠ u) (B : M →+ M →+ ZMod 2) (hBinv : ∀ (c : C) (x y : M), (B (c • x)) (c • y) = (B x) y) (hBnd : ∀ (x : M), (∀ (y : M), (B x) y = 0) → x = 0) (Deep E : AddSubgroup M) (hDeepStab : ∀ (c : C), ∀ x ∈ Deep, c • x ∈ Deep) (hiso : Deep ≤ pairPerp B Deep) (hsharp : pairPerp B Deep ≤ E) (hmid : ∀ (d : C), ∀ x ∈ E, (d * t₀ * d⁻¹) • x - x ∈ Deep) [instDeep : DistribMulAction C ↥Deep] (hjeq : ∀ (c : C) (x : ↥Deep), ↑(c • x) = c • ↑x) [instQ : DistribMulAction C (M ⧸ Deep)] (hπeq : ∀ (c : C) (m : M), ↑(c • m) = c • ↑m) : Nat.card ↥(equivHoms C U ↥Deep) = Nat.card ↥(equivHoms C U (M ⧸ Deep))

The abstract hduality (the deep-part proof §F): for a finite 2-torsion C-module M with a C-invariant nondegenerate pairing B, C-stable subgroups Deep ≤ E, the banked isotropy Deep ≤ Deep^⊥, the ONE sharp instance Deep^⊥ ≤ E, and the middle twist (conjugates of t₀ trivial on E/Deep), the equivariant-Hom counts from a simple, nontrivial, self-dual, packaged U into the deep subgroup and the quotient agree:

#Hom_C(U, Deep) = #Hom_C(U, M ⧸ Deep).

Instantiated at M := H¹(N,𝔽₂), U := V^∨, Deep := deepClassesSubgroup, E := U_e-classes with the conjugation actions, this is exactly the hduality input of the f6 capstone card_deepPart_sq_of_duality.

§G — the concrete E: mid (depth-e) Kummer classes

The U_e-classes in π-free norm vocabulary: IsMidUnit is the IsDeepUnit idiom with ‖b‖ ≤ 1 (‖A−1‖ ≤ ‖2‖ = ‖π‖^e) in place of ‖b‖ < 1. midClassesSubgroup and conjAct_midClasses mirror the deep versions (GQ2/AdmissibleCount.lean) with ≤ for <; deepClassesSubgroup ≤ midClassesSubgroup is strict-to-weak. These are the E-side instantiation inputs of card_equivHoms_deep_eq_quot (handoff §8).

def GQ2.IsMidUnit (N : Subgroup (Kummer.GaloisGroup ℚ_[2])) (A : AlgebraicClosure ℚ_[2]) : Prop

Mid unit (U_e in norm vocabulary): A = 1 + 2b with b N-fixed and ‖b‖ ≤ 1, i.e. ‖A − 1‖ ≤ ‖2‖. The ≤-relaxation of SectionSix.IsDeepUnit.

Equations

• GQ2.IsMidUnit N A = (A ≠ 0 ∧ (∀ g ∈ N, g • A = A) ∧ ∃ (b : AlgebraicClosure ℚ_[2]), (∀ g ∈ N, g • b = b) ∧ A = 1 + 2 * b ∧ ‖b‖ ≤ 1)

noncomputable def GQ2.midClassesSubgroup (N : Subgroup (Kummer.GaloisGroup ℚ_[2])) : AddSubgroup (ContCoh.H1 (↥N) (ZMod 2))

The mid Kummer classes in H¹(N, 𝔽₂): classes of restricted Kummer cocycles of mid units (the image of U_e(K)). The subgroup structure mirrors GQ2.deepClassesSubgroup.

Equations

• One or more equations did not get rendered due to their size.

§G′ — the middle twist (H5): residue-trivial conjugation moves mid by deep

Paper Lemma 6.10 in the π-free norm vocabulary. IsResidueTrivial N g says g acts trivially on the residue field of K = ℚ̄₂^N: every N-fixed integral x moves by norm < 1. The twist lemma: for such g and a mid class ξ = [κ_β] (β² = A = 1 + 2b, ‖b‖ ≤ 1), the difference conjAct ρ g ξ − ξ is a DEEP class. Since H¹ is 2-torsion the difference is the sum [κ_{g•β}] + [κ_β] = [κ_{(g•β)β}], and the PRODUCT (g•A)·A = 1 + 2·(g•b + b + 2(g•b)b) is a deep unit: g•b + b = (g•b − b) + 2b has norm < 1 by residue-triviality at x := b (p = 2 turns the paper's division (g•A)/A into a product — no root-factoring needed). Residue-triviality is conjugation-stable (norm_galois + normality of ker ρ) and depends only on the image under ρ at the conjAct level (conjAct_ker), so a single residue-trivial lift g₀ of t₀ yields the literal hmid input of card_equivHoms_deep_eq_quot for ALL C-conjugates d·t₀·d⁻¹ (conjAct_surjInv_conj_mid_sub_mem_deep). The arithmetic fact that tame-inertia lifts ARE residue-trivial is delivered at instantiation (f8).

def GQ2.IsResidueTrivial (N : Subgroup (Kummer.GaloisGroup ℚ_[2])) (g : Kummer.GaloisGroup ℚ_[2]) : Prop

Residue-trivial element (norm form): g moves every N-fixed integral x by norm < 1 — i.e. g acts trivially on the residue field of K = ℚ̄₂^N. Tame inertia lifts are residue-trivial (arithmetic input, f8); this predicate is all the twist lemma consumes.

Equations

• GQ2.IsResidueTrivial N g = ∀ (x : AlgebraicClosure ℚ_[2]), (∀ m ∈ N, m • x = x) → ‖x‖ ≤ 1 → ‖g • x - x‖ < 1

theorem GQ2.IsResidueTrivial.conj {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) {g : Kummer.GaloisGroup ℚ_[2]} (hg : IsResidueTrivial ρ.ker g) (h : Kummer.GaloisGroup ℚ_[2]) : IsResidueTrivial ρ.ker (h * g * h⁻¹)

Residue-triviality is conjugation-stable (for N = ker ρ, normal): conjugating the test vector back by h preserves N-fixedness (normality) and the norm (norm_galois).

theorem GQ2.conjAct_mid_sub_mem_deep {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (g : Kummer.GaloisGroup ℚ_[2]) (hg : IsResidueTrivial ρ.ker g) {ξ : ContCoh.H1 (↥ρ.ker) (ZMod 2)} (hξ : ξ ∈ midClassesSubgroup ρ.ker) : LocalKummer.conjAct ρ g ξ - ξ ∈ deepClassesSubgroup ρ.ker

The middle twist, class level (paper Lemma 6.10 / the (H5) core): a residue-trivial g moves a mid class by a deep class. With ξ = [κ_β], β² = A = 1 + 2b mid, 2-torsion turns the difference into [κ_{g•β}] + [κ_β] = [κ_{(g•β)β}] (kcf_mul_of_fixed), and (g•A)·A = 1 + 2(g•b + b + 2(g•b)b) is a deep unit by residue-triviality at x := b.

theorem GQ2.conjAct_surjInv_conj_mid_sub_mem_deep {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) {g₀ : AbsGalQ2} {t₀ : C} (hg₀ : ρ g₀ = t₀) (hg₀rt : IsResidueTrivial ρ.ker g₀) (d : C) {ξ : ContCoh.H1 (↥ρ.ker) (ZMod 2)} (hξ : ξ ∈ midClassesSubgroup ρ.ker) : LocalKummer.conjAct ρ (Function.surjInv hρsurj (d * t₀ * d⁻¹)) ξ - ξ ∈ deepClassesSubgroup ρ.ker

The middle twist, C-conjugate form — the literal hmid input of card_equivHoms_deep_eq_quot at the conjModule instantiation: if SOME lift g₀ of t₀ is residue-trivial, then for EVERY d : C the surjInv-lift of d·t₀·d⁻¹ twists mid classes by deep classes (conjAct only sees the ρ-image by conjAct_ker, and residue-triviality is conjugation-stable).

§H — the U-side inputs: self-duality from the invariant form, inertia dualization

The remaining module-theoretic inputs of card_equivHoms_deep_eq_quot at U := V^∨: eU (built from 6.17's invariant-form package (q, hq, hns, hinv) through the polar self-duality V ≃+ V^∨ and the banked double-dual evalDualEquiv) and ht₀U (the hram-inertia nontriviality transported to the dual by functional separation).

noncomputable def GQ2.polarSelfDual {V : Type} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (h2V : ∀ (v : V), v + v = 0) : V ≃+ (V →+ ZMod 2)

The polar form of a nonsingular quadratic map as a self-duality V ≃+ V^∨: v ↦ polar q v · — additive by IsQuadraticFp2, injective by nonsingularity, bijective by the 𝔽₂-dual count.

Equations

• GQ2.polarSelfDual q hq hns h2V = AddEquiv.ofBijective (AddMonoidHom.mk' (fun (v : V) => AddMonoidHom.mk' (fun (w : V) => GQ2.QuadraticFp2.polar q v w) ⋯) ⋯) ⋯

theorem GQ2.polarSelfDual_equivariant {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] [Finite V] (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (h2V : ∀ (v : V), v + v = 0) (hinv : QuadraticFp2.IsInvariant C q) (c : C) (v : V) : (polarSelfDual q hq hns h2V) (c • v) = SMul.smul c ((polarSelfDual q hq hns h2V) v)

Equivariance of the polar self-duality (target under dualModule).

noncomputable def GQ2.dualSelfDual {V : Type} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (h2V : ∀ (v : V), v + v = 0) : (V →+ ZMod 2) ≃+ ((V →+ ZMod 2) →+ ZMod 2)

The eU input: the induced self-duality of the dual module U := V^∨ — the polar self-duality inverted, then evaluated into the double dual.

Equations

• GQ2.dualSelfDual q hq hns h2V = (GQ2.polarSelfDual q hq hns h2V).symm.trans (GQ2.evalDualEquiv h2V)

theorem GQ2.dualSelfDual_equivariant {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] [Finite V] (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (h2V : ∀ (v : V), v + v = 0) (hinv : QuadraticFp2.IsInvariant C q) (c : C) (φ : V →+ ZMod 2) : (dualSelfDual q hq hns h2V) (SMul.smul c φ) = SMul.smul c ((dualSelfDual q hq hns h2V) φ)

The heU input: equivariance of dualSelfDual (source under dualModule, target under dualModule over it).

theorem GQ2.exists_dualModule_smul_ne {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] (h2V : ∀ (v : V), v + v = 0) (t₀ : C) (h : ∃ (v : V), t₀ • v ≠ v) : ∃ (φ : V →+ ZMod 2), SMul.smul t₀ φ ≠ φ

The ht₀U input: inertia nontriviality dualizes — if t₀ moves some vector of V, it moves some functional of V^∨ (under dualModule; by 𝔽₂-functional separation).

Paper-tag ledger (auto-generated by paperforge; do not edit)

• eq. (93) = ⟦eq-squareclassgraded⟧
• eq. (94) = ⟦eq-unitorth⟧
• Lemma 6.10 = ⟦lem-middlelayer⟧
• Lemma 6.11 = ⟦lem-faithfulprojective⟧