Catégorie de Kleisli

Une catégorie de Kleisli est une catégorie associée à une monade. Elle tient son nom du mathématicien suisse Modèle:Lien qui l'a introduite à l'origine pour montrer que toute monade est issue d'une adjonction.

Définition

On considère une monade $(T,\eta ,\mu )$ sur une catégorie $𝒞$. La catégorie de Kleisli ${𝒞}_T$ possède les mêmes objets que $𝒞$ mais les morphismes sont donnés par

${\mathrm{Hom}}_{{𝒞}_T}(X,Y)={\mathrm{Hom}}_{𝒞}(X,TY)$

L'identité est donnée par $\eta$, et la composition fonctionne ainsi : si $f\in {\mathrm{Hom}}_{{𝒞}_T}(X,Y)$ et $g\in {\mathrm{Hom}}_{{𝒞}_T}(Y,Z)$, on a

$g\circ f={\mu }_Z\circ Tg\circ f$

qui correspond au diagramme :

$X\stackrel{f}{⟶}TY\stackrel{Tg}{⟶}TTZ\stackrel{{\mu }_Z}{⟶}TZ$

Les morphismes de $𝒞$ de la forme $X\to TY$ sont parfois appelés morphismes de Kleisli.

Monades et adjonctions

On définit le foncteur $F:𝒞\to {𝒞}_T$ par :

$FX=X$

$F(f:X\to Y)={\eta }_Y\circ f$

et un foncteur $G:{𝒞}_T\to 𝒞$ par :

$GY=TY$

$G(f:X\to TY)={\mu }_Y\circ Tf$

Ce sont bien des foncteurs, et on a l'adjonction $F⊣G$, la counité de l'adjonction étant ${\epsilon }_Y=1_{TY}$.

Enfin, $T=GF$ et $\mu =G\epsilon F$ : on a donné une décomposition de la monade en termes de l'adjonction $(F,G,\eta ,\epsilon )$.

T-algèbres

Avec les notations précédentes, une T-algèbre (ou T-module) est la donnée d'un objet x de $𝒞$ et d'un morphisme $h:Tx\to x$ tels que

$h\circ {\mu }_x=h\circ Th$

$h\circ {\eta }_x=1_x$

Un morphisme $(h,x)\to (h^{\prime },x^{\prime })$ de T-algèbres est une flèche $f:x\to x^{\prime }$ telle que

$h^{\prime }\circ Tf=f\circ h$.

Les T-algèbres et leurs morphismes forment la catégorie d'Eilenberg-Moore ${𝒞}^T$.

Le foncteur d'oubli ${𝒞}^T\to 𝒞$ possède un adjoint à gauche $𝒞\to {𝒞}^T$ qui envoie tout objet y de $𝒞$ sur la T-algèbre libre $(Ty,{\mu }_Y)$. Ces deux foncteurs forment également une décomposition de la monade initiale. Les T-algèbres libres forment une sous-catégorie pleine de ${𝒞}^T$ qui est équivalente à la catégorie de Kleisli.

Monades et informatique théorique

On peut réinterpréter la catégorie de Kleisli d'un point de vue informatique  :

• Le foncteur T envoie tout type X sur un nouveau type $T(X)$ ;
• On dispose d'une règle pour composer deux fonctions $f:X\to T(Y)$ et $g:Y\to T(Z)$, donnée par la composition dans la catégorie de Kleisli, qui est associative et unitale. On obtient une fonction $g\circ f:X\to T(Z)$ ;
• Le rôle de l'unité est joué par l'application pure $X\to T(X)$.