From df0d5bcbc9db8ace3cb1eb383d18094e3bea07a6 Mon Sep 17 00:00:00 2001
From: Juan Marin Noguera <juan@mnpi.eu>
Date: Sun, 18 Jun 2023 00:41:13 +0200
Subject: Categorías asociadas a una mónada
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 ch6_monads.tex | 266 +++++++++++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 251 insertions(+), 15 deletions(-)

(limited to 'ch6_monads.tex')

diff --git a/ch6_monads.tex b/ch6_monads.tex
index 15103ff..da07c48 100644
--- a/ch6_monads.tex
+++ b/ch6_monads.tex
@@ -74,6 +74,8 @@ Este capítulo se basa principalmente en \cite[VI]{maclane}.
   \begin{enumerate}
   \item $\power:\bSet\to\bSet$ es una mónada con las operaciones indicadas 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
@@ -81,16 +83,17 @@ Este capítulo se basa principalmente en \cite[VI]{maclane}.
     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 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}), y las funciones
-    entre conjuntos se pueden llevar a morfismos de álgebras libres operando
-    sobre los elementos del dominio en el árbol.  Entonces el equivalente a la
-    lista de un elemento sería (la clase de equivalencia de) un árbol cuya raíz
-    es dicho elemento, y el equivalente a concatenar listas es sustituir cada
-    elemento base del árbol, que es a su vez una clase de equivalencia de
-    árboles, por un representante de esta clase a modo de subárbol. Claramente
-    estas transformaciones son naturales y forman una mónada.
+  \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}), y las funciones entre conjuntos se pueden llevar
+    a morfismos de álgebras libres operando sobre los elementos del dominio en
+    el árbol.  Entonces el equivalente a la lista de un elemento sería (la clase
+    de equivalencia de) un árbol cuya raíz es dicho elemento, y el equivalente a
+    concatenar listas es sustituir cada elemento base del árbol, que es a su vez
+    una clase de equivalencia de árboles, por un representante de esta clase a
+    modo de subárbol. Claramente 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>>
@@ -137,6 +140,10 @@ Este capítulo se basa principalmente en \cite[VI]{maclane}.
   \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.
@@ -155,7 +162,7 @@ Este capítulo se basa principalmente en \cite[VI]{maclane}.
   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.
+  conmutan, con la composición vertical y la identidad evidente.
   \begin{figure}
     \centering
     \begin{subfigure}{.45\linewidth}
@@ -187,10 +194,239 @@ Este capítulo se basa principalmente en \cite[VI]{maclane}.
   \end{figure}
 \end{definition}
 
-% TODO Todo esto el viernes:
-% TODO Definición de la categoría de mónadas
-% TODO Álgebras de una mónada (sin llegar al teorema de Beck)
-% TODO Categorías de Kleisli
+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 qué
+sí, y de hecho en general cada mónada se puede describir mediante dos
+adjunciones distintas 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$ tales 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 la identidad 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
+  $e=\eps_e:\mu_{\cod e}\to e$ 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 debemos ver que $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$,
+  $G\eps_d:GFGd\to Gd$ se puede ver 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}$ es
+  por 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$, $Kf$ es un morfismo de $T$-álgebras por la naturalidad de
+  $\eps$. 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 única. Si $d$ es un objeto de $\cD$, $Kd$ es una
+  $T$-álgebra y $G'Kd=Gd$ implica que el objeto subyacente a $Kd$ es $Gd$, y si
+  $f$ es un morfismo, $G'Kf=Gf$ implica que $Kf=Gf$. Ahora bien, las dos
+  adjunciones consideradas tienen el mismo $\eta$, con lo que la caracterización
+  de las transformaciones de adjunciones (\ref{prop:adj-transform}) aplicada a
+  estas dos adjunciones y a los funtores $1:\cC\to\cC$ y $K:\cD\to\cC^T$ 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}
+
+El que estas categorías son una generalización de las variedades algebraicas
+viene dado
+
+\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$, con aridades respectivas
+  $n_1,\dots,n_k$, y sea $(F,U,\eta,\eps)$ la adjunción mencionada, de modo que
+  $T=(UF,\eta,G\eps F)$, queremos definir un isomorfismo
+  $K:(\Omega,E)\dash\bAlg\to\cC^T$ en las condiciones del teorema anterior.
+
+  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 con operadores $s_1,\dots,s_k$ y elementos de $c$,
+  por lo que podemos definir $K(S,(\nu_i)_i)$ como la <<función de evaluación>>
+  $UFS\to S$ por los operadores $\nu_1,\dots,\nu_k$.
+
+  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 claramente $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, pero $K$ se ha definido de igual forma que en la
+  prueba del teorema anterior, por lo que es el mismo $K$.
+\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$. Dicha categoría también tiene un objeto inicial, la
+categoría de Kleisli, que como veremos en el siguiente capítulo es 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 fácil comprobar que estas definiciones de composición e identidad son válidas
+y 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}$. Ahora bien, si $L,L':\cC_T\to\cD$ son dos
+  funtores que cumplen la condición, por igualación $L\eps'_c=L'\eps'_c$ y, por
+  ser $\eps'_c$ una flecha universal desde un funtor, es un retracto y por tanto
+  un epimorfismo, con lo que $L=L'$.
+\end{proof}
 
 %%% Local Variables:
 %%% mode: latex
-- 
cgit v1.2.3

