The Frattini subgroup

We give the definition of the Frattini subgroup of a group, and three elementary results:

• The Frattini subgroup is characteristic.
• If every subgroup of a group is contained in a maximal subgroup, then the Frattini subgroup consists of the non-generating elements of the group.
• The Frattini subgroup of a finite group is nilpotent.

def frattini (G : Type u_1) [Group G] : Subgroup G

The Frattini subgroup of a group is the intersection of the maximal subgroups.

Equations

• frattini G = Order.radical (Subgroup G)

theorem frattini_le_coatom {G : Type u_1} [Group G] {K : Subgroup G} (h : IsCoatom K) : frattini G ≤ K

theorem frattini_le_comap_frattini_of_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] {φ : G →* H} (hφ : Function.Surjective ⇑φ) : frattini G ≤ Subgroup.comap φ (frattini H)

instance frattini_characteristic {G : Type u_1} [Group G] : (frattini G).Characteristic

The Frattini subgroup is characteristic.

Equations

• ⋯ = ⋯

theorem frattini_nongenerating {G : Type u_1} [Group G] [IsCoatomic (Subgroup G)] {K : Subgroup G} (h : K ⊔ frattini G = ⊤) : K = ⊤

The Frattini subgroup consists of "non-generating" elements in the following sense:

If a subgroup together with the Frattini subgroup generates the whole group, then the subgroup is already the whole group.

theorem frattini_nilpotent {G : Type u_1} [Group G] [Finite G] : Group.IsNilpotent ↥(frattini G)

When G is finite, the Frattini subgroup is nilpotent.