Monade (théorie des catégories)

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Page d'aide sur l'homonymie Pour les articles homonymes, voir Monade.

Une monade est une construction catégorique qui mime formellement le comportement que les monoïdes ont en algèbre. La notion a été introduite par Roger Godement sous le nom de « construction standard », et c'est Saunders Mac Lane qui les a appelé monades, en référence au terme philosophique. Elles sont parfois appelées triples bien que ce terme tende à disparaître.

Elles permettent notamment de formuler des adjonctions et ont (au travers des comonades) un rôle important en géométrie algébrique, notamment en théorie des topos. Elles constituent également la théorie sous-jacente à la construction du même nom en programmation fonctionnelle.

Les monades permettent de définir les F-algèbres (en), dont les algèbres initiales (en).

Histoire[modifier | modifier le code]

La notion apparaît pour la première fois, sous le nom de « construction standard », dans un article de Roger Godement publié en 1958[1]. Il s'agissait en fait d'une comonade, qui permettait de résoudre un problème de cohomologie des faisceaux. La notion est reprise pour l'étude de l'homotopie des catégories par Peter Huber[2], qui donne notamment la preuve que toute paire d'adjoint donne lieu à une monade. En 1965, Heinrich Kleisli (en)[3] et indépendamment, Samuel Eilenberg et John Coleman Moore[4] démontrent la réciproque. Ce sont ces derniers qui donnent le nom de « triples » à la construction.

En 1963, William Lawvere propose une théorie catégorique de l'algèbre universelle. Fred Linton montre en 1966 que cette théorie peut s'exprimer en termes de monades[5]. Les monades, issues de considérations plutôt topologiques, et a priori plus difficiles à manier que les théories de Lawvere, sont devenues la formulation la plus courante de l'algèbre universelle en termes de catégories : en 1971, Saunders Mac Lane leur donne le nom de « monades », par analogie avec le concept philosophique d'une entité capable de générer toutes les autres, dans son livre Categories for the Working Mathematician.

Dans les années 1980, Eugenio Moggi (en) utilise les monades en informatique théorique pour modéliser certains aspects des programmes informatiques, tels que la gestion d'exceptions ou les effets de bord[6]. Cette idée sera prise au sérieux dans l'implémentation de plusieurs langages de programmation fonctionnelle sous la forme de primitives appelées également « monades ».

En 2001, plusieurs mathématiciens réalisent le lien entre cette utilisation des monades, pour étudier la sémantique dénotationelle d'un programme, et les théories de Lawvere[7], un lien entre algèbre et sémantique qui constitue aujourd'hui un domaine de recherche actif.

Définition[modifier | modifier le code]

Une monade est la donnée d'un triplet (T, \eta, \mu) avec :

et telle que les diagrammes suivants commutent :

Monad multiplication explicit.svg
Monad unit explicit.svg

C'est-à-dire \mu \circ T\mu = \mu \circ \mu T (qui mime l'associativité d'un monoïde) et \mu \circ T \eta = \mu \circ \eta T = 1_{T} (existence d'un élément neutre).

Monades et adjonctions[modifier | modifier le code]

Soit une paire d'adjoints F \dashv G, ayant pour unité

\eta : \mathsf{id} \mapsto G \circ F

et co-unité

\varepsilon : F \circ G \mapsto \mathsf{id}

Alors le foncteur T = G \circ F, muni des transformations

\eta : \mathsf{id} \mapsto T
\mu = G(\varepsilon F) : T \circ T \mapsto T

forme une monade.

Réciproquement, pour toute monade (T, \eta, \mu), il existe une paire d'adjoints F \dashv G telle que T = G \circ F. Il existe potentiellement de nombreuses décompositions, la plus petite formant la catégorie de Kleisli, la plus large la catégorie d'Eilenberg-Moore.

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

  1. Roger Godement, Topologie algébrique et théorie des faisceaux, Hermann (1958)
  2. Peter J. Huber, Homotopy theory in general categories. Mathematische Annalen 144.5 (1961): 361-385.
  3. Heinrich Kleisli (en), Every standard construction is induced by a pair of adjoint functors, Proceedings of the American Mathematical Society 16.3 (1965): 544-546.
  4. Samuel Eilenberg, John Coleman Moore, Adjoint functors and triples, Am. J. Math. 9 (1965), 301-398
  5. Fred E. J. Linton, Some aspects of equational theories, Proc. Conf. on Categorical Algebra at La Jolla (1966), 84–95
  6. Eugenio Moggi (en), Notions on computation on monads
  7. Gordon D. Plotkin (en), A. J. Power, Adequacy for Algebraic Effects, Proc. FOSSACS 2001, Lecture Notes in Computer Science 2030 (2001), 1–24.