Définition d'une catégorie et catégories de Kleisli

L'auteur de ce sujet a trouvé une solution à son problème.
Auteur du sujet

Bonjour tout le monde,

Je suis en train de suivre cette série d'articles sur la théorie des catégories appliquée à Haskell et C++. Je n'ai jamais fait ça en cours (normal, je sors tout juste de prépa …) et c'est clairement vulgarisé, donc je n'ai pas le bagage formel qu'il faut. Voici l'article qui me pose problème. J'ai bien compris le principe de la catégorie de Kleisli associée à la monade Writer. Pour reprendre l'explication de l'article:

For our limited purposes, a Kleisli category has, as objects, the types of the underlying programming language. Morphisms from type A to type B are functions that go from A to a type derived from B using the particular embellishment.

Ça, j'ai bien compris. Par contre, ce qui me perturbe, c'est que le morphisme de A vers B aille vers autre chose que B. En effet, selon Wikipédia:

There are many equivalent definitions of a category.[2] One commonly used definition is as follows. A category C consists of

  • a class ob(C) of objects
  • a class hom(C) of morphisms, or arrows, or maps, between the objects. Each morphism f has a source object a and a target object b where a and b are in ob(C). We write f: a → b, and we say "f is a morphism from a to b". We write hom(a, b) (or homC(a, b) when there may be confusion about to which category hom(a, b) refers) to denote the hom-class of all morphisms from a to b. (Some authors write Mor(a, b) or simply C(a, b) instead.)

Si je m'appuie sur la définition d'une catégorie de Kleisli donnée par nLab:

The Kleisli category $C_T$ has as objects the objects of $C$, and as morphisms $M \to N$ the elements of the hom-set $C(M,T(N))$, in other words morphisms of the form $M \to T(N)$ in $C$, called Kleisli morphisms.

Je ne comprends pas pourquoi c'est permis que les morphismes soient de la forme $M \to T(N)$ au lieu de $M \to N$.

Pourriez-vous m'éclairer ? (Attention hein, je ne connais que ce que j'ai vu dans les articles de la série avant celui que j'ai posté, je n'ai aucune base formelle sur ce bazar).

+2 -0
Auteur du sujet

Cette réponse a aidé l'auteur du sujet

La monade $T$ engendre une catégorie $\mathcal{C}_T$ dont

  • les points sont ceux de $\mathcal{C}$
  • les flèches $f_{\mathcal{C}_T} : A → B$ sont les $f_{\mathcal{C}} : A → TB$. La flèche va bien de $A$ vers $B$ dans $\mathcal{C}_T$, simplement c'est « la même flèche » que celle qui va de $A$ vers $TB$ dans la catégorie de départ.
  • la loi de composition de $g : A → B$ et $f : B → C$ est donnée par $f \circ_{\mathcal{C}_{T}} g = µ_C \circ_{\mathcal{C}} T f \circ_{\mathcal{C}} g$. Note comme $g$ se compose avec $T f$ dans $\mathcal{C}$ !

C'est une définition : à partir d'une catégorie et d'une monade, on pose une nouvelle catégorie. Pour ça on doit fournir plusieurs choses : des objets, des morphismes entre les paires d'objets, une loi de composition, et une preuve que cette loi de composition se comporte bien. Pour définir tout ça (en particulier l'ensemble $Hom_{\mathcal{C}_T}(A, B)$), on donne ce qu'on veut, tant que les objets sont cohérents entre eux.

Edit : à ce stade il serait bon de prendre un exemple (tout bête, avec par exemple la catégorie des ensembles et la monade des exceptions), de prendre deux objets et de donner un exemple ou deux de morphismes. Moi j'en ai marre de taper \mathcal, donc à toi de faire.

Ça serait peut-être plus clair de distinguer dans un premier temps les objets de $\mathcal{C}$ et ceux de $\mathcal{C}_T$, comme je le fais ici pour les morphismes. Mais en fait il y a égalité, ce sont vraiment les mêmes objets et ensembles de flèches (ils ne sont pas seulement « isomorphes » comme souvent en théorie des catégories).

(PS : merci de poster dans « Sciences » la prochaine fois.)

Édité par anonyme

+1 -0
Auteur du sujet

C'est une définition : à partir d'une catégorie et d'une monade, on pose une nouvelle catégorie. Pour ça on doit fournir plusieurs choses : des objets, des morphismes entre les paires d'objets, une loi de composition, et une preuve que cette loi de composition se comporte bien. Pour définir tout ça (en particulier l'ensemble $Hom_{\mathcal{C}_T}(A, B)$), on donne ce qu'on veut, tant que les objets sont cohérents entre eux.

Lz36GQfANCkOchnWu2yv

Merci beaucoup pour ta réponse. Si je comprends bien, un morphisme ça peut être n'importe quoi tant que «ça compose» en respectant les règles, j'ai bon ? J'ai récupéré Category Theory for Computer Scientists, et la définition qu'ils utilisent semble effectivement indiquer que peu importe le «type» des morphismes tant que les règles sont respectées.

(Merci beaucoup Aabu).

+0 -0
Auteur du sujet

Déjà oui, c'est « à peu près n'importe quoi » tant que le $Hom$-set est un ensemble (et pas, par exemple, une collection plus large) et que la composition est bien définie et respecte l'associativité et la « neutralité » des identités à gauche et à droite — d'ailleurs dans mon message précédent j'ai oublié de parler de l'identité. Le livre CTfCS de Barr & Wells prend d'ailleurs le parti de présenter les catégories à partir de graphes, ce qui me semble plus clair (un bon exercice quand on débute est de dessiner un petit graphe, et de se poser la question « qu'est-ce qui manque pour que ça devienne une catégorie ? »). C'est pour ça que je parle volontiers de « points » pour désigner les « objets », et de « flèche » pour désigner les « morphismes » — ce sont des termes utilisés en pratique, simplement moins fréquemment.

Dans la catégorie de Kleisli associée à une monade $T$ sur $\mathcal{C}$, les morphismes entre $A$ et $B$ sont en plus vraiment définis à partir de ceux $\mathcal{C}$, tu as beaucoup d'informations sur eux. Si tu prends la monade $— + 1$, les morphismes dans $\mathcal{C}_T$ sont en gros tous les calculs qui ont le droit de « planter », même s'ils ne le font pas forcément. $\mathcal{C}_T$ permet simplement de parler de ces morphismes en disant qu'on ne regarde plus les autres (les $f_\mathcal{C} : A → B$). Bien sûr c'est juste pour l'intuition que je dis ça, construire une vraie catégorie $\mathcal{C}$ dont les morphismes correspondraient à des « calculs » informatiques est non-trivial.

Aabu> Merci !

+1 -0
Auteur du sujet

Je crois que j'ai compris. Il me reste un point que je comprends pas bien:

Déjà oui, c'est « à peu près n'importe quoi » tant que le $Hom$-set est un ensemble (et pas, par exemple, une collection plus large)

Lz36GQfANCkOchnWu2yv

Je comprends pas, je pensais qu'un $Hom$-set pouvait très bien être aussi une classe (et pas un ensemble).

Édité par anonyme

+0 -0
Staff

Cette réponse a aidé l'auteur du sujet

Je crois que j'ai compris. Il me reste un point que je comprends pas bien:

Déjà oui, c'est « à peu près n'importe quoi » tant que le $Hom$-set est un ensemble (et pas, par exemple, une collection plus large)

Lz36GQfANCkOchnWu2yv

Je comprends pas, je pensais qu'un $Hom$-set pouvait très bien être aussi une classe (et pas un ensemble).

Grimur

Ca dépend du cadre dans lequel tu te places. Souvent, on se place dans le cadre où les catégories sont petites et donc $Hom$-set est un ensemble. Mais ce n'est pas toujours le cas. Dans ce cas, on parle de classe, mais cela se réfère à une autre théorie. En particulier, on peut parler de la classe qui contient tous les ensembles. En ce sens là, une classe c'est moralement plus gros qu'un ensemble.

+0 -0

Souvent, on se place dans le cadre où les catégories sont petites et donc $Hom$-set est un ensemble.

Un détail, c'est les catégories localement petites qui ont des Hom-set. Les petites, c'est les localement petites dont les objets aussi forment un ensemble. Ou alors tu parlais de tous les morphismes qui doivent former un ensemble ?

@Grimur, regardes du côté des catégories enrichies.

Édité par blo yhg

+0 -0
Staff

Souvent, on se place dans le cadre où les catégories sont petites et donc $Hom$-set est un ensemble.

Un détail, c'est les catégories localement petites qui ont des Hom-set. Les petites, c'est les localement petites dont les objets aussi forment un ensemble. Ou alors tu parlais de tous les morphismes qui doivent former un ensemble ?

@Grimur, regardes du côté des catégories enrichies.

blo yhg

En effet, je ne souhaitais pas rentrer dans ces détails.

+0 -0
Vous devez être connecté pour pouvoir poster un message.
Connexion

Pas encore inscrit ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte