Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck 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.

Maximal subgroups of a finite p-group are the inverse images of Frattini hyperplanes

Statement

Let π:P→E:=P/Φ(P) be the quotient map. The maximal subgroups (Maximal proper subgroups) of a finite p-group P are exactly the inverse images of codimension-one subgroups of E. Equivalently, they are the subgroups

π−1(ker⁡λ)=ker⁡(λ∘π)

for nonzero Fp-linear homomorphisms λ:E→Z/p (Monoid homomorphism and group homomorphism).

Facts & Assumptions

Given: A finite p-group P and quotient map π:P→E:=P/Φ(P).

[F1]

The Frattini subgroup is the intersection of the maximal proper subgroups, so Φ(P)≤M for every maximal subgroup M (The Frattini subgroup Φ(G) as the intersection of the maximal subgroups of a finite group).

[L1]

The quotient E=P/Φ(P) is elementary abelian (The Frattini quotient is the largest elementary abelian quotient of a finite p-group).

[L2]

Every independent subset extends to a basis, every spanning subset contains a basis, and all bases have equal finite size (Finite elementary abelian p-groups have bases, basis extension, and a well-defined dimension, Fp-spanning sets, independence, and bases in an elementary abelian p-group).

[L3]

Subgroups of E correspond inclusion-preservingly to subgroups of P containing Φ(P) (Correspondence theorem: subgroups of G/N correspond to subgroups of G containing N, with normality preserved).

Proof

technique · direct
1.1givenF1L1L2L3algebra

If M is maximal in P, [F1] and [L3] make M/Φ(P) maximal proper in E. Choose a basis of this subgroup and extend it by [L2] to a basis of E. Maximality permits exactly one added basis vector, since two would create a proper intermediate span. Thus M/Φ(P) has codimension one.

2.1step 1.1L2L3givenalgebra

The coordinate of the omitted basis vector defines a nonzero linear homomorphism E→Z/p whose kernel is M/Φ(P). Conversely, let λ:E→Z/p be linear and nonzero and choose v∈E with λ(v)=1. Every x∈E splits as x=(x−λ(x)v)+λ(x)v with the first summand in ker⁡λ, and v∉ker⁡λ, so a basis of ker⁡λ together with v spans E and is independent; it is therefore a basis of E by [L2], and ker⁡λ has codimension one. Any subgroup strictly between ker⁡λ and E would contain some y with λ(y)≠0 and hence a scalar multiple of y equal to v modulo ker⁡λ, so it would be all of E; thus ker⁡λ is maximal proper and [L3] makes its inverse image maximal in P.

3.1step 1.1step 2.1L3∎

The quotient and inverse-image maps in [L3] are inverse, so steps 1.1 and 2.1 give the stated classification. The trivial group has neither maximal subgroups nor nonzero linear homomorphisms.

Depends on

Used by

Dependency tree · two levels

29 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