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.

The Fitting subgroup is nilpotent and is the largest normal nilpotent subgroup of a finite group

Statement

For every finite group $G$ , $F (G)$ is nilpotent and normal, and every normal nilpotent subgroup of $G$ is contained in $F (G)$ . See The Fitting subgroup $F (G) = \prod_{p} O_{p} (G)$ of a finite group.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

For a finite group $G$ , the Fitting subgroup is $F (G) : = \prod_{p ∣ ∣ G ∣} O_{p} (G),$ the product of its $p$ -cores (def-p-core-of-a-finite-group). The factors are normal, so their finite product is a normal subgroup and does not depend on the order of multiplication. For the trivial group the product is empty and equals $1$ . (The Fitting subgroup $F (G) = \prod_{p} O_{p} (G)$ of a finite group).

[L2]

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

[L3]

Let $N_{0}, \dots, N_{r - 1} ⊴ G$ . They form an internal direct product of $G$ if and only if every $g \in G$ has a unique expression $g = n_{0} \dots n_{r - 1}$ with $n_{i} \in N_{i}$ , equivalently the multiplication map $\prod_{i < r} N_{i} \to G$ is an isomorphism. (Internal direct products are external direct products, equivalently every element has a unique factorisation).

[L4]

If $K$ is characteristic in $N$ and $N ⊴ G$ , then $K ⊴ G$ . (If $K$ is characteristic in $N$ and $N$ is normal in $G$ , then $K$ is normal in $G$ ).

[L5]

The $p$ -core $O_{p} (G)$ is the unique largest normal $p$ -subgroup of the finite group $G$ . (The $p$ -core $O_{p} (G)$ as the largest normal $p$ -subgroup).

[L6]

Every $p$ -subgroup of a finite group is contained in a Sylow $p$ -subgroup, and all Sylow $p$ -subgroups are conjugate. (Sylow II: in a finite group every $p$ -subgroup lies in a conjugate of any Sylow $p$ -subgroup, and the Sylow $p$ -subgroups form a single conjugacy class).

[L7]

The order of a subgroup of a finite group divides the order of the group. (Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

Proof

technique · direct

1.1

For distinct primes $p$ and $q$ , normality puts every commutator of an element of $O_{p} (G)$ with an element of $O_{q} (G)$ in $O_{p} (G) \cap O_{q} (G)$ . By [L7], the order of this intersection divides powers of both $p$ and $q$ , so the intersection is trivial and the two $p$ -cores centralize one another. If a product $\prod_{p} x_{p}$ with $x_{p} \in O_{p} (G)$ equals $1$ , then for each $p$ the element $x_{p}$ lies both in the $p$ -group $O_{p} (G)$ and in the commuting product of the other prime-power groups; its order divides two coprime numbers and is therefore $1$ . Thus product expressions are unique, so [L3] identifies $F (G)$ with the internal direct product of the $p$ -cores. The direct-product order shows that $O_{p} (G)$ is the Sylow $p$ -subgroup of $F (G)$ ; [L2] makes $F (G)$ nilpotent, and [L1] gives its normality in $G$ .

L1L2L3L5L7givenalgebra

2.1

If $N ⊴ G$ is nilpotent, [L2] makes each Sylow subgroup normal in $N$ , and conjugacy [L6] makes it unique. Automorphisms preserve orders, so this unique Sylow subgroup is characteristic in $N$ ; [L4] makes it normal in $G$ , and the maximality clause [L5] puts it in the corresponding $p$ -core.

L2L4L5L6step 1.1givenalgebra

3.1

By [L2], $N$ is the product of its Sylow subgroups, and step 2.1 puts every factor in the corresponding $p$ -core. Hence $N \leq F (G)$ .

L1L2step 2.1given

4.1

For $G = 1$ the family of $p$ -cores is empty and $F (G) = 1$ , which is nilpotent and contains every normal nilpotent subgroup. This proves the stated claim.

L1step 1.1step 3.1givenalgebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 103 results over 17 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

David A. Craven, Finite Group Theory, Sections 1.4 and 2.3 (standard reference, not scraped)