Free Group

The free group on a H-Set $X$ is a Free Object with respect to the forgetful functor $U:\mathrm{Grp}{.}\to\mathrm{Sets}{.}$.

Constructions

There is a generic construction of free groups that proceeds by constructing syntax trees of groups, and then quotienting by the relation that $x\cdot x^{-1}\sim 1\sim x^{-1}\cdot x$. Note that unlike Free Monoids, this is not an "effective" construction of free groups, as performing some sort of normalization requires us to check if two adjacent elements are equal.

When we do have Decidable Equality on $X$, we can perform an "effective" construction of free groups by working with reduced words. The technical details of this are rather interesting, and I suspect that this is most naturally done with a Groud rather than a group, as it makes some of the inductions a bit easier.

Properties

• Free groups exist for every set, so the system of free objects assembles into a Left Adjoint $F:\mathrm{Sets}{.}\to\mathrm{Grp}{.}$.