TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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 derived subgroup is characteristic and the abelianization is universal

Statement

For every group $G$ , the derived subgroup $G^{'} = [G, G]$ is characteristic, hence normal. The quotient $G^{a b} : = G / G^{'}$ is abelian and has the following universal property: for every homomorphism $f : G \to A$ into an abelian group, there is a unique homomorphism $\overset{ˉ}{f} : G^{a b} \to A$ with $f = \overset{ˉ}{f} \circ q$ , where $q : G \to G / G^{'}$ is the quotient map.

Facts & Assumptions

Given: A group $G$ , its commutator subgroup $G^{'}$ , and a homomorphism $f : G \to A$ to an abelian group.

[F1]

$[G, G]$ is generated by the commutators $[x, y] = x y x^{- 1} y^{- 1}$ (Commutators $[g, h] = g h g^{- 1} h^{- 1}$ and the commutator subgroup $[G, G]$ ).

[F2]

A characteristic subgroup is preserved by every automorphism (Characteristic subgroups).

[L1]

Characteristic subgroups are normal (Characteristic subgroups are normal, and characteristicity is transitive).

[L2]

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

[L3]

If $N ⊴ G$ and $N \leq \ker f$ , then $f$ factors uniquely through $G / N$ (A homomorphism that kills a normal subgroup factors uniquely through the quotient group).

Proof

technique · direct

1.1

Every automorphism $α$ satisfies $α ([x, y]) = [α (x), α (y)]$ , so it maps the generating commutators of $G^{'}$ into $G^{'}$ ; applying the same argument to $α^{- 1}$ gives $α (G^{'}) = G^{'}$ .

F1algebra

1.2

For $x, y \in G$ , the group $A$ is abelian, so $f ([x, y]) = [f (x), f (y)] = 1$ ; hence every generator of $G^{'}$ lies in $\ker f$ , and $G^{'} \leq \ker f$ .

givenF1algebra

2.1

Thus $G^{'}$ is characteristic by [F2], and therefore normal by [L1].

step 1.1F2L1

3.1

Since $G^{'} \leq G^{'}$ , [L2] gives that $G / G^{'}$ is abelian.

step 2.1L2

4.1

By [L3] there is a unique $\overset{ˉ}{f} : G / G^{'} \to A$ with $f = \overset{ˉ}{f} \circ q$ . Together with step 3.1, this is the asserted universal abelian quotient.

step 2.1step 1.2L3∎

Depends on

Used by

Dependency tree · next 3 levels

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

J. S. Milne, Group Theory, Chapter 6 (standard reference, not scraped)
K. Conrad, Subgroup Series I (standard reference, not scraped)
K. Igusa, Notes on Jordan-Hölder, section 5 (standard reference, not scraped)