CATÉGORIES ET POINTS FIXES

CATÉGORIES ET POINTS FIXES

Ce chapitre est une introduction aux notions de théorie des catégories qui seront utiles dans les autres chapitres de cette thèse. La section 2.1 établit simplement les notations, relatives aux catégories, qui seront utilisées par la suite et fait le point sur les connaissances qui sont attendues de la part du lecteur. Quant aux sections 2.2 à 2.4, elles établissent la version catégorique de la théorie des points fixes, qui modélise notamment l’induction et la coinduction en programmation fonctionnelle. Un bon tutoriel des notions d’induction et de coinduction traitées dans ces sections est (Jacobs et Rutten, 1997), toutefois complété ici pour cadrer avec les systèmes dirigés d’équations, introduits dans (Santocanale, 2001) et revus (avec une nouvelle présentation) dans (Fortier et Santocanale, 2013). Ensuite, à la section 2.5, on décrit une solution canonique aux systèmes dirigés d’équations dans la catégorie des ensembles, telle que démontrée dans (Santocanale, 2002b). Enfin, la section 2.6 décrit le cadre général dans lequel on peut interpréter les systèmes dirigés d’équations, soit celui des catégories -bicomplètes.

Ce qu’il faut savoir sur les catégories

Notons que, pour des raisons visuelles et contrairement à ce qui est souvent pré- senté, on prendra l’habitude de composer les fonctions (et les flèches en général) dans la direction vers laquelle elles pointent et en utilisant l’opérateur 00. L’usageest plutôt (à cause de l’importance de la catégorie Ens ) de dénoter la composition par 00 et de composer à rebours. On suivra toutefois cette dernière convention pour la composition de foncteurs ou pour le passage d’un argument (qui se fera à droite). En résumé :Du reste, puisque cette thèse n’est pas un ouvrage d’introduction aux catégories, on prendra pour acquis que le lecteur soucieux d’en comprendre les détails possède au moins une connaissance de base en théorie des catégories. Une telle connais- sance peut être acquise dans l’excellent livre de Awodey (2006) ou encore dans les premiers chapitres de (Mac Lane, 1998).opposée (qu’on dénotera C plutôt que C op). Le lecteur est, d’ailleurs, présumé à l’aise avec le principe de dualité.

Algèbres initiales et induction

Exemple 1. La plupart des structures algébriques définies couramment en mathé- matiques sont des algèbres dans le sens présent. Par exemple, un groupe est un ensemble A (le support) muni d’un élément choisi (l’élément neutre), c’est-à-direune flèche e : 1 ! A dans Ens , d’une opération d’inversion ()1 : A ! A puis d’une opération binaire : A A ! A satisfaisant certains axiomes. La structure algébrique naît donc de ces trois fonctions, e, ()1 et , ou de façon équivalente, de la fonction suivante.Exemple 2. Considérons par exemple (toujours dans Ens ), l’algèbre des nombres naturels, donnée par le choix d’un élément 0 : 1 ! N et d’une opération suc- cesseur, Suc : N ! N. Il s’agit donc d’une algèbre du foncteur F (X) = 1 + X. Il s’agit en fait de la F -algèbre initiale, puisqu’étant donné une autre F -algèbreExemple 3. Toujours dans la catégorie des ensembles, soit F (X) = 1 + (A X), où A est un ensemble fixé. La F -algèbre initiale est le monoïde libre A (vu à la Section 1.1) dont la structure est donnée par une fonction Nil : 1 ! A dont l’image est le mot vide  » et la fonction Cons : A A ! A (appelée constructeur ) définie par Cons(a; u) = a:u. La propriété universelle de cette algèbre initialeExemple 4. Changeons un peu de catégorie. Rappelons qu’un treillis complet est un ensemble partiellement ordonné (T; ) tel que chaque sous-ensemble E T admet un infimum et un supremum. Or, les ensembles partiellement ordonnés2006, §1.4). Un endofoncteur F : T ! T est alors, tout simplement, une fonction croissante de T vers T .

Étant donné un tel foncteur, en déroulant la définition d’une F -algèbre, on constate qu’il s’agit simplement un élément x 2 T tel que F (x) x, c’est-à-dire s’il s’agit d’un point préfixe. Le point x est la F -algèbre initiale si, pour tout autre point préfixe y, on a x y. En d’autres mots, l’algèbre initiale est le pointLe carré gauche du diagramme commute par construction et le carré droit com- mute trivialement. Donc le rectangle extérieur commute. Par unicité, on trouve donc f a = idA. Ensuite, puisque le carré gauche est commutatif, on trouveEn d’autres mots, le lemme de Lambek affirme que les F -algèbres initiales sont des points fixes de F (à isomorphisme près). Ainsi, on écrira « A = F (A) » y pour indiquer que A est le support de l’algèbre initiale du foncteur F .