\documentclass{article}
\input{packages}
\input{def}

\homework{Monoids}

\begin{document}
\maketitle

\begin{exercise}
Given monoids $\alg{A}$ and~$\alg{B}$, give a monoidal structure~$\alg{A} \with \alg{B}$ to the set~$A \times B$ such that the projection functions $\pi_A$ and~$\pi_B$ are monoid homomorphisms from $\alg{A} \with \alg{B}$ to $\alg{A}$ and~$\alg{B}$ respectively.
\end{exercise}

\begin{notation}
$\alg{A} \with \alg{B}$ is called the \emph{product} of $\alg{A}$ and~$\alg{B}$, though it is more commonly denoted as $\alg{A} \times \alg{B}$ and sometimes called the \emph{direct} product.
\end{notation}

\begin{exercise}
Determine the monoid~``$\top$'' with the property that for every monoid~$\alg{A}$ there is exactly one monoid homomorphism from~$\alg{A}$ to~$\top$.
\end{exercise}

\begin{exercise}
Determine the monoid~``$0$'' with the property that for every monoid~$\alg{A}$ there is exactly one monoid homomorphism from~$0$ to~$\alg{A}$.
\end{exercise}

\begin{remark}
$\top$~is called the \emph{terminal} monoid (more commonly denoted with~$1$), and $0$~is called the \emph{initial} monoid.
\end{remark}

\begin{definition}
A multilinear homomorphism from $\alg{A}$ and~$\alg{B}$ to~$\alg{C}$ is a function~$f : A \times B \to C$ such that $f(e_\alg{A}, b) = e_\alg{C}$ always, $f(a_1 * a_2, b) = f(a_1,b) * f(a_2,b)$ always, $f(a, e_\alg{B}) = e_\alg{C}$ always, and $f(a, b_1 * b_2) = f(a,b_1) * f(a,b_2)$ always.
In other words, fixing either argument produces a monoid homomorphism.
\end{definition}

\begin{definition}
Given a type~$\tau$ and a binary relation~$\approx : \tau \times \tau \to \Prop$, the type~$\frac{\tau}{\approx}$ is called the quotient.
Set theoretically, it is the set of all equivalence classes of~$\approx$ on~$\tau$.
There is a function~$\lambda t.\; \frac{t}{\approx} : \tau \to \frac{\tau}{\approx}$ mapping each element of~$\tau$ to its equivalence class.
To construct functions from~$\frac{\tau}{\approx}$ to another type~$\tau'$, one uses $\select{t}{q}{e[t]}{\prf{p}}$, where $q$~is a~$\frac{\tau}{\approx}$, $t$~is a variable bound to some $\tau$~value in~$q$, $e[t]$~is an expression of type~$\tau'$ indicating how to use~$t$, and $\prf{p}$~is a proof that $\forall t, t' : \tau.\; t \approx t' \imply e[t] = e[t']$.
\end{definition}

\begin{definition}
Given monoids $\alg{A}$ and~$\alg{B}$, define the equivalence relation~$\approx$ on~$\List (A \times B)$ to be the least equivalence relation such that:
\begin{enumerate}
\item $\forall \vec{m}_1, \vec{m}_1', \vec{m}_2, \vec{m}_2' : \List (A \times B).\; \vec{m}_1 \approx \vec{m}_1' \wedge \vec{m}_2 \approx \vec{m}_2' \implies \vec{m}_1 \append \vec{m}_2 \approx \vec{m}_1' \append \vec{m}_2'$
\item $\forall b : B.\; [\langle e_\alg{A}, b \rangle] \approx \nil$
\item $\forall a_1, a_2 : A, b : B.\; [\langle a_1, b \rangle, \langle a_2, b \rangle] \approx [\langle a_1 * a_2, b \rangle]$
\item $\forall a : A.\; [\langle a, e_\alg{B} \rangle] \approx \nil$
\item $\forall a : A, b_1, b_2 : B.\; [\langle a, b_1 \rangle, \langle a, b_2 \rangle] \approx [\langle a, b_1 * b_2 \rangle]$
\end{enumerate}
We use requirement~1 to impose a monoidal structure~$\alg{A} \otimes \alg{B}$ on the quotient set~$\frac{\List (A \times B)}{\approx}$:
\begin{framed}
\begin{description}
\item[Operator $\frac{\append}{\approx} =$] $\lambda q_1, q_2.\; \select{\vec{m}_1}{q_1}{(\select{\vec{m}_2}{q_2}{\frac{\vec{m}_1 \append \vec{m}_2}{\approx}}{\noprf})}{\noprf}$
\item[Associativity] Follows from associativity of~$\append$ and the fact that quotienting only makes things more equal
\item[Identity Element $=$] $\frac{\nil}{\approx}$
\item[Identity] Follows from identity of~$\nil$ and the fact that quotienting only makes things more equal
\end{description}
\end{framed}
\end{definition}

\begin{exercise}
Show that, for any monoid~$\alg{C}$, there is a bijection between the set of multilinear homomorphisms from $\alg{A}$ and~$\alg{B}$ to~$\alg{C}$ and the set of monoid homomorphisms from~$\alg{A} \otimes \alg{B}$ to~$\alg{C}$.
\end{exercise}

\begin{notation}
$\alg{A} \otimes \alg{B}$ is called the \emph{tensor (product)} of $\alg{A}$ and~$\alg{B}$.
\end{notation}

\end{document}