The chief factor is elementary abelian, and R ≤ K ∩ S

lem:collapse steps (i)–(ii) (manuscript l.3674: "Since K/(K∩S) ≅ V is elementary abelian, R ≤ K∩S"):

• chief_sq_comm_mem_lower — squares and commutators of P lie in S: the Y-normal subgroup S ⊔ ⟨sq, comm⟩ is S or P by chief-ness, and = P would put every element of the nontrivial finite 2-group P/S inside its Frattini subgroup (Burnside forward) — impossible;
• kernelFrattini_le_lower — hence K/(K∩S) is elementary abelian, so by the Burnside converse R = Φ(K) ≤ K ∩ S ≤ S.

Everything here is proved — no axioms.

A conjugation-stable generating set closes to a normal subgroup

theorem Q2Presentation.Induction.closure_normal_of_conj_stable {G : Type u_1} [Group G] {S : Set G} (hS : ∀ (y z : G), z ∈ S → y * z * y⁻¹ ∈ S) : (Subgroup.closure S).Normal

The closure of a conjugation-stable set is normal.

Squares and commutators of the chief interval

def Q2Presentation.Induction.chiefSqCommSet {p : FramedPair} (chief : NonScalarChiefFactor p) : Set p.fst.Y

The generating set: squares and commutators of the upper term.

Equations

• Q2Presentation.Induction.chiefSqCommSet chief = {z : p.fst.Y | ∃ a ∈ chief.upper, z = a ^ 2} ∪ {z : p.fst.Y | ∃ a ∈ chief.upper, ∃ b ∈ chief.upper, z = ⁅a, b⁆}

theorem Q2Presentation.Induction.chiefSqCommSet_subset {p : FramedPair} {chief : NonScalarChiefFactor p} : chiefSqCommSet chief ⊆ ↑chief.upper

theorem Q2Presentation.Induction.chiefSqCommSet_conj_stable {p : FramedPair} {chief : NonScalarChiefFactor p} (y z : p.fst.Y) : z ∈ chiefSqCommSet chief → y * z * y⁻¹ ∈ chiefSqCommSet chief

theorem Q2Presentation.Induction.chief_upper_isTwoGroup {p : FramedPair} (chief : NonScalarChiefFactor p) : IsPGroup 2 ↥chief.upper

The upper term is a finite 2-group.

theorem Q2Presentation.Induction.chief_sq_comm_mem_lower {p : FramedPair} {chief : NonScalarChiefFactor p} : (∀ a ∈ chief.upper, a ^ 2 ∈ chief.lower) ∧ ∀ a ∈ chief.upper, ∀ b ∈ chief.upper, ⁅a, b⁆ ∈ chief.lower

Squares and commutators of the chief interval lie in the lower term.

R ≤ K ∩ S

theorem Q2Presentation.Induction.kernelFrattini_le_lower {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : kernelFrattini K ≤ chief.lower

R = Φ(K) ≤ S (lem:collapse step (ii)): K/(K∩S) is elementary abelian (squares and commutators of K ≤ P land in S), so the Burnside converse pins the Frattini subgroup inside K ∩ S.