diff options
Diffstat (limited to 'ch6_monads.tex')
| -rw-r--r-- | ch6_monads.tex | 266 |
1 files changed, 251 insertions, 15 deletions
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 |