Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-17
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.

Sylow and maximal-subgroup characterizations of finite nilpotence

Statement

For a finite group G, the following are equivalent: G is nilpotent; every Sylow subgroup is normal; G is the internal direct product of its Sylow subgroups; and every maximal subgroup of G is normal. See A finite group is nilpotent if and only if all Sylow subgroups are normal, if and only if it is their internal direct product.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

For a finite group G, the following are equivalent: G is nilpotent; every Sylow subgroup is normal; and G is the internal direct product of its Sylow subgroups. (A finite group is nilpotent if and only if all Sylow subgroups are normal, if and only if it is their internal direct product).

[L2]

Every maximal proper subgroup of a finite nilpotent group is normal and has prime index. (Maximal subgroups of finite nilpotent groups are normal of prime index).

[L3]

Let G be finite and let Φ(G)NG. Then N is nilpotent if and only if N/Φ(G) is nilpotent. In particular, G is nilpotent if and only if G/Φ(G) is nilpotent. (Nilpotence lifts over the Frattini subgroup of a finite group).

[L4]

For a finite group G, the Frattini subgroup is Φ(G):={MG:M is maximal proper}. If G=1, the family is empty and its intersection inside G is G itself. Thus Φ(1)=1. (The Frattini subgroup Φ(G) as the intersection of the maximal subgroups of a finite group).

[L5]

Let N0,,Nr1G. The following are equivalent: the Ni form an internal direct product of G; every gG has a unique expression g=n0nr1 with niNi; and the multiplication map μ:i<rNiG is an isomorphism. These statements include the empty family and the one-factor case. (Internal direct products are external direct products, equivalently every element has a unique factorisation).

[L6]

If a prime p divides the order of a finite group H, then H contains an element, and hence a subgroup, of order p. (Cauchy's theorem: if a prime p divides G, then G has an element of order p).

[L7]

Every finite p-group is nilpotent, including the trivial group. (Every finite p-group is nilpotent).

[L8]

Every subgroup and every quotient of a nilpotent group is nilpotent, and every finite direct product of nilpotent groups is nilpotent. (Subgroups, quotients, and finite direct products of nilpotent groups are nilpotent).

[L9]

For KG, subgroups of G/K correspond to subgroups of G containing K, and the correspondence preserves inclusion and normality. (Correspondence theorem: subgroups of G/N correspond to subgroups of G containing N, with normality preserved).

Proof

technique · direct
1.1

By [L1], the first three conditions are equivalent, and [L2] proves that any of them implies normality of every maximal subgroup.

L1L2given
2.1

Conversely, assume every maximal subgroup M is normal. The diagonal map G/Φ(G)MG/M is injective because its kernel is the intersection [L4]. By [L9] and maximality, each nontrivial quotient G/M has no nontrivial proper subgroup. If p divides its order, [L6] supplies a subgroup of order p, which must be all of G/M. Thus each factor has prime order and is nilpotent by [L7].

L4L6L7L9step 1.1givenalgebra
3.1

The finite product in step 2.1 is nilpotent and so is its subgroup G/Φ(G) by [L8]. The lifting theorem [L3] now makes G nilpotent.

L3L8step 2.1
4.1

This proves the reverse implication and hence all four equivalences.

step 1.1step 3.1
5.1

If the family of maximal subgroups is empty, finiteness forces G=1; the diagonal target is then the empty product 1, and every condition holds.

L1L4L5L7step 4.1given

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 130 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources