Details of Defining Free Group in Terms of Universal Property The only definition of the free group I have seen thus far (undergraduate) is an explicit construction
via reduced words and concatenation.
What I am now trying to do is see if it is possible to define the free group abstractly in terms of the universal property. The definition I think should work is:
A free group $F_S$ on a set $S$ is a group generated by $S$ such that for any group $G$ and any function $f: S \rightarrow G$, $f$ extends to a unique homomorphism $\tilde{f}: F_S \rightarrow G$.
So what I want to do now is prove existence and uniqueness (up to isomorphism?) from this abstract definition, and I'm struggling to make progress, so I'm looking for tips, specifically:

*

*Is my definition correct, or is there something I'm missing?

*Any tips on how to make progress on existence?

*Any tips on how to make progress on uniqueness?

 A: You actually don't need to specify that $F_S$ is generated by $S$, only that you've equipped $F_S$ with some map $i : S \to F_S$ (which you also don't need to require is injective in case you were thinking about doing that). Generation will turn out to follow from the universal property. Other than that, yes, this is how it goes.
Uniqueness (up to unique isomorphism) follows from the Yoneda lemma; this is a general feature of objects defined by universal properties and is a major reason why using universal properties is so convenient.
Existence is harder. You can show that the concrete definition using reduced words satisfies the universal property; it takes a bit of work but it's a convenient fact to be able to refer to. One possible more abstract argument is the following. We first consider the free monoid on $S$; this is easy to construct explicitly as the monoid
$$\text{List}(S) = \bigsqcup_{n \ge 0} S^n$$
of lists of elements of $S$, or equivalently as the monoid of words on the alphabet $S$, under concatenation, and it's easy to prove the universal property.
To get the free group from here we need to freely adjoin inverses to this monoid. The group obtained by freely adjoining inverses to the free monoid $\text{List}(S)$ can be constructed by starting from $\text{List}(S \sqcup S^{-1})$, where $S^{-1}$ is just another copy of $S$ that stands for the inverses we're adjoining, then quotienting by relations that say that each $s \in S$ actually has the corresponding formal symbol $s^{-1} \in S^{-1}$ as its inverse. How satisfying this is depends on how comfortable you are with taking quotients of monoids, but it does have the benefit that we don't need to talk about reduced words so the universal property is easier to check.
This construction is also a good prototype for how to construct other free objects. The list construction generalizes to constructing, for example, for example, the free $k$-algebra on a $k$-vector space $V$ as the tensor algebra
$$T(V) = \bigoplus_{n \ge 0} V^{\otimes n}.$$
In turn the tensor algebra is an important intermediate step for constructing other objects like the free commutative $k$-algebra on $V$, which is the symmetric algebra.
A: Your definition is right and uniqueness follows from it from a purely categorical argument. Namely, you're defining a free group $F_S$ over $S$ and, to make things more precise, you should make an "inclusion" $\iota:S \to F_S$ part of the definition, so that for every group $G$ and every function $f:S \to G$, there is a unique homomorphism $\widetilde{f}:F_S\to G$ with $f = \tilde{f} \circ \iota$.
Assume that $F_{S,1}$ and $F_{S,2}$ are two free groups over $S$, with inclusions $\iota_i:S \to F_{S,i}$, $i=1,2$. Apply the definition of free group to $\iota_1: S \to F_{S,1}$ to get a homomorphism $\widetilde{\iota_1}:F_{S,2}\to F_{S,1}$ with $\iota_1 = \widetilde{\iota_1}\circ \iota_2$. Switching roles of $F_{S,1}$ and $F_{S,2}$, we also obtain a group homomorphism $\widetilde{\iota_2}:F_{S,1}\to F_{S,2}$ with $\iota_2= \widetilde{\iota_2}\circ \iota_1$. Now we have a homomorphism $\widetilde{\iota_1}\circ\widetilde{\iota_2}:F_{S,1}\to F_{S,1}$, which has to be the identity, as $$(\widetilde{\iota_1}\circ\widetilde{\iota_2})\circ \iota_1 = \widetilde{\iota_1}\circ (\widetilde{\iota_2}\circ \iota_1) = \widetilde{\iota_1}\circ \iota_2 = \iota_1 $$and $${\rm Id}_{F_{S,1}}\circ \iota_1 = \iota_1.$$More precisely, we're able to conclude that $\widetilde{\iota_1}\circ\widetilde{\iota_2} = {\rm Id}_{F_{S,1}}$ because of the uniqueness of extensions in the definition. Switching roles of $F_{S,1}$ and $F_{S,2}$ again, we also get that $\widetilde{\iota_2}\circ\widetilde{\iota_1} = {\rm Id}_{F_{S,2}}$. So $F_{S,1}\cong F_{S,2}$.
Here's what's going on behind the scenes: defining a category $\mathcal{C}_S$ by setting $${\rm Obj}(\mathcal{C}_S) = \{ (F,\iota) \mid \iota:S \to F \mbox{ and $F$ is a group}\}$$ and $${\rm Mor}_{\mathcal{C}_S}((F_1,\iota_1),(F_2,\iota_2)) = \{ \phi:F_1\to F_2 \mid \phi \mbox{ is a homomorphism and }\phi\circ \iota_1=\iota_2\},$$a free group $(F_S,\iota)$ over $S$ is nothing more than an initial object in $\mathcal{C}_S$. But it's a general fact (which I invite you to prove --- mimicking the above) that in any category, initial objects are unique up to (unique!) isomorphism.
However, all of this fluff does not establish existence of $F_S$. But since we already know that if it exists, it will be unique up to isomorphism, to get existence it suffices to exhibit one construction. Then the usual construction fits the bill.
The universal property gives an elegant way of constructing homomorphisms between free groups. For example, if $S_1$ and $S_2$ are sets and we have a function $f:S_1\to S_2$, then apply the universal property of $F_{S_1}$ to $\iota_2\circ f$ to get a group homomorphism $\widetilde{\iota_2\circ f}:F_{S_1}\to F_{S_2}$. If $f$ is bijective, then $\widetilde{\iota_2 \circ f}$ is an isomorphism with inverse $\widetilde{\iota_1\circ f^{-1}}$ (check this without picking elements, it's instructive).
