Abelianization of Free Group is Free Abelian Group

Theorem

Let $X$ be a set.

Let $(F_X, \iota)$ be a free group on $X$.

Let $F_X^{\operatorname{ab}}$ be its abelianization.

Let $\pi : F_X \to F_X^{\operatorname{ab}}$ be the quotient group epimorphism.

Then $(F_X^{\operatorname{ab}}, \pi \circ \iota)$ is a free abelian group on $X$.