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

\homework{Monads}

\begin{document}
\maketitle

\begin{exercise}
Prove that for any 2-category~$\cat{C}$ and any adjunction $\mo{f} \dashv \mo{g}$ in~$\cat{C}$, one can build a monad in~$\cat{C}$ whose underlying morphism is $\mo{f} \cocomp \mo{g}$.
\end{exercise}

\begin{proof}
Let $\mo{f}$ be from $\ob{C}$ to $\ob{C}$, and let $\eta$ and $\varepsilon$ be the unit and counit of the adjunction.
Then $\langle \ob{C}, \mo{f} \cocomp \mo{g}, \mu, \prf{a}, \eta, \prf{i} \rangle$ is an adjunction, where $\mu$, $\prf{d}$, and $\prf{i}$ are defined as follows:
\begin{description}
\item[$\mu : \mo{f} \cocomp \mo{g} \cocomp \mo{f} \cocomp \mo{g} \nto \mo{f} \cocomp \mo{g} =$]
\begin{tikzpicture}[baseline=(e.base)]
\node(f1) at (-1.5,0) {$\mo{f}$};
\node(g1) at (-.5,0) {$\mo{g}$};
\node(f2) at (.5,0) {$\mo{f}$};
\node(g2) at (1.5,0) {$\mo{g}$};
\node(e)[circle,draw] at (0,1) {$\varepsilon$};
\node(f) at (-.5,2) {$\mo{f}$};
\node(g) at (.5,2) {$\mo{g}$};
\draw[->] (f1.north) .. controls +(0,.5) and ($(f.south) + (0,-.5)$) .. (f.south);
\draw[<-] (e.south west) .. controls +(-.25,-.25) and ($(g1.north) + (0,.25)$) .. (g1.north);
\draw[<-] (e.south east) .. controls +(.25,-.25) and ($(f2.north) + (0,.25)$) .. (f2.north);
\draw[->] (g2.north) .. controls +(0,.5) and ($(g.south) + (0,-.5)$) .. (g.south);
\end{tikzpicture}
\item[$\prf{a}$] is given by the fact that both compositions result in the following string diagram:
\begin{tikzpicture}[baseline=(e.base)]
\node(f1) at (-1.5,0) {$\mo{f}$};
\node(g1) at (-.5,0) {$\mo{g}$};
\node(f2) at (.5,0) {$\mo{f}$};
\node(g2) at (1.5,0) {$\mo{g}$};
\node(f3) at (2.5,0) {$\mo{f}$};
\node(g3) at (3.5,0) {$\mo{g}$};
\node(e1)[circle,draw] at (0,1) {$\varepsilon$};
\node(e2)[circle,draw] at (2,1) {$\varepsilon$};
\node(f) at (.5,2) {$\mo{f}$};
\node(g) at (1.5,2) {$\mo{g}$};
\draw[->] (f1.north) .. controls +(0,1.5) and ($(f.south) + (0,-.75)$) .. (f.south);
\draw[<-] (e1.south west) .. controls +(-.25,-.25) and ($(g1.north) + (0,.25)$) .. (g1.north);
\draw[<-] (e1.south east) .. controls +(.25,-.25) and ($(f2.north) + (0,.25)$) .. (f2.north);
\draw[<-] (e2.south west) .. controls +(-.25,-.25) and ($(g2.north) + (0,.25)$) .. (g2.north);
\draw[<-] (e2.south east) .. controls +(.25,-.25) and ($(f3.north) + (0,.25)$) .. (f3.north);
\draw[->] (g3.north) .. controls +(0,1.5) and ($(g.south) + (0,-.75)$) .. (g.south);
\end{tikzpicture}
\item[$\prf{i}$] is given by
\begin{tikzpicture}[baseline=(e.base)]
\node(f1) at (-1.5,-1) {$\mo{f}$};
\node(g1) at (-.5,-1) {$\mo{g}$};
\node(u)[circle,draw] at (1,0) {$\eta$};
\node(e)[circle,draw] at (0,1) {$\varepsilon$};
\node(f) at (-.5,2) {$\mo{f}$};
\node(g) at (.5,2) {$\mo{g}$};
\draw[->] (f1.north) .. controls +(0,1) and ($(f.south) + (0,-1)$) .. (f.south);
\draw[<-] (e.south west) .. controls +(-.5,-.5) and ($(g1.north) + (0,1)$) .. (g1.north);
\draw[->] (u) -- node[above right]{$\mo{f}$} (e);
\draw[->] (u.north east) .. controls +(.5,.5) and ($(g.south) + (0,-.5)$) .. (g.south);
\end{tikzpicture}
and
\begin{tikzpicture}[baseline=(e.base)]
\node(f2) at (.5,-1) {$\mo{f}$};
\node(g2) at (1.5,-1) {$\mo{g}$};
\node(u)[circle,draw] at (-1,0) {$\eta$};
\node(e)[circle,draw] at (0,1) {$\varepsilon$};
\node(f) at (-.5,2) {$\mo{f}$};
\node(g) at (.5,2) {$\mo{g}$};
\draw[->] (u.north west) .. controls +(-.5,.5) and ($(f.south) + (0,-.5)$) .. (f.south);
\draw[->] (u) -- node[above left]{$\mo{g}$} (e);
\draw[<-] (e.south east) .. controls +(.5,-.5) and ($(f2.north) + (0,1)$) .. (f2.north);
\draw[->] (g2.north) .. controls +(0,1) and ($(g.south) + (0,-1)$) .. (g.south);
\end{tikzpicture}
equal
\begin{tikzpicture}[baseline=-1.5cm]
\node(f12) at (0,0) {$\mo{f}$};
\node(f22) at (1,0) {$\mo{g}$};
\node(f11) at (0,-3) {$\mo{f}$};
\node(f21) at (1,-3) {$\mo{g}$};
\draw[->] (f11.north) .. controls +(0,1.5) and ($(f12.south) + (0,-1.5)$) .. (f12.south);
\draw[->] (f21.north) .. controls +(0,1.5) and ($(f22.south) + (0,-1.5)$) .. (f22.south);
\end{tikzpicture}
due to adjunction properties
.
\end{description}
\end{proof}

\begin{exercise}
Prove that, in the 2-category~$\cat{CAT}$, for every monad~$\alg{M}$ with underlying functor $M$ on a category~$\cat{C}$ there is some adjunction $F \dashv U$ such that $M$ equals $F \cocomp U$.
Hint: use the underlying functor $U : \cat{Alg}(\alg{M}) \mto \cat{C}$ as the right adjoint.
\end{exercise}

\begin{proof}
Let $\alg{M}$ be $\langle \cat{C}, M, \mu, \prf{d}, \eta, \prf{i} \rangle$.
Let $U : \cat{Alg}(\alg{M}) \mto \cat{C}$ be the underlying functor of $\cat{Alg}(\alg{M})$.
Let $F : \cat{C} \mto \cat{Alg}(\alg{M})$ be the functor mapping each object $\ob{C}$ to the algebra $\langle M(\ob{C}), \mu_\ob{C}, \prf{a}, \prf{i} \rangle$ and each morphism $\mo{f} : \ob{C}_1 \mto \ob{C}_2$ to the algebra morphism $\langle M(\mo{f}), \prf{d}_\mo{f} \rangle$ where $\prf{d}_\mo{f} : M(M(\mo{f})) \cocomp \mu_{\ob{C}_2} = \mu_{\ob{C}_1} \cocomp M(\mo{f})$ comes from naturality of $\mu$.
The fact that $F$ is functorial comes from functoriality of $M$.
$F \cocomp U$ then equals $M$, so we can define the unit of the adjunction $\eta : \cat{C} \nto F \cocomp U$ as the unit of the monad $\eta : \cat{C} \nto M$.
For the counit $\varepsilon$, we map each algebra $\langle \ob{C}, \mo{a}, \prf{d}_\mo{a}, \noprf \rangle$ to the morphism of algebras $\langle \mo{a}, \prf{d}_\mo{a} \rangle : U(F(\langle \ob{C}, \mo{a}, \prf{d}_\mo{a}, \noprf \rangle)) = \langle M(\ob{C}), \mu_\ob{C}, \prf{d}, \prf{i} \rangle \mto \langle \ob{C}, \mo{a}, \prf{d}_\mo{a}, \noprf \rangle$.
$\varepsilon$ is natural because all algebra morphisms are distributive.
Lastly, $((\eta \cdot F) \cocomp (F \cdot \varepsilon))_\ob{C}$ is defined as $M(\eta_\ob{C}) \cocomp \mu_\ob{C}$ which equals the identity since $\eta$ is an identity of $\mu$, and $((U \cdot \eta) \cocomp (\varepsilon \cdot U))_{\langle \ob{C}, \mo{a}, \noprf, \prf{i}_\mo{a} \rangle}$ is defined as $\eta_\ob{C} \cocomp \mo{a}$ which equals the identity by $\prf{i}_\mo{a}$.
Thus, $\langle \cat{C}, F, U, \eta, \varepsilon, \noprf, \noprf \rangle$ forms an adjunction with $F \cocomp U$ equal to $M$.
\end{proof}

\end{document}