Counting admissible families via the equivariant-Hom engine

The bridge identifying LocalKummer.AdmissibleFam ρ with the equivariant Homs equivHoms C (V →+ 𝔽₂) (H¹(N, 𝔽₂)) (the acting group C = H_V; H¹(N) carries the conjModule action from brick ii, V^∨ the dual action dualModule), so that the deep-part proof counting engine applies to the U_{e+1} filtration.

• dualModule — the dual C-action on V^∨ = V →+ 𝔽₂, (c • φ) v = φ (c⁻¹ • v).

WIP (this file is under construction for brick iii).

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

deepClasses as an additive subgroup of H¹(N, 𝔽₂): the deep Kummer classes are closed under 0/+/neg — deep units form a group (A₁A₂ deep), [a] + [b] = [ab] via kcf_mul_of_fixed, and H¹ is 2-torsion so neg = id. The subgroup form the U_{e+1} short exact sequence (the deep-part proof brick iii-b) and f2's orbit analysis consume.

Equations

• GQ2.deepClassesSubgroup N = { carrier := GQ2.LocalKummer.deepClasses N, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem GQ2.kcf_conj (β : AlgebraicClosure ℚ_[2]) (g n : Kummer.GaloisGroup ℚ_[2]) : Kummer.kummerCocycleFun β (g⁻¹ * n * g) = Kummer.kummerCocycleFun (g • β) n

The Kummer cocycle conjugates as κ_β(g⁻¹ n g) = κ_{g·β}(n) (the class of the conjugated root). Underlies the conjModule-invariance of deepClasses.

@[reducible]

noncomputable def GQ2.dualModule {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] : DistribMulAction C (V →+ ZMod 2)

The dual C-action on V^∨ = V →+ 𝔽₂: (c • φ) v = φ (c⁻¹ • v) (precomposition with the inverse action on V). Provided as a def (not a global instance — it competes with the trivial codomain action on V →+ 𝔽₂); consumers letI it.

Equations

• GQ2.dualModule = { smul := fun (c : C) (φ : V →+ ZMod 2) => φ.comp (DistribSMul.toAddMonoidHom V c⁻¹), mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

theorem GQ2.dualModule_smul_apply {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] (c : C) (φ : V →+ ZMod 2) (v : V) : (SMul.smul c φ) v = φ (c⁻¹ • v)

Evaluation rule for dualModule.

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

conjModule-invariance of deepClasses (the deep-part proof brick iii-b — the §4-handoff gate): the G_ℚ₂-conjugation conjAct ρ g carries a deep Kummer class to a deep Kummer class. Concretely conjAct ρ g [κ_β] = [κ_{g•β}] (via conjAct_h1ofFun + kcf_conj), and g • A is again a deep unit: normality of ker ρ keeps it N-fixed, and ‖g • b‖ = ‖b‖ by GQ2.norm_galois. This is the invariance that lets deepClassesSubgroup carry the restricted conjModule action (f5's W').

noncomputable def GQ2.conjActHom {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (g : AbsGalQ2) : ContCoh.H1 (↥ρ.ker) (ZMod 2) →+ ContCoh.H1 (↥ρ.ker) (ZMod 2)

conjAct ρ g packaged as an additive endomorphism of H¹(N, 𝔽₂) (conjAct_add), so it can feed QuotientAddGroup.map for the induced action on H¹(N) ⧸ deepClassesSubgroup.

Equations

• GQ2.conjActHom ρ g = AddMonoidHom.mk' (GQ2.LocalKummer.conjAct ρ g) ⋯

@[reducible]

noncomputable def GQ2.conjModuleDeep {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) : DistribMulAction C ↥(deepClassesSubgroup ρ.ker)

The restricted conjModule action on the deep subgroup (f5's W'): deepClassesSubgroup is conjModule-invariant (conjAct_deepClasses), so the conjugation action restricts to a DistribMulAction C on ↥(deepClassesSubgroup (ker ρ)). Provided as a @[reducible] def (like conjModule); consumers letI it.

Equations

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

noncomputable def GQ2.conjActQuotHom {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (g : AbsGalQ2) : ContCoh.H1 (↥ρ.ker) (ZMod 2) ⧸ deepClassesSubgroup ρ.ker →+ ContCoh.H1 (↥ρ.ker) (ZMod 2) ⧸ deepClassesSubgroup ρ.ker

The descent of conjAct ρ g to H¹(N) ⧸ deepClassesSubgroup, via QuotientAddGroup.map (well-defined because deepClassesSubgroup is conjAct-invariant, conjAct_deepClasses).

Equations

• GQ2.conjActQuotHom ρ g = QuotientAddGroup.map (GQ2.deepClassesSubgroup ρ.ker) (GQ2.deepClassesSubgroup ρ.ker) (GQ2.conjActHom ρ g) ⋯

theorem GQ2.conjActQuotHom_mk {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (g : AbsGalQ2) (a : ContCoh.H1 (↥ρ.ker) (ZMod 2)) : (conjActQuotHom ρ g) ↑a = ↑(LocalKummer.conjAct ρ g a)

Computation rule for conjActQuotHom on a class.

@[reducible]

noncomputable def GQ2.conjModuleQuot {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) : DistribMulAction C (ContCoh.H1 (↥ρ.ker) (ZMod 2) ⧸ deepClassesSubgroup ρ.ker)

The induced conjModule action on the quotient (f5's W''): since deepClassesSubgroup is conjModule-invariant, the conjugation action descends to H¹(N) ⧸ deepClassesSubgroup via conjActQuotHom. Provided as a @[reducible] def; consumers letI it.

Equations

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

theorem GQ2.fam_equivariant {C : Type} [Group C] [TopologicalSpace C] {V : Type} [AddCommGroup V] [DistribMulAction AbsGalQ2 V] [DistribMulAction C V] (ρ : AbsGalQ2 →ₜ* C) (hρ : ∀ (g : AbsGalQ2) (v : V), g • v = ρ g • v) (hρsurj : Function.Surjective ⇑ρ) (ξ : LocalKummer.AdmissibleFam ρ) (c : C) (φ : V →+ ZMod 2) : ξ.fam (φ.comp (DistribSMul.toAddMonoidHom V c⁻¹)) = LocalKummer.conjAct ρ (Function.surjInv hρsurj c) (ξ.fam φ)

The core equivariance of an admissible family matching the two C-actions: ξ.fam intertwines the dual action dualModule on V^∨ with the conjugation action conjModule on H¹(N). The AdmissibleFam.equiv' field is stated in the G_ℚ₂-conjugation form; this converts it to the C-form via a lift surjInv c and hρ (the G_ℚ₂/C action compatibility on V).

noncomputable def GQ2.admissibleFamEquiv {C : Type} [Group C] [TopologicalSpace C] {V : Type} [AddCommGroup V] [DistribMulAction AbsGalQ2 V] [DistribMulAction C V] (ρ : AbsGalQ2 →ₜ* C) (hρ : ∀ (g : AbsGalQ2) (v : V), g • v = ρ g • v) (hρsurj : Function.Surjective ⇑ρ) : LocalKummer.AdmissibleFam ρ ≃ ↥(equivHoms C (V →+ ZMod 2) (ContCoh.H1 (↥ρ.ker) (ZMod 2)))

The bridge AdmissibleFam ≃ equivHoms (brick iii): admissible families are exactly the C-equivariant additive maps V^∨ → H¹(N), under the dual action dualModule on V^∨ and the conjModule conjugation action on H¹(N). Forward equivariance is fam_equivariant; the converse re-derives equiv' from C-equivariance at c = ρ g (via conjAct_ker + hρ).

Equations

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

theorem GQ2.card_admissibleFam_eq {C : Type} [Group C] [TopologicalSpace C] {V : Type} [AddCommGroup V] [DistribMulAction AbsGalQ2 V] [DistribMulAction C V] (ρ : AbsGalQ2 →ₜ* C) (hρ : ∀ (g : AbsGalQ2) (v : V), g • v = ρ g • v) (hρsurj : Function.Surjective ⇑ρ) : Nat.card (LocalKummer.AdmissibleFam ρ) = Nat.card ↥(equivHoms C (V →+ ZMod 2) (ContCoh.H1 (↥ρ.ker) (ZMod 2)))

Count admissible families as equivariant Homs: #AdmissibleFam = #equivHoms C V^∨ H¹(N). This lets the deep-part proof engine (card_equivHoms_of_exact) count AdmissibleFam across the U_{e+1} filtration of H¹(N) ≅ M_K.

noncomputable def GQ2.deepFamEquiv {C : Type} [Group C] [TopologicalSpace C] {V : Type} [AddCommGroup V] [DistribMulAction AbsGalQ2 V] [DistribMulAction C V] (ρ : AbsGalQ2 →ₜ* C) (hρ : ∀ (g : AbsGalQ2) (v : V), g • v = ρ g • v) (hρsurj : Function.Surjective ⇑ρ) : { ξ : LocalKummer.AdmissibleFam ρ // ∀ (φ : V →+ ZMod 2), ξ.fam φ ∈ LocalKummer.deepClasses ρ.ker } ≃ ↥(equivHoms C (V →+ ZMod 2) ↥(deepClassesSubgroup ρ.ker))

The deep-families bridge (the deep-part proof step 4): the admissible families valued in the deep classes are exactly the C-equivariant maps V^∨ → deepClassesSubgroup (under dualModule on V^∨ and the restricted conjModuleDeep on the deep subgroup). Mirrors admissibleFamEquiv, restricted through deepClassesSubgroup.

Equations

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

theorem GQ2.card_deepFam_eq {C : Type} [Group C] [TopologicalSpace C] {V : Type} [AddCommGroup V] [DistribMulAction AbsGalQ2 V] [DistribMulAction C V] (ρ : AbsGalQ2 →ₜ* C) (hρ : ∀ (g : AbsGalQ2) (v : V), g • v = ρ g • v) (hρsurj : Function.Surjective ⇑ρ) : Nat.card { ξ : LocalKummer.AdmissibleFam ρ // ∀ (φ : V →+ ZMod 2), ξ.fam φ ∈ LocalKummer.deepClasses ρ.ker } = Nat.card ↥(equivHoms C (V →+ ZMod 2) ↥(deepClassesSubgroup ρ.ker))

Count the deep families as equivariant Homs into the deep subgroup: #{deep families} = #equivHoms C V^∨ deepClassesSubgroup (the deep-part proof step 4).

theorem GQ2.card_equivHoms_quotient_ses {C : Type} [Group C] [Finite C] {U A : Type} [AddCommGroup U] [AddCommGroup A] [DistribMulAction C U] [instA : DistribMulAction C A] [Finite U] [Finite A] (Deep : AddSubgroup A) [instDeep : DistribMulAction C ↥Deep] [instQuot : DistribMulAction C (A ⧸ Deep)] (h2A : ∀ (a : A), a + a = 0) {Nreg : ℕ} (ι : U →+ Fin Nreg → C → ZMod 2) (r : (Fin Nreg → C → ZMod 2) →+ U) (hι : ∀ (h : C) (u : U) (n : Fin Nreg) (x : C), ι (h • u) n x = ι u n (h⁻¹ * x)) (hr : ∀ (h : C) (F : Fin Nreg → C → ZMod 2), (r fun (n : Fin Nreg) (x : C) => F n (h⁻¹ * x)) = h • r F) (hri : ∀ (u : U), r (ι u) = u) (hj : ∀ (c : C) (w : ↥Deep), Deep.subtype (c • w) = c • Deep.subtype w) (hπ : ∀ (c : C) (w : A), (QuotientAddGroup.mk' Deep) (c • w) = c • (QuotientAddGroup.mk' Deep) w) : Nat.card ↥(equivHoms C U A) = Nat.card ↥(equivHoms C U ↥Deep) * Nat.card ↥(equivHoms C U (A ⧸ Deep))

The inclusion/quotient SES count, over an abstract invariant subgroup — the view-normalization brick. For any finite 2-torsion C-module A with a C-submodule Deep (carrying compatible C-actions on ↥Deep and A ⧸ Deep), the equivariant-Hom counts multiply along 0 → Deep → A → A ⧸ Deep → 0:

#Hom_C(U, A) = #Hom_C(U, Deep) · #Hom_C(U, A ⧸ Deep).

Stating this over a plain fvar Deep : AddSubgroup A is exactly what dodges the AbsGalQ2/GaloisGroup view mismatch (handoff §4/§7): Deep.Normal and the quotient's AddCommGroup/Finite structure resolve against Deep/A as fvars (no coercion), so card_equivHoms_of_exact applies cleanly; instantiating A := H¹(N), Deep := deepClassesSubgroup later is pure substitution. hj/hπ are the equivariance of the inclusion/quotient maps.

theorem GQ2.card_equivHoms_deepSES {C : Type} [Group C] [TopologicalSpace C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) [Finite (ContCoh.H1 (↥ρ.ker) (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 (ι φ) = φ) : Nat.card ↥(equivHoms C (V →+ ZMod 2) (ContCoh.H1 (↥ρ.ker) (ZMod 2))) = Nat.card ↥(equivHoms C (V →+ ZMod 2) ↥(deepClassesSubgroup ρ.ker)) * Nat.card ↥(equivHoms C (V →+ ZMod 2) (ContCoh.H1 (↥ρ.ker) (ZMod 2) ⧸ deepClassesSubgroup ρ.ker))

The U_{e+1} short exact sequence count (the deep-part proof step 3): instantiate card_equivHoms_quotient_ses at A := H¹(N), Deep := deepClassesSubgroup (ker ρ) with the conjugation actions. Yields #Hom_C(V^∨, H¹(N)) = #Hom_C(V^∨, deep) · #Hom_C(V^∨, H¹(N)/deep). The regular-summand package (ι, r) for V^∨ (Lemma-6.11 output shape) and Finite (H¹ N) are hypotheses; the lemma_6_11 instantiation of the package (f8) is proved (GQ2/RegularSummand.lean), so consumers' audits are clean. The abstract helper sidesteps the AbsGalQ2/GaloisGroup view mismatch (handoff §4/§7).

theorem GQ2.card_deepPart_sq_of_duality {C : Type} [Group C] [TopologicalSpace C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction AbsGalQ2 V] [ContinuousSMul AbsGalQ2 V] [DistribMulAction C V] (ρ : AbsGalQ2 →ₜ* C) (hρ : ∀ (g : AbsGalQ2) (v : V), g • v = ρ g • v) (hV2 : ∀ (v : V), v + v = 0) (hρsurj : Function.Surjective ⇑ρ) (hinf : LocalKummer.InflationVanishes ρ) (hext : LocalKummer.FamiliesExtend ρ) [Finite (ContCoh.H1 (↥ρ.ker) (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 (ι φ) = φ) (hduality : Nat.card ↥(equivHoms C (V →+ ZMod 2) ↥(deepClassesSubgroup ρ.ker)) = Nat.card ↥(equivHoms C (V →+ ZMod 2) (ContCoh.H1 (↥ρ.ker) (ZMod 2) ⧸ deepClassesSubgroup ρ.ker))) : Nat.card ↑(SectionSix.deepPart ρ) ^ 2 = Nat.card (ContCoh.H1 AbsGalQ2 V)

The deep-half dimension clause from the duality (the deep-part proof output, step 5): given the regular-summand package for V^∨, finiteness of H¹(N), the two deferred cohomological inputs hinf/hext (Lemma-6.11 projectivity), and the graded Hilbert duality #Hom_C(V^∨, deep) = #Hom_C(V^∨, H¹(N)/deep) (f7's job — the self-duality V ≅ V^∨ through the invariant form), the deep half squares to #H¹(ℚ₂,V): #X₊² = #H¹. This is the honest f6 reduction — everything is wired, and only the duality (f7) and the package (f8, lemma_6_11) remain to instantiate it. Chains card_H1_eq_card_fam · card_admissibleFam_eq · card_equivHoms_deepSES on one side, card_deepPart_eq_card_deepFam · card_deepFam_eq on the other; hduality collapses the SES product to a square.