Catégories comme fonctions

Question

Je travaille sur un livre sur la théorie des catégories pour les programmeurs .

Ici, dans le livre, je trouve la relation "<=" comme exemple de catégorie: elle respecte la relation d'identité ( a <= a) et elle est composable ( a <= b, b <= c -> a <= c).

Ce qui n'est pas clair pour moi, c'est l'analogie entre les morphismes et les fonctions, comme mentionné dans le livre à la page 3: une fonction ne peut pas implémenter la catégorie d'ordre, car elle ne peut renvoyer aucune valeur <= d'une donnée, donc ... qu'est-ce que c'est la relation entre morphismes et fonctions? Il semble que les morphismes soient des connexions entre les types, tandis que les définitions de fonctions sont des connexions entre des valeurs, donc cette dernière me semble être une implémentation spéciale de la première.

Ce serait en contraste avec tous les exemples de fonctions d'identité que j'ai vus là-bas, cependant, car une fonction d'identité mapperait un type avec le même type, pas une valeur avec la même valeur, donc, par exemple, f x = x + 1serait un correct " flèche "de et vers le même type, ce qui n'est évidemment pas vrai.

D'un autre côté, cependant, je vois de telles représentations de catégorie:

Ici A est un type ou est un objet?

Answer 1

Je ne comprends pas tout à fait de quoi vous êtes confus, et en particulier je ne comprends pas tout à fait ce que vous entendez par "une fonction ne peut pas implémenter la catégorie d'ordre", donc je vais juste dire certaines choses que j'espère pertinentes.

1. Les morphismes ne commencent pas par avoir une interprétation particulière en termes de fonctions. Les axiomes de la catégorie nue vous donnent juste un tas d'objets, de flèches et d'axiomes pour savoir comment les flèches doivent se composer, et ces axiomes sont satisfaits par tout ordre partiel $\le$, et c'est tout. Au début, je pense que la manière la moins déroutante de penser les catégories de cette manière "nue" est de les considérer comme des graphes dirigés équipés d'une opération de composition sur les arêtes.

2. D'autre part, chaque catégorie $C$a une intégration Yoneda $C \to [C^{op}, \text{Set}]$, ce qui nous donne une interprétation distinguée des morphismes $f : x \to y$ comme fonctions $f : \text{Hom}(a, x) \to \text{Hom}(a, y)$sur des points généralisés , où un point généralisé de$x$ est n'importe quel morphisme $a \to x$quoi que ce soit. Cela nous permet d'interpréter les morphismes$x \le y$dans un ordre partiel en tant que fonctions (nécessairement uniques) des downsets $\{ a : a \le x \}$ aux downsets $\{ a : a \le y \}$, à savoir la fonction unique d'envoi $a$ à $a$.

3. Les objets ne commencent pas non plus comme ayant une interprétation particulière en termes de types. La théorie des types est une manière particulière de regarder les catégories, ou une manière particulière de les générer, et ce n'est pas la seule. Dans la sémantique catégorielle standard des théories de type, les objets sont (interprétés comme) des types$A$ et morphismes $f : A \to B$ sont (interprétées comme) des fonctions avec un type d'entrée $A$ et type de sortie $B$. Si une catégorie a un objet terminal $1$ (qui peut être interprété comme un type d'unité) puis morphismes $1 \to A$ peut être interprété comme des termes de type $A$, et un morphisme $f : A \to B$ induit alors une véritable fonction $\text{Hom}(1, A) \to \text{Hom}(1, B)$ envoi de conditions de type $A$ aux termes de type $B$. Il n'y a souvent pas assez de "points" (fonctions$1 \to A$) pour en faire une opération intéressante dans de nombreuses catégories, cependant; par exemple, en posets$1$, s'il existe, est un élément maximal , donc$\text{Hom}(1, A)$ est vide sauf si $A$ est également maximale.