Theorem: Coproduct of Free Monoids

Let $\mathbf {Mon}$ be the category of monoids.
Let $\map M A$ and $\map M B$ be free monoids on sets $A$ and $B$, respectively.
Let $A \sqcup B$ be the disjoint union of $A$ and $B$.
Then the free monoid $\map M {A \sqcup B}$ on $A \sqcup B$ is the coproduct of $\map M A$ and $\map M B$ in $\mathbf {Mon}$.

Proof:
By Coproduct is Unique, it suffices to verify that $\map M {A \sqcup B}$ is a coproduct for $\map M A$ and $\map M B$.
By the universal mapping property of $\map M A$, $\map M B$ and $\map M {A \sqcup B}$, we have the following commutative diagram:
$\quad\quad \begin {xy}
<-5em,0em>*+{\map M A}         = "MA",
<0em,0em>*+{\map M {A \sqcup B} } = "MAB",
<5em,0em>*+{\map M B}          = "MB",
<-5em,-5em>*+{A}         = "A",
<0em,-5em>*+{A \sqcup B} = "AB",
<5em,-5em>*+{B}          = "B",
"A";"MA" **@{-} ?>*@{>}   ?*!/_.8em/{i_A},
"B";"MB" **@{-} ?>*@{>}   ?*!/^.8em/{i_B},
"AB";"MAB" **@{-} ?>*@{>} ?*!/_.8em/{i_{A \mathop \sqcup B} },
"A";"AB" **@{-} ?>*@{>} ?*!/^.8em/{i_1},
"B";"AB" **@{-} ?>*@{>} ?*!/_.8em/{i_2},
"MA";"MAB" **@{-} ?>*@{>} ?*!/_.8em/{j_1},
"MB";"MAB" **@{-} ?>*@{>} ?*!/^.8em/{j_2},
\end{xy}$
Here (in the notation for free monoids):
:$j_1 = \overline {\paren {i_{A \mathop \sqcup B} \circ i_1} }$
:$j_2 = \overline {\paren {i_{A \mathop \sqcup B} \circ i_2}}$
and $i_1$, $i_2$ are the injections for the coproduct.
Note that the above diagram is informal, in the sense:
:$j_1, j_2 \in \mathbf{Mon}_1$
but:
:$i_1,i_2, i_A, i_B, i_{A \mathop \sqcup B} \in \mathbf{Set}_1$
Below we distinguish $\mathbf{Mon}$ and $\mathbf{Set}$.
Let $N$ be a monoid.
Let:
:$f : \map M A \to N$
:$g : \map M B \to N$
be monoid homomorphisms.
Then we need to show the existence of a unique monoid homomorphism:
:$u : \map M {A \mathop\sqcup B} \to N$
such that:
:<nowiki>$\xymatrix{
&N& \\
\map M A \ar[ur]^f \ar[r]_{j_1} & \map M {A \mathop \sqcup B} \ar@{.>}[u]_u & \map M B \ar[ul]_g \ar[l]^{j_2}
}$</nowiki>
is a commutative diagram in $\mathbf{Mon}$.
To this end, observe the commutative diagram in $\mathbf{Set}$
:<nowiki>$\xymatrix{
&\size N& \\
\size {\map M A} \ar[ur]^{\size f} \ar[r]_{\size{j_1} } & \size {\map M {A \mathop \sqcup B} } & \size {\map M B} \ar[ul]_{\size g} \ar[l]^{\size{j_2} } \\
A \ar[u]^{i_A} \ar[r]_{i_1} & A \mathop \sqcup B \ar[u]_{i_{A \mathop \sqcup B} } & B \ar[u]_{i_B} \ar[l]^{i_2}
}$</nowiki>
where $\size \cdot : \mathbf{Mon} \to \mathbf{Set}$ is the underlying set functor.
By Disjoint Union is Coproduct in Category of Sets there exists a unique mapping:
:$\iota : A \mathop \sqcup B \to \size N$
such that:
:<nowiki>$\xymatrix{
&\size N& \\
A \ar[ur]^{\size f \circ i_A} \ar[r]_{i_1} & A \mathop \sqcup B \ar@{.>}[u]_\iota & B \ar[ul]_{\size g \circ i_B} \ar[l]^{i_2}
}$</nowiki>
is a commutative diagram.
By {{Defof|Free Monoid}} there exists a unique monoid homomorphism:
:$u : \map M {A \mathop \sqcup B} \to N$
such that:
:<nowiki>$\xymatrix{
\size {\map M {A \mathop \sqcup B} } \ar[r]^-{\size u} & \size{N} \\
A \mathop \sqcup B \ar[u]^{i_{A \mathop \sqcup B} } \ar[ur]_\iota  &
}$</nowiki>
is a commutative diagram.
Altogether:
:<nowiki>$\xymatrix{
&\size N& \\
\size {\map M A} \ar[ur]^{\size f} \ar[r]_{\size{j_1} } & \size {\map M {A \mathop \sqcup B} } \ar[u]_{\size u} & \size {\map M B} \ar[ul]_{\size g} \ar[l]^{\size{j_2} } \\
A \ar[u]^{i_A} \ar[r]_{i_1} & A \mathop \sqcup B \ar[u]_{i_{A \mathop \sqcup B} } & B \ar[u]_{i_B} \ar[l]^{i_2}
}$</nowiki>
is a commutative diagram.
Using the above diagram, we show this $u$ satisfies the claim.
Firstly, we need to show:
:$f = u \circ j_1$
:$g = u \circ j_2$
By definition of $\size \cdot$ we have:
:$\size {u \circ j_1} = \size u \circ \size {j_1}$
:$\size {u \circ j_2} = \size u \circ \size {j_2}$
In particular:
:<nowiki>$\xymatrix{
\size {\map M A} \ar@/_/[r]^{\size f} \ar@/^/[r]^{\size {u \circ j_1} } & \size{N} \\
A \ar[u]^{i_A} \ar[ur]_{\iota \circ i_1}   &
}$</nowiki>
are commutative diagrams.
By uniqueness part of definitions of $\map M A$ we have:
:$f = u \circ j_1$
Similarly, by definition of $\map M B$:
:$g = u \circ j_2$
Finally, we must show that $u$ is uniquely determined through $f = u \circ j_1$ and $g = u \circ j_2$.
:$v : \map M {A \mathop \sqcup B} \to N$
be also a monoid homomorphism such that $f = v \circ j_1$ and $g = v \circ j_2$.
Then:
{{begin-eqn}}
{{eqn | l = \size v \circ i_{A \mathop \sqcup B} \circ i_1
      | r = \size v \circ \size {j_1} \circ i_A
}}
{{eqn | r = \size {v \circ j_1} \circ i_A
}}
{{eqn | r = \size f \circ i_A
}}
{{end-eqn}}
and, similarly:
:$\size v \circ i_{A \mathop \sqcup B} \circ i_2 = \size g \circ i_B$
That is:
:<nowiki>$\xymatrix{
&\size N& \\
A \ar[ur]^{\size f \circ i_A} \ar[r]_{i_1} & A \mathop \sqcup B \ar[u]_{\size v \circ i_{A \mathop \sqcup B} } & B \ar[ul]_{\size g \circ i_B} \ar[l]^{i_2}
}$</nowiki>
is a commutative diagram.
Due to the uniqueness of $\iota$:
:$\size u \circ i_{A \mathop \sqcup B} = \iota = \size v \circ i_{A \mathop \sqcup B}$
In particular:
:<nowiki>$\xymatrix{
\size {\map M {A \mathop \sqcup B} } \ar@/_/[r]^-{\size v} \ar@/^/[r]^-{\size u} & \size{N} \\
A \mathop \sqcup B \ar[u]^{i_{A \mathop \sqcup B} } \ar[ur]_\iota &
}$</nowiki>
are commutative diagrams.
By uniqueness part of definitions of $\map M {A \mathop \sqcup B}$ we have:
:$u = v$.
{{qed}}