\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{proof}
Define $\langle a_1, b_1 \rangle * \langle a_2, b_2 \rangle$ to be $\langle a_1 * a_2, b_1 * b_2 \rangle$. This is associative because $*$ is associative for both $\alg{A}$ and $\alg{B}$.
Define $e_{\alg{A} \with \alg{B}}$ to be $\langle e_\alg{A}, e_\alg{B} \rangle$. This is an identity because $e_\alg{A}$ and $e_\alg{B}$ are identities for $\alg{A}$ and $\alg{B}$ respectively.
$\pi_A$ is a monoid homomorphism since $\pi_A(\langle a_1 * a_2, b_1 * b_2 \rangle) = a_1 * a_2$, preserving multipliation, and $\pi_A(\langle e_\alg{A}, e_\alg{B} \rangle) = e_\alg{A}$, preserving identity. Similarly for $\pi_B$.
\end{proof}

\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{proof}
The underlying set is $\mathbb{1}$, and multiplication and identity are the only functions with their respective signatures. Given two monoid homomorphisms from some monoid $\alg{A}$ to $\top$, they must both map everything to the unique inhabitant of $\mathbb{1}$, making them equal.
\end{proof}

\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{proof}
The underlying set is $\mathbb{1}$, and multiplication and identity are the only functions with their respective signatures. Given two monoid homomorphisms from $0$ to some monoid $\alg{A}$, their only input is the identity of $\top$ and so being monoid homomorphisms they must both map this only input to $e_\alg{A}$, making them equal.
\end{proof}

\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{proof}
Given a function $f : A \times B \to C$ that is a multilinear homomorphism from $\alg{A}$ and~$\alg{B}$ to~$\alg{C}$, define $\hat{f} : \List(A \times B) \to C$ to be $\lambda \vec{m}.\; \Pi \texttt{map}_f\vec{m}$ where $\texttt{map}_f$ is the function that takes a list and produces a new list by applying~$f$ to each element. $\hat{f}$ is a monoid homomorphism:
\begin{itemize}
\item $\hat{f}(\vec{m}_1 \append \vec{m}_2) = \Pi \texttt{map}_f(\vec{m}_1 \append \vec{m}_2) = \Pi (\texttt{map}_f\vec{m}_1 \append \texttt{map}_f\vec{m}_2) = (\Pi \texttt{map}_f\vec{m}_1) * (\Pi \texttt{map}_f\vec{m}_2) = \hat{f}(\vec{m}_1) * \hat{f}(\vec{m}_2)$
\item $\hat{f}(\nil) = \Pi \texttt{map}_f\nil = \Pi \nil = e_\alg{C}$
\end{itemize}
$\hat{f}$ has the property that it maps related lists to equal elements (skipping the additional rules for equivalence relations below):
\begin{enumerate}
\item Given $\vec{m}_1, \vec{m}_1', \vec{m}_2, \vec{m}_2' : \List (A \times B)$ such that $\vec{m}_1 \approx \vec{m}_1'$ and $\vec{m}_2 \approx \vec{m}_2'$ hold, by induction on the proof of $\approx$ we can assume $\hat{f}(\vec{m}_1) = \hat{f}(\vec{m}_1')$ and $\hat{f}(\vec{m}_2)$ = $\hat{f}(\vec{m}_2')$. $\hat{f}(m_1 \append m_2) = \hat{f}(\vec{m}_1) * \hat{f}(\vec{m}_2) = \hat{f}(\vec{m}_1') * \hat{f}(\vec{m}_2') = \hat{f}(m_1' \append m_2')$
\item Given $b : B$, $\hat{f}([\langle e_\alg{A}, b \rangle]) = \Pi\texttt{map}_f[\langle e_\alg{A}, b \rangle] = \Pi [f(e_\alg{A}, b)] = f(e_\alg{A}, b) = e_\alg{C} = \Pi \nil = \Pi \texttt{map}_f \nil = \hat{f}(\nil)$
\item Given $a_1, a_2 : A$ and $b : B$, $\hat{f}([\langle a_1, b \rangle, \langle a_2, b \rangle]) = \Pi \texttt{map}_f [\langle a_1, b \rangle, \langle a_2, b \rangle] = \Pi [f(a_1, b), f(a_2, b)] = f(a_1, b) * f(a_2, b) = f(a_1 * a_2, b) = \Pi [f(a_1 * a_2, b)] = \Pi \texttt{map}_f[\langle a_1 * a_2, b \rangle] = [\langle a_1 * a_2, b \rangle]$
\item Given $a : A$, $\hat{f}([\langle a, e_\alg{B} \rangle]) = \Pi\texttt{map}_f[\langle a, e_\alg{B} \rangle] = \Pi [f(a, e_\alg{B})] = f(a, e_\alg{B}) = e_\alg{C} = \Pi \nil = \Pi \texttt{map}_f \nil = \hat{f}(\nil)$
\item Given $a : A$ and $b_1, b_2 : B$, $\hat{f}([\langle a, b_1 \rangle, \langle a, b_2 \rangle]) = \Pi \texttt{map}_f [\langle a, b_1 \rangle, \langle a, b_2 \rangle] = \Pi [f(a, b_1), f(a, b_2)] = f(a, b_1) * f(a, b_2) = f(a, b_1 * b_2) = \Pi [f(a, b_1 * b_2)] = \Pi \texttt{map}_f[\langle a, b_1 * b_2 \rangle] = [\langle a, b_1 * b_2 \rangle]$
\end{enumerate}
Consequently, we can define $\tilde{f} : \frac{\List(A \times B)}{\approx} \to C$ to be $\lambda q.\; \select{\vec{m}}{q}{\Pi \texttt{map}_f \vec{m}}{\text{(proof above)}}$. This is a monoid homomorphism because $\hat{f}$ is a monoid homomorphism.

In the other direction, given a function $g : \frac{\List(A \times B)}{\approx} \to C$ that is a monoid homomorphism from~$\alg{A} \otimes \alg{B}$ to~$\alg{C}$, define $\bar{g} : A \times B \to C$ to be $\lambda \langle a, b \rangle.\; g(\frac{[\langle a, b \rangle]}{\approx})$. $\bar{g}$ is a multilinear monoid homomorphism from $\alg{A}$ and $\alg{B}$ to $\alg{C}$ since related lists are in equal equivalence classes and $g$ is a monoid homomorphism:
\begin{itemize}
\item Given $b : B$, $\bar{g}(e_\alg{A}, b) = g(\frac{[\langle e_\alg{A}, b \rangle]}{\approx}) = g(\frac{\nil}{\approx}) = e_\alg{C}$
\item Given $a_1, a_2 : A$ and $b : B$, $\bar{g}(a_1 * a_2, b) = g(\frac{[\langle a_1 * a_2, b \rangle]}{\approx}) = g(\frac{[\langle a_1, b \rangle, \langle a_2, b \rangle]}{\approx}) = g(\frac{[\langle a_1, b \rangle]}{\approx} \frac{\append}{\approx} \frac{[\langle a_2, b \rangle]}{\approx}) = g(\frac{[\langle a_1, b \rangle]}{\approx}) * g(\frac{[\langle a_2, b \rangle]}{\approx}) = \bar{g}(a_1, b) * \bar{g}(a_2, b)$
\item Given $a : A$, $\bar{g}(a, e_\alg{B}) = g(\frac{[\langle a, e_\alg{B} \rangle]}{\approx}) = g(\frac{\nil}{\approx}) = e_\alg{C}$
\item Given $a : A$ and $b_1, b_2 : B$, $\bar{g}(a, b_1 * b_2) = g(\frac{[\langle a, b_1 * b_2 \rangle]}{\approx}) = g(\frac{[\langle a, b_1 \rangle, \langle a, b_2 \rangle]}{\approx}) = g(\frac{[\langle a, b_1 \rangle]}{\approx} \frac{\append}{\approx} \frac{[\langle a, b_2 \rangle]}{\approx}) = g(\frac{[\langle a, b_1 \rangle]}{\approx}) * g(\frac{[\langle a, b_2 \rangle]}{\approx}) = \bar{g}(a, b_1) * \bar{g}(a, b_2)$
\end{itemize}

Given a function $f : A \times B \to C$ that is a multilinear homomorphism from $\alg{A}$ and~$\alg{B}$ to~$\alg{C}$, we have the following equality for all $a : A$ and $b : B$:
$$\bar{\tilde{f}}(a, b) = \tilde{f}(\frac{[\langle a, b \rangle]}{\approx}) = \select{\vec{m}}{\frac{[\langle a, b \rangle]}{\approx}}{\Pi \texttt{map}_f \vec{m}}{\noprf} = \Pi \texttt{map}_f [\langle a, b \rangle] = \Pi [f(a, b)] = f(a, b)$$
In the other direction, given a function $g : \frac{\List(A \times B)}{\approx} \to C$ that is a monoid homomorphism from~$\alg{A} \otimes \alg{B}$ to~$\alg{C}$, we have the following equality for all $q : \frac{\List(A \times B)}{\approx}$:
$$\begin{array}{r@{\ =\ }l}
g(q) & \select{\vec{m}}{q}{g(\frac{\vec{m}}{\approx})}{\noprf} \\& \select{\Sigma_i [\langle a_i, b_i \rangle]}{q}{g(\frac{\Sigma_i [\langle a_i, b_i \rangle]}{\approx})}{\noprf} \\& \select{\Sigma_i [\langle a_i, b_i \rangle]}{q}{\Pi_i g(\frac{[\langle a_i, b_i \rangle]}{\approx})}{\noprf} \\& \select{\Sigma_i [\langle a_i, b_i \rangle]}{q}{\Pi \Sigma_i g(\frac{[\langle a_i, b_i \rangle]}{\approx})}{\noprf} \\& \select{\Sigma_i [\langle a_i, b_i \rangle]}{q}{\Pi \texttt{map}_{\lambda \langle a, b \rangle.\; g(\frac{[\langle a, b \rangle]}{\approx})} \Sigma_i [\langle a_i, b_i \rangle]}{\noprf} \\& \select{\vec{m}}{q}{\Pi \texttt{map}_{\lambda \langle a, b \rangle.\; g(\frac{[\langle a, b \rangle]}{\approx})} \vec{m}}{\noprf} \\& \select{\vec{m}}{q}{\Pi \texttt{map}_{\bar{g}} \vec{m}}{\noprf} \\& \tilde{\bar{g}}(q)
\end{array}$$
\end{proof}

\end{document}