Consequences of Frattini centrality in the minimal kernel

Once R = Phi(K) centralizes K, the Burnside-basis facts for the finite 2-group K become pointwise algebra on the ambient target:

• squares from K lie in Phi(K) and hence centralize K;
• commutators from K lie in Phi(K) and hence centralize K; The commutator-square and fourth-power identities need a separate explicit class-two algebra calculation; this file keeps only the cheap packet inputs that are immediately available from the proved centrality theorem.

These are the local algebraic inputs for the remaining K^4 = 1 and Phi(K)-exponent-two part of lem:collapse.

theorem Q2Presentation.Induction.kernel_square_mem_frattini {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k : p.fst.Y) (hk : k ∈ K.Ksub) : k ^ 2 ∈ kernelFrattini K

Squares of elements of the minimal kernel lie in its literal Frattini layer.

theorem Q2Presentation.Induction.kernel_commutator_mem_frattini {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (a b : p.fst.Y) (ha : a ∈ K.Ksub) (hb : b ∈ K.Ksub) : ⁅a, b⁆ ∈ kernelFrattini K

Commutators of elements of the minimal kernel lie in its literal Frattini layer.

theorem Q2Presentation.Induction.kernel_square_central_in_K {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k : p.fst.Y) (hk : k ∈ K.Ksub) (x : p.fst.Y) : x ∈ K.Ksub → k ^ 2 * x = x * k ^ 2

Squares from K centralize K.

theorem Q2Presentation.Induction.kernel_commutator_central_in_K {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (a b : p.fst.Y) (ha : a ∈ K.Ksub) (hb : b ∈ K.Ksub) (x : p.fst.Y) : x ∈ K.Ksub → ⁅a, b⁆ * x = x * ⁅a, b⁆

Commutators from K centralize K.