Set-theoretical description of the free product?

In answer to your question about whether this is written somewhere: the construction of free products in my book Introduction to Topological Manifolds proceeds very much along these lines. (I'm not the only one who's written it down, but I don't have other references handy.) I don't go through the set-theoretic description of the set of ordered tuples in as much detail as you do, but it can be described more simply as just the disjoint union of the sets $(G\amalg H)^n$ over all n. I like the concreteness of this construction as a way of giving one a handle on what the free product looks like. Once the group is constructed, it's a relatively easy matter to prove after the fact that it is uniquely determined up to isomorphism as the coproduct in the category of groups.

You can see essentially the same construction in two different ways in George Bergman's An Invitation to General Algebra and Universal Constructions in Chapter 2 (link is to a postscript file) for the free group.

First, you define "the set of all terms in the elements of the set $X$ under the formal group operations $\mu$, $i$, $e$" to mean a set which is given with functions symb${}_T\colon X\to T$, $\mu_T\colon T^2\to T$, $i_T\colon T\to T$, and $e_T\colon T^0\to T$, such that each of these maps is one-to-one, their images are disjoint, and $T$ is the union of the images, and $T$ is generated by symb${}_T(X)$ under the operations $\mu_T$, $i_T$, and $e_T$. Such a set exists (it can be constructed inductively with enough care; given in Chapter 1 of the same notes). Then one defines an apropriate equivalence relation $\sim$ on $T$; the set $T/\sim$ gives the underlying set of the free group, and one defines the operations in the free group via representatives in the natural way. Bergman labels this "the logician's approach" (section 2.2).

An alternative construction ("the classical construction", section 2.4) gives "free groups as groups of words". Again, you start with a set $X$, and let $T$ be the set of all group-theoretic terms of $X$; identify $X$ with its image under symb, and one defines a subset $T_{red}$ of "reduced terms" (defining what this means appropriately) and then defining operations $\otimes$, ${}^{(-)}$, and $e_T$ on this set to make it into a group. Proving it is a group can be done either in the straightforward but tedious way, or by using "van der Waerden's trick" (embed the set $T_{red}$ into a group of permutations, and check that the operations you defined correspond to the operations in the image, so that "group"-ness gets inherited).

To get the free product, you let $X$ be the disjoint union of the underlying sets of $G$ and $H$, and either adds to the equivalence relation (in the "logician's approach"), or restricts the definition of "reduced words" (in the "classical approach"), in essentially the way you did.

In the question above, it seems that the description is far too complicated as it actually is. I will elaborate on the construction of coproducts of groups or monoids a bit. This will go beyond the scope of the specific question, but I hope it's helpful in other situations.

First assume $M,N$ are sets. What is their coproduct? Obviously it's the disjoint union, which I will denote by $M + N$. Now assume $M,N$ are monoids. What is their coproduct? Well we have to introduce products of elements in $M + N$. Thus consider $(M + N)^{<\omega}$, the set of finite sequences with entries in $M + N$. This is a monoid by concatenation, but the inclusions $M,N \to (M + N)^{<\omega}$ are no homomorphisms. Well, then let's force it! Mod out the smallest congruence relation $\sim$ on our monoid, which satisfies $1 \sim (1_M), (m,m') \sim (mm')$ for all $m,m' \in M$ and similarily for elements of $N$. Then the quotient $(M + N)^{<\omega} / \sim$ is obviously a monoid (since $\sim$ is a congruence relation), and the universal property of the coproduct is also verified easily.

Now what about groups? The correct definition of a group involves the operations of the underlying monoid and the inversion. But in practice, this inversion can be reconstructed from the rest of the data ($x=y^{-1}$ iff $xy=1$), and actually the category of groups is a full subcategory of the category of monoids. If the monoids $M,N$ above happen to be groups, their coproduct turns out to be a group, and clearly the universal property then also holds with respect to groups. Thus we have constructed the coproduct in the category of groups.

Let's turn back to monoids. The above construction of $M \coprod N$ is rather general, it shows the existence of colimits in every finitary algebraic category, but what can be said about the elements? Do they have a canonical representation? Now there are two ways of doing it:

a) The elegant, short, "geometric" one.

b) The long, tedious one. This one is preferred in textbooks ...

In our case, b) means that you write down the set of reduced words, endow it with a terribly complicated monoid structure, show that every monoid axiom is satisfied, and finally check the universal property. Good luck.

In a) you just use that $M \coprod N$ exists. We have constructed it, but the construction does not answer such simple questions as: Do $M$ and $N$ intersect in $M \coprod N$ trivially? Therefore we just use the existence of the coproduct together with the structure maps $i : M \to M \coprod N, j : N \to M \coprod N$. The idea is now to define an action of $M \coprod N$ on another object. This may be a geometric one, but in our case it's our desired set of reduced words.

Observe that the elements in $M \coprod N$, which are products of elements, which are in the image of $i$ or $j$, constitute a submonoid, which verifies the same universal property. In other words, every element in $M \coprod N$ is such a product. In such a product we may replace $i(m) i(m')$ by $i(mm')$ and cancel $i(1)$, similarily for $j$. Thus every element is in the image of the canonical map $X \to M \coprod N$, where

$X := \{(... ,m_1,n_1,m_2,n_2, ...) : m_i \in M - \{1\}, n_i \in N - \{1\}\}.$

Now we prove that this map $X \to M \coprod N$ is a bijection, i.e. every element of the coproduct has a unique representation as $... i(m_1) j(n_1) i(m_2) ...$. To do this, we define an action of the monoid $M \coprod N$ on $X$, i.e. a monoid homomorphism $M \coprod N \to End(X), (m \mapsto (x \mapsto mx))$, which should imitate the usual multiplication. By the universal property, it is enough to construct this homomorphism on $M$ and on $N$. If $m \in M$ and $x \in X$, define $mx$ as follows: If $x$ starts with an element in $N$, just concatenate with $(m)$. If $x$ starts with an element of $M$, which is not inverse to $m$, then multiply $m$ in the first entry. Otherwise delete the first entry. Similarily the homomorphism $N \to End(X)$ is defined. The resultung homomorphism $M \coprod N \to End(X)$ can be composed with the evaluation at the empty sequence to get a map $M \coprod N \to X$, which turns out to be a left inverse to $X \to M \coprod N$. Thus, $X \to M \coprod N$ is a bijection.