Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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 Gab:=G/G′ is abelian and has the following universal property: for every homomorphism f:G→A into an abelian group, there is a unique homomorphism fˉ:Gab→A with f=fˉ∘q, where q:G→G/G′ is the quotient map.

Facts & Assumptions

Given: A group G, its commutator subgroup G′, and a homomorphism f:G→A to an abelian group.

[F1]

[G,G] is generated by the commutators [x,y]=xyx−1y−1 (Commutators [g,h]=ghg−1h−1 and the commutator subgroup [G,G]).

[F2]

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

[L2]

For N⊴G, G/N is abelian if and only if [G,G]≤N (G/N is abelian if and only if [G,G]⊆N).

[L3]

If N⊴G and N≤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∈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′≤ker⁡f.

givenF1algebra
2.1

Thus G′ is characteristic by [F2], and therefore normal by [L1].

step 1.1F2L1
3.1

Since G′≤G′, [L2] gives that G/G′ is abelian.

step 2.1L2
4.1

By [L3] there is a unique fˉ:G/G′→A with f=fˉ∘q. Together with step 3.1, this is the asserted universal abelian quotient.

step 2.1step 1.2L3∎

Depends on

Used by

Dependency tree · two levels

18 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