Mónade (teoria das categorias)

Na teoria das categorias, uma mónade, mônade ou mônada (ou tripla, nome porém menos usado) é um endofunctor, junto a duas transformações naturais, satisfazendo regras formalmente análogas às de um monoide. Aplicações do conceito incluem a determinação de equivalências com as categorias de álgebras sobre mônades, sendo centrais na álgebra universal, além do uso na ciência da computação como modelo conveniente para, por exemplo, a manipulação de estado global e o não determinismo.

Definição

Uma mônade numa categoria Predefinição:Math consiste de um functor Predefinição:Math, uma transformação natural Predefinição:Math, chamada unidade, e uma transformação natural Predefinição:Math, chamada multiplicação, tais que os diagramas abaixo comutam:

Diagrama do elemento neutro	Diagrama da associatividade

Álgebra sobre mônada

Dada mônada Predefinição:Math na categoria Predefinição:Math, uma Predefinição:Math-álgebra é uma dupla consistindo de objeto Predefinição:Math e morfismo Predefinição:Math tais que os diagramas abaixo comutam:

Compatibilidade com a unidade	Compatibilidade com a multiplicação

Um morfismo Predefinição:Math entre Predefinição:Math-álgebras é um morfismo Predefinição:Math em Predefinição:Math tal que o diagrama abaixo comuta:

Assim, as Predefinição:Math-álgebras formam uma categoria, chamada categoria de Eilenberg–Moore para Predefinição:Math, e denotada por Predefinição:Math.

Exemplos

• Toda adjunção Predefinição:Math determina uma mônade, com endofunctor Predefinição:Math, unidade Predefinição:Math (isto é, a mesma que a unidade da adjunção) e multiplicação Predefinição:Math. A seguir, exemplos de mônades provenientes de adjunções:
  • A adjunção entre o functor livre $𝖲𝖾𝗍\to 𝖬𝗈𝗇$ e o functor "esquecidiço" $𝖬𝗈𝗇\to 𝖲𝖾𝗍$, em que $𝖬𝗈𝗇$ denota a categoria de monoides, origina a mônade de lista (como chamada na ciência da computação), na qual

    $T(A)=\coprod _{n\in \{0,1,\dots \}}{A}^n$, isto é, o conjunto de sequências finitas de elementos de $A$,

    ${\eta }_A(a)={\iota }_1(a)$, a sequência de um elemento,

    e $\mu$ pode ser descrito por concatenação de sequências.

    • As Predefinição:Math-álgebras correspondem biunivocamente a monoides, de modo que o morfismo Predefinição:Math corresponde à família de funções Predefinição:Math, levando uma sequência Predefinição:Math ao produto Predefinição:Math (que será a identidade se Predefinição:Math).
  • Denotando-se ${𝖲𝖾𝗍}_{\star }$ a categoria dos conjuntos com um dos elementos selecionado, chamado "base", e com morfismos as funções de conjuntos que levam uma base a outra base, há a adjunção entre $F:𝖲𝖾𝗍\to {𝖲𝖾𝗍}_{\star }$ e $G:{𝖲𝖾𝗍}_{\star }\to 𝖲𝖾𝗍$, onde $F(A)=(A⨿\{\bullet \},{\iota }_2(\bullet ))$ (adiciona uma base) e $G(A,a)=A$ (esquece qual é a base). A mônade correspondente é chamada de mônade "talvez", na qual:

    $T(A)=T⨿\{\bullet \}$, uma união disjunta com um novo elemento,

    ${\eta }_A(a)={\iota }_1(a)$,

    ${\mu }_A({\iota }_1({\iota }_1(a)))={\iota }_1(a)$, ${\mu }_A({\iota }_1({\iota }_2(\bullet ))={\mu }_A({\iota }_2(\bullet ))={\iota }_2(\bullet )$.

    • A categoria Predefinição:Math, neste caso, é isomorfa à categoria ${𝖲𝖾𝗍}_{\star }$.
• Quando Predefinição:Math é uma pré-ordem, uma mônada é uma função crescente Predefinição:Math satisfazendo Predefinição:Math, Predefinição:Math, para cada Predefinição:Math; no caso em que a ordem é parcial, Predefinição:Math é chamado operador de fecho, e as Predefinição:Math-álgebras correspondem aos elementos fechados (isto é, aqueles satisfazendo Predefinição:Math).
• Para cada monoide Predefinição:Math, há uma mônada na categoria dos conjuntos, na qual Predefinição:Math, Predefinição:Math e Predefinição:Math. Uma Predefinição:Math-álgebra é uma ação de monoide.

Adjunções a partir de mônadas

Dada mônada Predefinição:Math em Predefinição:Math, há uma adjunção

Predefinição:Math,

em que $$\begin{array}{cc}{G}^T((x,h)\stackrel{f}{\to }(x^{\prime },h^{\prime }))& =x\stackrel{f}{\to }{x}^{\prime }\\ F^T\left(x\stackrel{f}{\to }{x}^{\prime }\right)& =(T(x),{\mu }_x)\stackrel{T(f)}{\to }(T(x^{\prime }),{\mu }_{x^{\prime }})\\ ({\eta }^T{)}_x& ={\eta }_x\\ ({ϵ}^T{)}_{(x,h)}& =h,\end{array}$$ e ainda mais esta adjunção induz a mônada Predefinição:Math (isto é, Predefinição:Math, Predefinição:Math e Predefinição:Math).

A Predefinição:Math-álgebra Predefinição:Math, aparecendo na definição de Predefinição:Math, é chamada Predefinição:Math-álgebra livre.

Categoria de Kleisli

A categoria de Kleisli Predefinição:Math para uma mônada Predefinição:Math é definida por:

• ter os seus objetos Predefinição:Math em correspondência biunívoca com os objetos Predefinição:Math de Predefinição:Math;
• ter os seus morfismos Predefinição:Math em correspondência biunívoca com os morfismos Predefinição:Math, com identidades e composições $$\begin{array}{cc}{a}_T\stackrel{1_{a_T}}{\to }{a}_T& ={(a\stackrel{{\eta }_a}{\to }T(a))}_T\\ a_T\stackrel{f_T}{\to }{b}_T\stackrel{g_T}{\to }{c}_T& ={(a\stackrel{f}{\to }T(b)\stackrel{T(g)}{\to }{T}^2(c)\stackrel{{\mu }_c}{\to }T(c))}_T.\end{array}$$

Há também uma adjunção

Predefinição:Math,

em que $$\begin{array}{cc}{F}_T(a\stackrel{f}{\to }b)& ={(a\stackrel{f}{\to }b\stackrel{{\eta }_b}{\to }T(b))}_T\\ G_T(a_T\stackrel{g_T}{\to }{b}_T)& =T(a)\stackrel{T(g)}{\to }{T}^2(b)\stackrel{{\mu }_b}{\to }T(b)\\ a\stackrel{({\eta }_T{)}_a}{\to }{G}_T(F_T(a))& =a\stackrel{{\eta }_a}{\to }T(a)\\ F_T(G_T(a_T))\stackrel{({ϵ}_T{)}_{a_T}}{\to }{a}_T& ={(T(a)\stackrel{1_{T(a)}}{\to }T(a))}_T,\end{array}$$ e ainda mais esta adjunção induz a mesma mônada.

Functor monádico

A categoria de Eilenberg–Moore e a categoria de Kleisli satisfazem a propriedade universal a seguir. Para cada adjunção Predefinição:Math, denotando-se por Predefinição:Math a mônada associada, há único functor Predefinição:Math tal que Predefinição:Math e Predefinição:Math, e há único functor Predefinição:Math tal que Predefinição:Math e Predefinição:Math; com efeito, eles têm definições: $$\begin{array}{cc}K(d\stackrel{g}{\to }{d}^{\prime })& =(G(d),G({ϵ}_d))\stackrel{G(g)}{\to }(G(d^{\prime }),G({ϵ}_{d^{\prime }}))\\ L(a_T\stackrel{f_T}{\to }{b}_T)& =F(a)\stackrel{F(f)}{\to }F(G(F(b)))\stackrel{{ϵ}_{F(b)}}{\to }F(b).\end{array}$$

Um functor Predefinição:Math é dito monádico (respectivamente estritamente monádico) se e só se faz parte de uma adjunção Predefinição:Math (que é chamada uma adjunção monádica) para a qual o functor de comparação Predefinição:Math é uma equivalência de categorias (respectivamente um isomorfismo de categorias).

Teorema de monadicidade

Dado functor Predefinição:Math, um coequalizador que Predefinição:Math-cinde para uma dupla de morfismos paralelos Predefinição:Math em Predefinição:Math é um coequalizador que cinde para a dupla Predefinição:Math. O functor Predefinição:Math é dito

• estritamente criar coequalizadores que Predefinição:Math-cindem quando, sempre que Predefinição:Math é coequalizador que cinde para uma dupla Predefinição:Math, existe único morfismo Predefinição:Math em Predefinição:Math tal que Predefinição:Math, e ainda mais este Predefinição:Math é coequalizador para Predefinição:Math (não necessariamente que cinde).
• criar coequalizadores que Predefinição:Math-cindem quando, sempre que Predefinição:Math tem coequalizador que Predefinição:Math-cinde, Predefinição:Math tem coequalizador (não necessariamente que cinde) preservado por Predefinição:Math, e ainda mais, sempre que Predefinição:Math satisfaz Predefinição:Math e é tal que Predefinição:Math é coequalizador que cinde para Predefinição:Math, então Predefinição:Math deve ser coequalizador para Predefinição:Math (não necessariamente que cinde).

(Saunders Mac Lane usa o termo criar em vez de estritamente criar.)

Denotando-se por Predefinição:Math a mônada associada a uma adjunção Predefinição:Math, o functor Predefinição:Math estritamente cria coequalizadores que Predefinição:Math-cindem. Como, para cada Predefinição:Math-álgebra Predefinição:Math, o diagrama a seguir é coequalizador que cinde$$\begin{array}{cccc}& \stackrel{{\eta }_{T(a)}}{\curvearrowleft }& & \stackrel{{\eta }_a}{\curvearrowleft }\\ T^2(a)& \stackrel{{\mu }_a}{\underset{T(h)}{\rightrightarrows }}& T(a)& \underset{h}{\to }& a\end{array}$$tem-se o diagrama de coequalizador em Predefinição:Math$$\begin{array}{ccccc}(T^2(a),{\mu }_{T(a)})& \stackrel{{\mu }_a}{\underset{T(h)}{\rightrightarrows }}& (T(a),{\mu }_a)& \underset{h}{\to }& (a,h)\end{array}$$ chamado de presentação canônica da Predefinição:Math-álgebra Predefinição:Math; ela generaliza, por exemplo, a representação de um grupo como um quociente de um grupo livre.

O teorema de monadicidade de Beck diz que um functor adjunto direito Predefinição:Math é monádico (respectivamente estritamente monádico) se e só se cria (respectivamente estritamente cria) coequalizadores que Predefinição:Math-cindem.

Há uma versão "reflexiva" do teorema de monadicidade. Uma dupla de morfismos Predefinição:Math é dita ser reflexiva quando existe Predefinição:Math tal que Predefinição:Math. Então, dado functor Predefinição:Math, se

• Predefinição:Math é functor adjunto direito,
• Predefinição:Math reflete isomorfismos (isto é, Predefinição:Math é isomorfismo sempre que Predefinição:Math é isomorfismo),
• e Predefinição:Math admite coequalizadores de duplas reflexivas que Predefinição:Math-cindem e Predefinição:Math preserva esses coequalizadores,

então o functor Predefinição:Math é monádico.

O resultado permite demonstrar que os seguintes functores são monádicos:

• Os functores "esquecidiços" da categoria de monoides, grupos, anéis, e outras estruturas algébricas, para a categoria dos conjuntos.
• O functor "esquecidiço" da categoria de espaços compactos de Hausdorff para a categoria dos conjuntos.
• O functor Predefinição:Math de conjuntos de partes e pré-imagens.
• A inclusão Predefinição:Math de uma subcategoria reflexiva (plena) Predefinição:Math em Predefinição:Math.

A utilidade do teorema de Beck é que uma equivalência entre Predefinição:Math e Predefinição:Math faz com que essas duas categorias compartilhem algumas propriedades. Por exemplo:

• O functor Predefinição:Math reflete isomorfismos e estritamente cria todos os limites existentes em Predefinição:Math.
• O functor Predefinição:Math estritamente cria todos os colimites existentes em Predefinição:Math que são preservados por Predefinição:Math e Predefinição:Math.
• Se Predefinição:Math é cocompleta e Predefinição:Math admite coequalizadores, então Predefinição:Math também é cocompleta.

Bibliografia

• Predefinição:Citar livro
• Predefinição:Citar livro
• Predefinição:Citation