TheoremStatement: AI-adaptedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 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.

Philip Hall: in a finite solvable group the Fitting subgroup contains its own centralizer

Statement

Let $G$ be a finite solvable group. Then $C_{G} (F (G)) \leq F (G)$ .

Facts & Assumptions

Given: A finite solvable group $G$ . Write $F : = F (G)$ and $C : = C_{G} (F)$ .

[L1]

For a finite group $G$ the Fitting subgroup is $F (G) = \prod_{p ∣ ∣ G ∣} O_{p} (G)$ ; and if $A, B ⊴ G$ , then $A B$ is a subgroup, is normal, and satisfies $A B = B A$ (The Fitting subgroup $F (G) = \prod_{p} O_{p} (G)$ of a finite group).

[L2]

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

[L3]

$C_{G} (H) = {g \in G : g h = h g for every h \in H}$ , a subgroup of $G$ (The centralizer $C_{G} (H)$ of a subgroup).

[L4]

If $N ⊴ G$ , then $C_{G} (N) ⊴ G$ (The centralizer of a normal subgroup is normal).

[L5]

Every subgroup and every quotient of a solvable group is solvable; no finiteness hypothesis is required (Subgroups and quotients of solvable groups are solvable).

[L6]

For $N ⊴ G$ , the maps $H \mapsto H / N$ and $K \mapsto π^{- 1} (K)$ are inverse inclusion-preserving bijections between the subgroups $H$ with $N \leq H \leq G$ and the subgroups $K \leq G / N$ ; they preserve normality (Correspondence theorem: subgroups of $G / N$ correspond to subgroups of $G$ containing $N$ , with normality preserved).

[L7]

Let $Q$ be a solvable group and let $N ⊴ Q$ with $N \neq 1$ . Then $N$ contains a subgroup $A \neq 1$ that is abelian and normal in $Q$ (A nontrivial normal subgroup of a solvable group contains a nontrivial abelian subgroup normal in the whole group).

[L8]

Let $A, B, C \leq G$ with $A \leq C$ . If $A B$ is a subgroup of $G$ , then $A (B \cap C) = A B \cap C$ (Dedekind's modular law for subgroup products).

[L9]

Let $N ⊴ G$ . Then $G / N$ is abelian if and only if $[G, G] \subseteq N$ ( $G / N$ is abelian if and only if $[G, G] \subseteq N$ ).

[L10]

Let $G$ be a group and let $N$ be a nonempty family of normal subgroups of $G$ . Then $⋂_{N \in N} N$ is a normal subgroup of $G$ (The intersection of a nonempty family of normal subgroups is normal).

[L11]

A group $G$ is nilpotent if $Z_{c} (G) = G$ for some $c \in N$ , where $(Z_{r} (G))$ is its upper central series (Nilpotent groups and nilpotency class).

[L12]

The upper central series begins with $Z_{0} (G) = 1$ and satisfies $Z_{r + 1} (G) / Z_{r} (G) = Z (G / Z_{r} (G))$ ; in particular $Z_{1} (G) = Z (G)$ (The upper central series).

[L13]

$Z (G) = {z \in G : z g = g z for every g \in G}$ (The center $Z (G)$ of a group).

[L14]

For every group $G$ , the center $Z (G)$ is a normal subgroup of $G$ (The center of a group is a normal subgroup).

Proof

technique · contradiction

1.1

By [L2], $F ⊴ G$ and every normal nilpotent subgroup of $G$ is contained in $F$ .

L2given

1.2

Assume towards a contradiction that $C \leq̸ F$ .

assume-contragiven

2.1

$F$ is normal in $G$ , so $C = C_{G} (F) ⊴ G$ by [L4].

L4step 1.1

3.1

$C$ and $F$ are both normal in $G$ , so by [L1] the product $C F$ is a subgroup of $G$ , is normal in $G$ , and satisfies $C F = F C$ . Since the identity lies in $C$ , also $F \leq C F$ .

L1step 1.1step 2.1

4.1

$G$ is solvable, so its quotient $G / F$ is solvable by [L5]; and $C F ⊴ G$ with $F \leq C F$ , so $C F / F ⊴ G / F$ by [L6]. By step 1.2 some $c \in C$ lies outside $F$ , so $c F \neq F$ and $C F / F \neq 1$ .

L5L6givenstep 1.2step 3.1

5.1

Apply [L7] to the solvable group $G / F$ and its nontrivial normal subgroup $C F / F$ : there is a subgroup $\overset{ˉ}{A} \neq 1$ of $C F / F$ that is abelian and normal in $G / F$ . Let $A$ be its preimage under $G \to G / F$ . By [L6], $F \leq A \leq C F$ , $A ⊴ G$ , and $A / F = \overset{ˉ}{A}$ is nontrivial and abelian.

L6L7step 4.1

6.1

$F ⊴ A$ and $A / F$ is abelian, so $[A, A] \leq F$ by [L9].

L9step 5.1

6.2

Put $D : = C \cap A$ . Both $C$ and $A$ are normal in $G$ , so $D ⊴ G$ by [L10].

L10step 2.1step 5.1

7.1

Apply [L8] with its $A : = F$ , its $B : = C$ and its $C : = A$ . Its hypotheses hold: $F \leq A$ by step 5.1, and $F C = C F$ is a subgroup by step 3.1. Hence $F (C \cap A) = F C \cap A$ , and $A \leq C F = F C$ makes the right-hand side equal to $A$ . Therefore $A = F D$ .

L8step 3.1step 5.1step 6.2

7.2

$D \leq A$ , so $[D, D] \leq [A, A] \leq F$ by step 6.1. Also $D \leq C = C_{G} (F)$ , so by [L3] every element of $D$ commutes with every element of $F$ , in particular with every element of $[D, D]$ . Since $[D, D] \leq D$ , this says $[D, D] \leq Z (D)$ by [L13].

L3L13step 6.1step 6.2

8.1

$Z (D) ⊴ D$ by [L14], and $[D, D] \leq Z (D)$ , so $D / Z (D)$ is abelian by [L9].

L9L14step 7.2

9.1

By [L12], $Z_{1} (D) = Z (D)$ and $Z_{2} (D) / Z_{1} (D) = Z ⁣ (D / Z_{1} (D))$ . Step 8.1 makes $D / Z_{1} (D)$ abelian, and the center of an abelian group is the whole group by [L13], so $Z_{2} (D) / Z_{1} (D) = D / Z_{1} (D)$ and hence $Z_{2} (D) = D$ . By [L11], $D$ is nilpotent.

L11L12L13step 8.1

10.1

$D$ is a normal nilpotent subgroup of $G$ by steps 6.2 and 9.1, so $D \leq F$ by step 1.1.

step 1.1step 6.2step 9.1

11.1

Substituting into step 7.1 gives $A = F D \leq F$ , so $A / F$ is trivial, contradicting step 5.1. The assumption of step 1.2 is therefore untenable, and $C_{G} (F (G)) \leq F (G)$ . This proves the stated claim.

discharge-contradiction: step 1.2step 5.1step 7.1step 10.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 88 results over 21 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, Theorem 2.13 (standard reference, not scraped)