theorem Q2Presentation.Induction.kernel_frattini_bot {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) : frattini ↥K.Ksub = ⊥

Under R = 1 the kernel's Frattini subgroup is trivial.

theorem Q2Presentation.Induction.kernel_sq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (n : p.fst.Y) : n ∈ K.Ksub → n * n = 1

Under R = 1 the kernel has exponent 2.

theorem Q2Presentation.Induction.kernel_comm {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (a b : p.fst.Y) : a ∈ K.Ksub → b ∈ K.Ksub → a * b = b * a

Under R = 1 the kernel is abelian.

theorem Q2Presentation.Induction.mstage_theta {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (n : p.fst.Y) : n ∈ K.Ksub → p.fst.thetaY n = 1

The decoration kills the kernel.

def Q2Presentation.Induction.mstageKernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) : Lifting.ElementaryKernel p.fst

The mstage consumer kernel, bundled for the cocycle bridge.

Equations

• Q2Presentation.Induction.mstageKernel chief K hR = { N := K.Ksub, normal := ⋯, le_LY := ⋯, theta_dies := ⋯, comm := ⋯, exp2 := ⋯ }