Basic facts about the literal Frattini layer of the corrected Section 7 kernel #
These two facts are needed by several downstream Section 7 files. Keeping them
separate avoids importing the heavier raw-tower packet file just to obtain normality
and containment of Φ(K).
theorem
Q2Presentation.Induction.kernelFrattini_normal
{p : FramedPair}
{chief : NonScalarChiefFactor p}
(K : KernelMinimal chief)
:
(kernelFrattini K).Normal
The literal Frattini layer Φ(K) ≤ Y is normal in Y (characteristic in the
normal subgroup K).
theorem
Q2Presentation.Induction.kernelFrattini_le
{p : FramedPair}
{chief : NonScalarChiefFactor p}
(K : KernelMinimal chief)
:
The literal Frattini layer is contained in the kernel.