def Q2Presentation.Induction.xrKernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Lifting.ElementaryKernel p.fst

The Frattini layer R = Φ(K) as an elementary kernel (lem:collapse): normal, inside L_Y, θ-dead, elementary abelian.

Equations

• Q2Presentation.Induction.xrKernel chief K = { N := Q2Presentation.Induction.kernelFrattini K, normal := ⋯, le_LY := ⋯, theta_dies := ⋯, comm := ⋯, exp2 := ⋯ }

theorem Q2Presentation.Induction.card_NAdd_xr {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Nat.card (Lifting.NAdd (xrKernel chief K)) = 2 ^ Module.finrank (ZMod 2) (Lifting.NAdd (xrKernel chief K))

The Frattini-layer module cardinality is 2^{dim R}.