TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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 abelianisation of a free group on $X$ is a free abelian group on $X$

Statement

Let $(F(X),i)$ be a free group on $X$ , let $q:F(X)\to F(X)^{\mathrm{ab}}$ be the abelianisation map, and put $i_{\mathrm{ab}}=q\circ i$ . Then $(F(X)^{\mathrm{ab}},i_{\mathrm{ab}})$ is a free abelian group on $X$ .

Facts & Assumptions

Given: A free group $(F(X),i)$ , its quotient $F(X)^{\mathrm{ab}}=F(X)/[F(X),F(X)]$ , its canonical quotient map $q$ , and $i_{\mathrm{ab}}=q\circ i$ .

[L1]

For $N\mathrel{\trianglelefteq}G$ , the quotient $G/N$ is abelian if and only if $[G,G]\subseteq N$ ( $G/N$ is abelian if and only if $[G,G]\subseteq N$ ).

[L2]

If a homomorphism $f:G\to H$ kills a normal subgroup $N$ , then it factors uniquely through $G/N$ (A homomorphism that kills a normal subgroup factors uniquely through the quotient group).

[F1]

A free abelian group on $X$ is an abelian group $A(X)$ with a map from $X$ such that every function from $X$ to an abelian group extends uniquely to a homomorphism from $A(X)$ (Free abelian group on a set).

[F2]

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

Proof

technique · constructive

1.1

Taking $N=[F(X),F(X)]$ in [L1] shows that $F(X)^{\mathrm{ab}}$ is abelian.

L1given

1.2

Let $A$ be an abelian group and $u:X\to A$ a function; the free-group property gives a unique homomorphism $f:F(X)\to A$ extending $u$ , and $f([g,h])=f(g)f(h)f(g)^{-1}f(h)^{-1}=e_A$ because $A$ is abelian, so every commutator lies in the subgroup $\ker f$ ; since $[F(X),F(X)]$ is generated by those commutators by [F2], minimality gives $[F(X),F(X)]\subseteq\ker f$ .

F2given

2.1

By [L2], construct a homomorphism $\overline f:F(X)^{\mathrm{ab}}\to A$ with $f=\overline f\circ q$ ; then $\overline f\circ i_{\mathrm{ab}}=\overline f\circ q\circ i=f\circ i=u$ .

L2step 1.2construct

3.1

If $h:F(X)^{\mathrm{ab}}\to A$ also extends $u$ , then $h\circ q$ and $\overline f\circ q$ are homomorphisms $F(X)\to A$ agreeing with $u$ on $X$ , so free-group uniqueness makes them equal; both $h$ and $\overline f$ therefore factor the same map through the quotient, and uniqueness in [L2] gives $h=\overline f$ .

L2step 2.1given

4.1

Steps 1.1, 2.1, and 3.1 give the abelian target, extension, and uniqueness clauses in [F1], so $F(X)^{\mathrm{ab}}$ is free abelian on $X$ ; for $X=\varnothing$ both universal properties yield the trivial group.

F1step 1.1step 2.1step 3.1discharge-construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by Free abelian group on a set.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 34 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

Richard Elman, Lectures on Abstract Algebra, §18 (standard reference, not scraped)
John McKernan, Presentations and Groups of Small Order, Lecture 12 (standard reference, not scraped)

The abelianisation of a free group on XXX is a free abelian group on XXX