path: root/ch6_monads.tex

Al igual que cuando el dominio y el codominio de un morfismo coinciden hablamos
de un \conc{endomorfismo}, cuando esto le ocurre a un funtor hablamos de un
\conc{endofuntor}. Los endofuntores son particularmente relevantes en tanto que
se puede estudiar, por ejemplo, la relación de un objeto o morfismo con su
imagen, o lo que ocurre al aplicar el endofuntor varias veces.

Por ejemplo, tomemos el endofuntor $\power:\bSet\to\bSet$. Dado un conjunto $X$,
entre $X$ y $\power X$ existe un monomorfismo $\eta_X:X\to\power X$ dado por
$\eta_X(x)\coloneqq\{x\}$, que es natural. Por otro lado, aunque podemos aplicar
este funtor a $X$ varias veces, siempre podemos volver de $\power^nX$ a
$\power X$ aplicando sucesivamente la unión, que podemos ver como una función
$\mu_X:\power\power X\to\power X$ dada por $\mu_X(\cA)\coloneqq\bigcup\cA$. Esto
también define una transformación natural que, además, <<da igual>> en qué orden
se aplique, en el sentido de que, si $S\in\power^3X$, aplicar primero
$\mu_{\power X}$ a $S$ y luego $\mu_X$ al resultado es lo mismo que aplicar
$\mu_X$ a cada elemento de $S$ y a continuación aplicar $\mu_X$ al resultado.
Además, intuitivamente $\mu$ se puede ver como una inversa por un lado de
$\eta$, en tanto que $\mu_X(\eta_{\power X}(S))\equiv S$.

Muchos endofuntores comunes admiten transformaciones naturales con estas
propiedades, y cuando esto ocurre hablamos de mónadas. En este capítulo
estudiamos las mónadas y sus principales propiedades, basándonos principalmente
en \cite[VI]{maclane}.

\begin{definition}
  Una \conc{mónada} en una categoría $\cC$ es una tupla $(T,\eta,\mu)$
  formada por un funtor $T:\cC\to\cC$ y dos transformaciones naturales
  $\eta:1_\cC\to T$ y $\mu:T^2\to T$ que cumplen las siguientes
  condiciones, ilustradas en la figura \ref{fig:monad}.
  \begin{enumerate}
  \item $\mu\cdot T\mu = \mu\cdot\mu T$.
  \item $\mu\cdot\eta T = \mu\cdot T\eta = 1$.
  \end{enumerate}
\end{definition}

% \begin{proposition}
%   Si $(T,\eta,\mu)$ es una mónada en $\cC$ y $c$ es un objeto de $\cC$,
%   $\eta_c:c\monicTo Tc$ es una sección y $\mu_c:TTc\epicTo Tc$ es una
%   retracción.
% \end{proposition}

\begin{figure}
  \centering
  \begin{subfigure}{.45\linewidth}
    \centering
    \begin{diagram}
      \path (0,2) node(TTT){$T^3$} (2,2) node(TTP){$T^2$};
      \path (0,0) node(PTT){$T^2$} (2,0) node(T){$T$};
      \draw[->] (TTT) -- node[above]{$T\mu$} (TTP);
      \draw[->] (TTT) -- node[left]{$\mu T$}(PTT);
      \draw[->] (TTP) -- node[right]{$\mu$} (T);
      \draw[->] (PTT) -- node[below]{$\mu$} (T);
    \end{diagram}
    \caption{Conmutatividad de la unión}
  \end{subfigure}
  \hfil
  \begin{subfigure}{.45\linewidth}
    \centering
    \begin{diagram}
      \path (0,2) node(IT){$1\circ T$} (2,2) node(TT){$T^2$} (4,2) node(TI){$T\circ 1$};
      \path                            (2,0) node(T){$T$} node[below]{$\phantom{\mu}$};
      \draw[->] (IT) -- node[above]{$\eta T$} (TT);
      \draw[->] (TI) -- node[above]{$T\eta$} (TT);
      \draw[->] (TT) -- node[right]{$\mu$} (T);
      \draw[->] (IT) -- node[left]{$1$} (T);
      \draw[->] (TI) -- node[right]{$1$} (T);
    \end{diagram}
    \caption{Relación entre la unidad y la unión}
  \end{subfigure}
  \caption{Condiciones de coherencia de las mónadas.}
  \label{fig:monad}
\end{figure}

\begin{example}\;
  \begin{enumerate}
  \item $\power:\bSet\to\bSet$ es una mónada, descrita en la introducción del
    capítulo.
  \item Toda categoría admite una \conc{mónada identidad}, formada por el
    endofuntor identidad y dos transformaciones naturales identidad.
  \item Sea $(^*):\bSet\to\bSet$ el endofuntor que asocia a cada objeto $X$ el
    conjunto subyacente de su monoide libre, dado por $\bigcup_{n\in\sNat}X^n$,
    y que lleva cada función $f:X\to Y$ a la función
    $(x_1,\dots,x_k)\mapsto(fx_1,\dots,fx_k)$. Este endofuntor es una mónada con
    las transformaciones naturales $\eta:1\to(^*)$ que lleva cada elemento de un
    conjunto a la lista de un elemento ($\eta_X(x)=(x)$) y $\mu:(^*)^2\to(^*)$
    que concatena una lista de listas en una sola lista.
  \item \label{enu:monad-variety} Esto se puede generalizar a todas las
    variedades algebraicas. El álgebra libre sobre un conjunto $X$ es un
    conjunto cociente de árboles formados por operadores y elementos de $X$
    (\ref{prop:free-algebra}), o de expresiones formales que involucran a dichos
    operadores y elementos, y las funciones entre conjuntos se pueden llevar a
    morfismos de álgebras libres que operan elemento a elemento sobre las
    expresiones.  Entonces la unidad $\eta_X$ llevaría cada elemento de $X$ a
    (la clase de equivalencia de) la expresión formada sólo por dicho elemento,
    y la unión $\mu_X$ tomaría árboles cuyas hojas son (clases de equivalencia
    de) otros árboles y sustituiría las hojas por los subárboles que
    representan. Es fácil ver que estas transformaciones son naturales y forman
    una mónada.
  \item Sean $\cC$ una categoría con coproductos finitos y $d$ un objeto de
    $\cC$. Sea $E:\cC\to\cC$ un endofuntor que a cada objeto $c$ le asocia
    $c\oplus d$ y a cada morfismo $f:b\to c$ el morfismo <<suma>>
    $Ef=f\oplus 1_d:b\oplus d\to c\oplus d$. Si $\eta_c:c\monicTo c\oplus d$ es
    la inclusión canónica y $\mu_c:c\oplus d\oplus d\epicTo c\oplus d$ es la
    función que <<identifica>> las dos copias de $d$ en el sentido evidente,
    entonces $(E,\eta,\mu)$ es una mónada.
  \item Sean $s$ un conjunto y $S\coloneqq\hom(s,-\times s)$ un endofuntor en
    $\bSet$ que lleva cada conjunto $X$ al conjunto de funciones
    $s\to X\times s$ y cada función $f$ a $\hom(s,f\times 1_s)$. Entonces $S$ es
    una mónada con las transformaciones naturales $\eta:1\to S$ y $\mu:S^2\to S$
    dadas por la formación de pares $\eta_X(x)(y)\coloneqq(x,y)$ y la <<doble
    evaluación>> $\mu_X(f)(y)\coloneqq (p_1fy)(p_2fy)$, donde $p_1$ y $p_2$ son
    las proyecciones canónicas de $\hom(X,s)\times s$.
    % \begin{proof}
    %   Escribiendo $e(f,y)\coloneqq f(y)$, se tiene $\mu_X(f)(y)\equiv e(f(y))$ y
    %   $\mu_X(f)\equiv e\circ f$ (por abuso de notación, $e$ no representa una
    %   función fija, sino cualquier función expresada así independientemente de
    %   dominio y codominio). Entonces, para $f\in S^3X$,
    %   \begin{multline*}
    %     \mu_X((S\mu_X)(f))=\mu_X(\hom(s,\mu_X\times 1_s)(f))=\mu_X((\mu_X\times 1_s)\circ f)=
    %     e\circ(\mu_X\times 1_s)\circ f=\\
    %     =(y\mapsto e(\mu_Xpfy,qfy))=(y\mapsto(\mu_Xpfy)(qfy))=(y\mapsto e((pfy)(qfy)))=\\
    %     =e\circ e\circ f=e\circ(\mu_{SX}\circ f)=\mu_X(\mu_{SX}(f)),
    %   \end{multline*}
    %   y para $f\in SX$,
    %   \begin{multline*}
    %     \mu_X((S\eta_X)(f))=\mu_X(\hom(s,\eta_X\times 1_s)(f))=e\circ(\eta_X\times 1_s)\circ f=\\
    %     =(y\mapsto e(\eta_Xpfy,qfy))=
    %     (y\mapsto(\eta_Xpfy,qfy))=(y\mapsto fy)=f\\=e\circ(y\mapsto(f,y))=
    %     =e\circ(\eta_{SX}(f))=\mu_X(\eta_{SX}(f)).
    %   \end{multline*}
    % \end{proof}
  \item En un conjunto parcialmente ordenado $(S,\leq)$ visto como categoría, un
    endofuntor es una función $f:S\to S$ monótona, es decir, tal que
    $x\leq y\implies fx\leq fy$. Las transformaciones naturales asociadas a $f$
    en una mónada están unívocamente determinadas y existen si y sólo si, para
    todo $x\in S$, $x\leq fx$ y $f^2x\leq fx$, pues al ser una categoría fina
    los diagramas correspondientes siempre conmutan. Estas ecuaciones implican
    que $f$ es idempotente. Así, las mónadas en conjuntos parcialmente ordenados
    son \conc{operaciones de clausura}, funciones monótonas e idempotentes con
    $x\leq fx$ para todo $x$. Este término se usa especialmente cuando el orden
    es la inclusión de conjuntos.
  \end{enumerate}
\end{example}

El ejemplo \ref{enu:monad-variety} de la lista anterior se puede generalizar aún
más, de las variedades algebraicas a todas las categorías concretas que admitan
un funtor libre.

\begin{proposition}
  Si $(F,G,\eta,\eps)$ es una adjunción entre las categorías $\cB$ y $\cC$,
  entonces $(G\circ F, \eta, G\eps F)$ es una mónada.
\end{proposition}
\begin{proof}
  Al componer horizontalmente $\eps$ consigo mismo (\ref{def:comp-horiz})
  obtenemos que $\eps\circ\eps=\eps\cdot\eps FG=\eps\cdot FG\eps$, y componiendo
  con $G$ por la izquierda y con $F$ por la derecha obtenemos
  $G\eps F\cdot G\eps FGF=G\eps F\cdot GFG\eps F$, que es la primera condición
  de coherencia. Para la segunda basta componer con $F$ por la derecha en la
  identidad $G\eps\cdot\eta G=1$ y con $G$ por la izquierda en $\eps F\cdot F\eta=1$.
\end{proof}

\begin{definition}
  Dada una categoría $\cC$, la \conc{categoría de mónadas} de $\cC$ es una
  categoría $\Mnd{\cC}$ cuyos objetos son las mónadas sobre $\cC$ y cuyos
  morfismos $(S,\eta,\mu)\to(T,\eta',\mu')$ son las transformaciones naturales
  $\tau:S\to T$ tales que los diagramas en la figura \ref{fig:monad-morph}
  conmutan, con la composición vertical y las identidades evidentes.
  \begin{figure}
    \centering
    \begin{subfigure}{.45\linewidth}
      \centering
      \begin{diagram}
        \path (0,2) node(ID){$1$} (2,2) node(S){$S$};
        \path                     (2,0) node(T){$T$} node[below]{$\phantom{\mu'}$};
        \draw[->] (ID) -- node[above]{$\eta$} (S);
        \draw[->] (ID) -- node[left]{$\eta'$} (T);
        \draw[->] (S) -- node[right]{$\tau$} (T);
      \end{diagram}
      \caption{Conmutatividad de la unidad}
    \end{subfigure}
    \hfil
    \begin{subfigure}{.45\linewidth}
      \centering
      \begin{diagram}
        \path (0,2) node(SS){$S^2$} (2,2) node(S){$S$};
        \path (0,0) node(TT){$T^2$} (2,0) node(T){$T$};
        \draw[->] (SS) -- node[above]{$\mu$} (S);
        \draw[->] (TT) -- node[below]{$\mu'$} (T);
        \draw[->] (SS) -- node[left]{$\tau\circ\tau$} (TT);
        \draw[->] (S) -- node[right]{$\tau$} (T);
      \end{diagram}
      \caption{Conmutatividad de la unión}
    \end{subfigure}
    \caption{Morfismos de mónadas.}
    \label{fig:monad-morph}
  \end{figure}
\end{definition}

El concepto dual al de mónada es el de \conc{comónada}, aunque la utilidad de
las comónadas es más limitada.

\section{Categorías de Eilenberg-Moore}

Hemos visto que toda adjunción genera una mónada, por lo que cabe preguntarse si
toda mónada es generada de esta manera por una adjunción. La respuesta es que
sí, y de hecho en general cada mónada se puede describir mediante dos
adjunciones asociadas a dos categorías distintas, la categoría de
Eilenberg-Moore y la categoría de Kleisli. Empezamos viendo la primera, que
generaliza el concepto de variedad algebraica.

\begin{definition}
  Sea $T=(T,\eta,\mu)$ una mónada en una categoría $\cC$.
  \begin{enumerate}
  \item Una \conc{$T$-álgebra} es un morfismo $e:Tc\epicTo c$ para cierto objeto
    $c$ en $\cC$ tal que los diagramas en la figura \ref{fig:T-algebra}
    conmutan. Llamamos \conc{mapa de estructura} de la $T$-álgebra a $e$ y
    \conc{objeto subyacente} a $c$.
    \begin{figure}
      \centering
      \begin{subfigure}{.45\linewidth}
        \centering
        \begin{diagram}
          \path (0,2) node(TT){$T^2c$} (2,2) node(TE){$Tc$};
          \path (0,0) node(TM){$Tc$}   (2,0) node(C){$c$};
          \draw[->] (TT) -- node[above]{$Te$} (TE);
          \draw[->] (TM) -- node[below]{$e$} (C);
          \draw[->] (TT) -- node[left]{$\mu_c$} (TM);
          \draw[->] (TE) -- node[right]{$e$} (C);
        \end{diagram}
        \caption{Propiedad asociativa}
      \end{subfigure}
      \hfil
      \begin{subfigure}{.45\linewidth}
        \centering
        \begin{diagram}
          \path (0,2) node(S){$c$} (2,2) node(T){$Tc$};
          \path                    (2,0) node(E){$c$} (0,0) node[below]{$\phantom{e}$};
          \draw[->] (S) -- node[above]{$\eta_c$} node[above]{$\phantom{Te}$} (T);
          \draw[->] (T) -- node[right]{$e$} (E);
          \draw[->] (S) -- node[left]{$1$} (E);
        \end{diagram}
        \caption{Propiedad unitaria}
      \end{subfigure}
      \caption{Propiedades de las $T$-álgebras.}
      \label{fig:T-algebra}
    \end{figure}
  \item Un morfismo entre dos $T$-álgebras $e:Tc\to c$ y $e':Tc'\to c'$ es un
    morfismo $f:c\to c'$ en $\cC$ tal que $f\circ e=e'\circ Tf$.
  \item La \conc{categoría de Eilenberg-Moore} asociada a $T$, escrita
    $\cC^{(T,\eta,\mu)}$ o simplemente $\cC^T$, es la que tiene como objetos las
    $T$-álgebras y como morfismos los morfismos de $T$-álgebras, con la
    composición y las identidades de $\cC$.
  \end{enumerate}
\end{definition}

\begin{theorem}
  Sea $(T,\eta,\mu)$ una mónada en $\cC$, si $F:\cC\to\cC^T$ actúa sobre los
  objetos como $\mu$ y sobre los morfismos como $T$, $G:\cC^T\to\cC$ <<olvida>>
  el mapa de estructura, asociando a cada $T$-álgebra su objeto subyacente y a
  cada morfismo el mismo, y $\eps:FG\to 1$ lleva cada $T$-álgebra a su mapa de
  estructura, entonces $(F,G,\eta,\eps)$ es una adjunción cuya mónada asociada
  es $(T,\eta,\mu)$.
\end{theorem}
\begin{proof}
  Para cada objeto $c$ en $\cC$, $1_{Tc}$ es la identidad de la $T$-álgebra
  $\mu_c$, y para cada morfismo $f:c\to c'$, $Tf:\mu_c\to\mu_{c'}$ es un
  morfismo de $T$-álgebras por la naturalidad de $\mu$, luego $F$ es un
  funtor. Por otro lado, $G$ claramente es un funtor y $\eps$, que viene dado
  por $\eps_e\coloneqq e:\mu_c\to e$ para cada $e:Tc\to c$, es una
  transformación natural. Además, dada una $T$-álgebra $e:Tc\to c$,
  $G\eps_e\circ\eta_{Ge}=e\circ\eta_c=1$, y dado un objeto $c$ de $\cC$,
  $\eps_{Fc}\circ F\eta_c=\mu_c\circ T\eta_c=1$, luego $(F,G,\eta,\eps)$ es una
  adjunción. Finalmente, es obvio que $G\circ F=T$ siguiendo su actuación sobre
  morfismos, y para un objeto $c$, $G\eps_{Fc}=G\eps_{\eta_c}=\eta_c$ y por
  tanto $G\eps F=\eta$.
\end{proof}

La adjunción definida en este teorema es final en el sentido siguiente.

\begin{theorem}
  Dada una adjunción $(F,G,\eta,\eps)$ de $\cC$ a $\cD$, si $T$ es la mónada
  generada por la adjunción y $(F',G',\eta,\eps')$ es la adjunción de $\cC$ a
  $\cC^T$ definida en el teorema anterior, existe un único funtor
  $K:\cD\to\cC^T$ tal que $(1_\cC,K)$ es una transformación de adjunciones de
  $(F,G,\eta,\eps)$ a $(F',G',\eta,\eps')$.
\end{theorem}
\begin{proof}
  Ya tenemos $1\eta=\eta1$, y queda ver las condiciones $G=G'\circ K$ y
  $F'=K\circ F$.  Sea $(T,\eta,\mu)=(GF,\eta,G\eps F)$ la mónada, para cada
  objeto $d$ de $\cD$, podemos ver $G\eps_d:GFGd\to Gd$ como una $T$-álgebra en
  el objeto $Gd$, pues la propiedad asociativa
  $G\eps_d\circ GFG\eps_d=\eps_d\circ G\eps_{FGd}$ se deduce de la identidad en
  la composición horizontal y la unitaria $G\eps_d\circ\eta_{Gd}=1$ es una
  identidad de las adjunciones. Podemos entonces definir $K$ sobre objetos como
  $Kd=G\eps_d$, y sobre morfismos como $Kf=Gf$, pues la naturalidad de $\eps$
  asegura que $Gf$ es un morfismo de $T$-álgebras. Para cada objeto $c$ de
  $\cC$, $KFc=G\eps_{Fc}=\mu_c=F'c$, y para cada morfismo $f$,
  $KFf=GFf=Tf=F'c$. Del mismo modo, para cada objeto $d$ de $\cD$,
  $G'Kd=G'G\eps_d=Gd$, y para cada morfismo $f$, $G'Kf=G'Gf=Gf$.

  Queda ver que $K$ es único. Si $d$ es un objeto de $\cD$, $Kd$ debe ser una
  $T$-álgebra con objeto subyacente $Gd$, pues $G'Kd=Gd$. Por otro lado, si $f$
  es un morfismo, $G'Kf=Gf$ implica que $Kf=Gf$. Ahora bien, la caracterización
  de las transformaciones de adjunciones (\ref{prop:adj-transform}) aplicada a
  $(1_\cC,K)$ nos da $K\eps=\eps'K$, y entonces, para un objeto $d$, el mapa de
  estructura de $Kd$ es $Kd=\eps'_{Kd}=K\eps_d=G\eps_d$.
\end{proof}

La siguiente proposición muestra que, de hecho, estas categorías son una
generalización del concepto de variedad algebraica.

\begin{proposition}
  Sean $(\Omega,E)\dash\bAlg$ una variedad algebraica y $T$ la mónada generada
  por la adjunción entre el funtor libre y el funtor olvidadizo de dicha
  variedad. Entonces el funtor $K:(\Omega,E)\dash\bAlg\to\cC^T$ del teorema
  anterior es un isomorfismo de categorías.
\end{proposition}
\begin{proof}
  Sean $s_1,\dots,s_k$ las operaciones en $\Omega$ y $n_1,\dots,n_k$ sus
  aridades respectivas, y sea $(F,U,\eta,\eps)$ la adjunción mencionada, de modo
  que $T=(UF,\eta,U\eps F)$.

  Si $(S,(\nu_1,\dots,\nu_k))$ es una $(\Omega,E)$-álgebra, con cada
  $\mu_i:S^{n_i}\to S$, los elementos de $UFS$ son las (clases de equivalencia
  de) expresiones formales construidas a partir de los operadores
  $s_1,\dots,s_k$ y los elementos de $c$, por lo que podemos definir
  $K(S,(\nu_i)_i)$ como la <<función de evaluación>> $e:UFS\to S$ que lleva cada
  elemento de $c$ a sí mismo y cada expresión $s_i(x_1,\dots,x_{n_i})$ a
  $\nu_i(e(x_1),\dots,e(x_{n_i}))$.

  En este contexto, la propiedad asociativa de las $T$-álgebras nos dice que,
  dada una expresión formal sobre expresiones formales sobre elementos de $S$,
  da lo mismo evaluar las expresiones interiores y a continuación la global que
  considerar las expresiones interiores como partes de la expresión global y
  evaluar todo a la vez.  Por su parte, la propiedad unitaria nos dice que
  evaluar una expresión formada sólo por un elemento <<devuelve>> dicho
  elemento. Claramente ambas propiedades se cumplen, y de hecho juntas implican
  que cualquier función $e:UFS\to S$ que las cumpla viene dada por su actuación
  sobre expresiones <<de altura 1>>, es decir, de la forma
  $s_i(x_1,\dots,x_{n_i})$ con los $x_j\in S$, lo que nos da una serie de
  operaciones $\nu_i:S^{n_i}\to S$ que, además, cumplen las igualdades en $E$ al
  estar $e$ definida sobre clases de equivalencia, de modo que estas igualdades
  definen una $(\Omega,E)$-álgebra y $K$ es biyectiva sobre objetos.

  Para los morfismos $f:(S,(\nu_i)_i)\to(S',(\nu'_i)_i)$, podemos definir
  $Kf:S\to S'$ como la propia $f$, que es un morfismo
  $K(S,(\nu_i)_i)\to K(S',(\nu'_i)_i)$ por la conmutatividad de $f$ respecto a
  los operadores de $\Omega$. $K$ así definida es fiel y plena, pues la
  propiedad conmutativa que define los morfismos de $T$-álgebras es precisamente
  la que define los morfismos de $(\Omega,E)$-álgebras.

  Así, $K$ es un isomorfismo, y claramente esta definición de $K$ coincide con
  la del teorema anterior.
\end{proof}

\section{Categorías de Kleisli}

Hemos visto que, dada una mónada en una categoría $\cC$, la adjunción de
Eilenberg-Moore asociada es un objeto final de la categoría de las adjunciones
que definen dicha mónada junto con las transformaciones de mónadas que son la
identidad en $\cC$. Vamos a ver que esta categoría de adjunciones tiene también
un objeto inicial, la categoría de Kleisli, de gran importancia en teoría de la
computación.

\begin{definition}
  Dada una mónada $(T,\eta,\mu)$ en $\cC$, llamamos \conc{categoría de Kleisli}
  asociada a la mónada, escrita $\cC_{(T,\eta,\mu)}$ o simplemente $\cC_T$, a la
  categoría cuyos objetos son los de $\cC$ y cuyos morfismos $a\to b$ son los
  morfismos $a\to Tb$ en $\cC$, donde la composición de dos funtores $f:a\to b$
  y $g:b\to c$ viene dada por
  \[
    g\hat\circ f\coloneqq\mu_c\circ Tg\circ f
  \]
  y la identidad en un objeto $c$ es $\mu_c$.
\end{definition}

% Efectivamente, dados morfismos $f:x\to Ty$, $g:y\to Tz$ y $h:z\to Tw$,
% $(h\hat\circ g)\hat\circ f=\mu_w\circ T\mu_w\circ T^2h\circ Tg\circ
% f=\mu_w\circ\mu_{Tw}\circ T^2h\circ Tg\circ f=\mu_w\circ Th\circ\mu_z\circ
% Tg\circ f=h\hat\circ(g\hat\circ f)$,
% $f\hat\circ\eta_x=\mu_y\circ Tf\circ\eta_x=\mu_y\circ\eta_{Ty}\circ f=f$ y
% $\eta_y\hat\circ f=\mu_y\circ T\eta_y\circ f=f$.

Es rutinario comprobar que estas definiciones de composición e identidad definen
una categoría.

\begin{theorem}
  Sea $(T,\eta,\mu)$ una mónada en $\cC$. Si $F:\cC\to\cC_T$ lleva los objetos a
  ellos mismos y los morfismos $f:a\to b$ a $\eta_b\circ f$, $G:\cC_T\to\cC$
  actúa sobre los objetos como $T$ y lleva los morfismos $f:a\to b$ a
  $\mu_b\circ Tf$ y, para cada objeto $c$,
  $\eps_c\coloneqq 1_c\in\hom_{\cC_T}(Tc,c)$, entonces $(F,G,\eta,\eps)$ es una
  adjunción que genera $(T,\eta,\mu)$.
\end{theorem}
\begin{proof}
  Obviamente $F$ preserva identidades, y es fácil ver que también preserva
  composiciones, por lo que es un funtor. Del mismo modo, es fácil ver que $G$
  también preserva identidades y composiciones. Por su parte, para un objeto
  $c$,
  $G\eps_c\circ\eta_{Gc}=\mu_c\circ T1_c\circ\eta_{Gc}=\mu_c\circ\eta_{Tc}=1$ y
  $\eps_{Fc}\hat\circ F\eta_c=\mu_c\circ T\eps_{Fc}\circ F\eta_c=\mu_c\circ
  1_{TFc}\circ \eta_{Tc}\circ\eta_c=\eta_c$, que es la identidad en $\cC_T$, por
  lo que $(F,G,\eta,\eps)$ es una adjunción.

  Es fácil ver que $GF=T$ tanto para objetos como para morfismos, y finalmente,
  para un objeto $c$, $G\eps_{Fc}=G1_{Fc}=\mu_c\circ 1_{Fc}=\mu_c$, por lo que
  la adjunción genera $(T,\eta,\mu)$.
\end{proof}

\begin{theorem}
  Sean $(F,G,\eta,\eps)$ una adjunción de $\cC$ a $\cD$, $T=(T,\eta,\mu)$ la
  mónada en $\cC$ definida por la adjunción y $(F',G',\eta,\eps')$ la adjunción
  de $\cC$ a $\cC_T$ definida en el teorema anterior, existe un único funtor
  $L:\cC_T\to\cD$ tal que $(1,L)$ es una transformación de la segunda adjunción
  a la primera.
\end{theorem}
\begin{proof}
  Debemos ver que $G'=G\circ L$ y $F=L\circ F'$. Como $F'$ lleva los objetos a
  sí mismos, por la segunda identidad debe ser $Lc\coloneqq Fc$ para cada objeto
  $c$, y la primera identidad claramente se cumple. Para un morfismo $f:a\to b$
  en $\cC_T$ ($f:a\to GFb$ en $\cC$), definimos $Lf\coloneqq\eps_{Fb}\circ Ff$,
  de modo que $LF'f=\eps_{Fb}\circ F\eta_b\circ Ff=Ff$ por las propiedades de la
  adjunción y, por el otro lado, $GLf=G\eps_{Fb}\circ GFf=\mu_b\circ Tf=G'f$.

  Queda ver que $L$ es única. Claramente lo es sobre objetos. Sobre morfismos,
  la caracterización de las transformaciones de adjunciones
  (\ref{prop:adj-transform}) nos da $L\eps'=\eps L$, por lo que para cada objeto
  $c$, $L\eps'_c=\eps_{Lc}=\eps_{Fc}$. Entonces, si $L,L':\cC_T\to\cD$ son dos
  funtores que cumplen la condición, por igualación $L\eps'_c=L'\eps'_c$, pero
  $\eps'_c$ una flecha universal desde un funtor y por tanto es un retracto y un
  epimorfismo, con lo que $L=L'$.
\end{proof}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: