The Burnside converse: Φ(G) ≤ N for elementary abelian quotients

The second half of the Burnside basis theorem needed by lem:collapse (R = Φ(K) ≤ K ∩ S because K/(K∩S) embeds in the elementary abelian chief factor, manuscript l.3674): if G/N is elementary abelian (commutative of exponent 2), then frattini G ≤ N.

Proof (no duals needed): if x ∉ N, take a subgroup M of Q = G/N maximal among those missing x̄ (finiteness). Then M ⊔ ⟨x̄⟩ = ⊤ — otherwise a point q outside gives M ⊔ ⟨q⟩ still missing x̄ (exponent 2 splits ⟨q⟩ = {1, q}, and x̄ = m·q would force q = m⁻¹x̄ ∈ M ⊔ ⟨x̄⟩), contradicting maximality. Hence the preimage of M in G is a coatom (anything strictly larger contains N, so corresponds to a subgroup of Q strictly above M, which must contain x̄, hence contain M ⊔ ⟨x̄⟩ = ⊤), so it contains frattini G — but it misses x.

Everything here is proved — no axioms.

theorem Q2Presentation.Induction.frattini_le_of_elementary_quotient {G : Type u_1} [Group G] [Finite G] {N : Subgroup G} [N.Normal] (hcomm : ∀ (x y : G ⧸ N), x * y = y * x) (hsq : ∀ (x : G ⧸ N), x ^ 2 = 1) : frattini G ≤ N

The Burnside converse: if G/N is commutative of exponent 2, then frattini G ≤ N.