Catégorie de Kleisli

En théorie des Catégories (mathématiques), Catégorie associée à une monade

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

On considère une monade   sur une catégorie  . La catégorie de Kleisli   possède les mêmes objets que   mais les morphismes sont donnés par

 

L'identité est donnée par  , et la composition fonctionne ainsi : si   et  , on a

 

qui correspond au diagramme :

 

Les morphismes de   de la forme   sont parfois appelés morphismes de Kleisli.

Monades et adjonctions modifier

On définit le foncteur   par :

 
 

et un foncteur   par :

 
 

Ce sont bien des foncteurs, et on a l'adjonction  , la counité de l'adjonction étant  .

Enfin,   et   : on a donné une décomposition de la monade en termes de l'adjonction  .

T-algèbres modifier

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   tels que

 
 

Un morphisme   de T-algèbres est une flèche   telle que

 .

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

Le foncteur d'oubli   possède un adjoint à gauche   qui envoie tout objet y de   sur la T-algèbre libre  . Ces deux foncteurs forment également une décomposition de la monade initiale. Les T-algèbres libres forment une sous-catégorie pleine de   qui est équivalente à la catégorie de Kleisli.

Monades et informatique théorique modifier

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   ;
  • On dispose d'une règle pour composer deux fonctions   et  , donnée par la composition dans la catégorie de Kleisli, qui est associative et unitale. On obtient une fonction   ;
  • Le rôle de l'unité est joué par l'application pure  .

Référence modifier

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