Documentation

Q2Presentation.Induction.Section7FrattiniElementaryLayer

The literal Frattini layer is elementary #

This is the final elementary-layer step in the corrected lem:collapse proof. We work inside the manuscript kernel K and show that the Frattini subgroup is contained in the subgroup generated by squares and commutators. The already-proven fourth-power and commutator-square identities then make every element of Phi(K) square to one.

The square/commutator layer inside `K` #

def Q2Presentation.Induction.Section7FrattiniElementaryLayer.kernelSqCommSet {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) :

The square/commutator generating set inside the kernel K.

Equations

Q2Presentation.Induction.Section7FrattiniElementaryLayer.kernelSqCommSet chief K = {z : ↥K.Ksub | ∃ (a : ↥K.Ksub), z = a ^ 2} ∪ {z : ↥K.Ksub | ∃ (a : ↥K.Ksub) (b : ↥K.Ksub), z = ⁅a, b⁆}

Instances For

def Q2Presentation.Induction.Section7FrattiniElementaryLayer.kernelSqCommSubgroup {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) :

Subgroup ↥K.Ksub

The subgroup of K generated by squares and commutators.

Equations

Q2Presentation.Induction.Section7FrattiniElementaryLayer.kernelSqCommSubgroup chief K = Subgroup.closure (Q2Presentation.Induction.Section7FrattiniElementaryLayer.kernelSqCommSet chief K)

Instances For

theorem Q2Presentation.Induction.Section7FrattiniElementaryLayer.kernelSqCommSet_subset_frattini {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) :

kernelSqCommSet chief K ⊆ ↑(frattini ↥K.Ksub)

theorem Q2Presentation.Induction.Section7FrattiniElementaryLayer.kernelSqCommSubgroup_le_frattini {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) :

kernelSqCommSubgroup chief K ≤ frattini ↥K.Ksub

theorem Q2Presentation.Induction.Section7FrattiniElementaryLayer.kernelSqCommSet_conj_stable {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y z : ↥K.Ksub) :

z ∈ kernelSqCommSet chief K → y * z * y⁻¹ ∈ kernelSqCommSet chief K

theorem Q2Presentation.Induction.Section7FrattiniElementaryLayer.kernelSqCommSubgroup_normal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) :

(kernelSqCommSubgroup chief K).Normal

Burnside containment `Phi(K) <= <squares, commutators>` #

theorem Q2Presentation.Induction.Section7FrattiniElementaryLayer.frattini_le_kernelSqCommSubgroup {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) :

frattini ↥K.Ksub ≤ kernelSqCommSubgroup chief K

Exponent two on the generated layer and on `Phi(K)` #

theorem Q2Presentation.Induction.Section7FrattiniElementaryLayer.kernelSqCommSubgroup_commute {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {x y : ↥K.Ksub} (hx : x ∈ kernelSqCommSubgroup chief K) (_hy : y ∈ kernelSqCommSubgroup chief K) :

x * y = y * x

theorem Q2Presentation.Induction.Section7FrattiniElementaryLayer.kernelSqCommSubgroup_square_eq_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : ↥K.Ksub) :

x ∈ kernelSqCommSubgroup chief K → x ^ 2 = 1

theorem Q2Presentation.Induction.Section7FrattiniElementaryLayer.kernelFrattini_square_eq_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (r : p.fst.Y) (hr : r ∈ kernelFrattini K) :

r ^ 2 = 1

The literal Frattini subgroup R = Phi(K) has exponent two.