The Frattini quotient of a finite 2-group is elementary abelian

The Burnside-basis core needed by the §7 concrete tower (lem:collapse uses Φ(K) = K²[K,K], manuscript l.3610): for a finite 2-group G,

• every maximal subgroup is normal (IsPGroup.coatom_normal) with quotient of exponent 2 — so squares and commutators lie in every maximal subgroup, hence in frattini G (IsPGroup.sq_mem_frattini, IsPGroup.commutatorElement_mem_frattini);
• hence G ⧸ frattini G is elementary abelian: commutative (IsPGroup.frattiniQuotientCommGroup) of exponent 2 (IsPGroup.frattiniQuotient_sq_eq_one), so its additive form is a ZMod 2-module (IsPGroup.frattiniQuotientModule).

Everything here is proved — no axioms. Mathlib (this toolchain) has frattini as the subgroup-lattice radical but no Burnside basis theorem, so we derive what the tower needs directly.

theorem Q2Presentation.Induction.IsPGroup.mem_frattini_of_forall_coatom {G : Type u_1} [Group G] {x : G} (h : ∀ (M : Subgroup G), IsCoatom M → x ∈ M) : x ∈ frattini G

Membership in the Frattini subgroup from membership in every maximal subgroup (the radical is the infimum of the coatoms).

theorem Q2Presentation.Induction.IsPGroup.coatom_normal {G : Type u_1} [Group G] [Finite G] {p : ℕ} [Fact (Nat.Prime p)] (hG : IsPGroup p G) {M : Subgroup G} (hM : IsCoatom M) : M.Normal

In a finite p-group, every maximal subgroup is normal (nilpotency + the normalizer condition).

theorem Q2Presentation.Induction.IsPGroup.quotient_coatom_no_proper {G : Type u_1} [Group G] {M : Subgroup G} [M.Normal] (hM : IsCoatom M) (H : Subgroup (G ⧸ M)) : H = ⊥ ∨ H = ⊤

Every subgroup of the quotient by a maximal subgroup is trivial or everything (the correspondence theorem collapses the interval [M, ⊤] = {M, ⊤}).

theorem Q2Presentation.Induction.IsPGroup.sq_eq_one_and_comm_of_no_proper {Q : Type u_2} [Group Q] [Finite Q] (hQ : ∀ (H : Subgroup Q), H = ⊥ ∨ H = ⊤) (horder : ∀ (x : Q), ∃ (n : ℕ), orderOf x = 2 ^ n) : (∀ (x : Q), x ^ 2 = 1) ∧ ∀ (x y : Q), x * y = y * x

In a finite group all of whose subgroups are ⊥ or ⊤, in which every element has 2-power order, every square is trivial and any two elements commute.

theorem Q2Presentation.Induction.IsPGroup.quotient_orderOf_two_pow {G : Type u_1} [Group G] (hG : IsPGroup 2 G) {M : Subgroup G} [M.Normal] (x : G ⧸ M) : ∃ (n : ℕ), orderOf x = 2 ^ n

Elements of any quotient of a 2-group have 2-power order.

theorem Q2Presentation.Induction.IsPGroup.sq_mem_coatom {G : Type u_1} [Group G] [Finite G] (hG : IsPGroup 2 G) {M : Subgroup G} (hM : IsCoatom M) (x : G) : x ^ 2 ∈ M

Squares lie in every maximal subgroup of a finite 2-group.

theorem Q2Presentation.Induction.IsPGroup.commutator_mem_coatom {G : Type u_1} [Group G] [Finite G] (hG : IsPGroup 2 G) {M : Subgroup G} (hM : IsCoatom M) (x y : G) : ⁅x, y⁆ ∈ M

Commutators lie in every maximal subgroup of a finite 2-group.

theorem Q2Presentation.Induction.IsPGroup.sq_mem_frattini {G : Type u_1} [Group G] [Finite G] (hG : IsPGroup 2 G) (x : G) : x ^ 2 ∈ frattini G

Squares lie in the Frattini subgroup of a finite 2-group.

theorem Q2Presentation.Induction.IsPGroup.commutatorElement_mem_frattini {G : Type u_1} [Group G] [Finite G] (hG : IsPGroup 2 G) (x y : G) : ⁅x, y⁆ ∈ frattini G

Commutators lie in the Frattini subgroup of a finite 2-group.

def Q2Presentation.Induction.IsPGroup.frattiniQuotientCommGroup {G : Type u_1} [Group G] [Finite G] (hG : IsPGroup 2 G) : CommGroup (G ⧸ frattini G)

The Frattini quotient of a finite 2-group is commutative.

Equations

• Q2Presentation.Induction.IsPGroup.frattiniQuotientCommGroup hG = { toGroup := QuotientGroup.Quotient.group (frattini G), mul_comm := ⋯ }

theorem Q2Presentation.Induction.IsPGroup.frattiniQuotient_sq_eq_one {G : Type u_1} [Group G] [Finite G] (hG : IsPGroup 2 G) (x : G ⧸ frattini G) : x ^ 2 = 1

The Frattini quotient of a finite 2-group has exponent 2.

def Q2Presentation.Induction.IsPGroup.frattiniQuotientModule {G : Type u_1} [Group G] [Finite G] (hG : IsPGroup 2 G) : Module (ZMod 2) (Additive (G ⧸ frattini G))

The additive Frattini quotient of a finite 2-group as a ZMod 2-module.

Equations

• Q2Presentation.Induction.IsPGroup.frattiniQuotientModule hG = AddCommGroup.zmodModule ⋯