TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Frattini quotient is the largest elementary abelian quotient of a finite $p$ -group

Statement

For a finite $p$ -group $P$ , the quotient $P / Φ (P)$ is elementary abelian (Elementary abelian $p$ -groups, The quotient group $G / N$ and coset product $(g N) (h N) = g h N$ ), and for $N ⊴ P$ the quotient $P / N$ is elementary abelian if and only if $Φ (P) \leq N$ .

Facts & Assumptions

Given: A finite $p$ -group $P$ , its Frattini subgroup $Φ (P)$ , and a normal subgroup $N ⊴ P$ .

[F1]

For a finite group $G$ , $Φ (G)$ is the intersection of all maximal proper subgroups; for $G = 1$ the intersection is $G$ (The Frattini subgroup $Φ (G)$ as the intersection of the maximal subgroups of a finite group).

[L1]

Every finite $p$ -group is nilpotent; every maximal proper subgroup of a finite nilpotent group is normal and has prime index; Lagrange's theorem makes that index divide $∣ P ∣ = p^{n}$ , so the index is $p$ ; and every group of prime order is cyclic (Every finite $p$ -group is nilpotent, Maximal subgroups of finite nilpotent groups are normal of prime index, Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ , A finite group of prime order is cyclic and every nonidentity element generates it).

[L2]

Every finite elementary abelian $p$ -group has its canonical $F_{p}$ -linear structure, has a basis, and every independent subset extends to a basis (An elementary abelian $p$ -group has a canonical $F_{p}$ -vector-space structure, $F_{p}$ -spanning sets, independence, and bases in an elementary abelian $p$ -group, Finite elementary abelian $p$ -groups have bases, basis extension, and a well-defined dimension).

[L3]

For $N ⊴ G$ , subgroups of $G / N$ correspond inclusion-preservingly to subgroups of $G$ containing $N$ (Correspondence theorem: subgroups of $G / N$ correspond to subgroups of $G$ containing $N$ , with normality preserved).

[L4]

For every finite group $G$ , $Φ (G)$ is characteristic and hence normal (The Frattini subgroup of a finite group is characteristic).

Proof

technique · direct

1.1

By [L1], each maximal subgroup $M$ of $P$ is normal with $P / M$ cyclic of order $p$ . Hence every commutator and every $p$ th power lies in every $M$ . Their images are therefore trivial modulo the normal subgroup $Φ (P)$ from [L4] and [F1], so $P / Φ (P)$ is abelian of exponent at most $p$ , and thus elementary abelian, including the trivial quotient.

givenF1L1L4algebra

1.2

For the forward direction of the kernel criterion, suppose $P / N$ is elementary abelian and let $x \notin N$ . The nonzero vector $x N$ extends by [L2] to a basis of $P / N$ . The span of the other basis vectors is a maximal proper subgroup not containing $x N$ ; by [L3], its preimage is a maximal subgroup of $P$ containing $N$ but not $x$ . Thus $x \notin Φ (P)$ , and so $Φ (P) \leq N$ .

givenL2L3algebra

2.1

For the reverse direction, suppose $Φ (P) \leq N$ . Step 1.1 places every commutator and every $p$ th power of $P$ inside $Φ (P)$ and hence inside $N$ , so $P / N$ is abelian and every element of it has $p$ th power the identity. It is therefore elementary abelian, including the trivial quotient $N = P$ . Together with step 1.2 this proves the iff.

step 1.1step 1.2F1algebra∎

Depends on

Used by

A finite p-group has trivial Frattini subgroup exactly when it is elementary abelian Corollary
Every element outside Φ(P) belongs to a minimal generating set of P Corollary
Maximal subgroups of a finite p-group are the inverse images of Frattini hyperplanes Corollary
The generator rank d(P) of a finite p-group Definition
Automorphisms act linearly on the Frattini quotient Theorem
Burnside Basis Theorem Theorem
Φ(P)=P'Pᵖ for a finite p-group Theorem

Dependency tree · two levels

53 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

D. A. Craven, The Theory of p-Groups, Proposition 2.24 (standard reference, not scraped)
M. van Beek, Topics in Finite p-Groups, Lemma 3.4 (standard reference, not scraped)

The Frattini quotient is the largest elementary abelian quotient of a finite pp-group