Dual-invariant vanishing (M^∨)^C = 0 (lem:simplehead, part 2)

The deepest simple-head fact, proved from ⊆-minimality and chief-ness alone — no equivariant identification of M/T with the chief factor is needed:

Let φ : M →ₗ 𝔽₂ be C-invariant, and let J ≤ Y be the preimage in K of the multiplicative kernel of φ. Then J is Y-normal (invariance), Φ(K) ≤ J ≤ K, and J ⊔ S is a Y-normal subgroup between S and P. By chief-ness it is S or P:

• if J ⊔ S = P, ⊆-minimality of K forces J = K, so φ = 0;
• if J ⊔ S = S, then [Y, K] ≤ J ≤ S (the conjugation差 of any k ∈ K lands in the kernel because φ is invariant), and with P = K·S every chief-factor commutator [y, n] lands in S — the factor would be scalar, contradicting chief.nontrivial_action.

Hence φ = 0 (towerDualInv_zero). Everything here is proved — no axioms.

The multiplicative kernel and its ambient preimage

def Q2Presentation.Induction.dualKerGrp {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (φ : Module.Dual (ZMod 2) (towerM K)) : Subgroup (towerMgrp K)

The multiplicative form of ker φ inside the Frattini quotient.

Equations

• Q2Presentation.Induction.dualKerGrp K φ = Subgroup.toAddSubgroup.symm (LinearMap.ker φ).toAddSubgroup

theorem Q2Presentation.Induction.mem_dualKerGrp_iff {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (φ : Module.Dual (ZMod 2) (towerM K)) (m : towerMgrp K) : m ∈ dualKerGrp K φ ↔ φ (Additive.ofMul m) = 0

def Q2Presentation.Induction.dualKerAmbient {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (φ : Module.Dual (ZMod 2) (towerM K)) : Subgroup p.fst.Y

The ambient preimage J ≤ Y of the kernel of φ: elements of K whose Frattini class is killed by φ.

Equations

• Q2Presentation.Induction.dualKerAmbient K φ = Subgroup.map K.Ksub.subtype (Subgroup.comap (QuotientGroup.mk' (frattini ↥K.Ksub)) (Q2Presentation.Induction.dualKerGrp K φ))

theorem Q2Presentation.Induction.dualKerAmbient_le {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (φ : Module.Dual (ZMod 2) (towerM K)) : dualKerAmbient K φ ≤ K.Ksub

theorem Q2Presentation.Induction.mem_dualKerAmbient_iff {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (φ : Module.Dual (ZMod 2) (towerM K)) (y : p.fst.Y) : y ∈ dualKerAmbient K φ ↔ ∃ (hy : y ∈ K.Ksub), φ (Additive.ofMul ((QuotientGroup.mk' (frattini ↥K.Ksub)) ⟨y, hy⟩)) = 0

Invariance makes the preimage normal

theorem Q2Presentation.Induction.dualKerGrp_conj_stable {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (φ : Module.Dual (ZMod 2) (towerM K)) (hinv : ∀ (c : towerC K), φ ∘ₗ ↑((towerActM K) c) = φ) (y : p.fst.Y) {m : towerMgrp K} (hm : m ∈ dualKerGrp K φ) : (conjOnMgrp K y) m ∈ dualKerGrp K φ

The kernel subgroup is stable under all descended conjugations.

theorem Q2Presentation.Induction.dualKerAmbient_normal {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (φ : Module.Dual (ZMod 2) (towerM K)) (hinv : ∀ (c : towerC K), φ ∘ₗ ↑((towerActM K) c) = φ) : (dualKerAmbient K φ).Normal

J is normal in Y.

theorem Q2Presentation.Induction.conj_diff_mem_dualKerAmbient {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (φ : Module.Dual (ZMod 2) (towerM K)) (hinv : ∀ (c : towerC K), φ ∘ₗ ↑((towerActM K) c) = φ) (y : p.fst.Y) {k : p.fst.Y} (hk : k ∈ K.Ksub) : y * k * y⁻¹ * k⁻¹ ∈ dualKerAmbient K φ

The conjugation difference of any kernel element lies in J: y k y⁻¹ k⁻¹ ∈ J for all y : Y, k ∈ K.

The chief dichotomy

theorem Q2Presentation.Induction.towerDualInv_zero {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (φ : Module.Dual (ZMod 2) (towerM K)) (hinv : ∀ (c : towerC K), φ ∘ₗ ↑((towerActM K) c) = φ) : φ = 0

Dual-invariant vanishing (lem:simplehead): a C-invariant functional on M = K/Φ(K) is zero.