theorem Q2Presentation.Induction.ker_invariant_of_invariant {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (f : Module.Dual (ZMod 2) (Lifting.NAdd (mstageKernel chief K hR))) (hf : ∀ (y : p.fst.Y) (m : Lifting.NAdd (mstageKernel chief K hR)), f ((Lifting.conjEndN (mstageKernel chief K hR) y) m) = f m) (y : p.fst.Y) (m : Lifting.NAdd (mstageKernel chief K hR)) (hm : m ∈ LinearMap.ker f) : (Lifting.conjEndN (mstageKernel chief K hR) y) m ∈ LinearMap.ker f

The kernel of an invariant functional is a conjugation-invariant submodule.

theorem Q2Presentation.Induction.invariant_dual_eq_zero_of_radical_vanish {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (f : Module.Dual (ZMod 2) (Lifting.NAdd (mstageKernel chief K hR))) (hf : ∀ (y : p.fst.Y) (m : Lifting.NAdd (mstageKernel chief K hR)), f ((Lifting.conjEndN (mstageKernel chief K hR) y) m) = f m) (hfW : ∀ w ∈ radicalW chief K hR, f w = 0) : f = 0

Invariant duals reduce to the radical layer: an invariant dual vanishing on W vanishes.