Archives quotidiennes :

Lemme de Yoneda: Le exemple

Introduction à la théorie des Catégories

Pour reprendre sur la seconde remarque de mon commentaire sur le lemme de Yoneda, l’exemple qui m’a fait comprendre Yoneda (disons, atteindre la compréhension niveau 1 de Yoneda, parce que ce truc est diantrement profond), c’est la catégorie des contextes du lambda-calcul simplement typé. C’est la catégorie dont je parle au début de ce message.
Pour résumer, ses objets sont les contextes de typage genre $latex Gamma = (x_1: tau_1 ldots x_n: tau_n)$ et ses morphismes de $latex Gamma$ vers $latex Delta = (y_1: tau’_1 ldots y_m: tau’_m)$ sont les séquences $latex f = (e_1 ldots e_m)$, avec $latex Gamma vdash e_i : tau’_i$. On peut voir un tel morphisme comme une substitution $latex text{[} y_1 mapsto e_1 ldots y_m mapsto e_m text{]}$ et c’est comme ça qu’on définit la composition: cette substitution envoie n’importe quel terme typé dans $latex Delta$ vers un terme du même type dans $latex…

View original post 225 mots de plus

Publicités

Lemme de Yoneda

Introduction à la théorie des Catégories

Aujourd’hui, je vais tenter d’expliquer le plus clairement possible (c’est pas une mince affaire) le lemme de Yoneda. Cela nous permettra de parler bientôt des propriétés universelles, pour pouvoir enfin utiliser les catégories en informatique.

Rentrons maintenant dans le vif du sujet : soit $latex mathcal{C}$ une catégorie localement petite (i.e. une catégorie telle que pour tout couple d’objets A,B, Hom(A,B) est un ensemble), A un objet de $latex mathcal{C}$, alors on peut définir le foncteur covariant de $latex mathcal{C}$ dans $latex mathcal{S}et$ : $latex Hom(A,_) : X rightarrow Hom(A,X)$, et qui au morphisme $latex f : X rightarrow Y$ associe le morphisme $latex phi_f : u rightarrow f circ u$.

C’est maintenant que le lemme de Yoneda rentre en jeu : considérons un foncteur covariant $latex F: mathcal{C} rightarrow mathcal{S}et$, alors on peut établir une bijection entre les transformations naturelles de $latex Hom(A,_)$ dans $latex F$ avec les éléments…

View original post 538 mots de plus

Transformation naturelle et catégorie des foncteurs

Introduction à la théorie des Catégories

Je vais essayer de présenter dans ce premier post ce que j’ai compris des catégories de foncteurs.
Par foncteur j’entends ici foncteur covariant, mais on peut adapter sans trop de problème tout ce que je dis aux foncteurs contravariant.

Avant de présenter les catégories de foncteurs, je dois déjà présenter la notion de transformation naturelle :
Soit C et D deux catégories, F et G deux foncteurs de C dans D. On aimerait bien pouvoir transformer C en D de manière à conserver les propriétés essentielles des foncteurs (grosso modo la composition des morphismes). En fait, on cherche juste à définir un morphisme entre foncteur, mais pour éviter toute ambiguïté avec l’ensemble des morphismes d’une catégorie, on appelle plutôt ça une transformation naturelle.
Pour donner une définition précise, on appelle une transformation naturelle $latex eta$ de F dans G l’application qui à chaque objet X de C associe un morphisme…

View original post 487 mots de plus