Catégorie de Kleisli

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

Une catégorie de Kleisli est une catégorie associée à une monade. Elle tient son nom du mathématicien suisse Heinrich Kleisli (en) qui l'a introduite à l'origine pour montrer que toute monade est issue d'une adjonction.

Définition[modifier | modifier le code]

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

\operatorname{Hom}_{C_T}(X, Y) = \operatorname{Hom}_{C}(X, TY)

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

g \circ f = \mu_Z \circ Tg \circ f

qui correspond au diagramme :

X \overset{f}{\longrightarrow} TY \overset{Tg}{\longrightarrow} TTZ \overset{\mu_Z}{\longrightarrow} TZ

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

T-algèbres[modifier | modifier le code]

Avec les notations précédentes, une T-algèbre (ou T-module) est la donnée d'un objet x de C 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', x') de T-algèbres est une flèche f : x \to x' telle que

h' \circ Tf = f \circ h.

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

Le foncteur d'oubli C^T \to C possède un adjoint à gauche C \to C^T qui envoie tout objet y de C sur la T-algèbre libre (Ty, \mu_Y). Les T-algèbres libres forment une sous-catégorie pleine de C^T qui est équivalente à la catégorie de Kleisli.

Monades et adjonctions[modifier | modifier le code]

On définit le foncteur F : C\to C_T par :

FX = X
F(f : X \to Y) = \eta_Y \circ f

et un foncteur G : C_T \to C par :

GY = TY
G(f : X \to TY) = \mu_Y \circ Tf

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

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

Monades et informatique théorique[modifier | modifier le code]

Article détaillé : Monade (informatique).

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).

Référence[modifier | modifier le code]

(en) Saunders Mac Lane, Categories for the Working Mathematician [détail de l’édition]