TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedverified 2026-09-24 (gpt-6-sol)

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 generalized Fitting subgroup contains its centralizer

Statement

For a finite group $G$ , $C_{G} (F^{*} (G)) \leq F^{*} (G)$ .

Facts & Assumptions

Given: A finite group $G$ . Write $F = F (G)$ , $E = E (G)$ , $H = F^{*} (G) = F E$ , and $C = C_{G} (H)$ .

[L1]

$F (G)$ is characteristic, normal, and nilpotent; every normal nilpotent subgroup of $G$ lies in $F (G)$ (The Fitting subgroup is nilpotent and is the largest normal nilpotent subgroup of a finite group).

[L2]

A component is a subnormal quasisimple subgroup, and $E (G)$ is generated by all components. Quasisimple means perfect with a simple central quotient (Quasisimple groups, components, and the layer). Conjugation permutes components, so $E (G)$ , and hence $H = F E$ , is normal in $G$ .

[L3]

A minimal normal subgroup of a finite group is characteristically simple (Minimal normal subgroups of finite groups are characteristically simple), and a nontrivial finite characteristically simple group is an internal direct product of isomorphic simple groups (Finite characteristically simple groups are direct products of isomorphic simple groups).

[L4]

A characteristic subgroup of a normal subgroup is normal (If $K$ is characteristic in $N$ and $N$ is normal in $G$ , then $K$ is normal in $G$ ), and the centralizer of a normal subgroup is normal (The centralizer of a normal subgroup is normal).

Proof

technique · induction on $|G|$

1.1base

The result is immediate for $G = 1$ , since $F^{*} (1) = 1$ .

1.2IHL2L4

Assume the result for all finite groups of order smaller than $∣ G ∣$ . By [L2], $H ⊴ G$ , so $C ⊴ G$ by [L4].

2.1L1L2L4step 1.2algebra

The subgroup $F (C)$ is characteristic in $C$ : an automorphism of $C$ permutes its $p$ -cores. Thus $F (C) ⊴ G$ because $C ⊴ G$ ; it is nilpotent by [L1], so $F (C) \leq F (G)$ . Every component of $C$ is subnormal in $G$ , by appending $C ⊴ G$ to its subnormal chain in $C$ . Hence $E (C) \leq E (G)$ and $F^{*} (C) = F (C) E (C) \leq H \cap C .$

3.1givenstep 2.1

Every element of $C$ centralizes every element of $H$ . Consequently $H \cap C \leq Z (C)$ and $F^{*} (C) \leq Z (C)$ .

4.1step 1.2step 2.1step 3.1

If $C < G$ , step 1.2 applied to $C$ gives $C_{C} (F^{*} (C)) \leq F^{*} (C)$ . But step 3.1 makes the left side equal to $C$ . Therefore $C \leq F^{*} (C) \leq H$ , as required.

4.2givenL2step 3.1choose

It remains to consider $C = G$ . Then $H \leq Z (G)$ , in particular $F \leq Z (G)$ and $E \leq Z (G)$ . Suppose $G / F \neq 1$ . Choose a minimal nontrivial normal subgroup $A$ of the finite group $G / F$ , and let $N$ be its inverse image in $G$ . Such an $A$ exists by choosing a subgroup of least positive order among the nontrivial normal subgroups of $G / F$ . Thus $F < N ⊴ G$ and $N / F = A$ .

5.1L1step 4.2

If $A$ is abelian, then $[N, N] \leq F \leq Z (G)$ . Hence the lower central series of $N$ ends after at most two commutator steps, so $N$ is nilpotent. As $N ⊴ G$ , [L1] gives $N \leq F$ , contradicting $F < N$ .

5.2L2L3step 4.2algebra

If $A$ is nonabelian, [L3] writes it as a direct product of isomorphic nonabelian simple groups. Choose a simple direct factor $T ⊴ A$ , and let $N_{T}$ be its inverse image under $N \to N / F = A$ . Then $N_{T} ⊴ N ⊴ G$ , $F \leq Z (G)$ , and $N_{T} / F ≅ T$ . Put $K = [N_{T}, N_{T}]$ . The image of $K$ in $T$ is $[T, T] = T$ , since a nonabelian simple group is perfect. Thus $N_{T} = K F$ . Because $F$ is central, $K = [N_{T}, N_{T}] = [K F, K F] = [K, K],$ so $K$ is perfect. Also $K / (K \cap F) ≅ T$ . Since $K \cap F$ is central in $K$ and $T$ has trivial center, $Z (K) = K \cap F$ ; hence $K / Z (K) ≅ T$ is simple. Finally $K ⊴ N_{T} ⊴ N ⊴ G$ , so $K$ is a component of $G$ .

6.1step 4.2step 5.1step 5.2

Step 5.2 gives $K \leq E \leq H \leq Z (G)$ , whereas $K / Z (K) ≅ T$ is nonabelian. This contradiction rules out the nonabelian case. Together with step 5.1, it follows that $G / F = 1$ . Hence $C = G = F \leq H$ .

7.1discharge-inductionstep 4.1step 6.1∎

Steps 4.1 and 6.1 cover both possibilities for $C$ , proving $C_{G} (F^{*} (G)) \leq F^{*} (G)$ for all finite $G$ .

Depends on

Used by

What the library proves and does not prove about CFSG Remark

Dependency tree · two levels

24 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

Stephen D. Smith, CFSG—A User's Manual, p. 23 (statement, with reference to Aschbacher §31.13) (standard reference, not scraped)