This keeps cropping up, and every time it takes me some effort to rediscover the proof. It happened first with free groups, then with free vector spaces and again with free Lie algebras.
I’ll formulate the issue with groups, but it is easy to carry it over to other cases.
A free group on set is defined by its universal property; furthermore, a particular specimen can be constructed. This construction is essential for proving the existence of a free group, but that should be its only role.
The question is: Is the subgroup of generated by necessarily itself? Can’t there be any “maverick” elements in , that are not in that subgroup? It seems that there shouldn’t be any, because they would be “too free”; when applying the universal property, the value given to them by the supposedly unique group morphism from to the “test group” might not be uniquely determined. But how do we prove this?
If we examine the constructed specimen ‑ in the case of free groups, the set of “strings” of elements of considered as “letters” plus their “primed versions”, with a certain composition rule ‑ the answer is that indeed, the whole of is generated by . And since all free groups on a given set are isomorphic, this answers our question.
But having to make use of a particular specimen doesn’t seem right to me. I want a proof with the universal property alone! Here it is, for my own repeated reference.
Let be a set, and any free group on . Let be the subgroup of generated by .
Now since, by definition of a generated subgroup, , is also a mapping from to ; or rather, we will call it as the codomain has changed. Thus is the mapping .
We thus have a group and a mapping ; the universal property of free groups satisfied by implies the existence of a group morphism such that .
Now can also be seen as a mapping from to ; or rather, since again we have changed the codomain, we define the new mapping . Since is a group morphism, so is .
Our equality can be rewritten with the larger codomain , yielding . So is a group morphism from to such that . We know that there is only one such group morphism. Since we also have , necessarily .
For any , we have . Hence .