D IAGRAMMES C. O RIAT Étude des spécifications modulaires : constructions de colimites finies, diagrammes, isomorphismes Diagrammes, tome 39 (1998), p. 3-120 © Université Paris 7, UER math., 1998, tous droits réservés. L’accès aux archives de la revue « Diagrammes » implique l’accord avec les conditions générales d’utilisation (http://www.numdam.org/legal.php). Toute utilisation commerciale ou impression systématique est constitutive d’une infraction pénale. Toute copie ou impression de ce fichier doit contenir la présente mention de copyright. Article numérisé dans le cadre du programme Numérisation de documents anciens mathématiques http://www.numdam.org/ DIAGRAMMES VOLUME 39,1998 ETUDE DES SPECIFICATIONS MODULAIRES CONSTRUCTIONS DE COLIMITES FINIES, DIAGRAMMES, ISOMORPHISMES (*> PARTIE I (**) C. Oriat RESUME. La composition de spécifications modulaires peut être modélisée, dans le formalisme des catégories, par des colimites de diagrammes. La somme amalgamée permet en particulier d'assembler deux spécifications en précisant les parties communes. Notre travail poursuit cette idée classique selon trois axes. D'un point de vue syntaxique, nous définissons un langage pour représenter les spécifications modulaires construites à partir d'une catégorie de spécifications et de morphismes de spécifications de base. Ce langage est caractérisé formellement par une catégorie de termes finiment cocomplète. D'un point de vue sémantique, nous proposons d'associer à tout terme un diagramme. Cette interprétation permet de faire abstraction de certains choix effectués lors de la construction de la spécification modulaire. Pour cela, nous définissons une catégorie de diagrammes "concrète", c'est-à-dire dont les flèches peuvent être manipulées effectivement. En considérant le quotient par une certaine congruence, nous obtenons une complétion de la catégorie de base par colimites finies. Nous montrons que le calcul du diagramme associé à un terme définit une équivalence entre la catégorie des termes et la catégorie des diagrammes, ce qui prouve la correction de cette interprétation. Enfin, nous proposons un algorithme pour décider si deux diagrammes sont isomorphes, dans le cas particulier où la catégorie de base est finie et sans cycle. Cela permet de détecter des isomorphismes "de construction" entre spécifications modulaires, c'est-à-dire des isomorphismes qui ne dépendent pas des spécifications de base, mais seulement de la manière dont celles-ci sont assemblées. ABSTRACT. The composition of modular spécifications can be modeled, in a categoy theoretic framework, by means of colimits of diagrams. Pushouts in particular allow us to n Thèse d'Informatique, préparée et soutenue à l'Institut National Polytechnique de Grenoble (Laboratoire LSR-IMAG). ( **} La Partie II de ce travail sera publiée dans Diagrammes 40 et la Partie III dans Diagrammes 41. gather two spécifications sharing a common part. Our work extends this classic idea along three lines. From a syntactic point of view, we define a language to represent modular spécifications built from a category of base spécifications and base spécification morphisms. This language is formally characterized by afinitelycocomplete category of terms. From a semantic point of view, we propose to associate with each term a diagram. This interprétation allows us to abstract some choices made while constructing a modular spécification. We thus define a "concrète" category of diagrams, in which arrows can actually be handled. Considering the quotient by a certain congruence relation, we get a completion of the base category with finite colimits. We prove that this calculus defines an équivalence between the category of terms and the category of diagrams, which shows the soundness of this interprétation. At last, we propose an algorithm to décide whether two diagrams are isomorphic, when the base category is finite and cycle free. This allows us to detect "construction isomorphisms" between modular spécifications, i.e. isomorphisms which do not dépend on the base spécifications, but only on their combination. Remerciements Je remercie tout d'abord mon directeur de thèse, M. Didier Bert, pour son soutien et pour la confiance qu'il m'a accordée dans la préparation de cette thèse. Je remercie M. Jean-Pierre Verjus qui a accepté de présider ce jury. Je remercie M. Michel Bidoit pour l'intérêt qu'il a porté à mon travail et pour avoir accepté d'être rapporteur de ma thèse. Je remercie M. Christian Lair pour les améliorations qu'il m'a suggérées et pour les erreurs qu'il m'a signalées avec beaucoup d'indulgence et de gentillesse. Je suis particulièrement honorée qu'un catégoricien de sa compétence ait accepté de faire partie de mon jury en qualité de rapporteur. Je remercie M. Michel Sintzoff pour m'avoir fait l'honneur de participer à ce jury. Ce travail doit beaucoup à M. Jean-Claude Reynaud. Je le remercie d'une part pour le temps qu'il a consacré à suivre mon travail, et d'autre part pour toutes les suggestions qu'il m'a faites. Si, par hasard, ce travail contient quelques idées intéressantes, c'est probablement lui qui me les a soufflées (mais, en paraphrasant Mac Lane, je suis évidemment responsable des erreurs qui pourraient rester). Je remercie enfin les membres de l'équipe SCOP, auxquels j'associe les occupants présents ou passés du bâtiment D, pour leur accueil et leur soutien tout au long de ce travail. "Le département [.. J épousait l'opinion traditionnelle qui voulait que la recherche fût une occupation solitaire et érémitique, une mise à l'épreuve du caractère plus que de l'érudition, qu'un abus de contact humain pouvait vicier." — David Lodge, La chute du British Muséum Introduction Spécifier un problème consiste à le décrire sans décider prématurément de la façon dont il sera résolu. En informatique, une spécification de programme est une description des fonctionnalités attendues du programme indépendante des choix de mise en œuvre. Il existe plusieurs manières de spécifier un programme. On peut utiliser une langue naturelle, par exemple en écrivant un cahier des charges. Certaines activités, comme la validation de programme, la construction automatique d'un prototype, ou la production systématique de jeux de tests, nécessitent des spécifications formelles, qui possèdent une sémantique précise, en particulier non ambiguë. Nous nous intéressons ici aux spécifications algébriques, qui font partie des spécifications orientées propriétés1. Les spécifications orientées propriétés sont basées sur un système logique, qui définit l'ensemble des propriétés que doit satisfaire tout modèle de la spécification. 1 Spécifications algébriques Une spécification algébrique est composée d'une signature et d'un ensemble d'axiomes. La signature contient les symboles utilisés pour former des expressions, et les axiomes définissent certaines propriétés de ces expressions. La logique sousjacente décrit l'ensemble des théorèmes que l'on peut déduire des axiomes. De plus, la sémantique des spécifications algébriques associe à toute spécification une classe de modèles, c'est-à-dire une classe d'algèbres multi-sortes qui satisfont les axiomes. Historiquement, les spécifications algébriques sont issues de deux courants distincts : l'algèbre universelle en mathématiques [Coh65] et les types abstraits en génie logiciel. L'origine des types abstraits figure dans le concept de classe du langage de programmation Simula [DN66, BDMN73]. Un type abstrait, composé d'un ensemble de domaines de valeurs accompagné d'un ensemble d'opérations sur ces domaines de valeurs, permet de structurer les données. L'idée de base en spécification algébrique consiste à modéliser un type abstrait par une algèbre. Cette idée est motivée par l'analogie entre un type abstrait et une algèbre multi-sortes sur une signature. L'interprétation des sortes de la signature correspond en effet aux domaines de valeurs, et l'interprétation des opérateurs de la signature correspond aux opérations sur ces domaines de valeurs. Les premiers travaux sur les spécifications algébriques datent du milieu des années 1970, avec les travaux de B. Liskov et S. Zilles [LZ74], de J. Guttag [Gut75, 1. En anglais, property-oriented. 10 INTRODUCTION Gut77] et du groupe ADJ (composé de J. Goguen, J. Thatcher, E. Wagner et J. Wright) [GTWW75, GTWW77, GTW78]. Au départ, les spécifications algébriques étaient basées sur la logique équationnelle. Puis ont été introduites d'autres logiques, comme les clauses de Horn, la logique du premier ordre ou encore les spécifications avec contraintes [EM90]. D'autres extensions ont permis de prendre en compte la notion d'erreur [BBC86, BL93]. J. Goguen et R. Burstall ont proposé la théorie des institutions, qui offre un cadre général pour étudier les différents formalismes de spécification algébrique [GB84, GB90]. Il existe beaucoup de références sur les spécifications algébriques, parmi les bonnes synthèses, citons [EM85, MG85, Wir90]. Ces travaux ont donné naissance à de nombreux langages de spécification algébrique, comme Clear [BG77, BG80], ACT ONE et ACT TWO [EM85, EM90], ASL [SW83, Wir86], OBJ2 et OBJ3 [FGJM85, GKK+87], PLUSS [Gau84, Bid89], LPG [Ber83, BE86, B+90], GLIDER [Huf92]. On trouve un bon panorama des différents langages de spécification algébrique existants dans [Wir94]. 2 Théorie des catégories La théorie des catégories repose sur deux notions: Vobjet et la flèche, contrairement à la théorie des ensembles qui repose sur le seul concept d'ensemble. En théorie des ensembles, un ensemble est caractérisé de façon interne par ses éléments, alors qu'en théorie des catégories, un objet est caractérisé de façon externe par les relations entretenues par l'intermédiaire des flèches avec les autres objets. Pour cette raison, un grand nombre de concepts de théorie des catégories sont définis à un isomorphisme près. La théorie des catégories a été inventée au début des années 1940 par S. Mac Lane et S. Eilenberg. Bien que certains mathématiciens aient douté de l'intérêt des catégories, ce formalisme a joué un rôle unificateur en mathématiques, en particulier en algèbre et en topologie. Cette théorie définit les différents concepts de façon générale et abstraite, indépendamment de tout modèle. (C'est pour cette raison que ses détracteurs l'on surnommée unon-sens abstrait 2 ".) La théorie des catégories a commencé à intéresser les informaticiens au début des années 1970. Par exemple, la découverte de l'équivalence entre le À-calcul typé et les catégories cartésiennes fermées a permis de donner des solutions élégantes au problème des modèles du Àcalcul, lié à celui de la résolution des équations de domaines [SP77, Wan79, LS86]. Il existe de façon générale des liens très étroits entre la théorie des types et la théorie des catégories (cf. par exemple [See84, Poi92]). L'ouvrage de référence sur les catégories est le livre de S. Mac Lane [McL71], plutôt destiné aux mathématiciens. Pour les informaticiens, le livre de M. Barr et C. Wells [BW90] est plus accessible, car les différents concepts sont présentés de façon assez élémentaire et les exemples sont tirés de l'informatique. Il existe beaucoup d'autres ouvrages qui traitent des catégories, par exemple [MB70, AM75, Gol79, AL91]. Le formalisme des spécifications algébriques s'appuie largement sur la théorie 2. En anglais, abstract nonsense. INTRODUCTION U des catégories. Historiquement, le développement des spécifications algébriques (en particulier les travaux du groupe ADJ) a été influencé par les théories algébriques de Lawvere. Les théories algébriques de Lawvere permettent de modéliser les catégories d'algèbres en faisant abstraction de la syntaxe, c'est-à-dire indépendamment de la notion de signature [Law63, BW85, WBT85]. D'autre part, d'un point de vue pratique, on peut justifier l'utilisation des catégories par l'importance des morphismes de spécifications, qui jouent un rôle essentiel en spécification algébrique. Intuitivement, un morphisme de spécifications exprime une relation entre deux spécifications. Pour prendre un exemple mathématique, tout anneau peut être considéré comme un groupe, ce qui signifie qu'il existe un morphisme de spécifications entre la spécification des groupes et la spécification des anneaux. Il peut exister plusieurs morphismes de spécifications entre deux spécifications. Par exemple, on peut considérer tout anneau comme un monoïde de deux façons différentes, en considérant soit l'opérateur additif, soit l'opérateur multiplicatif de l'anneau comme l'opérateur du monoïde. Préciser quel opérateur de l'anneau sera l'opérateur du monoïde consiste exactement à définir un morphisme de spécifications entre la spécification des monoïdes et la spécification des anneaux. 3 Modularité Le développement de spécifications de grande taille nécessite un découpage des spécifications en plusieurs spécifications plus simples, appelées modules. Chaque module correspond à un problème plus simple à résoudre. Cette méthode, qui consiste à "diviser pour mieux régner" est classique en génie logiciel [LCW85]. De façon générale, la modularité permet d'une part le développement indépendant des différents modules, et d'autre part une meilleure compréhension de chaque module, ce qui facilite la maintenance. Cette vision de la modularité correspond à une approche descendante de résolution de problème, puisque l'accent est mis sur la décomposition du problème en plusieurs sous-problèmes plus simples. Dans notre travail, notre conception de la modularité est au contraire ascendante. Nous nous intéressons en effet à la composition des modules, c'est-à-dire à l'assemblage de modules élémentaires permettant de construire des modules plus complexes. Ces modules élémentaires sont regroupés dans une bibliothèque, la bibliothèque des modules de base. L'intérêt de la composition est de permettre la réutilisation des modules de base, préconisée en génie logiciel pour réduire les erreurs et les coûts de développement (cf. par exemple [Ber90]). Un aspect de la modularité est la possibilité de définir des spécifications génériques, c'est-à-dire paramétrées [SST92]. En effet, une spécification paramétrée peut être instanciée de différentes manières par d'autres spécifications, ce qui évite de réécrire une nouvelle spécification pour chaque variation d'un même problème. Le but est alors de définir des spécifications génériques suffisamment générales pour permettre de spécifier le maximum de problèmes par une simple instanciation [Mar95]. Le développement modulaire des spécifications est assisté dans les langages de spécification algébrique par des opérateurs de construction3 comme le renommage, 3. En anglais, spécification-building opérations. 12 INTRODUCTION Y enrichissement ou V abstraction [ST88, Wir90]. Ces primitives permettent de construire de nouvelles spécifications à partir de spécifications déjà définies. La composition de modules est un cas particulier d'opérateur de construction de spécifications, qui peut être modélisé par des colimites de diagrammes. Intuitivement, en théorie des catégories, un diagramme permet de décrire un assemblage de plusieurs objets en précisant des partages entre certains objets à l'aide de flèches. La colimite du diagramme permet de considérer le résultat de cette composition. Cette utilisation générale des colimites pour modéliser l'interconnexion de systèmes a été proposée par J. Goguen [Gog73, Gog92]. Un cas particulier de colimite est la somme amalgamée4, qui correspond à l'assemblage de deux objets B et C\ en spécifiant une partie commune entre ces deux objets par un objet partagé A et deux flèches / : A —> B et g : A —> C. En spécification algébrique, la somme amalgamée peut modéliser d'une part la composition de deux spécifications qui ont une partie commune, et d'autre part Y instanciation d'une spécification générique. 4 Notre travail Nous étudions la composition des spécifications algébriques modulaires. Nous supposons que nous disposons d'une bibliothèque de spécifications et de morphismes de spécifications de base, qui forment une catégorie de base, en général appelée Co dans ce mémoire. Les spécifications de base sont monolithiques, c'est-à-dire non décomposées. Notre travail repose sur une idée classique en spécification algébrique : la composition des spécifications peut être modélisée par des colimites de diagrammes finis. Nous proposons donc de considérer une spécification modulaire comme une spécification obtenue à partir de spécifications et morphismes de spécifications de base par une suite de constructions de colimites. Notre travail est indépendant de la logique sous-jacente du langage de spécification algébrique. Nous pouvons donc nous placer dans le cadre général des institutions. Nous devons uniquement supposer que la catégorie des spécifications est finiment cocomplète, c'est-à-dire que tout diagramme fini a une colimite. D'un point de vue syntaxique, c'est-à-dire en ce qui concerne le langage utilisé pour décrire ces constructions, nous ne considérons pas toutes les colimites finies, mais uniquement les sommes amalgamées. En effet, avec la spécification vide, objet initial de la catégorie des spécifications, les sommes amalgamées permettent de simuler la construction de toute colimite finie. Nous proposons la construction d'une catégorie de termes, appelée Terme(Co), pour représenter la composition de spécifications modulaires en utilisant les sommes amalgamées. En théorie des catégories, on travaille le plus souvent à un isomorphisme près. C'est une conséquence de la caractérisation externe des objets dans ce formalisme. Les colimites, par exemple, sont définies au départ à un isomorphisme près. La définition d'une syntaxe est au contraire un problème typiquement informatique, qui nécessite de faire des choix de représentation. C'est la raison pour laquelle nous devons utiliser des sommes amalgamées choisies au moment de la définition du langage 4. En anglais, pushout. Les catégoriciens utilisent également le terme de coproduit fibre. INTRODUCTION 13 d'expression pour les spécifications modulaires. Ces choix de sommes amalgamées correspondent à des choix de codage. Un terme correspond donc à une spécification modulaire construite par une succession de sommes amalgamées. Dans une seconde étape, nous proposons d'interpréter un terme par un diagramme dont la colimite est la spécification modulaire dénotées par ce terme. Nous considérons les diagrammes comme une sémantique pour les spécifications modulaires, par opposition aux termes qui constituent la syntaxe. L'interprétation des termes par des diagrammes nécessite de définir une catégorie de diagrammes puisqu'il faut non seulement associer à toute spécification modulaire un diagramme, mais aussi associer à tout morphisme de spécifications modulaires un morphisme de diagrammes. La définition d'un diagramme est relativement standard en théorie des catégories, bien qu'il existe quelques nuances. La définition de morphisme de diagrammes est moins connue, en particulier dans la littérature informatique où sont utilisées des définitions moins générales que celle dont nous nous servons ici. Nous présentons deux catégories de diagrammes, DIAGR(Co) et diagr(Co). Les objets de DIAGR(Co) sont des diagrammes, et les flèches de DIAGR(Co) des morphismes de diagrammes. La catégorie diagr(Co) est obtenue à partir de DIAGR(Co) par un quotient par une relation de congruence sur les flèches de DIAGR(Co). C'est la catégorie diagr(C0) qui possède les propriétés théoriques intéressantes. Il s'agit en effet d'une catégorie finiment cocomplète, c'est-à-dire que tout diagramme fini sur diagr(Co) a une colimite finie dans diagr(Co). D'autre part, diagr(C0) est une complétion par colimites finies de la catégorie C0- Sur le plan pratique, comme les flèches de diagr(Co) sont des classes d'équivalence de morphismes de diagrammes, on travaille en réalité avec des représentants, c'est-à-dire avec des flèches de DIAGR(Co). La catégorie DIAGR(Co) permet donc la manipulation effective des flèches de diagr(C 0 ). La représentation des termes par des diagrammes est définie par un foncteur V : Terme(Co) -¥ diagr(C0) entre les catégories Terme(Co) et diagr(Co). Nous montrons que ce foncteur définit une équivalence de catégories entre Terme(Co) et diagr(C 0 ), ce qui signifie que bien qu'elles ne soient pas isomorphes, ces catégories ont néanmoins essentiellement la même structure. Après avoir représenté les spécifications modulaires par des diagrammes, nous nous intéressons au problème de Y équivalence entre deux spécifications modulaires. Deux spécifications modulaires sont considérées comme équivalentes lorsque cellesci sont isomorphes en tant que colimites de diagramme. Détecter cet isomorphisme consiste en fait à détecter un isomorphisme entre deux diagrammes dans la catégorie diagr(Co). Nous appelons cet isomorphisme un isomorphisme de construction, parce qu'il ne dépend pas de la définition effective des spécifications de base, mais seulement de la manière dont celles-ci sont combinées pour construire les spécifications modulaires. Dans l'hypothèse où la catégorie C0 est finie et ne comporte pas de cycle, nous proposons un algorithme pour détecter si deux diagrammes sont isomorphes. Des résultats partiels concernant l'interprétation des termes par des diagrammes et la détection d'isomorphismes de construction ont été présentés dans [Ori94, Ori95]. 14 5 INTRODUCTION Comparaisons avec d'autres travaux Catégories de diagrammes La définition de diagramme est, à quelques nuances près, standard. Chez S. Mac Lane [McL71], un diagramme sur une catégorie C est un foncteur d'une catégorie J vers C. La définition de M. Barr et C. Wells [BW90], est moins générale, puisqu'un diagramme est un morphisme de graphes d'un graphe vers le graphe sous-jacent de C. Nous utilisons une définition ''intermédiaire" : pour nous, un diagramme est un foncteur d'une catégorie librement engendrée sur un graphe vers C. Partir d'un graphe nous permet de rester proche de l'informatique. Par contre, nous ne souhaitons pas nous restreindre à une petite catégorie C. La définition de morphisme de diagrammes est beaucoup moins standard. Par exemple dans Clear, un morphisme de diagrammes, appelé morphisme basé, correspond uniquement à une inclusion entre deux diagrammes. La définition proposée par A. Tarlecki, R. Burstall et J. Goguen dans [TBG91], bien que plus générale que celle utilisée dans la sémantique du langage Clear, n'est pas encore suffisamment générale pour notre travail. En effet, cette définition ne permet pas de représenter tout morphisme de spécifications modulaires par un morphisme de diagrammes. La définition de morphisme de diagrammes que nous utilisons n'est pas nouvelle en théorie des catégories. Une version duale de la catégorie diagr(Co) est par exemple utilisée par M. Barr et C. Wells dans [BW94]. Néanmoins, la reformulation de la définition de catégorie de diagrammes que nous proposons dans le chapitre 2 présente un intérêt en informatique, d'une part parce que la catégorie DIAGR(Co) permet de manipuler effectivement les morphismes de diagrammes, et d'autre part parce que les catégories DIAGR(Co) et diagr(Co) sont peu connues dans cette discipline. Calculs de colimites R. Burstall et D. Rydeheard proposent des algorithmes pour calculer certains concepts de théorie des catégories [Bur80, BR86], en particulier les colimites de diagrammes. Le calcul général de colimite est paramétré par certaines colimites, en l'occurrence un objet initial, des sommes et des coégalisateurs, qui permettent d'évaluer la colimite d'un diagramme quelconque. Ainsi, ayant défini l'objet initial, la somme et le coégalisateur par exemple dans la catégorie des ensembles Set, on en déduit un moyen de calculer la colimite d'un diagramme quelconque dans Set. Cet algorithme est en fait basé sur une preuve du résultat suivant : si une catégorie a un objet initial, des sommes et des coégalisateurs, alors celle-ci est Animent cocomplète. Notre travail est basé sur un théorème similaire : si une catégorie a un objet initial et des sommes amalgamées alors celle-ci est Animent cocomplète. Notre travail est différent, dans la mesure où nous ne cherchons pas à calculer des colimites dans une catégorie fixée. En particulier, nous nous intéressons au problème général de l'isomorphisme entre deux diagrammes, qui correspond à un isomorphisme entre leurs colimites respectives. Cet isomorphisme est indépendant de la catégorie sur laquelle ces diagrammes sont construits. INTRODUCTION 15 Utilisation des colimites en spécification algébrique L'utilisation des colimites pour représenter l'assemblage de spécifications est loin d'être nouvelle. R. Burstall et J. Goguen ont présenté cette idée dans la sémantique du langage de spécification Clear [BG80]. Dans Clear, la composition de plusieurs spécifications qui partagent un environnement commun, appelées théories basées, est en effet formalisée par la colimite d'un diagramme. Les colimites ont ensuite été assez intensivement utilisées en spécification algébrique. La somme amalgamée en particulier permet de modéliser l'instanciation de spécifications génériques [TWW82, EM85]. H. Ehrig, R. Jimenez et F. Orejas [EJ093] ont également présenté une forme plus générale distanciation à l'aide de sommes amalgamées multiples5, nouvel exemple de colimite. S y n t a x e pour les constructions modulaires J. Bergstra, J. Heering et R. Klint [BHK90] d'une part, et G. Renardel de Lavalette [Ren91] d'autre part, ont proposé de structurer les opérateurs de construction de spécifications sous forme d'algèbres de modules. Une algèbre de modules est un langage permettant d'écrire des expressions de composition des spécifications algébriques. Cette approche est voisine de notre travail sur le langage Terme(Co), puisque le problème de la composition des spécifications algébriques est abordé d'un point de vue syntaxique, et permet de comparer différentes spécifications modulaires. Par contre, nous ne nous intéressons pas aux mêmes opérateurs de constructions de spécifications, puisque nous ne considérons que les constructions de colimites. Notre syntaxe pour représenter les spécifications algébriques modulaires est largement inspirée des travaux de J.-C. Reynaud, qui a proposé un système de types pour représenter les constructions de colimites [Rey90a, Rey90b, Rey93]. Ce système est fondé sur les théories algébriques généralisées de Cartmell [Car86] qui permettent de spécifier des types dépendants, c'est-à-dire des types paramétrés par des termes. Les types dépendants ont été également utilisés par T. Streicher et M. Wirsing [SW91] pour modéliser la composition de spécifications algébriques modulaires. D'autre part, H. Ehrig, R. Jimenez et F. Orejas ont également proposé une syntaxe pour les spécifications algébriques modulaires dans [EJ093]. Cette syntaxe est en partie basée sur des constructions de sommes amalgamées. La principale difficulté en ce qui concerne la définition d'une syntaxe pour les constructions de colimites est le problème de circularité entre la définition d'une part des objets et des flèches de Terme(Co) et d'autre part de l'égalité entre deux flèches de Terme(Co). En effet, il existe une flèche, que nous appelons up dans ce mémoire, entre une somme amalgamée et un objet à condition qu'une égalité entre deux flèches de Terme(Co) soit vérifiée. La définition des flèches up dépend donc de la définition de l'égalité des flèches dans Terme(Co), qui elle-même présuppose que les flèches ont été définies. J.-C. Reynaud contourne le problème en proposant une définition concrète, c'està-dire sémantique, d'une catégorie librement engendrée par objet initial choisi et sommes amalgamées choisies [Rey93]. H. Ehrig, R. Jimenez et F. Orejas [EJ093] ne 5. En cinglais, multiple pushout. 16 INTRODUCTION définissent pas de syntaxe pour les flèches up. La syntaxe qu'ils proposent ne permet donc pas d'obtenir une catégorie finiment cocomplète. Une solution pour spécifier une catégorie finiment cocomplète sans utiliser d'égalités pour définir les flèches a été présentée par F . Cury dans [Cur91]. F. Cury propose de dédoubler les flèches up en deux flèches dont la définition ne dépend pas d'une égalité. Ces deux flèches, qui sont des exemples particuliers de flèches up, permettent de reconstruire a posteriori toutes les flèches up. La solution que nous proposons consiste à stratifier la construction de Terme(Co) en une suite de catégories C{. L'existence d'une flèche up dans la catégorie d dépend uniquement d'égalités dans la catégorie C,-_i. Nous évitons ainsi le problème de circularité entre la définition des flèches et la définition des égalités. Notre catégorie Terme(Co) peut être comparée au type d'une esquisse, introduit par C. Ehresmann [Ehr68]. Dans les travaux de D. Duval et J.-C. Reynaud [DR94a, DR94b], le type d'une esquisse est une catégorie librement engendrée à partir d'un graphe par sommes et produits. Par conséquent, la construction du type d'une esquisse est basée sur les catégories à sommes et produits alors que la construction de Terme(Co) est basée sur les catégories à colimites finies. D'autre part, une esquisse contient des cônes et cocônes distingués, qui spécifient certaines limites ou colimites. Par contre, dans la construction de Terme(Co) que nous proposons, il n'est pas possible de spécifier des sommes amalgamées distinguées dans la catégorie de base C$. 6 Plan de ce mémoire Ce mémoire est divisé en trois parties, chaque partie faisant l'objet d'un volume de Diagrammes. Ce volume contient la première partie de notre thèse, c'est-à-dire les chapitres 1 et 2, consacrés respectivement au cadre général (les spécifications algébriques modulaires) et aux bases théoriques (les catégories de diagrammes). Le chapitre 1 introduit les spécifications algébriques modulaires, présente le problème de la composition des spécifications et pose le cadre général de notre travail. Après quelques rappels sur les spécifications algébriques, nous proposons plusieurs exemples de spécifications modulaires d'anneaux, en utilisant quelques spécifications et morphismes de spécifications de base. Cet exemple académique présente d'une part la syntaxe pour les constructions modulaires, et d'autre part le problème de l'isomorphisme de construction entre deux spécifications modulaires. Le chapitre 2 contient les bases théoriques de notre travail. Nous effectuons quelques rappels de théorie des graphes en section 2.1, puis de théorie des catégories en section 2.2. Enfin, en section 2.3, nous présentons les notions de diagrammes, de colimites finies ainsi que les catégories de diagrammes DIAGR(Co) et diagr(Co). Nous montrons que la catégorie diagr(Co) est finiment cocomplète, et que diagr(Co) est une complétion par colimites finies de CQ. La deuxième partie, qui correspond au chapitre 3, est consacrée à la définition de la syntaxe des spécifications modulaires. Enfin, dans la troisième partie, nous proposons d'interpréter les termes par des diagrammes (chapitre 4), et nous présentons un algorithme pour détecter si deux INTRODUCTION 17 diagrammes sont isomorphes, dans le cas particulier ou la catégorie de base Co est finie et ne comporte pas de cycle (chapitre 5). Chapitre 1 Motivation Le but de ce chapitre est de présenter le problème de la composition des spécifications modulaires. Nous étudions différentes spécifications modulaires des anneaux, construites à partir de quelques spécifications de base. Cet exemple est décrit en utilisant le langage de spécification LPG (Langage pour la Programmation Générique) développé par D. Bert et R. Echahed [BE86, B+90]. Nous introduisons informellement une syntaxe pour représenter les spécifications modulaires, et expliquons — également de façon informelle — qu'une spécification modulaire peut être considérée comme la colimite d'un diagramme. Nous motivons ensuite l'intérêt des isomorphismes de construction. Enfin, nous posons le cadre général de notre travail. 1.1 Préliminaires Dans cette partie, nous rappelons quelques notions élémentaires de spécification algébrique, en particulier les définitions de signature, morphisme de signatures, algèbre, morphisme d'algèbres, équation et algèbre satisfaisant une équation. Cette présentation, loin d'être exhaustive, est inspirée de [GB90] et de [EM85]. Définition 1.1 (5-ensemble et 5-application) Soit un ensemble S. Un 5-ensemble A est une famille indicée par S d'ensembles disjoints (.4 s ) 5Ç s. Une S-application / entre deux S-ensembles A et B, notée / : A -+ B, est une famille indicée par S d'applications (fs : As —» Bs)sesDéfinition 1.2 (Ensemble des chaînes finies) Soit un ensemble .4. L'ensemble des chaînes finies sur .4 est l'ensemble m oo A =\J An. 71=0 Notations : • La chaîne vide est notée s. • La chaîne composée des éléments s\, ^ . . . , sn est notée s\S2 19 -..sn. 20 CHAPITRE 1. MOTIVATION L'ensemble des chaînes finies non vides sur A est oo A+ = A* x A= [j An. n=l Les opérations J" et J* s'étendent aux applications entre deux ensembles. Soit une application / : A —> B. On définit les applications /* : A* -> B* et / + : A+ —> B+ de la façon suivante. /*(«i .. .an) = f(ax).. .f(an) (pour n > 1) ; /+(<*] .. .a n ) = / ( a i ) . . . / ( a n ) (pour n > 1). On vérifie facilement que pour tout ensemble A. on a {id \)~ = irf^* {idA)+ = i d ^ et pour toutes applications / : .4 —» B et p : B —» C, on a ( W ) + = <7+°/+Ces deux propriétés signifient que J" et _+ sont des fondeurs _+ : Set —>• Set dans la catégorie des ensembles Set. _* : Set —> Set et Une signature comprend les symboles utilisés pour former des expressions. Plus précisément, une signature est composée d'un ensemble de symboles de sortes, qui représentent des types de données, et d'un ensemble de symboles d'opérateurs, qui représentent des opérations sur ces données. À chaque symbole d'opérateur est associé un profil, qui représente le type des données d'entrée et de sortie. Définition 1.3 (Signature multi-sortes) Une signature multi-sortes, ou plus simplement signature, est un triplet (S, Q, ZJ) où • S est un ensemble fini, dont les éléments sont appelés sortes; • Q est un ensemble fini, dont les éléments sont appelés opérateurs; • zu est une application TU : Q —> 5 + , qui à chaque opérateur u; de Q associe une chaîne non vide sur 5, appelée profil de u. Notation : si ZU(LJ) = s\ .. .sns (n > 0), on note UJ : s\,.. que u; est une constante, et on note u; : —> s. .sn —> s. Si n = 0, on dit Remarque 1.1 Une signature est souvent définie comme un ensemble de sortes S accompagné d'une famille indicée par S* X S d'ensembles d'opérateurs. Nous avons préféré considérer ici un unique ensemble aplati Q d'opérateurs, le profil étant décrit par l'application w : Q —> S + . Nous avons choisi cette définition parce qu'elle permet de définir facilement la somme amalgamée de deux signatures à partir de la définition de la somme amalgamée de deux ensembles (cf. section 1.4). 1.1. PRELIMINAIRES 21 Exemple 1.1 (Exemples de signatures) • La signature la plus simple est la signature vide, notée £ 0 , telle que l'ensemble des sortes et l'ensemble des opérateurs sont vides. • Un exemple classique de signature est la signature T>Nat = (S Nat i^ Nat ^ Nat) des entiers naturels où S Nat et Çl^at e t ^Nat s o n t définis de la façon suivante : SNat = {nat} ; &Nat = {0, suce, + } ; ^A'at(O) = nat ; zj^at(succ) = nat nat ; ^Nat{~\~) = na>t nal Tiat. Dans le langage de spécification LPG, les noms de sortes sont introduits par le mot clé s o r t s et les opérateurs par le mot clé o p e r a t o r s . La signature ^2Nat est donc définie en LPG par: sorts operators nat 0 : ->nat suce : nat ->nat + : n a t , n a t ->nat • Voici un autre exemple de signature, la signature EA/ des monoïdes. Dans cette signature, on a une seule sorte s, une constante 1 et un opérateur binaire *. En LPG, on peut définir la signature EA/ de la façon suivante : sorts operators s 1 : ->s * : s , s ->s Un morphisme de signatures entre deux signatures E et E' associe à toute sorte de E une sorte de E' et à tout opérateur de E un opérateur de E ; , en conservant les profils des opérateurs. Définition 1.4 (Morphisme de signatures) Soit deux signatures E = (S, Q, w) et E' = (Sf, Q', VJ'). Un morphisme de signatures m de E vers S', noté m : S -» E' est un couple (ms,mP) où • ms est une application ms : S —• S' ; • ran est une application m fi : Çl -» Qf ; tel que zo1 o mP" = m 5 + o w. Détaillons un peu la condition w' o ran = m 5 + o w. Considérons un opérateur u : s\,.. .,sn —> s de Q. 22 CHAPITRE G7'(m n M) = = = 1. MOTIVATION ™ 5 + M<")) ms+(si.. ,sns) ^5(^i) • ..ms(sn)ms(s) L'opérateur m n (u;) de Q' a donc pour profil rafi(u>) : ra5($i),..., ms(sn) -> ro5(s). On peut composer les morphismes de signatures. Soit trois signatures E = (s,n,a7) E' = (s',fi',:u') /# E" =(5 , n w ) et deux morphismes de signatures m={ms,mn) : S - > E' 5 n n = (n ,rc ):E'->E". Pour composer m et rc, il suffit de composer les applications sur les sortes et les applications sur les opérateurs. Autrement dit, nom = (ns o ms, n n o mn). Cela définit bien un morphisme de signatures car ~ " o w " o mn = ns+ o zz' o mQ = rcs+ o 7n 5+ ozz = (ns o 77?5)+ o zz (n : E' —> E" morphisme de signatures) (m : S —> E' morphisme de signatures) (_+ est un foncteur) On a une catégorie des signatures, notée Sig, dont les objets sont les signatures, et les flèches sont les morphismes de signatures. E x e m p l e 1.2 (Exemples de morphismes de signatures) • Pour toute signature E = (S, Q, zz), il existe un morphisme de signatures de la signature vide E 0 vers S. Ce morphisme, noté jV = (j^, jQ), est constitué de l'application vide de l'ensemble vide des sortes vers S, et de l'application vide de l'ensemble vide des opérateurs vers Q. De plus, ce morphisme est unique. Dans la catégorie des signatures Sig, E 0 est un objet initial puisqu'il existe une unique flèche de E 0 vers tout autre objet de Sig. • On a un morphisme de signatures de la signature des monoïdes vers la signature des entiers naturels m : EA/ —> Ejva* ? qui associe la sorte 5 de E M à, la sorte nat de EMZÉÎ la constante 1 à la constante 0, et l'opérateur binaire * à l'opérateur binaire + . ms(s) = nat ; m n ( l ) = 0; mn(*) = +. 1.1. PRELIMINAIRES 23 Soit une signature E. Définir une algèbre sur E, ou T,-algèbre, consiste à interpréter les sortes de E par des ensembles, et les opérateurs de E par des applications entre ces ensembles. Une E-algèbre est également appelée modèle ou interprétation de la signature E. Définition 1.5 (E-algèbre) Soit une signature E = (S, Q,zz). Une E-algèbre A est définie par: • un 5-ensemble A ; • pour tout opérateur u : s\,$2, • • • ?$n —>• s G fi, une application UJA : ASl x AS2 x • • • x ASn -+ .4S. Si u) est une constante u : —> s, uA est un élément de As. Définition 1.6 (Morphisme d'algèbres) Soit une signature E = (S, Q,ZJ) et deux algèbres A et B. Un morphisme d'algèbres h de A vers B, noté h : A —> B est une 5-application (hs : As -» Bs)sçs telle que pour tout opérateur u; : s\, 5 2 , . . . , sn —> s de fi, pour tout rc-uplet (ai, ci2,..., an) de „45l x AS2 x • • • X ASn, h8(uA(ai xeTr{X)s; - u ; : s i , 5 2 , . . . , 5 n - > s e n , tx eTz(X)St => u>{tut2,...,tn)£Tz{X)a. Les éléments de Tr(X)s (i= l,...,n) sont appelés termes de sorte s. • L'interprétation d'un opérateur u : s\, 5 2 , . . . , sn —> s G fi est l'application jr*{X) . 7V(À')51 x . . . x T s ( X ) S n -+ Tr(X)s {tl,...,tn) H-» U(tu...,tn). 24 CHAPITRE 1. MOTIVATION Lorsque l'ensemble des variables X est vide, on obtient l'algèbre des termes fermés 7v = r E (0). Une affectation d'un ensemble de variables X dans une E-algèbre A associe à toute variable de Xs un élément de As. Autrement dit, une affectation aff de X dans A est une 5-application aff : X —> A. L'algèbre des termes a une propriété importante: c'est une algèbre libre dans la classe des E-algèbres. Cela signifie que toute affectation de X dans une algèbre A s'étend de façon unique en un morphisme d'algèbres de TE (A) vers A. Théorème 1.1 (L'algèbre 7V(A) est libre dans Alg(E); Notons i : X —» TV (A") l'inclusion de X dans TV (A). Soit une T,-algèbre A. Pour toute affectation aff : X —> A, il existe un unique morphisme d'algèbres ô/f :Ï£(-Y)-> A tel que qlf oi = aff. Une équation est tout simplement composée d'un ensemble de variables et de deux termes. Définition 1.9 (E-équation) Soit une signature E = (S, fi, :^) et un ensemble de variables À' sur E. Une ^-équation sur E de sorte s est un triplet (À', /1,^2) où t\ et t2 sont des éléments de TV(A')5. En LPG, une signature peut être accompagnée d'un ensemble d'équations. Toutes ces équations ont le même ensemble de variables, qui sont introduites une seule fois par le mot clé v a r i a b l e s . Ensuite, les E-équations {X,ti,t2) sont introduites par le mot clé équations et notées t\ == t2. Définition 1.10 (Algèbre satisfaisant une équation, S-F-algèbre) Soit une signature E = (S,Q,zz). On dit qu'une E-algèbre A satisfait une équation (X,t\,t2) si et seulement si pour toute affectation aff : X —> A, aff{t\) = aff(t2). Etant donné un ensemble d'équations E sur E, une E-£-algèbre est une E-algèbre qui satisfait toutes les équations de E. Définition 1.11 (Fermeture sémantique d'un ensemble d'équations) Soit une signature E et un ensemble d'équations E. La fermeture sémantique E de E est l'ensemble des équations sur E qui sont satisfaites par toute E-E-algèbre. Définition 1.12 (Extension aux termes d'un morphisme de signatures) Soit deux signatures E = (S, Q,zz) et E' = (S7, fi7, 57'), ainsi qu'un morphisme de signatures m : E —> E7. Soit un ensemble de variables À' sur E, dont les éléments sont distincts des constantes de fi7. La traduction de X par le morphisme de signatures m : E —> E7 est le S7-ensemble A'* tel que pour toute sorte s' de 5 7 , x*= (J xs. sf=ms(s) 1.2. SPECIFICATIONS 25 IS extension du morphisme de signatures m : E —» E7 est une famille indicée par S d'applications ra# = (raf : T^(X)S -» Ts'(A#) m s( 5 )) s es. Pour toute sorte s G S, l'application raf : T%(X)S —> T n v/(A*) m 5( s \ est définie inductivement sur la structure des éléments de T s ( A ) s de la façon suivante. • Vx G A s , mf(x) = x(xe X*S{a)) • Vu; : si,s2,...sn -> s, Vf,- G TV(A')5t (i = l , . . . , n ) , mf{u(ti,t2,..., Étant donné un terme t G T^(X)S, ; tn)) = mçl(u){mfl {tx), mf2{t2),..., rri&{t) = mf(t) mfn(tn)). est appelé traduction de t par m. Exemple 1.3 Considérons le morphisme de signatures m : EA/ —> E J W et le terme 1 * .T de TrM(X). La traduction du terme 1 * x sur SA/ par m est le terme sur E^ a f m # ( l * x) = ra#(l) + m#(x) = 0 + x. Définition 1.13 (Traduction d'une équation par un morphisme de signatures) Soit deux signatures E = (S, fi, zz) et E7 = (S7, fi7, zzf), ainsi qu'un morphisme de signatures m : E —> E7. Soit une équation (A', t\, t2) sur E. La. traduction de l'équation (XJ\J2) par le morphisme de signatures m est l'équation (A'*, rn^(ti), m&fo)) sur la signature E7. E x e m p l e 1.4 Considérons par exemple l'équation {{x}, l*x, x) sur la signature EA/. La traduction de cette équation par le morphisme de signatures m : EA/ —> ^Nat est l'équation ({x},0 + x,x) sur Ejvaf- 1.2 Spécifications Dans ce paragraphe, nous présentons les spécifications algébriques, qui consistent en une signature et un ensemble de formules. Dans l'exemple des anneaux développé dans ce chapitre, les formules que nous considérons sont uniquement des équations. Pour cette raison, nous nous contentons de définir des spécifications équationnelles. Nous verrons en section 1.7 que cette hypothèse peut être affaiblie en se plaçant dans le cadre général des institutions. Définition 1.14 (Spécification équationnelle) Une spécification équationnelle est un couple (E, E), où E est une signature et E est un ensemble de E-équations. Définition 1.15 (Morphisme de spécifications) Un morphisme de spécifications entre deux spécifications (E, E) et (E7, E') est un morphisme de signatures m : E -> E7 tel que pour toute équation e G E, ra#(e) G E1. Rappelons que • ra#(e) est la traduction de l'équation e par le morphisme de signatures m; • E' est la fermeture sémantique de E', c'est-à-dire l'ensemble des équations sur E7 qui sont satisfaites dans toute E 7 -^-algèbre. 26 CHAPITRE 1. MOTIVATION Une autre façon de définir un morphisme de spécifications est d'imposer que la traduction par m * de toute équation de E appartienne à la théorie équationnelle de E', c'est-à-dire peut être déduite des équations de E* par déduction en logique équationnelle. Il s'agit d'une définition plus syntaxique de la notion de spécification. Nous avons choisi de suivre la définition donnée pour les institutions par J. Goguen et R. Burstall dans [GB90]. Dans le cadre des spécifications algébriques équationnelles, les deux définitions sont équivalentes puisque le système de déduction équationnel est complet. En effet, une équation e est satisfaite "dans toute E-£"-algèbre si et seulement si on peut déduire e des équations de E par raisonnement équationnel. On a une catégorie des spécifications équationnelles, notée Spec, dont les objets sont les spécifications (équationnelles) et les flèches sont les morphismes de spécifications. Exemple 1.5 • La spécification la plus simple est la spécification vide ( E 0 , 0 ) , construite sur la signature vide E 0 , et dont l'ensemble des équations est vide. Cette spécification est initiale dans la catégorie des spécifications, car pour toute spécification Sp, il existe un unique morphisme de spécifications de la spécification vide vers Sp. • Voici un exemple de spécification des entiers écrit en LPG : type sorts operators variables équations Nat nat 0 : ->nat suce : n a t ->nat +: nat, nat ->nat x, y : nat 0 + y == y s(x) + y == s(x + y) Le langage LPG permet de spécifier à la fois des types, comme le type Nat, qui ont pour interprétation une algèbre initiale (ou pour les types génériques une algèbre libre), et des propriétés, qui ont pour interprétation une classe d'algèbres satisfaisant les équations de la spécification. On peut consulter [Rey87] pour avoir une description plus détaillée de la sémantique de LPG. Dans l'exemple développé ici, nous utiliserons uniquement les propriétés, sans importation de type, ce qui signifie qu'un modèle ou une interprétation d'une spécification est tout simplement une algèbre qui satisfait les équations de la spécification. Le langage LPG permet également de déclarer des morphismes de spécifications. Un morphisme d'une spécification Sp vers une spécification Sp7 est défini au moment de la déclaration du codomaine Spf par une instruction commençant par le mot clé s a t i s f i e s ou par le mot clé i n h e r i t s . Le langage LPG permet également de considérer les compositions des morphismes de spécifications déclarés. Les règles de composition de ces morphismes et leur sémantique associée ont été décrits dans [B095]. 1.2. SPECIFICATIONS 27 Nous allons maintenant présenter les spécifications équationnelles et les morphismes de spécifications qui nous permettront de définir plusieurs spécifications modulaires des anneaux. Rappelons qu'un ensemble A, muni de deux opérations binaires + et * est un anneau si et seulement si A muni de l'opération + est un groupe commutatif, A muni de l'opération * est un monoïde, et l'opération * est distributive par rapport à l'opération + . Nous commençons par définir deux spécifications S et B qui comportent uniquement une signature et aucune équation. La spécification S contient une sorte unique s. Un modèle de S est donc un ensemble quelconque. property sorts S = UNE-SORTE s La spécification B contient une sorte s et un opérateur binaire op. Un modèle de B consiste donc en un ensemble muni d'une opération binaire. Nous avons également spécifié un morphisme de spécifications s : S —> B par la proposition s a t i s f i e s UNE-SORTE [s] dans B. Le morphisme de spécifications s associe la sorte s de 5 à la sorte s de B. B = property sorts operators satisfies OP-BIN s op : s , s ->s UNE-SORTE[s] Nous définissons maintenant une spécification AI pour les monoïdes. La signature de la spécification A/ comporte une sorte s, une opération binaire *, et une constante 1. La spécification M comporte également trois équations qui indiquent que 1 est élément neutre pour *, et que * est associative. Un modèle de M est donc un ensemble muni d'une opération binaire associative et d'un élément neutre. Il s'agit donc bien d'un monoïde. Nous avons également un morphisme de spécifications b : B —> M. Le morphisme 6 associe à la sorte s de B la sorte s de M et à l'opérateur op de B l'opérateur * de M. Ce morphisme de signatures est bien un morphisme de spécifications, puisque la spécification de l'opérateur binaire B ne comporte aucune équation. property sorts operators M = variables équations satisfies MONOÏDE s * : s , s ->s 1 : ->s x, y, z : s 1 * x == x x * 1 == x (x * y) * z == x * (y * z ) OP-BIN[s,*] CHAPITRE 1. MOTIVATION 28 Pour obtenir un groupe commutatif, nous devons ajouter une opération inverse i, et la commutativité de l'opérateur binaire. Cela nous donne la spécification G. property sorts operators G = variables équations inherits GROUPE-COMM s + : s , s ->s 0 : ->s i : s ->s x, y : s x + y == y + x i(x) + x ss 0 MONOÏDE[s, +, 0] Nous spécifions également un morphisme de signatures de la signature de M vers la signature de G, m : EA/ -> E G , par la proposition i n h e r i t s MONOÏDE [s,+ , 0 ] . Ce morphisme de signatures associe la sorte s de M à la sorte s de G, l'opérateur * de M à l'opérateur + de G, et la constante 1 de M à la constante 0 de G. Le mot clé inherits signifie que l'on ''recopie" les équations de la spécification M dans la spécification G via le morphisme de signatures m*. Autrement dit, G contient implicitement les équations variables équations x, y, z : s 0 + x == x x + 0 == x (x + y) + z == x + (y + z) Par conséquent, le morphisme de signatures m : E M —» E G est un morphisme de spécifications m : M —¥ G. Enfin, la propriété D spécifie deux opérateurs + et * tels que * est distributif par rapport à +, ainsi que deux morphismes de spécifications ra+, mx : B -+ D. property sorts operators variables équations satisfies D = DISTRIBUTIVITE s +, * : s , s ->s x, y, z : s x * (y + z) == (x * y) + (x * z) OP-BIN [ s f + ] , OP-BIN [ s , * ] Les deux morphismes ra+, mm : B —» D sont définis par : m+(s) m+(op) m*(s) = = = m = *• *(°P) s; +; s; Finalement, pour résumer, nous avons déclaré cinq spécifications S, B, M, G, D, et cinq morphismes de spécifications s, b, m, ra+, m*. Nous pouvons évidemment 1.3. COMPOSITION DE SPÉCIFICATIONS 29 EN LPG considérer également les morphismes de spécifications identités ids, tàs, idM, id>G et idp sur ces cinq spécifications, ainsi que toutes les compositions possibles pour les morphismes de spécifications. On vérifie facilement que l'on obtient ainsi quinze morphismes de spécifications différents. Autrement dit, nous considérons une catégorie de spécifications, appelée CQ, qui comporte ces cinq spécifications et ces quinze morphismes de spécifications. S - B ra+ -M •* G nu D Squelette de la catégorie CQ Nous avons défini les spécifications équationnelles, qui forment une catégorie Spec, ainsi qu'une sous-catégorie finie CQ de Spec, que nous appellerons catégorie des spécifications de base. La catégorie CQ représente l'ensemble des spécifications disponibles en bibliothèque. Nous nous intéressons ensuite uniquement aux spécifications que Ton peut construire en assemblant des spécifications de base. 1.3 Composition de spécifications en LPG Une spécification modulaire est soit une spécification de base, soit une spécification obtenue par un assemblage de plusieurs spécifications modulaires. Nous parlerons de composition de spécifications pour décrire l'assemblage de plusieurs spécifications permettant de construire une spécification plus complexe. La composition de spécifications en LPG est réalisée par ce qu'on appelle une combinaison de spécifications. Pour réaliser cette opération, il faut définir une signature — la signature de la spécification résultat — et des morphismes de spécifications des spécifications combinées vers la spécification résultat. Nous pouvons par exemple écrire une spécification des anneaux en combinant les propriétés MONOÏDE, DISTRIBUTIVITE et GROUP-COMM de la façon suivante. property sorts operators Ai = combines ANNEAU s + , * : s , s ->s 0, 1 : ->s i : s ->s MONOÏDE [ s , * , 1 ] , DISTRIBUTIVITE[s,+,*], GR0UPE-C0MM[s,+,0,i] 30 CHAPITRE 1. MOTIVATION Sémantiquement, cette combinaison signifie que chaque fois qu'on a un modèle de MONOÏDE, un modèle de DISTRIBUTIVITE et un modèle de GROUPE-COMM, tels que ces trois modèles ont la même interprétation pour la sorte s, que Vopérateur du monoïde est le second opérateur de la distributivité et Vopérateur du groupe commutatif est le premier opérateur de la distributivité, alors on a un modèle de la spécification ANNEAU. Ces partages de sorte et d'opérateurs sont évidemment cruciaux. Il ne suffit pas d'avoir un monoïde, un groupe commutatif et deux opérateurs distributifs l'un par rapport à l'autre pour avoir un anneau. Par exemple, si nous avions écrit combines . . . DISTRIBUTIVITE[s,*,+] à la place de combines . . . DISTRIBUTIVITE [ s , + , * ] nous n'aurions pas spécifié un anneau. (La multiplication est distributive par rapport à l'addition, et non l'inverse.) En LPG, les partages entre spécifications, en particulier lors de la construction de combinaisons de propriétés, sont exprimés de façon "implicite'', par des morphismes de spécifications. En pratique, on voit que la sorte s est partagée par les trois spécifications par l'apparition de s dans la définition des trois morphismes. combines MONOÏDE[s,*,1] , DISTRIBUTIVITE[s,+,*], GROUPE-COMM[s,+,0,i] Dans notre travail, ces partages effectués lors de la composition des spécifications sont exprimés par des colimites de diagrammes. La colimite est un concept de théorie des catégories qui sera présenté d a n s le chapitre 2. Cette construction permet, en particulier dans le cadre des spécifications algébriques, de modéliser l'assemblage de plusieurs objets en rendant explicites certains partages entre ces objets. Dans l'exemple ci-dessus, la spécification modulaire A\ correspond à la colimite du diagramme S\. B • •M hos \ m / m» os S • -• D mobos m+ B mob Si 1.4. SOMMES AMALGAMEES 31 Voici l'interprétation intuitive de ce diagramme: • Les trois nœuds étiquetés par les spécifications M, D et G, qui apparaissent comme des puits du graphe (aucun arc n'a pour source un nœud étiqueté par M, D ou G) sont les spécifications que l'on assemble. • Les trois nœuds étiquetés par B, S et B indiquent les partages. — La sorte s est partagée par les trois spécifications M, D et G. Ce partage est modélisé par les morphismes b o s : S —> M, m* o s : S —ï D et mobos:S-+G. — L'opérateur binaire * est partagé par les spécifications A/ et D. Ce partage est modélisé par les morphismes b : B —> M et m* : B —» D. — L'opérateur binaire + est partagé par les spécifications G et D. Ce partage est modélisé par les morphismes m o b : B -> G et ra+ : B —» D. Par la suite, nous privilégions une construction particulière de colimite: la somme amalgamée. La somme amalgamée correspond à la colimite d'un diagramme T qui ne comporte que trois spécifications SpA, SpB et Spc, liées par deux morphismes de spécifications / : SpA —> Sps et g : SpA —> Spc- La colimite de ce diagramme correspond à la composition des spécifications Sps et Spc où les partages entre ces deux spécifications sont indiqués par les deux morphismes / et g. 1.4 Sommes amalgamées Dans cette section, nous définissons la somme amalgamée de deux ensembles, puis de deux signatures, et enfin de deux spécifications. Autrement dit, nous présentons la somme amalgamée dans trois catégories particulières : Set (catégorie des ensembles), Sig (catégorie des signatures) et Spec (catégorie des spécifications). La définition générale sera revue dans le chapitre 2. CHAPITRE 32 1.4.1 1. MOTIVATION S o m m e a m a l g a m é e de d e u x e n s e m b l e s Considérons trois ensembles A, B, et C, ainsi que deux applications / : A -» B et g : A -> C. Intuitivement, faire la somme amalgamée de B et C par rapport à / et g consiste à faire l'union disjointe de B et C et à fusionner les éléments qui sont images par f et g d'un même élément a de A. Plus formellement, on peut définir la somme disjointe de B et C par l'ensemble B + C = ({1} x B)U {{2} x C). Il y a évidemment un choix de codage dans cette définition. L'idée est de faire la réunion des deux ensembles B et C après avoir renommé les éléments communs aux deux ensembles. Nous avons également deux applications i\ : B —> B + C et i2 : C —> B + C définies par h : B b -> B + C H+ (1.6) C c *2 -> H* B +C (2, c) Puis on définit une relation 7v sur l'ensemble B + C : TZ = {((l,f(a)),(2,g(a))) ; Va € A}. On considère ensuite la relation d'équivalence TZ engendrée par U et l'ensemble quotient P - (B + C)/ÏZ. On a une application de projection p^ B + C -> F , qui à tout élément de B + C associe sa classe d'équivalence modulo 7£. Notations • L'ensemble P est noté push (A, B,C, • L'application poix f,g). : B -> P est notée &.\{A, B,C, f,g). • L'application p o z2 : C ->• P est notée &.2{A, B, C, f, g). • Pour alléger un peu les notations, si P = push {A, B,C, f,g), nous écrirons - &i(P) à l a p l a c e d e & i ( A , f l , C , / , 5 ) ; 1.4. SOMMES AMALGAMEES 33 - &2{P) à la place de & 2 (^4,5,C,/,5). Définition 1.16 (Somme amalgamée dans Set) La somme amalgamée de fi et C par rapport à / et g est le triplet (push (A,B,CJ,g),^(A,B,CJ,g),L2(A,B,C,f,g)). Par abus de langage, l'ensemble push (A, B,C, f, g) sera également appelé somme amalgamée. Il ne faut pas oublier qu'en réalité les deux applications &i (.4, B, C, f, g) et &.2(A, B,C, f,g) font partie de la définition d'une somme amalgamée. Nous formulons maintenant la propriété générale des sommes amalgamées en théorie des catégories. Nous reverrons cette propriété dans le chapitre 2. Propriété 1.1 (Propriété caractéristique des sommes amalgamées) Une somme amalgamée (push (A, B,C, f,g),8il(A,B,C,f,g)^2(A,B,C, satisfait les propriétés suivantes. 1. bi(A,B.C,f,g)of = f,g)) b2(A,B,C,f,g)og; 2. pour tout objet D et flèches f : B -> D, g' :C -ï D telles que f o f = gf o g, il existe une flèche unique u : push (A, B, C, f,g) -> D telle que [uobl{A,B,C,f,g) \uob2(A D telles que / ' o / = g' og, il existe une application unique u : push (A, B, C, f,g) —> D telle que (uoiii(A,B,C,f,g) = f \uoëL2{A,B,C,f,g) = g'. Exemple 1.6 Soit A = {ai,a 2 }, B = {x,y,z} et C = {x}. Soit / = {{aux),(a2,y)}et g = {{au x), (a2, x)}. fî + C = { ( l , x ) , ( l , y ) , ( M ) , ( 2 , z ) } F = push(.4,B,C,/, 5 )={{(l,x),(l,y),(2,x)},{(l, 2 )}} &1(F)(x) = &i(P)(y) = {(l,x),(l,y),(2,x)} &i(P)(*) = {(l,*)} &2(P)(*) = {(!,*), (l,y),(2,x)} Remarque 1.2 Nous avons en réalité défini ici un codage de la somme amalgamée pour les ensembles. Dans la théorie des catégories, la somme amalgamée est définie à un isomorphisme près. Dans l'exemple 1.6, en prenant pour P un ensemble quelconque à deux éléments, la propriété 1.1 est encore vérifiée. 1.4.2 Somme amalgamée de deux signatures Nous définissons la somme amalgamée de deux signatures à partir de la définition de la somme amalgamée de deux ensembles. Soit trois signatures 1.4. SOMMES AMALGAMÉES 35 £U = {SA,&A,&A) EB=(SB^B^B) Se = {Sc,ttc,&c) et deux morphismes de signatures f=(fs,f"):XA^XB g=(gs,gn):XA^ZcOn définit la signature S p = (Sp, ftp, a?p), somme amalgamée des signatures S # et 2 e par rapport aux morphismes / : IU -> 2 # et 5 : XU ->• S e de la façon suivante. L'ensemble 5p est la somme amalgamée des ensembles SB et 5 c par rapport à / 5 et gs. Autrement dit, Sp = push ( 5 , 1 , 5 B , 5 e , / 5 , # 5 ) . L'ensemble Qp est la somme amalgamée des ensembles ftp et Qc par rapport à fn et gn. Autrement dit, nP = push(nA,nB,nc,fn,ga)- Il reste à définir uDP :ÇÎP -» Sp pour obtenir la signature 2 p . On a l'égalité &i (5p) + ozjB°fn = & 2 ( 5 P ) + o ^ c o S e morphisme de signatures) donc, comme QP = push (fi 4, ftp, fie, / n , 5") et d'après la propriété caractéristique des sommes amalgamées, il existe une unique application znp : Qp —ï Sp telle que wpobiiQp) = &l(Sp)+ovjB ZJP o & 2 (fi P ) = &.2{SP)+ o VDC (1) (2) On pose push (S>|, S B , S e , / , g) = Sp ; MSp) = M S ^ S B , S e , / , s ) = (MSp),Mftp)); &2(2P) = & 2 ( 2 . 4 , 2 B , 2 C , / , SA/ et mobos : s 5 ->s G . Une somme amalgamée de SA/ et S e par rapport à 60 s et mobos S p suivante : sorts operators est la signature s +, * : s , s ->s 0, 1 : ->s i : s ->s On doit fusionner la sorte s de SA/ avec la sorte s de S e - Remarquons que nous n'avons pas été obligés de renommer certaines sortes ou opérateurs. En effet, les deux sortes à fusionner ont le même nom dans les deux signatures 2A/ et 2 G , et les opérateurs que Ton doit distinguer ont des noms distincts dans les deux signatures. Finalement comme la signature partagée 2 s est Y intersection des signatures 2A/ et 2 e , et comme les deux morphismes de signatures sont les inclusions correspondantes, la somme amalgamée 2 p est la réunion de 2A/ et 2 e 1.4.3 S o m m e a m a l g a m é e de d e u x spécifications On définit la somme amalgamée de deux spécifications de façon similaire : la signature de la spécification résultat est la somme amalgamée des signatures, et l'ensemble des équations de la spécification résultat est "l'union" (après traduction) des équations des deux spécifications. Soit trois spécifications SPA = (EA,EA) SPB = ( £ B , £ B ) SPc = (Zc,Ec) et deux morphismes de spécifications / : SpA -> SpB g : SPA ->• SpcOn définit la spécification Spp = (2p, Ep) somme amalgamée des spécifications Sps et Spc par rapport aux morphismes de spécifications / et g de la façon suivante. La signature 2 p est la somme amalgamée des signatures : 2 p = push ( 2 j 4 , 2 B , 2 e , / , f f ) . On note & i ( S P ) = &!(£,!, E B , £ c , / , f l f ) ; & 2 (£p) = &2(£U, S B , S e , / , g). 1.4. SOMMES AMALGAMEES 37 Intuitivement, Ep contient les équations de Es et de Ec- Comme les équations de EB et de Ec sont respectivement des équations sur les signatures 2 B et 2 e , on les traduit respectivement par les morphismes de signatures &i(2p) : 2 p —• S p et & 2 (Sp) : S e —> S p . On pose donc EP={(X*,gll('£P)*(t),gtlCSp)*(f)) ; V(X,M')££B} U{(A-#,&2(EF)#(0,&2(Sp)#(O) ; V(X,t,t')tEc}. Remarque 1.3 Les équations présentes dans EA ne jouent pas directement de rôle. En effet, elles sont déjà ''contenues'" dans Es et Ec puisque f et g sont des morphismes de spécifications. Lemme 1.1 Les morphismes de signatures &!(SP):SB->SP & 2 (S P ) : S e -^ S p sont des morphismes de spécifications. Preuve. C'est évident, par définition de Ep. D On pose & I ( 5 > P ) = &L\{SpA,SpB,Spc,f,g) &.2(SpP) = &.2(SpA,SpB.Spc,f,g) = & I ( S . 4 , S B , S C . / , # ) : 5 > B -+ SpP; = & 2 ( S J 4 , 2 B , 2 C , / ^ ) : Spc -> SpP. Théorème 1.3 Le triplet (push {SpAiSpB,Spc, / , g ) , &i(S/M, 5 > B , S p c , / , g ) , &.2(SpA, SpB, Spc, /,g)) est une somme amalgamée dans la catégorie des spécifications Spec. Preuve. On vérifie facilement que la propriété 1.1 est satisfaite. D Exemple 1.8 Pour poursuivre l'exemple 1.7, on fait la somme amalgamée des spécifications M et G par rapport aux morphismes de spécifications b o s : S —» M et mobo s : S -» G. Cela nous donne la spécification P suivante : P = push (5, M,G,bo s,mobo s). Détaillons le contenu de la spécification P. CHAPITRE 1. MOTIVATION 38 property sorts operators P = variables équations PSEUDO_ANNEAU s + , * : s, s ->s 0, 1 : ->s i: s ->s x, y, z : s 1 * X == X X * 1 == X (x * y) * z == x * (y * z) 0 + x == x x + 0 == x (x + y) + z == x + (y + z) x + y == y + x i(x) + x == 0 Nous avons appelé cette spécification PSEUDO JINNEAU car il s'agit d'une spécification des anneaux sans distributivité entre les opérateurs * et +. 1.4.4 S y n t a x e a b s t r a i t e p o u r les c o n s t r u c t i o n s m o d u l a i r e s Nous récapitulons la syntaxe abstraite qui nous permet de représenter des constructions modulaires. Les deux constructions autorisées sont la spécification vide et la somme amalgamée de deux spécifications. En effet, ces deux seules constructions permettent de simuler la construction de toute colimite finie. • La spécification vide ( S 0 , 0 ) est notée 0 . L'unique morphisme de spécifications de 0 vers une spécification quelconque Sp est noté } S p : 0 —> Sp. • Etant donné trois spécifications SpA, Sps, Spc et deux morphismes de spécifications / : SpA -» SPB et g : SpA —> Spc, la somme amalgamée de Sps et Spc par rapport à / et g est donnée par une spécification push (SpA, SpB, Spc, f, g) et deux morphismes de spécifications i&.\{SpA,SpB,Spc,f,g) \&L2{SpA,SpB,Spc,f,g) :SpB -+ push '-Spc -> push (SpA,SpB,Spc,f,g) {SpA,SpB,Spc,f,g)- De plus, étant donné une spécification Spo et deux flèches / ' : SpB —• Spo et g' : Spc —> Spo telles que f o f = g1 og, l'unique morphisme de spécifications u : push (SpA, SpB, Spc, f, g) -> SpD tel que { uob1(A,B,C,f,g) uob2(A,B,C,f,g) = f = g' est notée up (A, B, C, D, f,g, /', g') : push (SpA, SpB, Spc, f,g) -* Spo- 1.4. SOMMES 1.4.5 AMALGAMEES 39 S o m m e disjointe de d e u x spécifications Il est possible de coder la somme disjointe de deux spécifications en utilisant la spécification vide et une somme amalgamée. Soit deux spécifications SpA et SpsLa somme disjointe de SpA et Sps est la somme amalgamée de SpA et Sps par rapport à j S p A et']SpB. SpA + SpB = push (0,SpA,SpB,}SpA,ispB) De plus, les deux injections de 5p,4 vers SpA + SpB et de Sps vers SpA + Sps sont les deux flèches & i ( 0 , SPA, SpB,}sPA,}SpB) &.2{0,SpA,SpB,]sPA,}SpB) :S : PA -> SpA + SpB; SPB - • SpA +SpB. Exemple 1.9 Considérons par exemple la somme disjointe B2 de deux opérateurs binaires. B2 = push{0,B,B.'JB/iB) Cette somme amalgamée correspond à la propriété LPG suivante property sorts Bo = operators DEUX-DPJIN s i , s2 opl : s i - > s l op2 : s2 ->s2 Les deux morphismes de spécifications &.i(B2) : B —» B2 et & 2 (JB 2 ) : B —» B2 sont définis par si; opl; s2; op2. &I(B2)(B) &i(fi 2 )(op) &2(B 2 )(S) & 2 (B 2 )(op) Nous avons deux morphismes de spécifications m» : B —> D et ra+ : B —» D. Ces deux morphismes vérifient l'égalité m* o ]B = m+ o j B car 0 est initial dans la catégorie Spec. Par conséquent, il existe un unique morphisme de spécifications u2 = up ( 0 , B, B, D,\B,\B, mM, m+) : B2 -+ D tel que (u2 o8i\(B2) = m* \u2 o & 2 ( £ 2 ) = m + . Le morphisme de spécifications u2 : B2 —ï D est défini par u2(sï) u2{s2) u2(opl) w2(op2) = s; = s; = *; = +. CHAPITRE 40 1.5 1. MOTIVATION Spécifications modulaires d'anneaux Nous avons vu en section 1.3 un exemple de spécification modulaire des anneaux, en combinant les trois spécifications M, G et D. On peut coder cette combinaison en utilisant deux sommes amalgamées successives. Par exemple, on peut commencer par combiner M et D. puis combiner le résultat avec G. MD = property sorts operators combines property sorts operators A2 = combines MONOIDE-DISTRIBUTIF s +, * : s , s ->s 1 : ->s MONOÏDE [ s , * , 1 ] , DISTRIBUTIVITE[s,+,*] ANNEAU2 s +, * : s , s ->s 0, 1 : ->s i : s ->s MONOIDE-DISTRIBUTIF[s, + , * , 1] , GR0UPE-C0MM[s,+,0,i] La combinaison des spécifications M et D peut être exprimée à l'aide d'une somme amalgamée, en partageant l'opérateur binaire * de M avec l'opérateur * de D. La spécification modulaire MD peut donc être exprimée de la façon suivante : 1.5. SPECIFICATIONS MODULAIRES D'ANNEAUX 41 MD = push {B, M, D, b, m*) On peut remarquer que dans cette expression, il est nécessaire d'avoir exprimé la spécification B pour l'opérateur binaire partagé, alors qu'en LPG, cette spécification partagée reste implicite. En effet, on n'a pas fait référence à OP-BIN dans la spécification MONOIDE-DISTRIBUTIF. On peut ensuite exprimer A2 comme la somme amalgamée de MD et G en partageant l'opérateur binaire + de MD avec l'opérateur binaire + de G. A2 = push (B, MD, G, &L2{MD) o m+,m o b) On peut effectuer ces deux combinaisons successives différemment, en combinant d'abord les spécifications G et D (en partageant l'opérateur +), puis en ajoutant la spécification M (en partageant l'opérateur *). Cela donne la spécification A!2. CHAPITRE 1. MOTIVATION 42 DG = push (B, D, G, ra+, mob) D my/ \&i(DG) B DG mob\^ /IL^DG) G A!2 = push (B, M, DG, b, &! {DG) o mm) &i(-4'2) On peut maintenant se poser la question suivante : Avons-nous bien obtenu une spécification des anneaux? Dans ce cas particulier, on peut s'en convaincre assez facilement, en connaissant une définition indépendante des anneaux. Ici, on va s'intéresser à la question plus facile : Est-ce que les spécifications A2 et A2 sont équivalentes ? Pour répondre à cette question, il est inutile d'avoir une définition indépendante des anneaux. On cherche simplement à savoir si les deux spécifications modulaires sont isomorphes. Ici, il est facile de voir que A2 et Af2 sont bien isomorphes. Intuitivement, les deux constructions sont équivalentes parce que l'opération de somme amalgamée est "associative" (dans un sens qui resterait à définir formellement). En fait, les deux 43 1.5. SPÉCIFICATIONS MODULAIRES D'ANNEAUX constructions A2 et A2 sont un codage par des sommes amalgamées de la colimite du même diagramme S2 suivant. Mais des cas plus complexes peuvent se produire, comme le montre l'exemple suivant. Nous commençons par spécifier un pseudo-anneau, c'est-à-dire un anneau sans la propriété de distributivité. On peut faire cela par exemple avec le terme P . ou avec le terme P'. P = push ( 5 . A/, G, b o 5,77? o b o s) Qx = push (5, 5 , £ , * , * ) Q2 = push(fl,A/,Qi,6,&i(Qi)) P' = push ( f i , Q 2 , G \ & 2 ( Q 2 ) o gL2(Ql),77706) M t \&i(Q2) B MP) Q2 &i(Qi) F mobos / M^) S Q\ / \fci(P') P' CHAPITRE 44 1. MOTIVATION En fait, P et P' sont deux spécifications isomorphes des pseudo-anneaux, qui correspondent à la colimite du diagramme a. a Nous allons maintenant "ajouter la distributivité" à la spécification P. Pour cela, nous considérons le morphisme de spécifications ux = up {0, B. B. P,]B,]B, &i{P) o b, &2(P) o m o b) : B2 - • P Cette flèche existe car comme 0 est initial, &i(P) o bojB = & 2 (P) o m o bo']B. Nous avons vu en exemple 1.9 qu'il existe un morphisme de spécifications u2 = up ( 0 , B, B, D,\B,\B,m«, ra+) : B2-> D On obtient alors une spécification ^3 des anneaux en faisant la somme amalgamée de D et P par rapport à u2 et U\. Cela revient à partager les deux opérateurs binaires de P et D. A$ = push (B2, P, D, ui, u2) 1.5. SPECIFICATIONS MODULAIRES D'ANNEAUX 45 = push (push ( 0 , B, B,]B,]B), P, D, up{0,B,B,P,'iB,'JB,&L1(P)ob,8,2(P)omob), up ( 0 , B, B, D,iB,'}B, m*, m+)) Enfin, voici une dernière spécification modulaire des anneaux, en utilisant la spécification P' des pseudo-anneaux à laquelle on ajoute la propriété de distributivité. A4 = push (push ( 0 , B, B,]B,]B), P', D, up ( 0 , B, 5 , P',\B,]B, &i [P') o & 2 (Q 2 ) o &!(Q!), &i(P,)o&2(Q2)o&2(Q1)), up ( 0 , B, B. D,]B,]B. m,, 777+)) Les deux constructions modulaires d'anneaux As et A4 correspondent aux colimites des diagrammes S3 et S4 ci-dessous. En utilisant la définition de colimite en théorie des catégorie, on peut vérifier que les colimites des diagrammes S\, S2, 63 et S4 sont isomorphes. Cet isomorphisme vient de l'égalité des morphismes de spécifications m+ o s = m* o s. Cette égalité signifie que le fait que les deux opérateurs + et * opèrent sur le même ensemble est contenu dans la spécification D des opérateurs distributifs. Nous verrons dans le chapitre 2 que dans la catégorie de diagrammes diagr(Co), les diagrammes S\, 82, 63 et S4 sont isomorphes. 46 1.6 CHAPITRE 1. MOTIVATION Isomorphisme de construction Nous venons de voir qu'il existe plusieurs manières équivalentes de spécifier des anneaux à partir d'une catégorie de spécifications de base donnée. Dans ce paragraphe, nous examinons quelques équivalences possibles entre deux spécifications. Formellement, deux spécifications sont équivalentes si elles sont isomorphes dans une certaine catégorie de spécifications. Nous présentons les isomorphismes de construction, qui nous semblent présenter un intérêt particulier dans l'étude des spécifications modulaires. Identité. Deux spécifications sont équivalentes si et seulement si celles-ci sont identiques. Il s'agit de la plus faible équivalence possible, qui n'est pas très intéressante. Équivalence structurelle. Deux spécifications sont équivalentes si et seulement si celles-ci ont été construites de la même façon, indépendamment de noms intermédiaires qui ont pu être utilisés pendant la construction. Avec cette approche, on a la possibilité de nommer des spécifications modulaires intermédiaires et de réutiliser ces noms par la suite. Cette équivalence n'est pas beaucoup plus intéressante que l'identité. Isomorphisme dans Spec. Deux spécifications sont isomorphes si et seulement si il existe un isomorphisme entre ces deux spécifications dans la catégorie des spécifications Spec. La difficulté ici est tout d'abord d'exhiber l'isomorphisme entre les deux signatures, et surtout de vérifier qu'il s'agit bien d'un isomorphisme de spécifications. Avec la définition de morphisme de spécifications donnée ici, il faut être capable de savoir si une équation appartient à la fermeture sémantique d'un ensemble d'équations. Ce n'est pas trivial puisqu'il faut pouvoir dire si une équation est satisfaite par une classe d'algèbres spécifiée par un ensemble d'équations. On peut pour cela utiliser un système logique, mais ce système n'est pas forcément complet. De plus, même si l'on dispose d'un système de déduction complet, le problème est, en général, uniquement semi-décidable. Isomorphisme de construction. Dans tout notre travail, les isomorphismes que nous considérons sont des isomorphismes de construction. Deux spécifications sont isomorphes si on peut le prouver en utilisant les propriétés générales des colimites. Il s'agit d'un isomorphisme dans la catégorie librement engendrée par certaines colimites finies sur la catégorie des spécifications de base CQ. L'intérêt de cet isomorphisme réside d'une part dans le fait qu'il n'est pas trop général, parce qu'il reflète la construction de la spécification modulaire; et d'autre part dans le fait qu'il est suffisamment général pour faire abstraction des étapes particulières choisies pour la construction modulaire. Ces isomorphismes de construction ne dépendent pas de la définition effective des spécifications, mais seulement de la manière dont ces spécifications, liées par des morphismes de spécifications, sont combinées. En particulier, une modification ^mineure" dans la catégorie des spécifications de base ne remettra pas en 1.7. CADRE GENERAL 47 cause des isomorphismes de construction. (Par "mineure" on entend ici que la modification ne change pas les égalités entre morphismes de spécifications de base existants). Par contre, si deux spécifications de base sont isomorphes et que cet isomorphisme ne fait pas partie de la catégorie des spécifications de base, alors celles-ci ne seront évidemment pas liées par un isomorphisme de construction. 1.7 Cadre général Les spécifications que nous avons données au cours de ce chapitre sont des spécifications équationnelles. En effet, les seules formules utilisées sont des équations. Il existe évidemment des spécifications plus générales, par exemple des spécifications qui utilisent des clauses de Horn, ou la logique du premier ordre, ou encore les spécifications avec contraintes. Pour formaliser la notion de système logique, J. Goguen et R. Burstall ont proposé les institutions [GB84, GB90]. Ce formalisme permet de parler de façon abstraite des signatures, des formules sur une signature, des modèles sur une signature et de la notion de satisfaction d'une formule par un modèle. L'intérêt des institutions est de fournir des résultats indépendants de la logique sous-jacente choisie. Dans notre travail, nous étudions la composition des spécifications pour former des spécifications plus complexes à l'aide de colimites. Ce problème est identique qu'on se place par exemple dans le cadre des spécifications équationnelles, ou des spécifications avec clauses de Horn. En fait, on peut raisonner indépendamment de la logique sous-jacente en se plaçant dans le cadre général des institutions. La seule propriété que nous exigeons est l'existence de colimites finies dans la catégorie des spécifications. 1.7.1 Institutions Rappelons d'abord la définition d'une institution [GB90]. Définition 1.17 (Institution) Une institution consiste en • une catégorie Sig, dont les objets sont appelés signatures, et les flèches morphismes de signatures; • un foncteur Sen : Sig —y Set qui associe à chaque signature un ensemble de propositions, et à chaque morphisme de signatures une application entre deux ensembles de propositions ; • un foncteur Mod : Sig —> C a t o p qui associe à chaque signature une catégorie de modèles, et à chaque morphisme de signatures un foncteur contravariant ; • pour tout objet E de Sig, une relation \=% entre les objets de Mod(E) et les éléments de Sen(E), appelée relation de satisfaction, telle que pour tout 48 CHAPITRE 1. MOTIVATION morphisme de signatures m : E —• E', tout modèle Mf objet de Afod(E'), et toute équation e de Sen(E), M1 f=E/ 5en(m)(e) ^ A/o E7 l'application m# qui traduit les équations. • Mod associe à toute signature S la catégorie des E-algèbres Alg(E), et à tout morphisme de signatures m : E —> E' le foncteur d'oubli Um : Alg(S') -> Alg(S). Ce foncteur d'oubli permet de considérer toute E'-algèbre comme une Ealgèbre. • Soit une signature E, une E-algèbre A et une équation e sur E, .4 f=£ e «=> l'algèbre A satisfait l'équation e (cf. définition 1.10). La propriété (i) est vérifiée car pour toute algèbre A' de Alg(E'), A1 \=m*{e) & Um{A') \= e (cf. par exemple [GB90, EM90]). Définition 1.18 (Spécification) Une spécification est un couple (E, E) où E est un objet de Sig, et E un sous-ensemble de 5en(E). C'est ce que J. Goguen et R. Burstall appellent une E-présentation [GB90]. Définition 1.19 (Fermeture sémantique d'un ensemble de propositions) Soit une signature E et un ensemble de propositions E Ç Sen(E). La fermeture sémantique E Ç Sen(E) de E est définie par: e G f1 si et seulement si pour tout modèle M de Morf(E), Ve0 G E, M (= s e 0 => M \=z e. On dit que E est fermé si et seulement si E = E. Définition 1.20 (Morphisme de spécifications) Soit deux spécifications (E, E) et ( E 7 , ^ ) . Un morphisme de spécifications de (E, E) vers (E', E') est un morphisme de signatures m : E —> E', tel que VeeE, Sen(m){e)eËJ. 1.7. CADRE GENERAL 49 Les spécifications, avec les morphismes de spécifications, forment une catégorie, notée Spec. Notre but est de composer les spécifications par des constructions de colimites. Nous devons donc travailler dans une catégorie pour laquelle tout diagramme fini a une colimite, c'est-à-dire dans une catégorie finiment cocomplète. J. Goguen et R. Burstall ont montré qu'il suffit que la catégorie des signatures ait des colimites pour que la catégorie des spécifications associée ait des colimites. Théorème 1.4 ([GB90]) La catégorie Spec est finiment cocomplète si et seulement si la catégorie associée de signatures Sig est finiment cocomplète. Remarque 1.4 J. Goguen et R. Burstall ont montré ce résultat pour les théories, c'est-à-dire les spécifications (E, E) telles que E est fermé. On vérifie facilement qu'on peut adapter leur démonstration dans le cas des spécifications. Cela permet de déduire que la catégorie des spécifications algébriques équationnelles, la catégorie des spécifications du premier ordre ... etc. sont finiment cocomplètes. 1.7.2 T e r m i n o l o g i e et h y p o t h è s e s Hypothèses • Nous nous plaçons dans une institution, dans laquelle la catégorie des signatures Sig est finiment cocomplète. Cela implique que la catégorie des spécifications associée Spec est finiment cocomplète. • On considère une sous-catégorie finie Co de Spec. Terminologie Rappelons brièvement la terminologie employée. Spécification et morphisme de spécifications. Une spécification et un morphisme de spécifications sont respectivement un objet et une flèche de la catégorie Spec. Spécification de base et morphisme de spécifications de base. On fixe une sous-catégorie finie Co de Spec. Les objets de Co sont appelés spécifications de base, et les flèches de Co morphismes de spécifications de base. Intuitivement, cette catégorie représente l'ensemble des spécifications et morphismes de spécifications "déclarés" par l'utilisateur, qui forment une bibliothèque de spécifications réutilisables. Spécification modulaire et morphisme de spécifications modulaires. Une spécification modulaire est soit une spécification de base soit une spécification construite à partir d'autres spécifications modulaires par certaines constructions de colimites. Les morphismes de spécifications modulaires sont des morphismes de spécifications également obtenus par des constructions de colimites. 50 CHAPITRE 1. MOTIVATION Angles d'études Nous nous intéressons à la composition des spécifications de base sous différents angles : Syntaxe. Peut-on définir une syntaxe, c'est-à-dire un langage pour décrire des constructions modulaires ? Dans le chapitre 3 nous proposons la construction d'une catégorie Terme (Co). Cette catégorie permet de représenter la construction des spécifications modulaires à partir de spécifications de base en utilisant uniquement la spécification vide et des sommes amalgamées. Ce chapitre permet de justifier formellement la syntaxe abstraite utilisée dans l'exemple des anneaux. Interprétation. Quel est le résultat de plusieurs constructions modulaires successives? Nous montrons dans le chapitre 4 que des constructions successives de sommes amalgamées peuvent être vue comme le calcul d'une seule colimite. Nous montrons comment calculer le diagramme associé à un terme qui représente une spécification modulaire. Dans ce chapitre, une spécification modulaire est vue de façon plus abstraite comme la colimite d'un diagramme sur CoCalcul. Peut-on détecter des isomorphismes de construction ? Nous résolvons ce problème uniquement dans lé cas simple où la catégorie Co est finie et ne comporte pas de cycle. Nous proposons un algorithme qui permet, par exemple, de déduire que les spécifications A\, A2, A3 et A4 des anneaux que nous avons présentées dans ce chapitre sont équivalentes. Cet algorithme est présenté dans le chapitre 5. Chapitre 2 Graphes, catégories et diagrammes Le but de ce chapitre est de présenter les bases formelles de notre travail, en particulier les concepts de diagramme et de morphisme de diagrammes, issus de la théorie des catégories. Pour cela nous avons besoin de quelques notions sur les graphes, présentées en section 2.1. Nous introduisons la définition des morphismes généralisés de graphes. En section 2.2, nous faisons quelques rappels de théorie des catégories. La plupart des résultats sont tirés de [McL71] ou [MB70]. Sur ce sujet, il est également intéressant de consulter [BW90] qui introduit les concepts de base de façon assez claire et élémentaire. En section 2.3, nous présentons les notions de diagramme et de morphisme de diagrammes. La définition de morphisme de diagrammes que nous utilisons, bien qu'elle ne soit pas nouvelle, est plus générale que celles présentées classiquement dans la littérature informatique (cf. par exemple [TBG91]). Nous avons en effet besoin d'une définition suffisamment générale pour "refléter" le maximum de flèches entre colimites de diagrammes par des morphismes entre les diagrammes correspondants. Nous nous basons ensuite sur cette définition pour reformuler les notions classiques de cône sur un diagramme et de colimite d'un diagramme. Nous présentons deux catégories de diagrammes: DIAGR(C) et diagr(C). La catégorie DIAGR(C), qui est une généralisation de catégories de diagrammes utilisées en informatique, permet, de façon pratique, de manipuler les morphismes de diagrammes. La catégorie diagr(C), obtenue comme un quotient de DIAGR(C) par une relation de congruence sur les flèches de DIAGR(C), possède deux propriétés théoriques importantes. D'une part, diagr(C) est une catégorie finiment cocomplète (théorème 2.6). De plus, diagr(C) est une complétion de la catégorie C par colimites finies (théorème 2.7). 2.1 Graphes Définition 2.1 (Graphe) Un graphe a® est un ensemble de nœuds Nœud(a^), un ensemble d'arcs Avc(a^), et deux fonctions Source, But : Arc(o^) —» Nœud(a^). Si a est un arc de source m et de but n, on note a : m —> n. 51 52 CHAPITRE 2. GRAPHES, CATEGORIES ET DIAGRAMMES Un graphe est fini lorsque l'ensemble des nœuds et l'ensemble des arcs sont finis. Définition 2.2 (Morphisme de graphes) Soit deux graphes a® et /?*. Un morphisme de graphes a® de or* vers /?*, noté a® : a* -> /?*, est une application qui à tout nœud n de a^ associe un nœud c®(n) de /?* et à tout arc a : m —> n de a* associe un arc c^(a) : 0"*(m) —• 0"*(w) de ^8*. Composition des morphismes de graphes. Soit trois graphes a*, /?*, 7*, et deux morphismes de graphes a* : a* —>• /?* et r * : /3* —>- 7*. La composition de a* et r ^ est le morphisme r® o a® : a* —> 7^ qui associe à tout nœud n de a^ le nœud r®((T®(n)) de 7*, et à tout arc a : m —y n de a* associe l'arc r*(<7*(a)) : 7-^((7^(777)) -» r*(a*(n)). En résumé, r ^ o a® est défini de la façon suivante. r$o^ : a* 77 a:m->n -+ 7* »-» r*(<7*(n)) H-> r*(a*(a)) : r*(a*(m)) - • r*(a*(n)) Définition 2.3 (Zigzag sur un graphe) Soit un graphe a*. Un zigzag Z sur a* est un triplet (fc,Z,v,Z^) où • À; est un entier naturel, appelé longueur du zigzag Z ; • Z/v est un (A: + l)-uplet (n 0 , T?I, . . . , n^) de nœuds de Û^ ; • Z\ est un fc-uplet (ao,a\,.. ,,ak-i) d'arcs de Q*, tel que pour tout entier naturel / tel que 0 < i < k — 1. at est soit un arc de source n,- et de but n,+i, soit un arc de source 71,+1 et de but 77.;. On appelle 770 la source du zigzag Z, et nk son 6uf. On note Z : 770 ~-> 77/,.. Pour tout nœud 7?. de a*, on a un zigzag nul de longueur nulle noté 0 n : n ~-ï n. Par la suite, pour plus de lisibilité, un zigzag Z : TZO ~-> n* sera représenté de la façon suivante : Z = 77o ao > n\ ai < 772 < a-2 7?3 • ' • 7ÏJfc_i a/e-i > 77fc. On choisit une orientation arbitraire pour la représentation de chaque arc a t . Etant donné un graphe Q $ , on a un graphe Zigzag(a^), dont les nœuds sont les nœuds de a*, et les arcs les zigzags de a*. À tout zigzag Z : 770 ^-> nk Z = 77 0 ao > 77i < ai 77 2 i a2 77 3 • • • 7 7 ^ - 1 a/c-i > Tlfc, on peut associer un zigzag opposé Z : n* ^-)- no ~ry Z <*k-i = Uk < a2 77jt-l - - - 7 7 3 ai > ^2 a0 • 77l « 77Q 2.2. CATEGORIES, FONCTEURS ... 53 obtenu en "parcourant le zigzag dans l'autre sens". Plus formellement, on définit l'opposé d'un zigzag de la façon suivante. Définition 2.4 (Zigzag opposé) Soit un zigzag Z = {k,Z^,ZA) sur un graphe a*, avec Zjv = {no, ni,.. .,nk) et ZA = {p>v,a>\, • - .,a*:-i)- L'opposé du zigzag Z : no ~-> nk est le zigzag Z : nk ~ - • 770 = (k, Z'N, Z'A) où • Z'N = {nk,nk-i,...,n0) ; • ZA ~ (ûfc-i,---,ao)Définition 2.5 (Morphisme généralisé de graphes) Soit deux graphes oft et /3 $ . Un morphisme généralisé de graphes a® : Q $ *<*-> /3* entre les graphes Û $ et /3* est un morphisme de graphes entre a* et Zigzag(/3*). Le morphisme généralisé de graphes a® associe donc à tout nœud n de a® un nœud (T*(n) de /3^, et à tout arc a : m —» 77 de a® un zigzag 0"*(a) : a* (m) ^—» 0^(7?) du graphe /3®. Tout morphisme de graphes est donc un morphisme généralisé, puisqu'un arc est un cas particulier de zigzag. Un morphisme généralisé associe donc à tout arc un zigzag, en conservant les sources et les buts. On peut étendre la définition d'un morphisme généralisé de graphes a® : Û $ ~-> /3* en associant à tout zigzag un zigzag. Il suffit pour cela de "mettre les zigzags bout à bout". Étant donné un zigzag Z : n0 ~-> nk a0 Z ai a-k-i = n0 <— 77i —> n2 • • • 77fc_i —> nk, on définit le zigzag a*(Z) : &®{nk) par: a (Z) = 7*. Le morphisme généralisé r^ o a* est défini de la façon suivante. r^ o a® : Û$ —> 77 h+ r*( r*(a*(a)) : r * ( a * ( m ) ) ^ r * ( < r * ( n ) ) a : m _ > n 2.2 7^ Catégories, foncteurs ... Dans cette partie, nous rappelons les définitions de catégorie, foncteur, transformation naturelle et adjonction. Ces définitions sont tirées de [McL71, MB70, BW90]. 54 CHAPITRE 2.2.1 2. GRAPHES, CATEGORIES ET DIAGRAMMES Catégories Définition 2.6 (Catégorie) Une catégorie C est définie de la façon suivante. • On a une classe d'objets, notés A, B, C ... • Pour chaque couple d'objets (A, B), on a un ensemble home {A, B) de flèches, noté plus simplement hom(A,B) s'il n'y pas d'ambiguïté sur la catégorie. / G hom{A, B) est noté / : A-^ B. A est appelé domaine de / , et B est appelé codomaine de / . • Pour chaque triplet d'objets (A, B,C), on a une opération de composition o : hom(B,C) x hom(A,B) {9,f) -> ^ hom(A,C) go J • Pour tout objet B, on a une flèche idB : B -> B. • Pour tout objet B, la flèche idB est une identité: V/ : A -> B, V# : B -> C, idB o f = f et go idB = g. • La composition est associative : V/ : .4 -> B, \fg : B -> C, V/* : C -> D, h o {g o f) = (ho g) o f. Exemples de catégories • La catégorie des ensembles, notée Set, dont les objets sont les ensembles, et les flèches sont les applications entre deux ensembles. • La catégorie des signatures, notée Sig, dont les objets sont les signatures, et les flèches sont les morphismes de signatures. • La catégorie des spécifications, notée Spec, dont les objets sont les spécifications algébriques, et les flèches sont les morphismes de spécifications. • La catégorie des graphes, notée Graph, dont les objets sont les graphes, et les flèches sont les morphismes de graphes. Définition 2.7 (Isomorphisme) Soit une catégorie C et / : A —• B une flèche de C. On dit que / : A —> B est un isomorphisme si et seulement si il existe une flèche g : B —• A de C telle que g o f = id^ et / o g = idB. Si / est un isomorphisme, la flèche g est alors unique, et est notée f"1. On dit alors que / et f"1 sont inverses et que les objets A et B sont isomorphes. On note A = B. Définition 2.8 (Petite catégorie) Lorsque la classe d'objets d'une catégorie C est un ensemble, on dit que C est une petite catégorie. Par exemple, les catégories Set, Sig, Spec et Graph ne sont pas des petites catégories. 2.2. CATEGORIES, FONCTEURS ... 55 Remarque 2.1 • Toute petite catégorie est un graphe. • Réciproquement, on peut associer à tout graphe a® la catégorie librement engendrée sur ce graphe. Cette catégorie a pour objets les nœuds du graphe a*, et pour flèches les chaînes d'arcs composables de a^, où deux arcs a et a! sont composables si et seulement si But (a) = Source(a'). La composition est définie comme la concaténation des chaînes : (6162 • ••&/) ° («1^2 • • -ûjt) = [a\a2 .. .akbib2 .. .6/). Les flèches identités sur un objet 77 sont les chaînes de longueur nulle de source et but 77, notées en. 2.2.2 Foncteurs Un foncteur est l'équivalent d'un morphisme de graphes pour les catégories. Définition 2.9 (Foncteur) Soit C et P deux catégories. Un foncteur F de C vers P , noté F : C —» P , est une application qui à tout objet .4 de C associe un objet F(A) de P , et à toute flèche / : A - • B de C associe une flèche F{f) : F{A) -» F{B) de P , et telle que • pour tout objet A de C, F(idA) = 'C?F(,4) ; • pour toutes flèches / : A -> B et g : B -> C de C, F{g o f) = F {g) o F{f). Etant donné une catégorie C, il y a foncteur identité Idc : C —> C, qui est l'identité sur les objets et sur les flèches. Soit trois catégories C, P et S, et deux foncteurs F :C —> V et G :V -> £. On définit la composition de F et G de façon évidente: GoF : C A f : A ^ B -+ £ ^ G(F{A)) ^ G(F(f)): G(F(A))-> G(F(B)) Catégorie Cat La classe des petites catégories, avec les foncteurs, forme une catégorie Cat. Catégorie CAT Par la suite, nous aurons besoin d'une catégorie qui contient non seulement des petites catégories mais également des catégories comme Set ou Spec qui ne sont pas petites. Nous considérons pour cela la catégorie CAT des "grandes catégories", qui contient les petites catégories, ainsi que les autres catégories qui nous intéressent. Pour des problèmes de fondations, de même qu'on ne peut pas considérer l'ensemble de tous les ensembles, CAT n'est pas la catégorie de toutes les catégories. En particulier CAT n'est pas un objet de CAT. Pour plus de détails, on peut consulter [McL71] pages 21-24. Propriété 2.1 Soit un foncteur F : C —» P . L'image par F d'un isomorphisme de C est un isomorphisme de P . CHAPITRE 2. GRAPHES, CATÉGORIES ET DIAGRAMMES 56 Preuve. Soit un foncteur F : C -> V, et / : A -> B un isomorphisme de C. F{f) : F{A) ->• F ( 5 ) est un isomorphisme, et F ( / ) _ 1 = F ( / _ 1 ) : F ( 5 ) -> F ( 4 ) . En effet, = = = De même, F{f'1) F(/ o /_1) F{idB) id F(B) ( F est un foncteur) (définition de / - 1 ) ( F est un foncteur) o F{f) = idF{A), et donc F(f) est un isomorphisme. D Définition 2.10 (Endofoncteur) Un foncteur F : C -> C est appelé endofoncteur. Si F est un endofoncteur, on pose F°=Jdc; F1 = F o F 1 " 1 , V?: > 1. Définition 2.11 (Foncteur plein) Soit deux catégories C et P , et un foncteur F : C -» p . On dit que F est />/em si pour tout couple d'objets (A,B) de C, et pour toute flèche g : F{A) -> F(fî) de P , il existe une flèche f : A-> B de C telle que Q = F(f). Intuitivement, entre deux objets de P images par F d'objets de C, il n'y a pas de flèches autres que les images par F de flèches de C. F est, d'une certaine façon, "surjectif sur les flèches". Définition 2.12 (Foncteur fidèle) Soit deux catégories C et P , et un foncteur F : C -> p . On dit que F est fidèle si pour tout couple d'objets (AJ3) de C, et pour tout couple de flèches /, / ' : A -> B. on a F ( / ) = F ( / ' ) => / = / ' . Autrement dit, F est fidèle si F est injectif sur les flèches. 2.2.3 Transformations naturelles Définition 2.13 (Transformation naturelle) Soit deux catégories C et P . Soit deux foncteurs F, G :C -> P. Une transformation naturelle a de F vers G, notée a : F -^ G, est une application qui à tout objet A de C associe une flèche aA : F (A) -> G(A) de P , telle que pour toute flèche / : A -» B de C, G(f)ocrA = F(A) aBoF(f). °A G(A) G(f) F(f) f B F(B) -ÔW-G(B) 2.2. CATÉGORIES, FONCTEURS 57 ... Catégorie des foncteurs de C vers P Soit trois foncteurs F, G, H : C -> P , et deux transformations naturelles a : F -^ G et r : G -1» # . La composition de a et r est la transformation naturelle r-a : F -^ H telle que pour tout objet A de C, (r • a)A = rAoaA Cela définit bien une transformation naturelle. En effet, H(f)o(r-a)A = H(f)orAoaA = TB o G(f) o aA = TB OCTB O F(f) = (r • (T)B° F(f) A f F(A) (définition de r • a) (T transformation naturelle) (cr transformation naturelle) (définition de r • a) °A • G {A) F(B) °B G(B) • //(-4) H(f) G(f) F(/) B TA TB H(B) Remarque 2.2 Cette composition des transformations naturelles est souvent appelée composition verticale, par opposition à la composition horizontale dont nous n'avons pas rappelé la définition ici. Soit un foncteur F : C ->- P . On a une transformation naturelle identité, notée jdF : f -i> F, qui associe à tout objet A de C la flèche idF(A). On vérifie facilement que pour tous foncteurs F,G :C -*V, et toute transformation naturelle a : F -^ G, on a a • idp = (7 ; id G - a = a. On vérifie facilement que la composition des transformations naturelles est associative, donc on a une catégorie, notée Ve, dont les objets sont les foncteurs de C vers P , et les flèches sont les transformations naturelles. Définition 2.14 (Isomorphisme naturel) Soit deux catégories C et P . Soit deux foncteurs F,G : C -> P . Un isomorphisme a : F ^ G de la catégorie Ve est appelé isomorphisme naturel. Si a : F -4 G est un isomorphisme naturel, on dit que les foncteurs F et G sont naturellement isomorphes, et on note F = G. 58 CHAPITRE 2. GRAPHES, CATÉGORIES ET DIAGRAMMES Propriété 2.2 Soit deux catégories C et P . Soit deux foncteurs F, G : C —>V. Une transformation naturelle a : F -^ G est un isomorphisme naturel si et seulement si pour tout objet A de C, aA : F(A) -> G(A) est un isomorphisme. De plus, a"1 : G -^ F est la transformation naturelle qui associe à tout objet A de C la flèche a~l : G{A) -> F {A) de P . Preuve. relle. Notons rA = o~^. On vérifie d'abord que r est une transformation natuG(f) o aA = CTB O F(f) => (TQ1 oG(f) = F(f) o a^1 => TB O G(/) = F ( / ) o rA (a transformation naturelle) (crA et as isomorphismes) (définition de rA et TB) donc r : G -^ F est une transformation naturelle. Montrons maintenant que a et r sont inverses. Pour tout objet A de C, (a - T ) A — aA o rA = aA o G~ = idG(A) donc a -r — idc- De même, on montre que r • a = idp. Par conséquent, a~l = r. • Considérons quatre catégories B, C, P et £ : et quatre foncteurs A" : B —> C, F.G : C —> P , et H : P —> S. Considérons une transformation naturelle a : F -^ G. On a une transformation naturelle HaiHoF-^ HoG telle que pour tout objet A de C, (Ha)A = H{aA) : H(F(A)) -> H(G(A)) (fl èch e de £) Cela définit bien une transformation naturelle. Soit une flèche / : A —> B de C. G(f) o aA = OB o F(f) =• H(G(f)oaA) = H(aBoF(f)) => H{G(f))oH(GoK telle que pour tout objet A de B, {aK)A = aK(A) : F{K(A)) -+ G(K(A)) (flèche de V) Cela définit bien une transformation naturelle. En effet, soit une flèche / : A —• B deB. G(K(f)) o OK(A) = CTK(B) ° F(K(f)) =» (G o K)(f) o {oK)A = (oK)B O ( F O K)(f) ia transformation naturelle) (définition de aK) 2.2. CATEGORIES, FONCTEURS ... 59 Propriété 2.3 Soit quatre catégories B, C, V et £ ; et quatre foncteurs K : B —» C, F,G:C->V, et H : P -> £. Supposons F^G. Alors, 1. HoF^HoG; 2. FoK^GoK. Preuve. Soit a : F -^> G l'isomorphisme naturel entre F et G. 1. Pour tout objet A de C, aA est un isomorphisme, donc, d'après la propriété 2.1, H(aA) = (Ha)A est un isomorphisme. Par conséquent, d'après la propriété 2.2, Ha : H o F -^ H o G est un isomorphisme naturel, et donc H o F = H o G. 2. Pour tout objet A de B, (JK(A) = {(JK)A est un isomorphisme. Par conséquent, aK : F o K -^ G o K est un isomorphisme naturel, et donc F o K = G o K. 2.2.4 Adjonctions Un des concepts les plus importants de la théorie des catégories est l'adjonction. Par exemple les constructions libres (comme les constructions d'algèbres libres, de groupes libres ou de monoides libres) sont caractérisées par des adjonctions. Définition 2.15 (Adjonction) Soit deux catégories C et P . Soit deux foncteurs F : C —> P et G : P —¥ C. Les foncteurs F et G forment une adjonction notée ( F H G) si et seulement si il existe une transformation naturelle r/ : Idc -^ G o F telle que pour tout objet A de C, pour tout objet B de P , et pour toute flèche / : A —> G(B) de C, il existe une unique flèche g : F (A) —> B de P telle que G(g) o r]A = f. A VA G(F(A)) F(A) G(g) G(B) La transformation naturelle r/ (F-iG). Idc -1* G o F est appelée unité de l'adjonction Théorème 2.1 Soit deux catégories C et V, et deux foncteurs F : C —» P et G : P —> C. Alors, ( F H G) est une adjonction si et seulement si il existe une transformation naturelle e : FoG -^ Idj) telle que pour tout objet BdeV, pour tout CHAPITRE 2. GRAPHES, CATÉGORIES ET DIAGRAMMES 60 objet A de C et pour toute flèche g : F(A) -+ B de P , il existe une unique flèche f:A-> G{B) de C telle que eB o F(f) = g. B • €B F(G(B)) G(B) F(f) f F(A) La transformation naturelle e : F o G -^ Idv est appelée coûnité de l'adjonction (F-tG). Preuve. On peut trouver une preuve de ce théorème dans [BW90], page 275. D Propriété 2.4 Soit une adjonction {F -\ G), ayant pour unité la transformation naturelle 77 : Idc -^ G o F et pour coûnité la transformation naturelle e : FoG -^ Wp. Alors, on a les égalités suivantes entre transformations naturelles: 1. Ge • 77G = idc : 2. eF - Fr]= idF. Preuve. On peut trouver une preuve de cette propriété dans [McL71], page 80. • Exemple 2.1 (Adjonction entre la catégorie Graph et la catégorie Cat) À toute petite catégorie C. on peut associer un graphe U{C), dont les nœuds sont les objets de C, et les arcs les flèches de C. Réciproquement, à tout graphe a*, on peut associer la catégorie F (a*) librement engendrée sur le graphe a* (cf. remarque 2.1). F et U sont en fait des foncteurs F : Graph -> Cat U : Cat -> Graph qui forment une adjonction ( F H U). En effet, pour toute catégorie C, pour tout graphe Û $ , pour tout morphisme de graphes m : a® -* U(C), il existe une unique extension de m en un foncteur M : F(a®) -» C. Par abus de notation, dans toute la suite la catégorie librement engendrée sur un graphe a $ sera également notée a®. 2.3. DIAGRAMMES 2.3 (tt Diagrammes Dans cette section, nous définissons les diagrammes sur une catégorie de base C. Intuitivement, un diagramme décrit un assemblage d'objets de C à l'aide de flèches de C. Nous rappelons la définition de la colimite d'un diagramme, qui peut être vue intuitivement comme le résultat de l'assemblage décrit par le diagramme. Nous avons besoin de définir non seulement des diagrammes sur C, mais également des morphismes de diagrammes, afin d'obtenir une catégorie de diagrammes. En effet, l'idée principale de notre travail est d'associer à toute spécification un diagramme, et à tout morphisme de spécifications un morphisme de diagrammes. Dans cette section, nous commençons par définir la catégorie DIAGR(C), qui a pour objets les diagrammes et pour flèches les morphismes de diagrammes. Notre définition de morphisme de diagrammes, basée sur les notions de zigzag SUT un graphe et de morphisme généralisé de graphe est plus générale que celle par exemple donnée dans [TBG91]. Puis, nous reformulons la définition de cône et de cône colimite. Nous définissons ensuite une congruence « sur les flèches de DIAGR(C) et la catégorie diagr(C) est le quotient de DIAGR(Co) par cette relation. La catégorie diagr(Co) a pour objets les objets de DIAGR(C), et pour flèches les classes d'équivalence modulo ^ de flèches de DIAGR(C). Nous montrons que la catégorie diagr(C) est finiment cocomplète et que le calcul d'une colimite consiste à aplatir un diagramme de diagrammes dans la catégorie DIAGR(C). Nous montrons enfin que diagr(C) est une complétion de C par colimites finies. 2.3.1 C a t é g o r i e d e s d i a g r a m m e s DIAGR(C) Un diagramme Q sur une catégorie C est un graphe Q $ , dont les nœuds n sont étiquetés par des objets a(n) de C, et les arcs a : n —» n1 sont étiquetés par des flèches a(a) : a(n) —> a(nf) de C. De manière équivalente : Définition 2.16 (Diagramme) Un diagramme sur une catégorie C est un couple Q = (a*, a : a * - » C ) , avec: • Û^ est une catégorie librement engendrée sur un graphe (ce graphe est également noté a®) ; • a : a® —ï C est un foncteur. Le graphe a $ est appelé graphe sous-jacent du diagramme ô. Un diagramme a est fini si et seulement si son graphe sous-jacent a* est fini. 62 CHAPITRE 2. GRAPHES, CATEGORIES ET DIAGRAMMES Remarque 2.3 1. S. Mac Lane [McL71] définit un diagramme comme un foncteur F : J —> C, où J est une catégorie quelconque ("habituellement petite et souvent finie"). Notre définition est donc moins générale, dans la mesure où nous imposons que la catégorie a* soit librement engendrée sur un graphe, donc petite. De plus la catégorie J peut contenir des égalités entre certaines flèches, ce qui n'est pas le cas pour une catégorie librement engendrée sur un graphe. 2. M. Barr et C. Wells [BW90] définissent un diagramme comme un morphisme de graphes entre le graphe a® et le graphe sous-jacent de la catégorie C. Leur définition est donc un peu moins générale que celle que nous utilisons, puisqu'ils imposent que la catégorie C soit petite. 3. Lorsque le graphe Q $ est fini, cela n'implique pas forcément que la catégorie a® soit finie. En effet, si le graphe comporte une ou plusieurs boucles, c'est-à-dire des arcs qui ont mêmes source et but, alors la catégorie librement engendrée sur Û $ comporte un nombre infini de flèches. La définition de diagramme fini donnée par S. Mac Lane, qui consiste à considérer un foncteur a : a® —» C où la catégorie a® est finie, exclut donc les diagrammes dont le graphe sous-jacent comporte des boucles. 4. Nous définissons un diagramme à partir d'un graphe parce que nous pensons que cette définition est plus proche de l'informatique : on a au départ, de façon effective, un graphe, et le fait de considérer la catégorie engendrée par ce graphe doit être vu comme un simple outil de formalisation. 5. Pour définir un foncteur a• : Û $ —> C où a® est une catégorie librement engendrée sur un graphe, il suffit de définir a sur les nœuds et les arcs du graphe a*. Comme les flèches de la catégorie a® sont les chaînes d'arcs composables sur le graphe a^, il suffit de poser a{en) = idQ(n) a ( a i a 2 .. .an) = a{an) ° • --00-(02) o a(ai) pour terminer la définition du foncteur a : a® —» C. 6. Lorsque nous définissons un diagramme â, nous ne tenons pas compte des noms des nœuds et des arcs du graphe sous-jacent a*. Autrement dit, le graphe a® est considéré à un isomorphisme près. Plus précisément, soit deux diagrammes Q = (a*, a : a* -* C) et 0 = (/?*, j3 : 0* -> C). Si on a un isomorphisme de graphes a* : a* —» (3* (qui correspond à un foncteur entre les catégories Q * et (3*) tel que a = /3 o a® (Vue Vn G Nœud( Nœud(a<1>), o(n) = /î(<7*(n)) \ Va :n -* n ; e A r c ( a * ) , a{a) = (3{a*{a)) alors, nous considérons que les diagrammes a et /3 sont égaux. 2.3. DIAGRAMMES 63 Nous donnons maintenant quelques exemples de diagrammes sur une catégorie C. Exemple 2.2 (Diagramme Ic{A)) Soit 1* le graphe comportant un seul nœud, appelé *, et aucun arc. Soit A un objet de C. On a un foncteur l£ : 1* —> C défini par Ic(*) = A. On peut donc définir un diagramme fc(-4) = (1*, Ié:l*-*C). © CD graphe 1* diagramme le (A) Exemple 2.3 (Diagramme de somme) Soit 2* le graphe comportant deux nœuds, et aucun arc. Soit A et B deux objets de C. On a un foncteur a : 2* —• C, qui associe l'un des nœuds à .4 et l'autre des nœuds à B. On a donc un diagramme de somme de A et B â=(2*, a:2*->C). CED A graphe 2* diagramme a B Exemple 2.4 (Diagramme de coégalisateur) Soit K® le graphe contenant deux nœuds 0 et 1, et deux arcs a et b de source 0 et de but 1. Si A et B sont deux objets de C, et f, g : A —» B deux flèches de C, on a diagramme de coégalisateur n = (K*, K : K® —» C) défini par K(0) = .4 K(1) = B n{a) = / K(fc) =g. •: 0 :• 1 graphe K^ •: B diagramme K 64 CHAPITRE 2. GRAPHES, CATEGORIES ET DIAGRAMMES Exemple 2.5 (Diagramme de somme amalgamée) Considérons le graphe 7T*, appelé "graphe de somme amalgamée", qui comporte trois nœuds 0, 1 et 2, et deux arcs a : 0 ->• 1 et b : 0 -» 2. Si A, B, C sont des objets de C et f : A —> B, g : A -» C des flèches de C, on a un diagramme de somme amalgamée W = (7T*, 7T : 7T* - • C) 2 J B défini par TT(0) = ;4 TT(1) = fl TT(2)=C 7r(a) = / TT(6) =g. 1 a 0 b graphe 7r* \ f A 9 C diagramme 7r Morphismes de diagrammes Nous venons de définir les diagrammes finis. Pour obtenir une structure de catégorie, nous devons ajouter des flèches entre les diagrammes. Intuitivement, une flèche entre deux diagrammes a et (3 sur C est un ensemble de flèches de C, une par nœud de a**, qui ont certaines propriétés de commutation. Différentes catégories de diagrammes ont été présentées dans la littérature. Par exemple, S. Mac Lane définit une catégorie de diagrammes, qu'il appelle '"supercomma catégorie" ([McL71], exercice 5.(b), page 111). A. Tarlecki et al. ont défini une catégorie Funct(C) [TBG91], qui peut être obtenue à partir de la "super-comma catégorie" de S. Mac Lane en dualisant. Dans cette catégorie, une flèche entre deux diagrammes â = {a*, a: a* -> C) et /? = (/?*, /3 : /3* -> C) est un couple a : a -* (3 = (a* : a* -» (3* ; a : a -^ (3 o C et (3o(j* :a* ->C. 2.3. 65 DIAGRAMMES Ces catégories de diagrammes ne sont pas suffisamment générales pour notre propos, car elles ne comportent pas assez de flèches. Intuitivement, et en anticipant un peu sur la suite, nous souhaitons avoir une flèche entre deux diagrammes chaque fois qu'il existe une flèche entre les colimites des deux diagrammes. Avec la définition ci-dessus, certaines flèches entre colimites de diagrammes ne correspondent à aucune flèche entre les deux diagrammes. Exemple 2.6 Reprenons l'exemple des anneaux du chapitreJ^. Nous avons un morphisme de diagrammes du diagramme â vers le diagramme 52 qui correspond à un morphisme de spécifications de Colimâ vers Colim S2 : up (S, M, G, A2,bos,mobo s, 8n{A2) o ^ {MD),b2(A2)). Mais il n'y a pas de morphisme de diagrammes de a vers S2 avec la définition cidessus. /3 . Rappelons qu'un morphisme généralisé de graphes associe à tout nœud de a* un nœud de /3*, et à tout arc de a® un zigzag de /3*, c'est-à-dire une séquence linéaire d'arcs de /3* (définition 2.5). De même, au lieu de considérer une transformation naturelle a : a -^ (3 o a*, nous devons considérer une transformation naturelle généralisée a : a ~^> (3 oa . Exemple 2.6 (Suite) Avec cette définition, nous pouvons définir une flèche a : S% et une a -_> S2, qui consiste en un morphisme généralisé de graphes a a* transformation naturelle généralisée a : a ~^> 82 o a . Le morphisme généralisé de graphes a® peut être défini par exemple de la 66 CHAPITRE 2. GRAPHES, CATÉGORIES ET DIAGRAMMES façon suivante : a* : a* —> <5| 0 -> 0' 1 •-»> 1 ' 2 h-> 2' a • La transformation naturelle généralisée a : a ^^> S2 o a® est définie par : (jQ = mM o s = ra+ o s ai = id\j a2 = idcDéfinition 2.17 (Relation de connexion entre deux flèches) Soit un diagramme S = (£*, £:<$*-> C), et deux nœuds n 0 et nfc de Nœud(£*). Soit u : A ->• <5(n0) et i; : .4 -» £(rcfc) deux flèches de C. On dit que les flèches u et v sont connectées par le diagramme S (figure 2.1) si et seulement si il existe un zigzag Z = n0 —> nx i— n2 i— n2 - - - ^ - 1 —> nk sur £*, et un ensemble de flèches de C {d :A->6{ni) ; i G {0 k}}, tels que: • w = co ; • u = c/, : • ViG { 0 , . . . , f c - 1 } : £(az) oct- = Cî+i, si a; est orienté de n% vers n J + i ; S(a{) oc,-+i = c,, si a{ est orienté de n î + i vers n,-. On note i/ ~ j i; ; ou w ~ j u [Z], si l'on souhaite préciser le zigzag Z. Définition 2.18 (Catégorie des diagrammes finis DIAGR(C)) Soit une catégorie C. • Un objet S de DIAGR(C) est un diagramme fini sur C. . Soit deux diagrammes â = (a*, o• : a* -+ C) et J = (/3*, /3 : /3* -> C). Une /ïec/ie r : â -» /3 de DIAGR(C), ou morphisme de diagrammes, est un couple r : â -> /3 = (r* : a* - ^ /3*, r : a ~^> /3 o r * ) , avec: - r * : o?^ ~-> /3* est un morphisme généralisé de graphes. 2.3. 67 DIAGRAMMES FlG. 2.1 - : u ~ j v [Z : n0 ~-+ n4] - r : a ^* / j o r $ est une '"transformation naturelle généralisée", c'est-àdire un ensemble de flèches rn : a{n) -> J(r*(n)). Vr? G Nœud(a*) telles que Va : m -> n G Arc(a*), r n o a(a) ^ rm [^(a)]. Remarquons que dans le cas particulier où r * est un morphisme de graphes, alors T* s'étend en un foncteur r* : Û ° -» /5*, et r est alors une transformation naturelle r : a -1» (3 o r*. • On définit la composition de deux flèches de DIAGR(C) de la façon suivante : Soit trois diagrammes: â = (a*, a : a* —• C) ; £=(/3*, 0:/3*->C); T =(->*• 7 : 7 * - > C ) Soit deux flèches: y : ^ -> ]3 = (a* : a* ~-> /3*, a : Q ^ > /3 o a*) ; r : /3 - • 7 = O"* : /?* ~-> 7*, r : /3 ~^> 7 ° r * ) . La composition T o â de â et r est le couple fo?:cF^7 = (r*o(r*:û*^7*iA:a^7or*oa*) ou - r $ o ( j $ est la composition des deux morphismes de graphes généralisés; 68 CHAPITRE 2. GRAPHES, CATÉGORIES - À : a ^^> 7 o r * o a* est la transformation par ET DIAGRAMMES naturelle généralisée définie Vn G Nœud(a^), An = v > ( n ) o an. a(n)^%*(n))^S(rV(n))) On vérifie sans difficulté que A est bien une transformation naturelle généralisée, c'est-à-dire que Va : m -> n G Arc(o*), V* ( n ) oano a(a) ~yVt» ( m ) o a m [r {a (a))]. • On vérifie que cette composition est associative. • Pour tout diagramme a, on a une flèche identité l(îâ : ô -» Q = {ida* : a* '•*—• a*, idâ • » " ^ <*)* où idâ • Q ^ > Q e s t ' a transformation naturelle identité idQ : a -^ a. Autrement dit, Vn G Nœud(a*), (/dâ)n = ida{n). 2.3.2 Colimites La façon standard de définir une colimite (comme par exemple dans [McL71]) est de commencer par fixer un graphe sous-jacent Q*, puis de définir un foncteur diagonal A:C->CÛ*, où Ca* est la catégorie des foncteurs de o? vers C, qui correspond à une catégorie de diagrammes de graphe sous-jacent a*. Cette présentation ne nous convient pas, parce que nous ne voulons pas fixer de graphe a priori. En définissant la catégorie DIAGR(C), nous n'avons pas non plus fixé de graphe sous-jacent, puisqu'un diagramme est donné à la fois par un graphe et un foncteur. Dans ce paragraphe, nous reformulons la définition de colimite dans notre cadre. Cette définition correspond à la définition standard, et évite de fixer trop tôt un graphe sous-jacent. Définition 2.19 (Foncteur d'inclusion Ic : C -> DIAGR(C)) La catégorie C peut être plongée dans DIAGR(C) en considérant tout objet de C comme un diagramme sur le graphe 1*. Autrement dit, on a un foncteur Ic : C -> DIAGR(C) A >-> ÇTA) f:A->B H+ Ç£ïyJ-jÇTB) 2.3. 69 DIAGRAMMES Le foncteur correspondant au diagramme Ic(A) est noté l£ : 1* -> C. La transformation naturelle généralisée correspondant au morphisme de diagrammes Ic(f) est notée Ï5C : l£ ~^-> l£. Nous avons donc : / C (A) = (1*, # : 1 * - > C ) /c(B) = (l», / C B :1*->C) /c(/) = (»«/,•, IJc:l£^I?). Soit * Tunique nœud de 1^. Nous avons: lf(*) = A /*(*) = B (//), = f:A^B. Définition 2.20 (Cône) Soit un diagramme a = (a^, Q : Q $ —y C). Un cône 1 sur et est un couple (A, \:â-+Ic(A)) où .4 est un objet de C, et À est une flèche entre les diagrammes a et Ic{A). À* est Tunique morphisme généralisé de Q^ vers 1* : à tout nœud de a*, \® associe Tunique nœud * de 1*, et à tout arc de Q*, A^ associe le zigzag de longueur nulle 0* : * ~—• *. Remarquons que 0* : * ^-* * est Tunique zigzag de 1*. Iç o A^ est en Remarque 2.4 La transformation naturelle généralisée A : a fait une transformation naturelle A : a -1» IQ o A*. En détaillant, on a Vra, n G Nœud (a*), Va : m ->• n G Arc(a*), An o a{a) = Xr Définition 2.21 (Cône colimite) Le cône [A, A : a -> Ic{A)) est un cône colimite du diagramme a si et seulement si pour tout cône (D, IjX : Q -> Ic{D)), il existe une unique flèche : A —» D de C telle que /<;(<£) o = /Z. 1. Pour respecter la terminologie usuelle, nous devrions parler de cône inductif ou de cocône, car nous allons définir des colimites et non des limites. Dans la mesure où nous ne parlons ici jamais de limites, nous utiliserons le mot cône. CHAPITRE 70 2. GRAPHES, CATEGORIES ET DIAGRAMMES Détaillons un peu cette dernière égalité. Ic{) o\ = J[ «• Vne Nœud(a*), /c(^) A *(„) ° K = ^n «• Vn G Nœud(a^), ¢0 Xn = /i n Si (/1, A : ô - > /c(-4)) est un cône colimite, on appelle .4 la. colimite du diagramme a, et on note A = Colimc â . Cette notation compacte ne doit pas faire oublier qu'en réalité, une colimite .4 est toujours définie en même temps qu'un cône, c'est-à-dire une flèche A : Q —> le {A). Les deux lemmes suivants montrent qu'une colimite est définie à un isomorphisme près. L e m m e 2.1 (Deux colimites d'un même diagramme sont isomorphes) Soit un diagramme a surC. Si (.4, A : ô —» /c(-4)) et (B, Jl :â —^ Ic{B)) sont deux cônes colimites du diagramme Q, alors A = B. Preuve. Comme (B, p, : a —> Ic(B)) est un cône sur a, il existe une unique flèche 0 : A -¥ B telle que Ic{(t>)oX = /i (0 Comme (A, A : a —> Ic{A)) est un cône sur a, il existe une unique flèche ifi : B —¥ A telle que le {¢)0/1 = A (^) Nous avons donc Ic(tf> o(f>) o \ = = = Ic{^)° Ic{ le {A)) est un cône colimite, il existe une unique flèche u : A -» A telle que Ie{u) o A = A. Or V ° et îd^ satisfont toutes les deux cette propriété, donc ift o cj) = idA- De même, on montre que o tp = idB- Par conséquent, A et B sont isomorphes. • 2.3. DIAGRAMMES 71 Lemme 2.2 Soit un diagramme et surC, ayant pour cône colimite (A, \:JS-+Ic(A)). Soit B un objet de C isomorphe à A. On note (f> : A —> B cet isomorphisme. (B, Ic() ° A : a —> Ic{B)) est un (autre) cône colimite du diagramme â. Alors Preuve. Il faut montrer que pour tout cône (D, /7 : a —> Ie{D)), il existe un unique ty : B -» D tel que Ie(ip) o Ic() o \ = JI. Existence. Soit £ : A ->• D Tunique flèche telle que /c(£) ° A = /Z. On pose /c(¥')o/cWo _ 1 = ^c(£° 0" ) ° A:(<£) ° A (définition de ¢) = lc{0 ° A (le foncteur) = JL (définition de £) Unicité. Soit \p' : B —¥ D tel que le (*!'') o Ic(4>) o X = JI. On montre que V' = V''/c(^) o /<;() ° A = Ie(t') ° ^c(0) ° A = JI (définitions de ip et V7') => /c(0o) o A = le(V?/ ° (j>) o X — JI (le foncteur) Comme (.4, A : a —> /c(-4)) est cône colimite du diagramme ô, il existe une unique flèche u : A -> £> de C telle que /c(u) o A = Jî. Comme jj: o et 0' o à satisfont cette propriété, •(/? o (f) = ift' O (f). Or

• A dans C. Exemple 2.7 (Objet initial) L'ensemble vide est initial dans la catégorie Set. La spécification vide est initiale dans la catégorie Spec. Le diagramme vide O (diagramme dont le graphe sous-jacent ne comporte aucun nœud et aucun arc) est initial dans DIAGR(C). Si le diagramme vide O a, une colimite 0 dans C, alors 0 est un objet initial de C. Soit (0, A : O -> ^c(0)) le cône colimite de O - Soit A un objet de C. Comme O est initial dans DIAGR(C), on a une flèche /J : O -> le (A). 0 est colimite du diagramme O , donc il existe une unique flèche JA '• 0 —» A telle que IC(JA) O X = JI. Soit j : 0 —» A une autre flèche de C. On a Ie(j) o X = Jî car O est initial dans DIAGR(C). Par conséquent, j = JAExemple 2.8 (Colimite du diagramme Ic(A)) Soit un objet A de C. Considérons le diagramme Q = /c(-4). Le cône (.4, id^ • cf —> le (A)) est un cône colimite de et. Preuve. Soit (B, Jî : Q —» Ie(B)) un cône sur a. Il existe une unique flèche 4> : A -» B de C telle que Ie(4>) o idâ = Jî- En effet, le (à) o idâ = Tl <=> o idA = //,* 4=> = / / « Exemple 2.9 (Coégalisateur) Soit deux objets .4 et B, ainsi que deux flèches / , g : A -+ B. Le coégalisateur de / et g est la colimite du diagramme K, construit sur le graphe K $ . •: 0 graphe K-* / B diagramme K 2.3. DIAGRAMMES 73 Soit un cône (D,JI : n -> Ic(D)) sur K. Ce cône est entièrement déterminé par une flèche h : B -» D telle que ho f = ho g. En effet, il suffit de poser fi0 = hof = hog /il = h pour définir la flèche // : K —• Ic(D). Soit (C, A : K —» /c(C)) le cône colimite de 7c. Alors, pour tout objet D et flèche q : B -» D telle que g o / = q o g, il existe une unique flèche u : C —» D telle que u o p = q. Dans la catégorie des ensembles Set, le coégalisateur C est le quotient de l'ensemble B par la relation d'équivalence engendrée par {(f(a),g(a)), Va G .4}. L'application p : B -» C est la projection de B sur le quotient C. Une application q : B —> D telle que qo f = qog est une application compatible avec la relation d'équivalence, qui se factorise donc à travers p. Il existe par conséquent une unique application u : C —¥ D telle que u o p = q. La construction de somme amalgamée de deux ensembles proposée dans le chapitre 1 (section 1.4.1) est en réalité une façon générale de construire une somme amalgamée à partir d'une somme et d'un coégalisateur. Exemple 2.10 (Somme amalgamée) Soit trois objets A,B,C et deux flèches / : A —> B, g : A —> C dans C. La somme amalgamée de B et C par rapport à / : A —> B et g : A —» C est la colimite du diagramme W, construit sur le graphe 7T*. • -• • •»• 1 q 0 6 2 graphe 7r^ -+- • • * A C B f diagramme K Soit (P, & : 7r -» Ie(P)) le cône colimite de n. Ce cône colimite consiste en trois flèches & 0 : A -> P, kx : B -> F et &2 : C -> F telles que Ce cône est donc entièrement déterminé par les deux flèches Sz\ et &2- 74 CHAPITRE 2. GRAPHES, CATÉGORIES ET DIAGRAMMES Soit (D, JI:T-¥ Ic(D)) un autre cône sur n. Ce cône est constitué de trois flèches ^ : A -* D, f = /ii : B -> D et g1 = /i 2 : C -> D telles que Vo = f'of = g'og. Un cône sur W est donc entièrement déterminé par deux flèches / ' : B -* D et g' :C -ï D telles que / ' o / = g' o g. Comme P est la colimite de W, il existe une unique flèche up : P -> D telle que Ic(up) o& = /I. Cette égalité est équivalente aux deux égalités wpo&i = / ' up o &2 = (i) ff' (") car l'égalité (/) — comme Tégalité (U) — implique up o & 0 = /^o- somme amalgamée, colimite du diagramme n Définition 2.23 (Catégorie finiment cocomplète) Une catégorie C est finiment cocomplète si et seulement si tout diagramme fini a une colimite. Théorème 2.2 Une catégorie C est finiment cocomplète si et seulement si C a un objet initial et des sommes amalgamées. Preuve. Pour montrer ce théorème, on utilise le théorème suivant : Théorème 2.3 Une catégorie C est finiment cocomplète si et seulement si C a un objet initial, des sommes pour tout couple d'objets de C, et des coégalisateurs pour tout couple de flèches f,g : A-ï B de C. Le dual de ce théorème est démontré dans [McL71], page 109. On vérifie facilement qu'on peut adapter la démonstration de S. Mac Lane à notre définition de diagramme. Ensuite, pour montrer le théorème 2.2, il suffit de montrer qu'on peut simuler la construction d'une somme et d'un coégalisateur à l'aide d'un objet initial D et de sommes amalgamées. 2.3. DIAGRAMMES 2.3.4 75 A d j o n c t i o n (Colimc H le) Dans ce paragraphe, nous considérons une catégorie C finiment cocomplète. Tout diagramme fini â= (a*, a : a * - > C ) a donc un cône colimite que Ton va noter (Colimc <*, 77- : Q —» /c (Colimc a ) ) . Nous montrons que Ton peut étendre la fonction Colimc sur les flèches de DIAGR(C) de façon à ce que Colimc : DIAGR(C) —> C soit un foncteur. La définition des flèches de DIAGR(C) a été justement choisie afin que cette extension soit possible. Soit deux diagrammes Q = (a*, a: a* -+C) et p = (/3*, p :/3* -+C) ayant respectivement pour cônes colimites (Colimc a, Tfe : ôF-» Ie(Co\\me a)) et (Colimc/î, rf^ : fi —>• /c(Colimc /3)). S o i t â : â - > ^ = (a* : a * ^ / J * , t r : a ^ / 3 o a * ) une flèche de DIAGR(C). Considérons le cône sur a (Colimc/3, rjjjoâ : a - » / c (Colimc/?)). Comme (Colimc a, 7/^- : a —» /c(Colimcâ)) est un cône colimite de â, il existe une unique flèche Colimc o : Colimc Q -» Colimc /3 telle que /c (Colimc a) o Tj- = rjp o W. Théorème 2.4 Soit C une catégorie finiment cocomplète. Alors, on a les résultats suivants. 1. Colimc : DIAGR(C) ->- C est un foncteur. 2. La fonction r}, qui à tout diagramme a associe la flèche du cône colimite de â vers le (Colimc cf) est une transformation naturelle V : ^DIAGR(C) -^ k o Colimc. 3. (Colimc H le) ' DIAGR(C) -> C estf une adjonction, dont Vunité est la transformation naturelle rj : /rfoiAGR(C) -^ k ° Colimc. 4. La coûnité de Vadjonction e : Colimc o le -1» /de es/ im isomorphisme naturel. 76 CHAPITRE 2. GRAPHES, Preuve. CATÉGORIES ET DIAGRAMMES Ces résultats sont des conséquences immédiates de la définition de Colimc- 1. Soit un diagramme â. = id lc(Co\\mcâ) °VQ {k est un foncteur) = *k* Or, Colimc id-Q est Tunique flèche telle que le (Colimc idâ) o rj^ = rj-^, donc Colimc idâ = idcolimcôSoit trois diagrammes a, /3 et y, et deux flèches a :â —>l3etr:(3 —• 7. Ic (Colimc T o Colimc cr) o r\— = le (Colimc r) o Ic (Colimc cr) o rj- (Ic est un foncteur) = le (Colimc r) olj^oW (définition de Colimc c) = rj^oToG (définition de Colimc r) Or, Colimc(ro^) est Tunique flèche telle que Colimc (roc) o rj- = 77- o r o W donc Colimc (Toa) = Colimc r o Colimc ~ô. Par conséquent, Colimc : DIAGR(C) —> C est un foncteur. 2. Soit deux diagrammes a, 3 et une flèche a : a —> f3. Par définition de Colimc Ie(B). Nous avons un cône (B, a : ci —> Ic(B)) sur le diagramme Q, donc il existe une unique flèche g : Colimc Û —> B de C telle que k(g)orj^ = â. 4. D'après la propriété 2.2, il suffit de montrer que pour tout objet B de C, eB : Colimc le (B) -> B est un isomorphisme. Comme on a un adjonction (Colimc H le), et d'après la propriété 2.4, Ice • 7]IC = idIc _ id => k(tB) °Vlc(B) = Ic(B) => £B o (rilc(B))* = idB- 2.3. DIAGRAMMES 77 D'autre part, Ic{tB)°Vlc(B) = idIc(B) => VlcW ° lofa) ° Vlc(B) = Vlc(B) =» ^((»?/c(B))* ° € s ) O»// C (B) = %c(B) (7C foncteur) Comme (Colimc Ic(B), Vic(B) : k(B) -t le (Colimc le (B))) est un cône colimite du diagramme Ic(B), il existe une unique flèche : Colimc h(B) -* Colimc /c(5) de C telle que Ic()°TJic(B) = Vic(By Or, les flèches (Ï]IC(B))* ° eB et idç0yimc ic(B) satisfont cette propriété, donc (rçjc(fî))- ° ^ = ^Colimc lc(B)' Donc 6^ ^ Colimc Ic(B) —> B est un isomorphisme, et e^1 = (rç/c(B))*. 2.3.5 C o n s e r v a t i o n de c o l i m i t e s Dans ce paragraphe, on considère deux catégories C et V, et un foncteur F :C —*V. Nous définissons l'image d'un diagramme et d'un morphisme de diagrammes par ce foncteur: l'image d'un objet de DIAGR(C) est un objet de DIAGR(P), et l'image d'une flèche de DIAGR(C) est une flèche de DIAGR(P). Définition 2.24 (Image d'un diagramme par un foncteur F : C —> V) Soit un diagramme a = (Q*, a : a® -» C) sur C. L'image par F de Q est le diagramme sur V Foâ= (a*, F O Û : Q $ -> V). Intuitivement, F o a est un diagramme construit sur le graphe sous-jacent a® du diagramme â. Les nœuds n de a® sont étiquetés par les objets F(a(n)) de V, et les arcs a : m —y n de a* par les flèches F(a(a)) : F(a(m)) —» F(a(n)) de V. Par exemple, étant donné un objet A de C, le diagramme F o Jc(A) est le diagramme h(F(A)). • F(A) & diagramme le (A) diagramme F o le (A) = Iz>(F(A)) L e m m e 2.3 Soit un diagramme a sur C. Soit no et nk deux nœuds de a®. Soit u : A —> a(no) et v : A —> a(nk) deux flèches de C telles que U~Û^ [Z :n0 ^-+ n*]. 78 CHAPITRE 2. GRAPHES, CATÉGORIES ET DIAGRAMMES Alors, F(u) ~ F o â F(v) [Z : n0 —-> nk]. Remarquons que si Z : n 0 ~*-> rc* est un zigzag sur le diagramme ô , alors c'est également un zigzag sur le diagramme F o a, puisque ces deux diagrammes sont construits sur le même graphe sous-jacent a . Preuve. D Application immédiate des définitions de F OQ, ~- et ~FOÔ- Définition 2.25 (Image d'un morphisme de diagrammes par F) Soit â : â -> 0 = (a* : a* ~-> /?*, t r : a ^ / } o j * ) une flèche de DIAGR(C). L'image par F de â est la flèche de DIAGR(£>) F?=(ff*:û*^]8*, F(r:Foa^Foflocr*) où Fa : F o G ^^> F o /3 o tr* est la. transformation naturelle généralisée définie par V7*eNœud(a*), (Fcr) n = F(an). On vérifie que cela définit bien une transformation naturelle généralisée. Considérons un arc a : m —>• n de a . a n o o(a) ^-3 F(anoa(a))^F^F(am) [a*(a)] => F(a„) o F(a(a)) ~ F o ^ F ( a m ) [a*(a)] => ( F a ) n o F(a(a)) - F o ^ ( F a ) n [ B de C. La flèche FIc(f) flèche / c ( / ) est égale à morphisme de diagrammes Flc(f) Iv(F(f)). = /p(F(/)) Pour tout diagramme a de DIAGR(C), nous avons donc défini un diagramme FoôF de DIAGR(P) ; et pour toute flèche â : â -> ]} de DIAGR(C), nous avons défini une flèche F â : F o â - » F o / 3 d e DIAGR(P). Ces deux applications forment en fait un foncteur. Lemme 2.4 L'application DIAGR(F) : DIAGR(C) â DIAGR(P) »-> F oâ »->• Fa : F o â - > F o / 3 est un foncteur DIAGR(F) : DIAGR(C) -> DIAGR(P). 2.3. DIAGRAMMES 79 Finalement, nous avons donc défini DIAGR à la fois sur les catégories (objets de CAT) et sur les foncteurs (flèches de CAT). De nouveau, nous avons défini un foncteur. Lemme 2.5 L'application DIAGR : CAT C F:C-^V -+ CAT i-> DIAGR(C) *-> DIAGR(F) : DIAGR(C) -> DIAGR(P) est un foncteur DIAGR : CAT -+ CAT. Propriété 2.5 L'application I qui à toute catégorie C associe le foncteur le : C —» DIAGR(C) est une transformation naturelle I : IdcAT^ Preuve. DIAGR. Pour tout foncteur F : C —• V, on a DIAGR(F)o/c = / p o F Lemme 2.6 Soit deux foncteurs F, F' : C —¥ V. Alors, F^Ff => D I A G R ( F ) ^ D I A G R ( F / ) . Preuve. Soit ^ : F -^ Ff Tisomorphisme naturel entre ces deux foncteurs. On définit une transformation naturelle Ç : DIAGR(F) -* DIAGR(F'). À tout objet â de DIAGR(C), on associe une flèche ^ : F O Û 4 F ' O Û de DIAGR(D) définie la façon suivante. • Les deux diagrammes F o â et F ' o â sont construits sur le graphe a® donc on peut définir Ç® = ida*. • Pour tout nœud n de a*, on pose (&)n = ua(n) : F(a(n)) -+ F'(a(n)). 80 CHAPITRE 2. GRAPHES, CATÉGORIES ET DIAGRAMMES Comme u est une transformation naturelle, pour tout a r c a : m - > n d e a $ , o n a F'(a(a)) o uQ(m) = ua(n) o F(a(a)) <=> F'(«(a)) o (fe) m = (fe) n o F(a(a)) Par conséquent, & • F o ô -4> F ' o Q est une transformation naturelle, et donc Jc_ : p 0 â -> F' o â est bien une flèche de DIAGR(2>). De plus, £5- est un isomorphisme, et pour tout nœud n de Û $ , (f^ ) n = ^2(n)' On montre que l : DIAGR(F) ^> DIAGR(F') est une transformation naturelle. Pour toute flèche â : â -> /3 de DIAGR(C), il faut vérifier que _ ÇjoDIAGR(F)(â) = DIAGR(F')(Ic(A)). On dit que le foncteur F :C —^ X> conserve la colimite de â si et seulement si (F(A), D\AGR(F)(rj-):Foa-+Iv(F(A))) est un cône colimite du diagramme Foc*. 2.3. DIAGRAMMES 8± Définition 2.27 (Foncteur conservant les colimites finies) Soit deux catégories finiment cocomplètes C et V. On dit qu'un foncteur F :C —¥ V conserve les colimites finies si et seulement si pour tout diagramme fini â sur C, F conserve la colimite de â . Propriété 2.6 Soit deux catégories finiment cocomplètes C et V, et un foncteur F :C —» V qui conserve les colimites finies. Alors, il existe un isomorphisme naturel Colimp oDIAGR(F) S F o Colimc. Preuve. Soit un diagramme â sur C, ayant pour cône colimite (Colimc o. rjâ : Q -> le (Colimc Q ) ) . On considère le diagramme F o â sur V, qui a pour cône colimite ( C o l i m p ( F o â ) , rjFo- : FoôF-> /p(Colimp(Fo Q ) ) ) . Comme F conserve la colimite de Q, et d'après le lemme 2.1, Colim7>(Foâ) S F(Colimcâ) et Tisomorphisme 4>â '• Colimp(F oôF) —> F(Colimcô) est Tunique flèche telle que Iv(4>ô) °TJFOÔ = DIAGR(F)(Tfe). Il suffit de montrer qu'on a une transformation naturelle : Colimp o DIAGR(F) - ^ F o ColimcSoit un diagramme /3, ayant pour cône colimite (Colimc^, TipiP^Ic(Colimc/3)). Soit 4^ : Colimx>(F o /?) -> F(Colimc /3) Tunique flèche telle que Soit â : a —)• /3 une flèche de DIAGR(C). Pour montrer que est une transformation naturelle, il faut montrer que F(Colim c â) o fe = ^ o Colimp(DIAGR(F)(â)). 82 CHAPITRE 2. GRAPHES, CATÉGORIES ET DIAGRAMMES Pour cela, il suffit de montrer que Iv{F{Co\\mcâ) cxfe) orj Fo5 - = /D((^oColimx)(DIAGR(F)(â))) o ^ F o 5 . /•p(F(Colimc ^ ) 0 ^ ) 0 Tjprt = Iv(F(Co\\mc â))oIv((F(Colimc â)) o DIAGR(F)(%) (définition de (Colimî,(DIAGR(F)(â)))o77 F o ^ (déf. Coli m î ,(DIAGR(F)(â))) = 7p(<^oColimî>(DIAGR(F)(â : )))o77 Fo5 {h est un foncteur) Par conséquent, on a bien une transformation naturelle

• C), ayant pour cône colimite choisi (A, Tfc:â-*Ic{A)). On dit que le foncteur F : C -»• V conserve fortement la colimite choisie de 07 si et seulement si (F(.4), DIAGR(F)(%-) : Foâ^ IV(F(A))) est le cône colimite choisi du diagramme F o 57 sur V. Si F conserve fortement la colimite choisie de ô, on a donc F(Colimcô) = C o l i m p ( F o â ) . 2.3. DIAGRAMMES 2.3.6 83 Aplatissement Diagrammes de diagrammes: catégorie DIAGR2(C) Étant donné une catégorie C, on peut considérer la catégorie DIAGR2(C) = DIAGR(DIAGR(C)) qui a pour objets des "diagrammes de diagrammes", c'est-à-dire des diagrammes sur DIAGR(C). Un objet  de DIAGR 2 (C) est donc un couple K = (A*, A : A* -> DIAGR(C)) où A* est un graphe, et A : A* -+ DIAGR(C) est un foncteur. Détaillons Faction de ce foncteur sur les nœuds et les arcs de A . • Pour tout nœud N du graphe A $ , on a un diagramme sur C ~Â(N) = (A(N)*, A(N) : A(;V)* -+ C) ou - A(Ar) est un graphe; - A(Ar) : A(N)® -> C est un foncteur, qui associe à tout nœud n du graphe A(N)* un objet A(N)(n) de C, et à tout arc a : n -» ri du graphe A(iV)* une flèche A(N)(a)[de C. Pour tout arc A : N -¥ N' du graphe A*, on a un morphisme de diagrammes ÂpT : Â(N) -> ÂlN7) sur C Â(Â) = (A(Af : A(Nf —> A(N'f, MA) : A(N) ~ * A(iV') o A(.4)*), ou - A(,4)* : A(N) ^ A(Nf)® est un morphisme généralisé de graphes, qui associe à tout arc a : n -» ri de A(N)(I> un zigzag A(A)*(a) : A(A)*(n) ~-> A(-4)*(n') du graphe A(W')* ; - A(i4) : A(AT) ^ » A(AT')°A(i4)* est une transformation naturelle généralisée, qui associe à tout nœud n de A(AT)* une flèche A(A) n : A(N)(n) -> A(N')(A(A)*(n))deC. A p l a t i s s e m e n t Apl c : DIAGR2(C) - • DIAGR(C) Étant donné une catégorie C, le foncteur Ic : C -> DIAGR(C) permet de créer un objet de DIAGR(C) à partir d'un objet de C, et une flèche de DIAGR(C) à partir d'une flèche de C. La fonction d'aplatissement Apl c : DIAGR 2 (C) -> DIAGR(C) 84 CHAPITRE 2. GRAPHES, CATEGORIES ET DIAGRAMMES permet au contraire de "détruire de la structure", en transformant tout diagramme de diagrammes (c'est-à-dire tout objet de DIAGR 2 (C)) en un simple diagramme (c'est-à-dire en un objet de DIAGR(C)). Considérons par exemple le diagramme A sur DIAGR(C), figure 2.2. 1 = (A*, A : A* -» DIAGR(C)) FlG. 2.2 - : diagramme A, objet de DIAGR 2 (C) Intuitivement, aplatir le diagramme de diagrammes A consiste à faire la réunion de tous les sous diagrammes de A, et à transformer toutes les flèches de DIAGR(C) en (ensembles de) flèches de C (cf. figure 2.3). FlG. 2.3 - : Aplatissement du diagramme A S = A p l c ( l ) , objet de DIAGR(C) Définition 2.29 (Aplatissement Apl c : DIAGR 2 (C) -» DIAGR(C)) Soit __  = (A*, A : A* -> DIAGR(C)) un objet de DIAGR 2 (C). On définit le diagramme S = Apl c (Â) de DIAGR(C) Apl c (A) = * = ( * * , 6:6*->C) 2.3. DIAGRAMMES 85 de la façon suivante. • £* est un graphe, déterminé par l'ensemble de ses nœuds et l'ensemble de ses arcs. Nceud(5*) = { (N, n);Ne Arc(8*) Nœud(A*) ; n G Nœud(A(JV)*) } ={(N,a):{N,n)-*(N,ri); AT e Nœud (A*) ; n,n' (A". A(.4)*(n)) ; AT, A" € Nœud ( A * ) ; A : N -»• N' £ Arc(A*) ; n€Nœud(A(iV)*)} • S : 6* -» C est un foncteur, défini sur les nœuds et arcs de S* de la façon suivante. — Action sur les nœuds : 5{N,n) = A(AT)(n) — Action sur les arcs: <5(A,«) = A(A")(«) S(A,n) = MA)n Définition 2.30 (Ensemble de flèches {7^ : A (#)_-» 6, VA G_Nœud(A*)}) Pour tout nœud A de A*, on définit une flèche JN : A(A) -> S de DIAGR(C) J J v " :  ( i V ) ^ 5 = ( 4 : A ( y V ) * ^ < î * , JN : A(A) ^ <5o J » ) Le foncteur généralisé J $ : A(AT)* ~-> 6* est défini par 4 : A(A)* n a:n^n' —• S* H+ (N, n) ( A, a) : (A, n)->(AT, n') •-»• Ce foncteur généralisé est en réalité un foncteur, car à tout arc de A( A ) * est associé un arc de S* (et non un zigzag quelconque). La transformation naturelle généralisée Jjv : A(A) ~-^ Sojft associe à tout nœud n de A(JV)* la flèche de C (^jv)n = idA{N)(n) = ^5(JV,n)- 86 CHAPITRE 2. GRAPHES, CATEGORIES ET DIAGRAMMES Pour montrer que JJSJ : A(N) —> S est bien une flèche de DIAGR(C), et comme J * est un foncteur, il suffit de vérifier que Jjy est une transformation naturelle JN:A(N)^SoJ%. C'est le cas, car pour tout arc a : n —» ri de A(N)®, par définition de 8(N, a), on a (JN)no A(N)(a) = 6(N,a)o (JN)n,. Remarque 2.6 Nous avons donc une famille de flèches JJ7 : Â{N) - • 6, VA € Nœud(A*). Pour tout nœud n de A ( A ) * on a donc une flèche (JN)n:A(N)(n)^8(N,n). Comme on a défini S(N,n) égal à A(N)(n), départ (JN)TI = *dA(N)(n) cela est cohérent avec la définition de = idS(N,n)- En fait, il n'est pas toujours commode de confondre les objets A(N)(n) et ô(N,n), parce que lors des raisonnements, le diagramme A( AT) ou S est en fait aussi important que 1 objet 6{N, n) = A(N)(n) de C. Pour cette raison, pour tout arc a : n -* ri de A ( N ) ^ , nous distinguerons les deux flèches A(AO(a):A(A-)(n)->A(A)(n'), 5{N,a) :6(N,n)^6{N,n'). De même, pour tout arc A : N —» A ' de A*, et pour tout nœud n de A(A)*, nous distinguerons les deux flèches A(.4)„ : A(A)(n) -4 A(A')(A(A)*(7i)), S(A, n) : S(N, n) -> 6{N', A(A)*{n)). Enfin, pour tout nœud Ar de A*, et tout nœud n de A(A r )*, nous distinguerons également les trois flèches (JN)n:A(N)(n)^S(N,n), idA{N){n) •• A{N){n) -*• A{N){n), idS(N,n) :6(N,n)^6(N,n). Pour respecter ces contraintes, nous n'utiliserons donc pas les deux égalités suivantes A(N)(a) = 6(N,a), A(A)n = 6(A,n). A la place, nous utiliserons les deux propriétés équivalentes suivantes. 2.3. 87 DIAGRAMMES Propriété 2.7 1. VAT € Nœud(A*), Va : n -> n' € Arc(A(A)*), (JN)n, o A(A)(a) = 6{N, a) o ( J N ) n . « W B ) ^(A,n') (JN)U' («/jv)n A(A)(n) A(A)(n') A(-V)(o) 2. VA : A -> A ' G Arc(A*), Vn € Nœud(A(A)<î>), (^N')A(^)*(n) ° A ( ' 4 ) n = S(A^ n) ° ( ^ n - 6{A n) *(JV,n) ' • ^ A ^ n ) ) (^Af')A(^)*(n) {JN)TI A(A)(n)- A(.4) n -A(A')(A(.4) £, VA G Nœud(A) ne permet pas de construire une flèche J : A -> /DIAGR(C)(^) dans la catégorie DIAGR 2 (C). En effet, il faudrait pour cela que pour tout arc A : N -> A ' de A*, on ait JN> o A(A) = Js «• Vn G Nœud(A(A) ), {JN')A(A)*(U) ° A(A) n = ce qui n'est pas vérifié. Lemme 2.7 Pour tout diagramme â de DIAGR(C), on a Apl C (/DIAGR(C)(S))=Ô. (JN)n, CHAPITRE 88 Preuve. 2. GRAPHES, CATEGORIES ET DIAGRAMMES Posons A = /DlAGR(C)(a) et 5 = Apl c (A)). Le graphe 8* est défini par Nœud(**) = {(*, n), Vrc € Nœud(a*)} A r c ( ^ ) = {(*, a) : (*, n) -> (*, ri), Va : n —>ri€ Arc(a*)} donc les graphes a* et 6* sont isomorphes. D'autre part, Vn G Nœud(a*), £(*, n) = A(*)(n) = a(n) Va:n-> ri e Arc(a*), £(*,a) = A(*)(a) = a(a). Par conséquent, a = 6. Donnons un exemple. On considère le diagramme a suivant. K 'DIAGR(C)W = B f A 9 C J r ^ fi / A 5 C J i . i . J Il est clair que l'aplatissement de /DIAGR(C)( Q ) donne le diagramme a. L e m m e 2.8 Pour tout diagramme â de DIAGR(C), on a Aplc(DlAGR(Ic)(â))=â. Preuve. Posons A = DIAGR(/c)(ôF) = Ic oâ, et S = Apl c (A). Le graphe S* est défini par N œ u d ( ^ ) = {(n, *), Vr* G Nœud(a*)} Arc(£*) = {(a, *) : (n, *) -> (ri, *), Va : n -> n7 )} donc les graphes Q * et (J* sont isomorphes. D'autre part, 8(n, *) = A(n)(*) = /c(a(n))(*) = a(n) 82 tel que Colim â = up (5, M,G,A2,bo s,mobo s, &x(A2) o &! (MD), &2(A2)). La définition de W que nous avons donnée n'était pas la seule possible. Considérons par exemple le morphisme de diagrammes r : Q —• 82 suivant. • Morphisme généralisé de graphes r $ : a* 0 1 2 a 3' 1' 2' 6 0 ' £ i 4 ' 1 0 6 2' • Transformation naturelle r : a ^-^- #2 o r^ : r0 = s 7"2 = ic?GLes colimites des morphismes de diagrammes â et r sont égales. Colim T = Colim â = up (S, A/, G, A2,6 o s, 77? o 6 o s, &i (.42) o fc^A/D),^!^)). n = zofjv/ En fait, on peut choisir pour la flèche r 0 une flèche quelconque du "faisceau" de flèches bas : a*(0)->#(!') a*(0)-><5*(3') m» o s = m+ o s a*(0)-^(00 s a*(0)-»<5*(4') mobos a*(0)^^(2'). CHAPITRE 2. GRAPHES, CATEGORIES ET DIAGRAMMES 90 Il faut évidemment définir r* en conséquence. De même, deux diagrammes non isomorphes dans la catégorie DIAGR(C) peuvent avoir des colimites isomorphes. Par exemple, on peut vérifier que les diagrammes ^i) <$2i ^3 et <$4 définis dans le chapitre 1 (section 1.5) ont des colimites.isomorphes. >M B» bas m, _ m . os _ S • ••£> mobos ra+ •M B» •M A B A \m» • D /m+ B» » S • mob G VA v• G \mob B • D H \mob • G Si Pour prouver que les colimites de ces quatre diagrammes sont isomorphes, il faut bien sûr utiliser les propriétés des colimites, ainsi que l'égalité entre flèches de Co : m+ o s = m* o s. Le but de ce paragraphe est de définir une catégorie dans laquelle les égalités entre flèches colimites et les isomorphismes entre objets colimites seront reflétées au niveau des diagrammes. Pour cela, nous définissons une relation de congruence » sur les flèches de DIAGR(C), compatible avec les colimites, et diagr(C) est la catégorie quotient diagr(C) = DIAGR(C)/«. Lemme 2.9 (La relation de connexion ~j est une relation d'équivalence) Soit un diagramme 8 sur C, et A un objet de C. La relation ~ j est une relation d'équivalence sur l'ensemble de flèches de C {u:A->8(n) ; n G Nœud(£*)}. Preuve. • La relation ~ j est réflexive. En effet, pour toute flèche u : A —ï 8(n) de C, u~$u [0 n ]. • La relation ~ j est symétrique. En effet, soit deux flèches u : A —> 8(no) et v : A -> 8(n\) de C. On a u~jv [Z] =• v~ju [Z], où Z \n\ ***-* no est le zigzag opposé de Z : no ^+ ni (cf. définition 2.4). 2.3. DIAGRAMMES 91 • La relation ~ j est transitive. En effet, soit trois flèches u : A -> 8(no), v : A 8(n\) et w : A -> £(n 2 ) de C. On a M ~j v [Z\] et v ^j w [Z2] => u ~ j w [Z], où Z : no ^-)- n 2 est le zigzag obtenu en mettant bout à bout Z\ : no ~-» n\ et Z2 : n\ ~—ï n2. L e m m e 2.10 (~j est une demi-congruence à droite) Soit u : A-ï 8(n0), v : A -> 8(n^) et w : A' -> A. On a u ~j v [Z] => uow^jvow [Z] (cf. figure 2A). Preuve. Application immédiate de la définition de ~y. FlG. 2 . 4 - : u o u » ~ j v o w [Z] L e m m e 2.11 Soit a et fi deux diagrammes sur C. Soit a : a —> /3 une flèche de DIAGR(C). Soit u : A —> a(m) et v : A —» a(n) deux flèches de C. Alors, U ~ Ô V [Z] => (TmOU^-anOV [ (3 deux flèches de DIAGR(C). On définit la relation » sur les flèches de DIAGR(C) par â % r <=> Vn G Nœud(a 4> ), crn^rn. Remarquons que c'est une bonne définition car Vn G Nœud(a^), an :a(n) -+(3(a*(n)), :a(n)->f3(T*(n)). Tn P r o p o s i t i o n 2.1 La relation « est une congruence. Preuve. • La relation % est réflexive car ~^j est réflexive. Soit W : a -> /3 une flèche de DIAGR(C). Vn G Nœud(a<ï>), an ^ an => â % â • La relation % est symétrique car ~-j- est symétrique. Soit G,T : â -+ f3 deux flèches de DIAGR(C). â « r => Vn G Nœud(o (|> ), a n ~^ r n =$> Vn G Nœud (a4*), r n ~^ an => r « â (définition de « ) (~p symétrique) (définition de « ) • De même, la relation « est transitive car ~-@ est transitive. • Soit ïï,T:â-ï]îetx:8-+'â trois flèches de DIAGR(C). Montrons que â ^ r => W ox ~T oxSupposons â % f. Il suffit de montrer que Vn G N œ u d ( ^ ) , < V » ° X n ~£ V » ° * n ' â wr => Vn G N œ u d ^ * ) , 0"x*(„) ~ ^ V » =ï Vn€ N œ u d ( ^ ) , crx*{n) o X n ^ r x * ( n ) o Xn (définition de w) (lemme 2.10) 2.3. DIAGRAMMES 21 • Soit cr,T:â->]3etÇ:]3-+j trois flèches de DIAGR(C). Montrons que Supposons que ~d « r . Il suffit de montrer que Vn G Nœud(a^), ^{n) â ^ r o an ~^ fT*(n) o r n . => Vn G Nœud (a*), VnGNœud(a^), ^ * ( n ) o an ~ T £T4>(n) o r n (définition de « ) (lemme 2.11) Lemme 2.12 So/Ï deuz catégories C et V et un foncteur F : C -> V. Soit deux flèches â, r : â -> ~j3 de DIAGR(C). Alors, â^T => D I A G R ( F ) ( â ) ^ D I A G R ( F ) ( r ) . Preuve. â %r => Vn G Nœud (a*), a n ~ ^ r n (définition de « ) => Vn G Nœud(a*), F(an) ~ F O J J F(r n ) (lemme 2.3) => DIAGR(F)(â) « DIAGR(F)(r) (définitions de DIAGR(F) et « ) Définition 2.32 (Catégorie diagr(C)) Comme « est une congruence (proposition 2.1), nous pouvons définir la catégorie diagr(C) comme le quotient de DIAGR(C) par « . diagr(C) = DIAGR(C)/^. Les objets de diagr(C) sont les objets de DIAGR(C). Étant donné deux objets â et f3 de diagr(C), une flèche entre Q et /? est une classe d'équivalence modulo « de flèches de DIAGR(C) entre â et /3. On a un foncteur de projection [-]c : DIAGR(C) â : â -> /3 -> diagr(C) •-» [â] : â -» /3 94 CHAPITRE 2. GRAPHES, CATÉGORIES ET DIAGRAMMES qui est l'identité sur les objets, et associe à toute flèche /3 de DIAGR(C) sa classe d'équivalence [ô] : â —y /3 modulo « dans diagr (C). Comme le foncteur de projection [-]c : DIAGR(C) -> diagr(C) est l'identité sur les objets, on notera de la même façon un objet â de DIAGR(C) et son image par [-]c dans diagr (C). Propriété 2.8 Soit F : DIAGR(C) -> V un foncteur compatible avec « , c'est-à-dire tel que pour toutes flèches ~Ô,T :~â -¥ f3 de DIAGR(C), â^r => F(W) = F(T). Alors, le foncteur F se factorise à travers [-]c- Autrement dit, il existe un unique foncteur G : diagr(C) —>> V tel que F = G o [—]c. Définition 2.33 (Foncteur diagr(F)) Soit deux catégories C et î>, et un foncteur F : C -> V. D'après le lemme 2.12, le foncteur [-]v o DIAGR(F) : DIAGR(C) - • diagr(X>) est compatible avec %. Donc, d'après la propriété 2.8, il existe un unique foncteur diagr(F) : diagr(C) -> diagr(P) tel que diagr(F) o [-]c = [~]v o DIAGR(F). Lemme 2.13 L'application diagr : CAT C F:C^V -• CAT ^ diagr(C) .-> diagr(F) : diagr(C) -+ diagr(P) est un foncteur diagr : CAT —» CAT. Preuve. Application immédiate de la définition de diagr sur les flèches. Propriété 2.9 L'application [—] qui à toute catégorie C associe le foncteur de projection [-]c : DIAGR(C) -> diagr(C) est une transformation naturelle [-] : DIAGR ^ diagr. Preuve. Résulte immédiatement de la définition de diagr(F). Lemme 2.14 Soit deux foncteurs G,Gf : diagr(C) -» V. Alors, Go[-]c = G ' o H c => G^Gf. D 2.3. DIAGRAMMES 95 Preuve. Soit UJ : G o [—]c -1» G' o [—]c l'isomorphisme naturel entre G o [—]c et G1 o [—]Q. Comme [—]c : DIAGR(C) -» diagr (C) est l'identité sur les objets on peut définir une transformation naturelle f : G -1» G' par Cela définit bien une transformation naturelle car pour toute flèche f : a —> (3 de diagr(C), il existe une flèche â : Q —y (3 de diagr (C) telle que T = [â]. Comme UJ est une transformation naturelle, ^0G([(T])=G'([â})0USâ =» ^oG(r)=G'(F)ofe De plus, £5- est un isomorphisme pour tout diagramme a de diagr (C), donc on a bien un isomorphisme naturel G^G'. Jusqu'à la fin de ce paragraphe, nous considérons une catégorie C finiment cocomplète. Nous allons montrer que les colimites sont compatibles avec la relation de congruence %, c'est-à-dire que le foncteur Colimc envoie des flèches équivalentes sur des colimites égales. Intuitivement, cette propriété prouve que la relation de congruence n'est pas trop "forte", c'est-à-dire n'identifie pas trop de flèches, et permet de définir un foncteur colimc • diagr(C) -» C. Lemme 2.15 Soit un diagramme Q de diagr(C), B un objet de C. et deux flèches ~ô,T :â —• Ic(B). Alors, a % r => a = r. Preuve. D'abord, a® — r® car Ic(B) est construit sur le graphe 1*, qui ne comporte qu'un seul nœud *, et qu'un seul zigzag 0* : * ~—> *. D'autre part, comme â « r, pour tout nœud n de a $ , on a crn ~ic(B) r n- Comme 0* : * ~-> * est le seul zigzag de 1*, on a nécessairement an — rn. Par conséquent, â —r. D Proposition 2.2 (Le foncteur Colimc est compatible avec « j Soit C une catégorie finiment cocomplète. Le foncteur Colimc est compatible avec %. Autrement dit, soit â et (3 deux diagrammes et ô,r : â —>• /3 deux flèches de DIAGR(C). Alors, â « T => Colimc ~ô — Colimc r. CHAPITRE 96 2. GRAPHES, CATÉGORIES ET DIAGRAMMES Preuve. Soit (A, A : â -> /c(A)) et (B, \' : j3-+ IC(B)) les cônes colimites des diagrammes â et /3. =>. => => => Â7 o r « Â7 o o ( « e s t une congruence) ^07 = ^ 0 ^ (lemme 2.15) /c (Colimc r) o À = Â7 o â (définition de Colimc r) Colimc â7 = Colimc r (définition de Colimc â) Corollaire 2.1 D'après la propriété 2.8, /e foncteur Colimc : DIAGR(C) -± C se factorise à travers [-]<;. Autrement dit, il existe un unique foncteur colimc : diagr(C) -> C tel que colimc o [—]c = ColimcRemarque 2.8 Dans la catégorie diagr(C), il existe plus d'isomorphismes entre diagrammes, et plus d'égalités entre flèches de diagrammes que dans la catégorie DIAGR(C). Néanmoins, dans le cas général, 1. colimc 01 = colimc r fi â=r; 2. colimc â ^ colimc/3 fi o S /3. La raison intuitive est qu'on peut avoir des égalités entre flèches de C qui ne proviennent pas des propriétés générales des colimites, mais de la catégorie C elle-même. Contrexemple. On considère la catégorie (N, /) définie de la façon suivante. • Les objets de ( N , / ) sont les entiers naturels. • On a une flèche unique de n vers m si et seulement si n divise m. (IN,/) est une catégorie finiment cocomplète. (Par exemple, la somme catégorielle de 77? et n est le ppcm de m et n.) Les diagrammes â et /3 dessinés ci-dessous, ne sont pas isomorphes dans diagr(IN, / ) , et ont pourtant des colimites isomorphes. 2x3 5 ) C 2 3x5 /3 a Les deux diagrammes ont en effet pour colimite l'entier 2 x 3 x 5 . De même, les flèches â et r, dessinées ci-dessous, ne sont pas égales dans diagr(IN, / ) , et ont pourtant des colimites égales: la flèche de l'entier 2 vers l'entier 2 x 3 x 5 . 2.3. DIAGRAMMES 97 Ici, la définition de la catégorie indique que deux flèches entre deux objets sont forcément égales. C'est la raison pour laquelle colimc ô — colimc r. Dans une autre catégorie, il n'y a a priori aucune raison pour que cette égalité soit vérifiée. T h é o r è m e 2.5 Soit C une catégorie finiment cocomplète. 1. Les deux foncteurs colimc : diagr(C) -> C [-]co/c:C->diagr(C) forment une adjonction (colimc H [-]c °Ic)- 2. La coûnité de cette adjonction est la coûnité de l'adjonction (Colimc -\Ic)Preuve. 1. On définit une transformation naturelle 77' : /ddiagr(C) -^ [~]c ° k o colimc àe la façon suivante. Pour tout objet â de diagr(C), on pose 7â = Pte] où 77 : /dDlAGR(C) -^ /c°Colimc est l'unité de l'adjonction (Colimc H /c). C'est une bonne définition car le foncteur [-]c est l'identité sur les objets. On vérifie facilement que 7/ est bien une transformation naturelle. Montrons maintenant que (colimc H [-]c ° le) est une adjonction dont l'unité est 777. Soit un diagramme â de diagr (C), B un objet de C, et [â] : Q -> / c ( # ) une flèche de diagr(C). Il faut montrer qu'il existe une unique flèche de C : colimc ô —> B telle que [ W ) ] ° [%] = [*]• Existence. Comme (Colimc H /c) est une adjonction dont l'unité est rj : ^DIAGR(C) -^ k° Colimc, U existe une unique flèche

)o:riâ = ë. En considérant Q comme un objet de diagr (C), la flèche a pour domaine colimc Û. ^ ( ¢ ) 0 ^ 0 = 07 => [ W ) o » y = [â] => [ W ) ] ° [%] = [*] ([-]c foncteur)_ =• [k{)} o ifo = [ôl (définition de V) 98 CHAPITRE Unicité. 2. GRAPHES, CATÉGORIES ET DIAGRAMMES Soit 0, t/> : colimc <* -> B deux flèches de C telles que [W)]orfrr=\*\, [IcM)°T/ë=[°]On montre que = ij). [W)Wff=[W)]oife =* [/c(0)]o[fe] = [/c(0)]o[%.] => [ / c ^ o f e ] = [ W ) o ife] => Ic($)°Vâ~ Ic(i>)°Vâ => / c ( ^ ) o % = IcW)°Vâ = > (j> = t/; (définition de rf) ([-]c foncteur) (définition de « ) (lemme 2.15) (adjonction (Colimc H /c)) 2. Considérons € : Colimc o Ic -^ /de la coîinité de l'adjonction (Colimc H /c). Comme Colimc = colimc °[—]c? * est bien une transformation naturelle € : colimc o[-]c ° le "^ M:Pour montrer que 6 est la coîinité de l'adjonction (colimc H [—]c ° /c) : diagr(C) —• C, on utilise le théorème 2.1. Soit une flèche g : colimc â -» B de C. Il faut montrer qu'il existe une unique flèche [a] : Û -> /c(#) de diagr(C) telle que É# o colimc[ôr] = #. Existence. Comme (Colimc H /c) est une adjonction, il existe une unique flèche â : Q -> /C(JB) de DIAGR(C) telle que €B O Colimc €B ocolimc[â] = g Unicité. (définition de colimc) Soit [a], [r] : â -> Ie(B) deux flèches de diagr(C) telles que eB o colimc [â] = ff, €5 O colimc [T] = 9- On montre que [ ^ = 7 => 1*1 = M- (définition de colimc) (adjonction (Colimc H /c)) 2.3. DIAGRAMMES 2.3.8 99 L a c a t é g o r i e diagr(C) est finiment c o c o m p l è t e Dans ce paragraphe, nous considérons une catégorie C quelconque, et nous allons montrer que la catégorie diagr(C) est finiment cocomplète. Pour cela nous devons montrer que tout diagramme T de DIAGR(diagr(C)) a une colimite dans diagr (C). Intuitivement, pour construire une colimite de T, on commence par construire un diagramme A de DIAGR 2 (C) construit sur le même graphe sous-jacent que T, tel que pour tout arc A : N —> N', A(A) est un représentant de la classe d'équivalence T(A) de flèches de DIAGR(C). Ensuite, l'aplatissement de A donne une colimite du diagramme T. L e m m e 2.16_ Soit un objet F de DIAGR(diagr(C)). // existe un objet  de DIAGR2(C) tel que f =DIAGR([-]c)@ = H c o I . Preuve. On définit un diagramme ^ = (A*, A : A* -> DIAGR(C)) de la façon suivante : • Le graphe sous-jacent de A est le graphe sous-jacent de T. Autrement dit, • Le foncteur A : A^ -» DIAGR(C) est défini par son action sur les nœuds et sur les arcs du graphe A*. - Tout nœud N de A^ est étiqueté par T(N). A(N) = T(N); - Pour tout arc A : N -> N' de A*, T(A) : T(N) -* T(N') est une flèche de diagr(C), c'est-à-dire une classe d'équivalence de flèches de DIAGR(C). On choisit un représentant A(A) de cette classe d'équivalence. Autrement dit, A(A) est tel que T(Â) = [Â(Â)]. Cela définit bien un foncteur car A(A) : A(N) -> &(N'). On vérifie immédiatement que F=[-]c°I. 100 CHAPITRE 2. GRAPHES, CATÉGORIES ET DIAGRAMMES Soit F un objet de DIAGR(diagrJC)). D'après le lemme 2.16, il existe un objet A de DIAGR2(C) tel que F = [-]c o  . Comme dans le paragraphe 2.3.6, on note ? = Aplc (¾ l'aplatissement de Â, et pour tout nœud N de A*, on a une famille de flèches de DIAGR(C) JN : &(N) -* S. On avait vu en remarque 2.7 que la famille de flèches JN:A(N)-+6 de DIAGR(C) ne permet pas de définir une flèche J : A -> /DIAGR(C)(<*) dans la catégorie DIAGR 2 (C). Par contre on a une flèche de T vers /diagr(C)(<*) d a n s la catégorie DIAGR(diagr(C)), grâce au lemme suivant. L e m m e 2.17 Pour tout arc A : N -> N' de A*, JNi o A(A) « J/v. Preuve. Il suffit de montrer que Vn G Nœud(A(A r )*), (JN>)MA)*(n) ° A(.4) n - y ( J*)*- Cette relation est vérifiée, car par définition de S, on a (JN')A(A)*(TI) ° -M-4)n = &{A, n) o (J A r) n . D On définit une famille de flèches de diagr (C), en posant, pour tout nœud N de A*, W=[JN]:F(N)^6. L e m m e 2.18 (6, î\ : F -> /diagr(C)(^)) e5 * w n c é n e 5 w r r Preuve. Il suffît de montrer que J\ : F -> /diagr(C)(<*) est une flèche de la catégorie DIAGR(diagr(C)), c'est-à-dire que pour tout arc A : N -> N' de A(N)*, on a 7^77 oT(A) = 7/N. Pour tout arc A : N -> N' de T(N)*, on a J^To A(A) « JN =» [JJv^o A(-A)] = [7/v] =» [JV] o [A(i4)] = [7yv] =» [7^7] o F g y = [J^] => 77^ o Y(A) = rfx (lemme 2.17) (définition de [-]c) ( [ - ] C est un foncteur) (définition de A(A)) (définition de rfjv et 7^7) Par conséquent, (S, îj : F -> /diagr(C )(<*)) est un cône sur T. D 2.3. DIAGRAMMES 10J L e m m e 2.19 Soit un ensemble de flèches de DIAGR(C) (K^ : AjN) -> 57, VA7 € Nœud(A*)} tel que VA : A7 -> A7' G Arc(A*), A > o A(A) « KN. Alors, 1. il existe une flèche â :8 ->â de DIAGR(C) telle que VA7 e Nceud(A ¢ ), ôoJ^&K^; 2. pour toute flèche T :6 ->â de DIAGR(C) telle que VA7 €Nceud(A*), TOTN ^ 1• A r 'eArc(A*),  > o A(A) « ÂÔv". 1. Considérons la flèche de DIAGR(C) ô : S -* Ô7 = (cr* : d'* ~-> o*, a : <5 ~^> Q O a* est un morphisme généralisé de graphes. - V(iV, n) £ Nceud(^), cr^A 7 , n) = A $ ( n ) . - V(Ar, a) : (A7, n) -»• (A7, n') € Arc(£*), a * ( N , a ) = A'» (a) : K%(n) -> A * K ) 7 - V(A, n) : (A , n) -> (A7', A(A)*(n)) € A r c ( ^ ) , a*(.4, n) = Z, où Z : K%(n) ~-> K%,{A{A)(n)) est le zigzag tel que {I)A(A)*(n) ° MA)n ~ÔF (A'jv)„ [Z]- • (A 7 ,^) € Arc(<5*), 102 CHAPITRE 2. GRAPHES, CATEGORIES ET DIAGRAMMES (b) V(A, n) : (A7, n) -> (A7', A(A)*(n)) € Arc(• (A'jv)n' o (J^)„' o ^(A7, a) ~ Ô (A'iv)n o (J^/)^1 => <7(JV,n') o 5(AT, a) ~ â a{N,n) [o-*{N, a)] (lemme 2.10) (définition de S(N, a)) (définition de ( A » A W ( n ) o A(A) n o ( J N ) - i ~x (I {I)A{A)*{n) o {JN')A\A)*{n) => CT 0 (iV',A(4)*(n)) ^(^»") ° HA, n) ~cr (KN)n ["(4,n)*] Il reste à montrer que VA7 G Nœud(A $ ), ), TOJATWÂV On montre que • V(A7, n) G Nœud(<54>), r(7V)n) o (JN)n ~ Ô (A'iv)n =• V(N,n) G Nœud(«*), r ( A > ) ^ (Ajv)„ o (J^)" 1 => V(AT, n) G Nœud (5*), r(;v,„) ~ Ô <7(7V,n) Lemme 2.20 Le cône (6, n : F —> / /diagr(C)(<*)) u n autre cône sur T. Nous devons montrer qu'il existe une unique flèche [W] : 5 -*• â de diagr(C) telle que 2.3. DIAGRAMMES 103 Existence. Pour tout nœud N de r * , \N : T(Af) —• a est une flèche de diagr(C). On choisit un représentant KN *• T(AT) -> ÔF dans DIAGR(C) de À^. Autrement dit, on a VJV G Nœud(r*), [Â^] = Â^. Comme À : T —> /diagr(C)(#) e s t u n e flèche de DIAGR(diagr(C)), pour tout arc .4 : N -> AT' du graphe T* = A*, on a \w O T(A) = À^ =-> [I [ A > o A ( , 4 ) ] = [~KN] => A";v' O A(A) % A'w (définition de KN, KN, et A) ([-]e foncteur) (définition de diagr(C)) donc, d'après le lemme 2.19 (1), il existe une flèche ~a : S —> â de DIAGR(C) telle que VA^GNœud(A<ï>), WoJ^^l^. VATeNœud(r*), â o J ^ % Â Ô 7 => ViV G Nœudfr*), [âojjy] = [Ayy] => VW G Nœud(r^), [â] o [J N ] = ]A/v] => VA r eNœud(r*), [5F]oç3v = A^ Unicité. Soit [r] : 5 —» a une flèche de diagr(C) telle que ^diagr(C)([^])°^=^ => VA^GNœud(r<ï>), [r]or[û_= XN_ => VN G Nœud(r a> ), [f] o ÇhJ] = [K^] => VAr G Nœud(r*), [ f o J N ] = [A N ] => VATeNœudfr*), r o J ^ « A'iv donc d'après le lemme 2.19 (2), cr % r, et par conséquent [a] = [r]. D T h é o r è m e 2.6 La catégorie diagr(C) est finiment cocomplète. Preuve. Conséquence immédiate du lemme 2.20. • R e m a r q u e 2.9 Dans cette preuve, nous avons montré l'existence d'une colimite pour le diagramme T. Pour chaque arc de r * , nous avons effectué un choix de représentant A(A) pour la flèche T(A). Un choix différent de représentant conduit à un autre diagramme colimite (isomorphe) pour T. Nous avons donc défini la colimite de T à un isomorphisme près. 104 CHAPITRE 2. GRAPHES, CATÉGORIES ET DIAGRAMMES Une colimite est définie à un isomorphisme près, mais lorsque les classes d'équivalence r(i4) ne contiennent qu'un élément, alors il n'existe qu'un seul diagramme A tel que f = [-]c oÂ. Soit un diagramme â de DIAGR(C). Considérons le diagramme de DIAGR(diagr(C)) F = DIAGR([-]c o Ic){a) = [-]c oIcoâ. Pour tout arc a : n -» n1 du graphe r * = a*, r(a) = [/c(a(a))], et le seul élément de la classe Y (a) est Ic{a(a)). Donc I = / c o ô = DIAGR(/c)(â). D'après le lemme 2.8, Apl c ( ¾ = Apl c (DIAGR(/c)(5)) = â. Finalement, la colimite de T est donc 07. L e m m e 2.21 Soit une catégorie C. Colim diagr(C) oDIAGR([-] c o Ic) = [ - ] c Preuve. • Pour tout diagramme Q de DIAGR(C), Colim diagr (C)(DIAGR(Hc o / c ) ( â ) ) = â. • Soit une flèche â : a -> /3 de DIAGR(C). Soit (5", ^ : [-]c o /c o â ^ /diagr(C)(â) et _ = _ _ (A rf : [-]c o /c o /3 -> / diagr( c)(/î) les cône colimites respectifs des diagrammes [-]c o le o â et [-]c o le o /3. Posons Il faut montrer que D = [-]c o Ic oW. _ Colim diagr (c) S = [â]. Comme Colimdiagr(C) S est l'unique flèche telle que /diagr(C)(Colimdiagr(C) S ) O ^ = 7?' O S, il suffit de prouver Jdiagr(C)([^])°^ = ? ° S ^ _ <î=> VnGNœud(a^), [ ^ ] o ^ = r / > ( n ) o S n . 2.3. DIAGRAMMES 105 Remarque 2.10 Ce lemme montre que le foncteur [-]c o le : C —> diagr(C) est dense, c'est-à-dire que tout diagramme â est colimite d'un diagramme construit sur les images des objets et flèches de C dans diagr(C). En effet, tout diagramme â de diagr(C) est la colimite du diagramme T = DIAGR([-]c ° ^c)(â). 2.3.9 La c a t é g o r i e diagr(C) est u n e c o m p l é t i o n de C par c o l i m i t e s finies La catégorie diagr(C) a une propriété importante: c'est une complétion de C par colimites finies. Intuitivement, cela signifie que diagr(C) est une catégorie "minimum" qui contient C, et toutes les colimites finies que l'on peut construire à partir d'objets et de flèches de C. Soit une catégorie C quelconque, et V une catégorie finiment cocomplète. Soit un foncteur F :C —» V. On considère le foncteur G = Colimp o DIAGR(F) : DIAGR(C) -> V. L e m m e 2.22 On a un isomorphisme naturel G o le =• F. Preuve. D'après le théorème 2.4, c : Colimp o /p -^ Id-j), coîinité de l'adjonction (Colim-p H Iv) est un isomorphisme naturel. Par conséquent, Colimp o / p == Idf> => Colimp o I-p o F =. F => Colimp o DIAGR(F) o Ic * F => GoIc = F (composition par F) (I : IdCAT -^ DIAGR) (définition de G) Soit A un objet de DIAGR 2 (C), S = Aplc-(A) l'aplatissement de A, et la famille de flèches de DIAGR(C) JN : A(A') -> S, VN G Nœud(A^). Pour tout nœud N de A^, on considère la flèche \N = G(JN):G(A(N))->G(6) dans P . Nous allons considérer les diagrammes suivants. • Le diagramme Fo8=(6*, Fo6:6* ->V) est un objet de DIAGR(Î>), qui a pour cône colimite (G(6),rjFor.Fo6^Iv(G(S)))- 106 CHAPITRE 2. GRAPHES, CATÉGORIES ET DIAGRAMMES • Pour tout nœud N de A*, on a un diagramme F o AjN) = (A(AT)*, F o A{N) : A(JV)* -»• V) dans DIAGR(I>), qui a pour cône colimite (G(A(N)), ^ F o Z M : Fo A(N) -> IV(G(A(N)))). Par définition, XN = G{7^) = Colimî>(DIAGR(F)(JÂr)), donc XN est l'unique flèche telle que h(XN) o VF0Â(m = VFOS ° DIAGR(F)(JÂF). (i) Lemme 2.23  : G o l -> /p(G(î)) es* une /ïèc/ie de DIAGR(I>). Preuve. Il suffit de montrer que pour tout arc A : N ->• Ar/ de A*, on a \N,oG(A(A)) = \,\: 7^OA{A)^7N =» DIAGR(F)(J^7o A(A)) ss DIAGR(F)(J,y) =>. Colimî>(DIAGR(F)(J^7oA(/l])| = Colimp(DIAGR(F)(J A ')) =• G(J^oAjÂ)) = G(J^) => G ( T O o G{A~(Â)) = GjJpj => XN,oG(A{A)) = XN (lemme 2.17) (lemme 2.12) (proposition 2.2) (définition de G) (G foncteur) (définition de A;v et XN>) Lemme 2.24 (G(<5), A : G o A ^ I-p(G(5))) est un cône colimite du diagramme GoldeDIAGR(î>). Preuve. Soit un cône (A, JT : G o A -> Iv{A)) sur le diagramme GoA.Ji est donc une flèche de DIAGR(X>). Nous allons montrer qu'il existe une unique flèche 4> : G(S) - • A de V telle que Iv{4>)oX = /ï. 2.3. DIAGRAMMES Existence. 107 Pour tout nœud N de A* et tout nœud n de A(iV)*, on pose V>N,n = fiN ° (VFoK(N))n ° ^ ( ( ^ ) ^ ) : F{S{N, n)) -» A. Cette définition est correcte car F ( ( J N ) " 1 ) : F(*(JV,n)) -+ F(A(N)(n)) (TlFom))n : F(A(N)(n)) -+ G(A(JV)) /iiv : G(A(N)) -> A On montre que est une flèche de DIAGR(P). • Pour tout arc (N, a) : (N, m) -+ (N, n) de 6®, i'N,noF(6(N,a)) = VN o (VFoA(N))n o F((JN)~x) o F(S(N, a)) = VN o (VFoA(N))n ° F((JN)~X o 5(N, a)) = VN o (r)FoA(N))n o F(A(N)(a) o (JN)~l) = VN o (VFoMN))n o F(A(N)(a)) o F((JN)-1) = VN O (?lFoMN))m O F((JN)^1) = iJN,m (définition de ipN,n) (F foncteur) (définition de S(N, a)) (F foncteur) (^FoÂfïV) C Ô n e ) (définition de V'A/,m) • Pour tout arc (A,m) : (M,m) -> (N N G Arc(A*), m G Nœud(A(M)*), et n = A(-4)*(m) G Nœud(A(JV)*), i'N.n°F(S(A,m)) = VN o (r)FoA(N))n o F((JN)~l) o F(S(A,m)) = VN o (r]FoA(N))n o F ^ J ^ ) " 1 O S(A, m)) = VN o (r)FoMN))n o F(A(,4) m ) o F((J A /)" 1 ) = VN o G(A(A)) o (7]FoA{M))m oF((J A /)" 1 ) = VM o (rjFoA(M))m o F((JM)m) = ipM,m (définition de ipN^n) (F foncteur) (définition de S(A, m)) (définition de G) iv cône) (définition de I^M,™) On a donc bien une flèche ¢: Foô-> IV(A) dans V. De plus on vérifie immédiatemment que ^oDIAGR(F)(Jîv) = W / v ) o ; ? F o X ^ y . (2) Comme on a un cône (A,^:Fo6^Iv(A)), il existe une unique flèche : G(8) -*• ,4 de î> telle que /î>(<£)°rçFoï = ?- (3) 108 CHAPITRE 2. GRAPHES, CATÉGORIES ET DIAGRAMMES Il reste à montrer que Iv(4>) oA = /i & VATGNœud(A*), cf>o\N = fiN :G(A{N))-> A Comme (G(A(N)), rçFoZ^ : F o A(N) -> IV(G(A(N)))) est cône colimite de A(N), il suffit de montrer que h{°*N)or)FoK^ = IV{»N) °VFoÂ(N~y Iv(oXN)orjFo^pj Unicité. = = = h{) ° h{XN)°rjFoÂ{N) Iv{)orjFjoDlAGR(F){JN) voDlAGR{F)(JN) (Ji> f o n c t e u r ) (1) (3) = /©(/ijv) °VFOÂ(N) (2) Soit ' : G(£) ->• 4 une flèche de P telle que h(4>') oX = JL. On montre que = 0'. Pour cela, il suffit de montrer que h{ t '(N.n)oXN0(ïlFoÂ{N))nOF({JN)-1) = Miv°(^FoÂ(jv))n = ipNjtl oF J 1 (( ^)n ) (1) (définition de 0) (définition de Vw.n) Proposition 2.3 Soit une catégorie C et une catégorie finiment cocomplète V. Soit un foncteur F :C -ïV. Posons G = Colimî) oDlAGR(F) : DIAGR(C) -> D H = colimp odiagr(F) : diagr(C) -> D. .4/ors, 1. ffo[-]c 2. Ho [-]c = G; oIc^F; 3. 77 conserve les colimites finies. 2.3. DIAGRAMMES Preuve. 109 On prouve successivement les points 1, 2 et 3. 1. On a H o [—]c = colimp o diagr(F) o [—]c = colimp o [-]p o DIAGR(F) = Colimp oDIAGR(F) = G (définition de H) (définition de diagr (F)) (définition de colimp) (définition de G) 2. D'après le lemme 2.22, Go le — F, donc, d'après le point 1, H o[—]c oie = F . 3. Soit un diagramme T de DIAGR(diagr(C)). On considère un diagramme A de DIAGR2(C) tel que _ _ r=[-] c oï. On pose S = Apl c (A), et le cône colimite du diagramme T (S, ^:F-*/ d ia S r(C)(<*)) avec lfx — [JN]> On a _ //or = _ tfo[-]co _ = GoA et \s = G(Jiï) = H{ÇÏÏÏ) = H(m- D'après le lemme 2.24, (G(ô), \:Go^-+Iv(G(ô)) est un cône colimite de G o A, donc (H(S), Hfj-.HoT ->IV(H(S))) est un cône colimite du diagramme H o F. Par conséquent, H conserve les colimites finies. D Théorème 2.7 (Complétion) SoitC une catégorie quelconque. La catégorie diagr(C) est une complétion de C par colimites finies. Autrement dit, pour toute catégorie finiment cocomplète V, et tout foncteur F : C —>• V, il existe un foncteur H : diagr(C) —y V, unique à un isomorphisme naturel près, qui conserve les colimites finies, et tel que : H o [-}c oIc = F. 110 CHAPITRE 2. GRAPHES, CATEGORIES ET DIAGRAMMES Preuve. Soit une catégorie C quelconque, et une catégorie V finiment cocomplète. Soit un foncteur F :C -» V. On montre l'existence, puis l'unicité à un isomorphisme près, d'un foncteur H : diagr(C) -> V qui conserve les colimites finies et tel que H o [-]c ole^F. Existence. On pose H = colimp odiagr(F). D'après la proposition 2.3, H o [-]e o le = F et H conserve les colimites finies. Unicité de H à un isomorphisme naturel près. Soit deux foncteurs H. H1 : diagr(C) —> V qui conservent les colimites finies, et tels que Ho[-]coIc^ H'o[-]coIc. On montre qu'il existe un isomorphisme naturel H^H1. H o [-] c ole^H'o [-]c o Ic => DIAGR(# o [-] c o Ic) £ DIAGR(//' o [-}c o Ic) => D I A G R ( / / ) o D I A G R ( [ - ] c o / c ) ^ DIAGR(tf') o DIAGR([-] C o Ic) => Colimp o DIAGR(#) o DIAGR([-] C o Ic) ^ Colimp o DIAGR(tf') o DIAGR([-] C o Ic) => Ho Colim diagr(C) o DIAGR([-] C o Ic) £ H' o Colim diagr(C) o DIAGR([-]c o Ic) => floHca/î'oHc H^W (lemme 2.6) (DIAGR foncteur) (propriété 2.3) (propriété 2.6) (lemme 2.21) (lemme 2.14) Remarque 2.11 Nous avons montré que la catégorie diagr(C) est finiment cocomplète. Par contre, nous n'avons pas montré que diagr(C) a des colimites choisies. En effet, nous n'avons pas montré l'existence d'une colimite canonique pour un objet de DIAGR(diagr(C)), puisque pour montrer l'existence d'une colimite, nous devons choisir un représentant pour une classe d'équivalence de flèches de DIAGR(C). 2.4 Conclusion Dans ce chapitre, nous avons défini une catégorie de diagrammes DIAGR(C), dont les objets sont les diagrammes finis, et les flèches sont les morphismes de diagrammes (définitions 2.16 et 2.18). Nous avons rappelé la définition de colimite d'un diagramme et de colimite d'un morphisme de diagrammes (paragraphe 2.3.2). Nous avons défini une opération d'aplatissement Apl c : DIAGR2(C) —>• DIAGR(C) qui 2.4. CONCLUSION 1U permet de considérer tout diagramme de diagrammes comme un simple diagramme (définition 2.29). Nous avons défini une relation de congruence sur les morphismes de diagrammes, ce qui nous a permis de considérer la catégorie quotient diagr(C) (définition 2.32). Nous avons montré que la catégorie diagr(C) est finiment cocomplète, c'est-à-dire que tout diagramme fini sur diagr (C) a une colimite dans diagr(C) (théorème 2.6). Cette colimite d'un objet T de DIAGR(diagr(C)) peut être construite en aplatissant un diagramme A de DIAGR 2 (C) obtenu à partir de T en remplaçant chaque classe d'équivalence qui étiquete un arc par un représentant de cette classe. Enfin, nous avons montré que la catégorie diagr(C) est une complétion de C par colimites finies (théorème 2.7). Références bibliographiques [AL91] A. Asperti and G. Longo. Catégories, Types and Structures, An Introduction to Category Theory for the Working Computer Scientist. Foundations of Computing Science, MIT Press, 1991. [AM75] M. A. Arbib and E. G. Mânes. Arrows, Structures and Functors: The Categorical Imperative. Académie Press, 1975. [B+90] D. Bert et al. Référence manual of the spécification language LPG. Technical Report 59, LIFIA, Mars 1990. Anonymous ftp at imag.fr, in /pub/SC0P/LPG/NewSun4/man_lpg.dvi. [BBC86] G. Bernot, M. Bidoit, and C. Choppy. Abstract data types with exception handling: An initial approach based on a distinction between exception and errors. Theoretical Computer Science, 46(1):13-45, 1986. [BDMN73] G. Birtwistle, O.-J. Dahl, B. Myrhaug, and K. Nygaard. Simula Begin. Auerbach Pub., New York, 1973. [BE86] D. Bert and R. Echahed. Design and implementation of a generic, logic and functional programming language. In Proceedings of ESOP'86, number 213 in LNCS, pages 119-132. Springer-Verlag, 1986. [Ber83] D. Bert. Refinements of generic spécifications with algebraic tools. In Proceedings of IFIP'83, Paris, pages 815-820, 1983. [Ber90] D. Bert. Spécification de logiciels réutilisables. Technical Report RR828-I-IMAG-116, LIFIA, Octobre 1990. [BG77] R. M. Burstall and J. A. Goguen. Putting théories together to make spécifications. In Proceedings of the 5th International Joint Conférence on Artificial Intelligence, pages 1045-1058, 1977. [BG80] R. M. Burstall and J. A. Goguen. The semantics of CLEAR, a spécification language. In Proceedings of Advanced Course on Abstract Software Spécification, number 86 in LNCS, pages 292-332. SpringerVerlag, 1980. [BHK90] J. A. Bergstra, J. Heering, and R. Klint. Module algebra. J. ACM, 37(2):335-372, Apr. 1990. 113 114 REFERENCES BIBLIOGRAPHIQUES [Bid89] M. Bidoit. PLUSS, un langage pour le développement de spécifications algébriques modulaires, Mai 1989. Thèse d'Etat, Université de ParisSud. [BL93] G. Bernot and P. Le Gall. Exception handling and term labelling. In Proceedings of TAPSOFT93, number 668 in LNCS, pages 421-436. Springer-Verlag, 1993. [B095] D. Bert and C. Oriat. A model inference system for generic spécification with application to code sharing. In Proceedings of TAPSOFT'95, number 915 in LNCS, pages 741-755. Springer-Verlag, 1995. [BR86] R. M. Burstall and D. Rydeheard. Computing with catégories. Technical Report ECS-LFCS-86-9, University of Edinburgh, September 1986. [Bur80] R. M. Burstall. Electronic category theory. In Proceedings of the 9th Symposium on Mathematical Foundations of Computer Science, 1980. [BW85] S. L. Bloom and E. G. Wagner. Many-sorted théories and their algebras with some applications to data types. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 4, pages 133-168. Cambridge University Press, 1985. [BW90] M. Barr and C. Wells. Category Theory for Computing Prentice-Hall International, 1990. [BW94] M. Barr and C. Wells. The categorical theory generated by a limit sketch, Nov. 1994. [Car86] J. Cartmell. Generalized algebraic théories and contextual catégories. Annals of Pure and Applied Logic, 32:209-243, 1986. [Coh65] P. M. Cohn. Universal Algebra. Harper and Row, 1965. Revised version 1980. [Cur91] F. Cury. Catégories lax-localement-cartésiennes et catégories localement cartésiennes: un exemple de suffisante complétude connexe de sémantiques initiales. In diagrammes, volume 25, pages 1-155, Llniversité Paris 7, Juillet 1991. [DN66] O.-J. Dahl and K. Nygaard. Simula - an Algol-based simulation language. Communications of the ACM, 9:671-678, Sept. 1966. [DR94a] D. Duval and J.-C. Reynaud. Sketches and computation (part 1): Basic définitions and static évaluation. Mathematical Structures in Computer Science, 4:185-238, 1994. [DR94b] D. Duval and J.-C. Reynaud. Sketches and computation (part 2): Dynamic évaluation and applications. Mathematical Structures in Computer Science, 4:239-271, 1994. Science. REFERENCES BIBLIOGRAPHIQUES 115 [Ehr68] C. Ehresmann. Esquisses et types de structures algébriques. Bulletin de rinstitut Polytechnique, Iasi 14, 1968. [EJ093] H. Ehrig, R. M. Jimenez, and F. Orejas. Compositionality results for différent types of parameterization and parameter passing in spécification languages. In Proceedings ofthe 4th International Joint Conférence CAAP/FASE, number 668 in LNCS, pages 31-45. Springer-Verlag, 1993. [EM85] H. Ehrig and B. Mahr. Fundamentals of Algebraic Spécification 1. Equations and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985. [EM90] H. Ehrig and B. Mahr. Fundamentals of Algebraic Spécification 2. Module Spécifications and Constraints, volume 21 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1990. [FGJM85] K. Futatsugi, J. A. Goguen, J.-P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Proceedings of Principles of Programming Languages, pages 52-66, 1985. [Gau84] M.-C. Gaudel. A first introduction to PLUSS. Technical report, Université d'Orsay, France, 1984. [GB84] J. A. Goguen and R. M. Burstall. Introducing institutions. In Proceedings ofthe Workshop on Logic of Programming, number 164 in LNCS, pages 221-256. Springer-Verlag, 1984. [GB90] J. A. Goguen and R. M. Burstall. Institutions: Abstract model theory for spécification and programming. Research Report ECS-LFCS-90106, Lîniversity of Edinburgh, January 1990. [GKK+87] J. A. Goguen, C. Kirchner, H. Kirchner, A. Mégrelis, J. Meseguer, and T. Winkler. An introduction to OBJ3. In Proceedings of the lst International Workshop on Conditional Term Rewriting Systems, number 308 in LNCS, pages 258-263. Springer-Verlag, 1987. [Gog73] J. A. Goguen. Categorical foundations for gênerai Systems theory. In Advances in Cybernetics and System Research, pages 121-130. Transcripta Books, 1973. [Gog92] J. A. Goguen. Sheaf semantics for concurrent interacting objects. Mathematical Structures in Computer Science, 2:159-191, 1992. [Gol79] R. Goldblatt. Topoi: The Categorial Analysis of Logic, volume 98 of Studies in Logic and the Foundations of Mathematics. North Holland, 1979. [GTW78] J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the spécification, correctness, and implementation of abstract data types. In R. T. Yeh, editor, Current Trends in Programming 116 REFERENCES BIBLIOGRAPHIQUES Methodology, volume 4: Data Structuring, pages 80-149. Prentice-Hall, 1978. [GTWW75] J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Abstract data types as initial algebras and the correctness of data représentation. In Computer Graphics, Pattern Récognition and Data Structure, pages 89-93, 1975. [GTWW77] J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Initial algebra semantics and continuous algebra. J. ACM, 24:68-95, 1977. [Gut75] J. V. Guttag. The spécification and application to programming of abstract data types. PhD thesis, University of Toronto, 1975. [Gut77] J. V. Guttag. Abstract data types and the development of data structures. Communication ofthe ACM, 6:396-404, 1977. [Huf92] J.-M. Hufflen. Proposai for GLIDER version 1.0: Principles and main features. ICARUS Technical Report, INRIA-LORRAINE & CRIN, 1992. [La\v63] W. Lawvere. Functorial semantics of algebraic théories. Proc. Nat. Acad. Sci.. 50:869-873, 1963. [LCW85] D. Lorge Parnas, P. C. Cléments, and D. M. Weiss. The modular structure of complex Systems. IEEE Transactions on Software Engineering, SE-ll(3):259-266, March 1985. [LS86] J. Lambek and P. J. Scott. Introduction to higher order categorical logic. Cambridge studies in advanced mat hématies, 1986. [LZ74] B. Liskov and S. Zilles. Programming with abstract data types. ACM SIGPLAN Notices, 9(4):50-59, 1974. [Mar95] A. Martins. La généralisation: un outil pour la réutilisation. thesis, INPG, Grenoble, Mars 1995. [MB70] S. Mac Lane and G. Birkhoff. Algèbre. 1. Structures fondamentales. Gauthier-Villars, 1970. [McL71] S. Mac Lane. Catégories for the Working Mathematician. SpringerVerlag, 1971. [MG85] J. Meseguer and J. A. Goguen. Initiality, induction, and computability. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 14, pages 459-541. Cambridge University Press, 1985. [Ori94] C. Oriat. Representing modular spécifications as diagrams. In Compte Rendu des Journées du GDR Programmation, Lille, pages 53-68, Septembre 1994. PhD RÉFÉRENCES BIBLIOGRAPHIQUES 117 [Ori95] C. Oriat. Detecting isomorphisms of modular spécifications with diagrams. In Proceedings of AMAST'95, number 936 in LNCS, pages 184-198. Springer-Verlag, 1995. [Poi92] A. Poigne. Basic category theory. In Handbook of Logic in Computer Science, Volume 1. Background: Mathematical Structures, pages 413640. Oxford Science Publication, 1992. [Ren91] G. Renardel de Lavalette. Logical semantics of modularisation. In Proceedings of CSL '91, number 626 in LNCS, pages 306-315. SpringerVerlag, 1991. [Rey87] J.-C. Reynaud. Sémantique de LPG. Research Report 651 I IMAG, LIFIA, Mars 1987. [Rey90a] J.-C. Reynaud. Putting algebraic components together: A dépendent type approach. Research Report 810 I IMAG, LIFIA, Avril 1990. Extended version. [Rey90b] J.-C. Reynaud. Putting algebraic components together: A dépendent type approach. In Proceedings of DISCO'90, number 429 in LNCS. Springer-Verlag, 1990. [Rey93] J.-C. Reynaud. Isomorphism of typed algebraic spécifications. Internai Report, LGI-IMAG, Avril 1993. [See84] R. A. G. Seely. Locally cartesian closed catégories and type theory. Math. Proc. Camb. Phil. Soc, 95(33):33-48, 1984. [SP77] M. B. Smyth and G. D. Plotkin. The category-theoretic solution of recursive domain équations. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 13-17, 1977. [SST92] D. Sannella, S. Sokolowski, and A. Tarlecki. Toward formai development of programs from algebraic spécifications: Parameterisation revisited. Acta Informatica, 29:689-736, 1992. [ST88] D. Sannella and A. Tarlecki. Spécifications in an arbitrary institution. Information and Computation, 76:165-210, 1988. [SW83] D. Sannella and M. Wirsing. A kernal language for algebraic spécification and implementation. In Proceedings of the îlih Colloquium on Foundations of Computation Theory, number 158 in LNCS, pages 413-427. Springer-Verlag, 1983. [SW91] T. Streicher and M. Wirsing. Dépendent types considered necessary for spécification languages. In Proceedings of the 7th Workshop on Spécification of Abstract Data Types, number 534 in LNCS, pages 323339, 1991. 118 RÉFÉRENCES BIBLIOGRAPHIQUES [TBG91] A. Tarlecki, R. M. Burstall, and J. A. Goguen. Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed catégories. Theoretical Computer Science, 91:239-264, 1991. [TWW82] J. W. Thatcher, E. G. Wagner, and J. B. Wright. Data type spécification: Parameterization and the power of spécification techniques. ACM Trans. Prog. Lang. Syst., 4:711-773, 1982. [Wan79] M. Wand. Fixed-point constructions in order-enriched catégories. Theoretical Computer Science, 8:13-30, 1979. [WBT85] E. G. Wagner, S. L. Bloom, and J. W. Thatcher. Why algebraic théories? In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 17, pages 607-634. Cambridge University Press, 1985. [Wir86] M. Wirsing. Structured algebraic spécifications: A kernel language. Theoretical Computer Science, 42:123-249, 1986. [Wir90] M. Wirsing. Algebraic spécification. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 13, pages 677-788. Elsevier Science Publishers B.V., 1990. [Wir94] M. Wirsing. Algebraic spécification languages: An overview. In Récent Trends in Data Type Spécification. I0th Workshop on Spécification of Abstract Data Types, number 906 in LNCS, 1994. Table de la première partie Introduction 1 Spécifications algébriques 2 Théorie des catégories 3 Modularité 4 Notre travail 5 Comparaisons avec d'autres travaux 6 Plan de ce mémoire 9 9 10 11 12 14 16 1 Motivation 1.1 Préliminaires 1.2 Spécifications 1.3 Composition de spécifications en LPG 1.4 Sommes amalgamées 1.4.1 Somme amalgamée de deux ensembles 1.4.2 Somme amalgamée de deux signatures 1.4.3 Somme amalgamée de deux spécifications 1.4.4 Syntaxe abstraite pour les constructions modulaires 1.4.5 Somme disjointe de deux spécifications 1.5 Spécifications modulaires d'anneaux 1.6 Isomorphisme de construction 1.7 Cadre général 1.7.1 Institutions 1.7.2 Terminologie et hypothèses 19 19 25 29 31 32 34 36 38 39 40 46 47 47 49 2 Graphes, catégories et diagrammes 2.1 Graphes 2.2 Catégories, foncteurs 2.2.1 Catégories 2.2.2 Foncteurs 2.2.3 Transformations naturelles 2.2.4 Adjonctions 2.3 Diagrammes 2.3.1 Catégorie des diagrammes DIAGR(C) 2.3.2 Colimites 2.3.3 Exemples de colimites 51 51 53 54 55 56 59 61 61 68 72 119 120 TABLE DE LA PREMIERE 2.3.4 2.3.5 2.3.6 2.3.7 2.3.8 2.3.9 2.4 PARTIE Adjonction (Colimc ~\Ic) Conservation de colimites Aplatissement Catégorie diagr(C) La catégorie diagr(C) est finiment cocomplète La catégorie diagr(C) est une complétion de C par colimites finies Conclusion Références bibliographiques Laboratoire LSR (Logiciels, Systèmes, Réseaux) Institut IMAG (Institut d'Informatique et de Mathématiques Appliquées de Grenoble) 681, rue de la Passerelle B.P. 72 38402 Saint Martin d'Hères Cedex 75 77 83 89 99 105 110 113