# 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.

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)

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

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.

When `G`

is finite, the Frattini subgroup is nilpotent.