D IAGRAMMES F. C URY Catégories lax-localement-cartésiennes et catégories localement cartésiennes : un exemple de suffisante complétude connexe de sémantiques initiales Diagrammes, tome 25 (1991), p. 1-155 © Université Paris 7, UER math., 1991, 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 25 1991 CATEGORIES LÀX-LOCÀLEMENT-CÀRTESIENNES ET CATEGORIES LOCALEMENT CARTESIENNES : UN EXEMPLE DE SUFFISANTE COMPLETUDE CONNEXE DE SEMANTIQUES INITIALES. F. CURY Introduction Depuis ouelaue temps la loçique catégcricue est venue ren-forcer la place (considérable) occupée oar la 1 cgi que classiaue en informatique fondamentaleCette logique modélisation catégorique permet, satisfaisante de en effet, nombreuses une questions concernant aussi bien les types abstraits de données aue les langages fonctionnels de programmation, ou Bnaors le calcul formel ou la démonstration autcmatiaue... Dans le présent travail, nous nous intéressons particulièrement à ces modélisations qui mettent en des catégories A . M. S . muni&s SUB. d& construc CLASS. : 18 A te-urs ÎO , S8 (comme, u^r C 20 , 08 A 5Û œu^rs exemole, Introduction \-calcul,,,-). intéressons Plus à la orécisèment description encore, "mécanique" nous des nous sémantiques initiales de ces structures. Les constructeurs, dont une catégorie peut "être munie, produisent des résultats de deux sortes : - soit ils construisent des objets, - soit ils construisent des flèchesDans le premier cas, interprétant catégorie comme autant de types, constructeurs sont des lois Dans le second cas, les objets de la on dira que ces flèches comme des typantes* interprétant les fonctions (i.e. des "actions élémentaires" è. accomplir^, on dira que ces constructeurs sont lois des codantes fi. s. produisant du c o d e ) . Bien entendu- ces constructeurs indépendants : ils sont un certain nombre axiomes, dits de codants? et astreints d'axiomes config-uratiorim fixant ne sont aue généralement (dont. bien à rarement vérifier entendu- des associés à chacune des lois domaine et ccdomaine des flèches qu* elles construisent) . En toute généralité- sont des formules limiterons Question Horn à on pourrait (closes) l'aspect en supposant du l supposer eue ces axicmes dr mais ordre- "essentiellement de la aue des formules de que ces que ce ne sont alçébricue" nous (universelles—équationnelles). A ce point, il semble donc l'étude de Qu'une parcelle catégories munies de constructeurs ne soit du nous terrain (assez) bien connu des théories de Horn équationnelles. Autrement dit- pour décrire "mécaniouement" leurs sémantiques initiales, il semble au*il utiliser des "systèmes de réécriture conditionnelle" classi ques- faille assez Introduction On doit cependant apporter à cette façon de voir les choses trois restrictions notables. Tout d'abord, les constructeurs (qui apparaissent pratique) ne sont définis"; pas "partout dans la autrement dit, pour qu'ils puissent s'appliquer, ils doivent satisfaire à des clauses de définition* En deuxième lieu, on s'interdit des clauses de définition qui égalités obligeraient point à tester des de flèches : du de vue des langages fonctionnels de programmation, ceci signifierait qu'il faudrait exécuter "diverses parties du programme" — a priori "non étrangères" — avant d'espérer même en obtenir une compilation complète. Enfin, en troisième lieu, écrivant les axiomes (formules de Horn) sous la forme d'implications, mêmes raisons que leurs on interdit pour les "parties hypothèses" contiennent des tests d'égalités de flèches. On se trouve donc devoir "assouplir" une présentation "essentiellement constructeurs équationnelle" en une d'une catégorie "présentation munie de essentiellement relationnelle", en se plaçant dans le cadre suivant : - d'une part, présentation on choisit essentiellement (si c'est possible) une vérifiant les objets, dits équationnelle conditions suivantes : (i) on accepte tests des tests Cgéométriques0 d'égalité de configuration, entre i.e. on accepte des clauses (de définition des lois ou "hypothèses" dans les formules de Horn) d'égalités entre objets, (ii) on refuse des tests d'égalité de flèches dans ces clauses, - d'autre part, lors de l'assouplissement, on impose à la présentation essentiellement relationnelle de vérifier les conditions suivantes : (i) les clauses peuvent comporter des égalités d'objets, Introduction mais pas d'égalités de flèches, (ii) on accepte des clauses "de type relationnel" (entre objets ou entre flèches), (iii) les "parties conclusions" de ceux des axiomes qui ne sont pas de configuration devront être "de type relationnel". Ainsi, il faut commencer par autres que ceux "assouplir" les axiomes de configuration : ils n'imposeront plus des égalités mais seulement des réécritures entre flèches (qui ont des domaines égaux et des codomaines égaux). Ces 2-flèches. réécritures seront matérialisées par des Dans un premier considérée temps, on assouplit donc en celle d'une 2-catégorie, constructeurs (avec les mêmes la structure munie des mêmes et les mêmes clauses configurations), mais A^/mc des axiomes affaiblis. Dès lors, (fréquent) où il se pose un des constructeurs problème dans d'objets ne le sont arité-objets. Dans ce cas, des objets différents avoir été produits par une même loi typante, cas pas à peuvent cette loi ayant pris successivement en arité deux n-uples de flèches se réécrivant les unes en les autres. Il convient dans de telles situations, de considérer peuvent se réécrire suggérons de fléch.es, ces particulière que des objets travail, nous en d'autres : dans ce ma térialiser flèches l es réécrit constituant ures donc, d*objets une en sous-classe (contenant les flèches identités) de la de toutes les réécriture (entre objets). des classe flèches m De telles flèches seront dites de Le type de structure assouplissant (du point de vue de la réécriture) celui constitué par une catégorie munie de constructeurs est finalement de la forme : - 2-catégorie, - munie d'une classe de flèches particulières "de Introduction réécriture entre objets", - munie de constructeurs, dont sont icsir "essentiellement d'objets) relationnelles les clauses de on accepte aussi (les relations définition des égalités étant celles formules de de réécriture)", - ces constructeurs vérifiant des Horn universel1es (essentiel1ement) relationnel1es. La manière d'assouplir étant ainsi dégagée, il ne faut pas croire qu'il suffit de partir de la présentation essentiellement équationnelle donnée et d'y remplacer, dans les "parties conclusions" des flèches) par des (2-flèches) par des (1-)flèches assouplissement description serait pour =» le cas pour la structure i.e. construction, explicite de la = catégorie = (entre (entre objets) pour obtenir permettant ou un calcul, sémantique des théories de les et les réécriture convenable, (ou une mécanisation) de axiomes, un une ou une initiale. Ce équationnel les, cartésienne ou même fermée, mais c'est en général bien insuffisant. En effet, que recherche-t-on en assouplissant de la sorte (étant entendu que cet assouplissement a une sémantique i.e. que initiale constituée de termes)? Tout d'abord la suffisante complétude, chaque élément de la sémantique initiale "rigide" ait au moins une écriture (un terme) qui le représente dans la sémantique initiale assouplie. Ensuite, on souhaite que, si deux termes de la sémantique initiale assouplie représentent sémantique initiale reconnaître mécaniquement. passe lorsqu'on rigide, dispose de un même élément de la alors cela puisse se Idéalement, c'est ce qui se normales. A défaut, formes d'autres moyens moins contraignants, mais qu'on peut aussi envisager de mécaniser, permettent également de vérifier ce Introduction qui, en tout état de cause, est l'essentiel les termes connexe en (où question la dans sont connexion est une : à savoir que même composante matérialisée par des (l-)flèches de réécriture et des 2-flèches de réécriture). En général, complétude pour connexe la sémantique seulement qu'une condition suffisante de de la sémantique initiale assouplie sur initiale rigide soit il faut non "dédoubler", par réécriture., les objets et les flèches (i.e. les éléments aussi telle assurée, de la sémantique initiale) mais "dédoubler suffisamment" les lois et axiomes de la structure considérée, i.e. les consti tuants de la théorie. D'où de nouveaux constructeurs et de nouveaux axiomes, qui, bien entendu, deviennent totalement redondants si l'on rigidifie. Nous fournissons explicitement dans ce texte, à titre d'exemple considéré comme "générique", un assouplissement de la structure de catégorie "localement cartésienne" pour lequel la propriété de suffisante complétude connexe est vérifi ée. Au SI, on détaille complètement cet assouplissement. Autrement dit, on présente ("à la Freyd(1>") ce que nous avons appelé les catégories Au §2, on démonstration) explicite la lax-localement-cartésiennes. complètement propriété de (mais suffisante sans la complétude connexe de ces catégories lax-localement-cartésiennes sur les catégories localement cartésiennes : on peut donc y trouver une formalisation des considérations énoncées dans cette i ntroducti on. (i) in catégories, Propertx.es invariant vuthin in Eilenberg Festschnft, équivalence Ac. Press, types 1973. of Introduction Aux §3, 4. 5 et 6, on démontre, par étaoes successives, les résultats énoncés dans le §2- et notamment cette oropriété de suffisante complétude connexe- i. 1. Catégories lax-localement-cartésienne9 (LLCC) Catégories lax-localement-cartésiennes (LLCC) Définition 1 : Nous dirons aue (C^., =s=>) est une catégorie lax-localement-cartésienne (en abrégé une LLCC), ou encore que à objet final à choix homogène de c'est une catégorie lax—objet—Final) choisi et assoucli 'ou. crcduits fibres assouplis (ou 1 ax-orodui ts-f i br és> , si et seulement si : - C est une catégorie, dont les lois sont notées comme il est usuel : dont pour domaine. codom cour codomaine. oour identi id té (et. plus simolement- on notera souvent comp composition oour (et on oosera souvent 31 est une oartie de comD(v,x) = y-x >- FI (C) sont acoelées des il-)flèches (alors, les flèches de de réécriture par des flèches "ondulées" du type seront en général désignées par - "—$" est (de réécri 3t et représentées —>N~N~N~N^-> et elles des lettres grecaues). une relation'1' sur ainsi des 2 - f l è c h e s id(A) = id >. FI (C) tureï (en introduit notées indifféremment : e ' e => e' ou # S, Il • e' Pour définir la structure de LLCC, nous avons choisi les sens de réécriture qui nous ont semblé opportuns, tant pour les 1-fléches que pour les 2-fléches, mais on pourrait modifier certains de ces sens sans conséquence pour le r é s u l t a t r e c h e r c h é , i . e . p o u r l e t h é o r è m e du § 2 . i. Catégories lax-localement-cartésiennes (LLCC) puisqu'on oeut constater à la lecture des divers axiomes oui suivent GV.&. si e =£ e' - alors on a ^éce=sai '-e'Tvent dom(e) = dom(e') et codom(e) = codom(s') >. — C est munie lois des s tructurelles (relatives au lax-objet-final) : un et cte m telles que : un + la loi comme lax-111 " ou lax-ob ( un jet-finale est typante et sélectionne simolement un objet de 1 lax-objet-final)- (et appelé, bien entendu, + la loi cte ( cte lax-ConstanTE) comme est codante et configurée par V - : cte C est A « ctg munis des > » 1 lois s tructurelles (relatives lax—produits-fibrés) : PF , f , s , b , d et o , telles que : + la loi PF î PF lax-Produit-Fibré) comme est tyoante et configurée par : V C , noté PF ••. e1 .e ) PF(B i 4 2 e io au; 1. Catégories + les lois et f , lax-localement-cartésiennes s et (LLCC) b ( f comme lax-First ou lax-première-projection, s comme lax-Second ou lax-deuxième-projection, b comme lax-Bissectrice ou lax-troisième-projection) sont codantes et configurées par : f ,s5b PF comme lax-Préfactorisation) e s t c o d a n t e e t c o n f i g u r é e par : p < ,e ,e > 4 'V bit S<< v ^ ,e ^ Ve2> K. **, •-. 2 ..J I—> 3.* b(e .e 1 f(e -e 1 -.. , e 3 --. 3 .e 2 PF f ,f) k t ,^-M' > PF (2) Pour une présentation plus agréable, nous en fin de définition les axiomes «hf>, d'homogénéité. Cependant, nous ne nous sommes les utiliser; ainsi, ici, ce sont eux qui l e s l a x - p r o j e c t i o n s sont automatiquement é l é m e n t s de Jt <3> une Nous loi t aurions pu, pour plus simple, mais alors "contourner plus rigide. 13 les avons rejeté et < n b >J dits pas privé de assurent que trous". choisir 1. + la loi < c C a t é g o r i e s l PF,f 1 2 (où l'on a abrégé les s,f en f e' * < - , , « , >....-- i k, J Si J PF(e ,e ) i 2. v-> m <.--. — .—... — ... PF(e',e') b i 2 ± 2 » « 1 e' • c " i ••»>"" , - • • • « < • ; • • ; > 2 ^ ^ • i ' 15 - ! ^ . ' 2 - ^ 1. Catégories lax-localement-cartésiennes + l a loi pq ( p comme Réécritwre e s t c o n f i g u r é e par : et q (LLCC) comme "duale" de p ) e* PF *e2>- • 'V bp q 1 2 x:; f k s < X . e 4 , X . e2> b P F < X - e 16 l ,X-e ) ) 1. + la loi C a t é g o r i e s l a x - l o c a l e m e n t - c a r t é s i e n n e s (LLCC) pc ( p comme Réécriture est configurée par : et c y x^ • -> s s f) PF 2 PF : on a + axiome (,R, comp) (relatif à la classe on a 18 3t ) : suivent, 1. Catégories lax-localement-cartésiennee + axiome (=^, =) (relatif à la relation (LLCC) => ) on a "X S + axiome (=», =^) (relatif à la relation =* ) on a / + axiome (=*,comp) (relatif à la relation =» ) : on a e' 1 i 1 x (=*,comp) e' e' .e 2 2 19 ^ 2 1. C a t é g o r i e s l a x - l o c a l e m e n t - c a r t é e i e n n e s (LLCC) + axiome (cte,l) (relatif au lax-objet—final, en abrégé l.o.f.) : on a + axiome (cteFl> (relatif au l . o . f ) : on a cte ^SBBBBSSBSS -» • 20 cte(codom et (db) (relatifs aux l.p.f.) on a 22 1. Catégories axiomes on / (pf ) , lax-localement-cartéeiennes (p3) et (pb) (relatifs b p(e 3" -e > 2 S < e ,e 1* -e , e 1 -e * PF ^ f(e -e 1 3 f ) 4 ) s(e -4 -e 1 PF 1 -e ,e a' 2 .e 4 ) ,e 3* -e 2 ) 4 1. Catégories + axiome (p' c o > COTno mp lax-localement-cartésiennes (relatif aux l . p . f . ) (LLCC) : on a PF(e - e - e , e - e . e ) 1 3 5' p(e .e , e K 1 3' 2 4 6 -e , e , e > 2 4" 3' 6 'Pcomp* ! PF 2 1" 2' .e ,e .e > 5? 3 4 6 4- (relatif aux l . p . f . ) : on a e e d 1. C a t é g o r i e s lax—localement—cartésiennes (LLCC) + axiome (p,f,s,b,d) (relatif aux l.p.f.) : on a PF(d,\) ,f(d>,\) s(d P) PF PF d> 2 *' PF PF \ \' ,M MV PF r .,X>{ ... x s ;f X' l -, s p'r s,f> t 26 (relatifs aux l.p.f.) on a e i -e 2 (cfb) PF PF PF X' 1 e -e 2 1 2 PF) 1 (Cff ) Cf * ,X,X'> PF (où l'on a abrégé s les en f ,*> , les en 1. Catégories lax-localement-cartésiennes (LLCC) + axiomes 1.p.f.) <» < a > e t <b> (relatifs aux : on a B <- b B 1 bb> 7-r— P F < e ' „ e ' ) f < e 1' ,' e '2) i 2 <f> p^ , * 2* 2 ^•*-V PF 5(e',e') A 2 1. C a t é g o r i e s l a x - l o c a l e m e n t - c a r t é s i e n n e s (LLCC) + axiome (pfl,d) (relatif aux l.p.f.) : on a Pt, PF(e',e') d e e' -i- axiome (pfl,p> (relatif aux l . p . f . ) : on a PF >p„, i 2 1. Catégories + axiomes <, 1.p.f.) lax-localement-cartésiennes <a> et <b> (LLCC) (relatifs aux : on a ba> X A R P« r f> q PFa> > 1 2 -X.e,)'/ 1 2 ,X-e ^- ) 1. Catégories lax-localement-cartésiennee (LLCC) + axiome (pq,d) (relatif aux l.p.f.) on a d + axiome (pQ,p) on (relatif aux l.p.f.) a PF ,\-e »e i -e , \ - e .e ) ai 2 4 ,e^> 2 ^ s. (pq,P> P , ( X ' e i - e 3 ' ^ Z - V p ^ ±- 2 ' a ' 4 PF ^ sp f > st < X -e . X ) s 2* <—^V~%~N~N^> 2 # PF 2 .f(e 2 —-^N~X^ ,f) ,X>) 1 • 1. + axiome C a t é g o r i e s l a x - l o c a l e m e n t - c a r t é s i e n n e s (LLCC) (pcîlp) (relatif aux l . p . f . ) : on a PF s (relatif aux l . p . f . ) : on a P R e e i ' e 2 > •.. e 1 .- -.2 : \l :>x !P PF rx axiome (h 8 ) on (relatif à l'homogénéité des l.p.f.) des l.p.f.) a "-L.X PF "L. X U * P F < X ,X ) 1 2 .r" x 33 1. C a t é g o r i e s l a x - l o c a l e m e n t - c a r t é o i e n n e s (LLCC) Nous définissons la rigidification maintenant de la structure de catégorie lax-localement-cartésienne. Définition 2 ; Nous rigide - qu'une LLCC (C,,ft,s«*>) id(C) , où est si et seulement si : X. est l'ensemble des flèches l'ensemble - dirons Ob(C) la relation C décrit des objets de C , as> est l'égalité entre flèches de C . Un certain nombre de conditions (axiomes et même existence de lois) requises par la définition d'une LLCC se simplifient notablement et d'autres deviennent redondantes dans le cas d'une LLCC rigide. La proposition suivante caractérise, dans cet esprit, les LLCC rigides. Proposi t i on 1 : Une catégorie C est de LLCC rigide si : - est C et munie des un , de si cte , seulement lois munie d9une h 29 d et cas 9 structure : PF , f» même configuration que s - les axiomes suivants + axiomes ils e t (d restent remplaçant* de réécriture + axiome pour toutes sont (cte.,1), comp> (cteFl) , : (df ) • (da) , (pf ) » (pa) » : analogues bien vérifiés à. ceux entendu^ par des de ^mm^* la par définition "=" et i les Cen y flèches identités^» (cône) ; flèches e1 et e2 de même codomaine* on a : e1.f = e2.s 1. + axiome pour toutes C a t é g o r i e s l a x - l o c a l e m e n t - c a r t é s i e n n e s (LLCC) (p,f,s,b,d) ; flèches et e± e2 de même codomainet on a : p(e±,e2,f ) = id , + axiome pour toutes (pc,p) : flèches e± et e2 consécutives, on a : p(e19id,e2,id) = e 2 , + axiome pour toutes (p«> •' flèches et et e2 de ntéme codomaine* p) ) et les axiomes (t1) et (t2) deviennent tous deux : t(e„id,id,id,id) = e . Il en est de même de la loi cf et des axiomes (cff) et (cfs) pour des raisons du même genre (et l'axiome (cfb) est alors une conséquence de l'axiome (p c ,p)). Quant aux lois pfl , pq et p c , elles doivent être à valeurs dans l'ensemble des flèches de réécriture i.e. dans l'ensemble des identités et elles sont déterminées (notons, à propos de donc entièrement p c , que, si et et e2 sont deux flèches consécutives, on a bien : PF ) . Et, pour terminer, signalons que les autres axiomes qui "disparaissent" sont, en fait et bien entendu, trivialement vérifi es. Fin de la preuve. On remarquera que, par rigidifi cation, on passe de la présentation essentiellement relationnelle précédente à une présentation montrer essentiellement que cette équationnelle. dernière est Nous équivalente allons à la présentation essentiellement équationnelle (plus standard) des catégories localement cartésiennes. Précisons ce que nous entendons exactement par "catégorie une catégorie 1ocalement cartésienne". Définition 3 : Nous dirons que localement abrégé : est cartésienne seulement si à choix C de (en est une LCC) si et est une catégorie à objet final choisi et produits fibres c'est-à-dire vérifiant, pour toute flèche f(e,id> = id et 38 d' homogène, qualifié e s, d : : f, que dans 9 le cas LLCC* (cône), (df ) , (cte,l), (cteFl) , (Pcomp** (d (p,f,s,b,d), structure de LLCC rigide Ccf et d une axiomes comP>» structure (hf) et la proposition des lois p, (ds) , (pf ) , de la ÎJ> sont et cte (hs) vérifiés. Preuve. Prouvons d'abord accompagnée que de celle la donnée des axiomes un (cte, 1) et (cteFl) est équivalente à la donnée d'un objet final. Si 1 est final, il détermine une loi (celle qui associe, à tout objet vers un et une loi cte A , l'unique flèche de A 1 ) . Par unicité, les axiomes (cte,l) et (cteFl) sont alors vérifiés. Réciproquement, supposons que les lois un et cte sont données et que les axiomes (cte,l) et (cteFl) sont vérifiés et prouvons qu'alors l'objet final. Soit donc un objet 1 (déterminé par A . La flèche 39 cte (en vertu de l'axiome (cteFl) ) et donc : c = cte et de id(dom(e)> , ce qui équivaut à la satisfaction des axiomes (df) et (ds) : et, pour tout quadruplet convenable, on (e1,e2,e3,e4) de configuration définit p comme étant le "crochet" (il existe bien) de e3.f * (d comp ) et composition des conséquences de avec les l'unicité (p,f,s,b,d), on projections d'un les voulues, crochet (et de 1'homog en é i t é éventuel1ement). Réciproquement, supposons ( b ,) p d et que les lois PF , f , s , sont données et que les axiomes (cSne) , éO 1. C a t é g o r i e s l a x - l o c a l e m e n t - c a r t é s i e n n e s (LLCC) (df), (d s ), (pf), (p s ), (pcomp), (dCOTnp) et (o,f,s,b,d) sont vérifiés et prouvons qu'alors C est à produits fibres (déterminés par les lois PF . f et s ). Soient donc deux flèches et et e 2 de même codomaine et soient xt et x2 deux flèches, de même domaine noté A , vérifiant : e On note e 2 " *2 " la valeur commune de ces deux composés. On montre alors (grâce aux axiomes (ps) et que la flèche x A d y i •x i = PF (pf) , (df ) , (da) ) définie comme la composée suivante : - PF(«i-*t* •*•*»> p < e i ? e 2 ? X i ? X 2 ) ^ PF-x = x 2 b -x' (en posant fi = p(et,e2,f (e1,e2) ,s(e1,e2) ) ) = ^-p(b(e1,e2) ,b(e19e2) ,x' ,x' ) -d(b . x' > (en vertu de l'axiome (d comp ) ) = /v.p(e1.f -x' ,s(e1,e2) . x' ) d sont automatiquement vérifiés. Or on déduit aisément l'axiome (pc,p) des axiomes (pf) et (hf) et l'axiome (p«) des axiomes (pf) et (pa) et de l'unicité d'un crochet. Fin de la preuve. Il découle donc de ce théorème que les axiomes (pcmp) et (p ) étaient redondants dans la caractérisâtion d'une LLCC rigide donnée dans la proposition 1. 42 2. 2. La s u f f i s a n t e complétude connexe d e s LLCC sur l e s LCC La suffisante complétude connexe des LLCC sur les LCC Considérons maintenant les trois catégories suivantes : - d'une part, la catégorie graphes orientés QJLCC , puisque toute LCC s'identifie à une LLCC rigide. Bien entendu, nous disposons aussi des foncteurs d'oubli "graphe orienté sous—jacent" : <5 canollcc(G) un graphe QjD(llcc(G)) orienté, on peut lui associer deux relations d'équivalence : - l'une, R o b , sur l'ensemble 44 Obdlcc(G)) des objets de 2. La s u f f i s a n t e complétude connexe d e s LLCC sur l e s LCC la LLCC qu'il engendre, - l'autre, de Rfl , sur l'ensemble FI (11 ce (G)) des flèches llcc(G) . La relation d'équivalence R ob entre objets est aisée à expliciter : - les objets si A et A B et B vérifient sont connectés flèches appartenant à A R ob B si et seulement par un zigzag constitué de (nous dirons un tk—zig&ag) , Jfc ce que nous pouvons représenter comme suit : A Rob B il existe A • t> B On montrera plus loin (cf §3) que : Proposition 1 ; Tout tR.-izig'zag peut "co-confluence" locale} en 3t-izigzag constitué 9 d une seule un 99 "branche ^. se modifier C par simple Cqui dit* on a : Autrement est A Rob B il existe A Maintenant d'équivalence la classe X nous B allons construire la Rfl , tant en utilisant la relation relation => que (il faut en effet s'attendre à ce que des 45 2. flèches La s u f f i s a n t e complétude c o n n e x e d e s LLCC sur l e s LCC équivalentes n'aient pas nécessairement des n'utilise la domaines et codomaines égaux). Procédons par étapes. Etape 1. Dans un premier relation d'équivalence temps, Rfll on engendrée par la que relation as* . Autrement dit, on a : - pour que deux flèches f,f : A 1 » B * Rfll *' ? ^ "Faut et il suffit qu'elles soient par un 2—zigzag 9 i.e. un zigzag de 2—flèches, ce que l'on peut représenter comme suit : vérifient reliées f Rfll f f'= f Etape 2. On tient compte maintenant des "identifications" d'objets dues relation Rfl2 à la classe entre flèches &. . Ainsi g et g' on définit une qui n'ont plus nécessairement mêmes domaines et mêmes codomaines mais qui sont cStés d'un carré (non nécessairement commutatif) tel que : 46 2. La s u f f i s a n t e complétude connexe d e s LLCC sur l e s LCC ot g' or Et, - dans ce c a s , on a : g Rfl2 g ' s i e t seulement s i a l o r s l e carré précédent a.g et qui s u i t g'.a' , a - g R f l l g' - a ' "se r e m p l i t " ; d'un 2-zigzag ce que l ' o n r e p r é s e n t e par le reliant &\$&—carré : a -Uta g' En résumé, on a donc g Rft2 g ' g' a' Etape 5. Maintenant on d é f i n i t Rfl3 = Rfl relation d ' é q u i v a l e n c e engendrée par Rfl2 comme é t a n t la Autrement dit. on a : - pour que deux flèches il faut et il suffit h et qu'elles 47 h' vérifient soient h Rfl h' , connectées par un 2. La s u f f i s a n t e &J$*—zigzag (i.e. complétude connexe d e s LLCC sur l e s LCC un zigzag de i^./SS—carrés) . ce que l'on peut représenter comme suit : h Rfl h' il existe h' tf * On montrera plus loin (cf §3) que : Proposition 2 : co-confluence Cqui est Tout locale constitué 9 v&Jlb-zigzag peut se modifier Cpar notamment} en &\;}*-zigzag simple d une seule "branche"}. on a : h Rfl h' il existe -t,* * * 48 un Autrement dit* 2. La s u f f i s a n t e complétude connexe d e s LLCC s u r l e s l^GC Comme annoncé dans l'introduction. le but de ce te;;ta est d'établir le théorème ci-dessous : Théorème (suffisante LCC) : Si les (i) est G lois la catégorie engendrée complétude un graphe orienté, de la catégorie sont par Rob Csur Fl(llcc( } et RfL Csur par conséquent de est par cartésienne = lcc«Ê) > cartésienne librement La flèche canonique d9adjonction i.e. que engendrée propriétés par est la G. : suivantes » lcc(G) les (iv) (complétude sur les objets) A' € Ob(lcc«G)) , structure llcc <= FI ( l e c (G) ) , il Icc'G)ï existe : canc(G) (x") = x' , (vi) (connexité de la comolétude sur les objets> pour tous A" > B'' il existe A" Cvu (vii) B" la proposition 1} * (connexité de la complétude sur les flèches! pour toutes x" * y" «s FI(1lec «G)> cano(G)(x") = cano(G)(y"> il CTJ*U (viii) (complétude existe lÉ.* j£..3a La propos i t ion 2} * lais de pour les 5Û la structure 2. La s u f f i s a n t e complétude connexe des LLCC s u r les LCC catégorie) pour toutes que y' . x' e FI(lec(G)) consécutives i.e. telles : dcm(y') = codom(x'> , il existe y" * ?Î " ) , po^ir tout A' ^ Ob(lcc(G)) , il existe A" «s Ob Cl l e c «G)? t e t cite : id(A') Cil résulte en lice(G) Sstrict" est * et = cano(G) (id(A">> particulier ce point catégorie quotient* et cano (G) est une que de le (/iiiî même "quotient "y passage fondeur que au quotient"}* (ix) (complétude pour les lois de la structure local emenl cartésienne) pour toutes x' , y' Paris, Voir 1965. C. E h r e s m a n n , m Catégories 51 et Structures, Dunod, 2. La s u f f i s a n t e complétude connexe des LLCC s u r les LCC PF(x'.y') = eano(G) 'PF) et b(x',y') = cano(G) 'b(x".v") ) > pour toutes x' , y' * v' * w' <= F l ( l e e ( G ) : telles que : codom(x'} = codom(v') > domdi' ) = codom(v') il existe x" , y" et dom(y') = codom(w') , telles , v" , w" e FI (1 lec (G)) que : p(x',y',v',w') = cano(G) (o<:î",v",v".w"n , et* bien entendu pour toute tel le que : x' € FI (lec (G) ) , il existe x" € FI (11 ce (G)) : d(x'> = cano(G) pour tout A' tel cte(A') et* enfin > il existe A" e 3b (1 l e c ( G ) ) = cano(G)*cte(A"}) , : 1, ,^ l c c ( G )v = cano(G)(l., .^. llcc(^;) . Les paragraphes suivants sont consacrés à la démonstration de ce théorème (et des propositions précèdent). 52 1 et 2 oui le 3. 3. P r e u v e s de s i m p l i f i a b i l i t é des zigzags Preuves de simplifiabilité des zigzags Prouvons tout d'abord la proposition 1 (§2), i.e- que tout Jt-zigzag peut se modifier en un Jfc-zigzag simple. Preuve de la proposition 1 (§2). Il est clair qu'il suffit de prouver le résultat pour les ^-zigzags constitués de deux branches. Soit donc un tel #,-zigzag : A • # # D En v e r t u des axiomes (hf) et (hs), on a : • D On a donc m o d i f i é l e ^ - z i g z a g donné en un J^-zigzag A # simple # D a - f Fin de la preuve. En vue d'établir la proposition 2 (§2), nous prouvons maintenant un groupe de trois lemmes (de translation flèche le long d'un ^-zigzag). 53 d'une 3. Lemme 1 : Si Preuves de s i m p l i f i a b i l i t é des zigzags l9 on a B \ / Kïy x o w / et PF o PF .w > 2 2 ~> • = a alors il existe une flèche d2 telles s élément X. et une flèche que : > B < f -> A «- b • < -...-..---.---.^.--.--^--.---.---.--^--.---.---.------^---.-fl i o' i' o P f l < V i ' V 2 ' W i ' W 2 > = a =a et 34 3. Preuves de simplifiabilité des zigzags d R^ d 2 » f -(1^((1,¾) = ^ A <-» C <- O o une flèche ,w ) n-1 £ n élément de f O n que : -> B «- o ,v ,w n-1 PF„=), à deux déduit, de 3. Preuves de s i m p l i f i a b i l i t é des zigzags PF O PF w o> -» A <- b f r" s s W oO' oo> r s <-.-.-.-.-.-.-.-.-,. et d Rfi d * f.d.Ç . Toujours en vue de prouver la proposition 2 (§2), nous sommes désormais en mesure d'établir un lemme qui permet de construire une sorte d'extension de la loi 58 PF à certaines 3. P r e u v e s de s i m p l i f i a b i l i t é des zigzags flèches (convenables). Lemme 4 : Si l9on a : alors il existe une flèche 1 telles que : Ç élément de 31 et une f PF . 1 tfyfc l ± . f < i , j ) -C > s .1 i*yb l 3 . s < i , j ) -C > b et (cône2) ) : l 2 b && g - l f f d . j ) et l2.b%* h.l9.s(i,j) . On peut appliquer le lemme 3 à ces deux 2—zigzags : l2.b%* g.lt.-F et l2.b là;* h.l3.s> (dont le codomaine est bien Il existe ainsi une flèche d PF<12.b. C élément de 3t et une flèche telles que : PF<1 .b> PF,h.l .s> 2 (notamment) 1 3 # : f < g - l t . f < i , j ) , h . l 3 s < i , j>>-d &%& f < l 2 - b < i , j ) , l 2 - b < i , j ) ) - d - C s)-d «%fc s < l 2 - b < i , j ) , l 2 b < i , j > > . d - C b)-d tfyfc b)-d.Ç Définissons 1 comme l a c o m p o s é e • aussi 1 Et prouvons que la flèche > . Ç p l1.f)-d-C =» l 1 f C (en vertu de l'axiome (df) et car d = d C 61 de 3L 3. Preuves de s i m p l i f i a b i l i t é des zigzags et s ^ j o - i tfyfc y.s comme aux représenté axiomes (hf> par et le diagramme C - ci-dessous (obtenu grâce (ha> > : PF »s<^,^> * 7* -f "V .^•î ot *M w 7\ "i R. à'.S' ot' *M *.£i * s<0',y'> PF<^?' ,r'> Définissons les flèches, é l é m e n t s de « = a.f C : et 77 = <5.s L S "fi que l'ensemble des composantes connexes de flèches de llcc( # x autrement dit* si y lr on a : id r^ alors X.id on a : comp(y,x, id, id) Rfl y-x . Preuve. On a s(x,id) *£.£• x.f(x,id) (en vertu des axiomes (cônet) et (cSne2) ) , et donc : comp(y,x,id,id) = y.s connexes • ' on a : dom R ob dom> t < x , a , a ' ,/3,/?') On a a l o r s : comp ( y , x , f ? , a ) = y./3-s . f , f < x , a ' ) ) (car f y.t(x,ot,a' ,/?,/?') (en vertu de l'axiome (t±)) . On montre de même (grâce à l'axiome (t2)) que : comp Rfi y-t(x,a,a',/?,^) , ce qui achève la démonstration. Fin de la preuve. Ce lemme 1, qui qualifié de lemme est de tout à fait essentiel, peut "être contournement. Il exprime que, si, a priori, il n'est pas possible raison du "trou central") dans le dessin suivant : 69 (en •4. La c a t é g o r i e des composantes connexes y,x,/?, a) comp (x, y,/?' , a' ) f de "glisser par connexité" directement de comp(y,x,/?,«) comp C'est l'existence s'y rapportant) Lemme 2 : Si même de l a l o i t (ainsi qui nous a p e r m i s de l e l9on a : m T, >m 70 que l e s faire. axiomes 4. autrement dit* La c a t é g o r i e des composantes l9on si connexes a id w" alors y on a : comp • *„* et donc* vérifient si les flèches w w Rfl w' , alors et ont w' même codomaine on a : y . w Rfl y . w ' . Preuve. On a : y • w Rf i y - w - 6 6 € 31 ) •*•£• y-r-w" w.6 lâ^i y.**" ) (car (car et de même : y.w' Rfl y. Y9 •*' Le lemme 3 permet alors de conclure. Fin de la preuve. Lemme 5 : Si l9on a : -> • \(*' x' et donc* en particulier a' * si l9 on a 72 x Rfl x' , alors on a et 4. La c a t é g o r i e des composantes como - : . et 4. La c a t é g o r i e d e s composantes connexes fet-ÂI >Ot >CT et donc* en particulier* 6 ^ si l9on a y Rfl y' * alors on a comp • On a donc : comp(y,x,f3,a) Rfl comp(y,x nfî. f (a, a' ) ,a' -s-s • x et v é r i f i a n t On a a l o r s des > • y en o u t r e composantes et x Rfl x ' • et connexes -,—» # x' y Rfl y' . —> # y' : y.x Rfl comp) , alors et dom > / R et C f l = FI ( l l c c « D ) ) nous pouvons donc /Rn légitimement ' poser la définition ci-dessous et affirmer alors la proposition oui la suit. Définition 2 : Si un x e Cfl , alors Cet cela a bien sens} et codom(x) = codom(x) . Cet cela dom o-ù (a,/?) les objets langage* est une connexion codom) et *alors , alors codom(x) on a = codam(x) on a : xd si ccdom(x) = A on a ; Fd<Â) . x = x et x.FdCB) = x . Preuve. P^r hypothèse, on a : x : B' > A' On a donc : Avec ÊF = 3 et A7" =  - id ^ et 6 telles que : • ot Par définition, on a z.(y.x) = z . -> • • V f , (hs) , (cSne t ?, (c3ne 2 ) , ps) x (oDtenu grâce et = y Vf £ à ^ a -> « < * > « > > PF f > ) P F ( x , a . f > - s ( x , a - f ) ) ? on a : v Rfl w . Dans ce qui suit, on utilise é v i d e n c e dans l e s deux d i a g r a m m e s On a d ' u n e p a r t les propriétés mises ci-dessus. : v Rfl dcAr r-v Y « & > = ^-s ) - s ( x , a . f (,'?,f ( y , ? ) ) ) *:p y.f (y,^) s<^?,f < y , ^ ) ) - s ( x , a . f > - s ( x , a . f > ) 4 = y . / ? - s < x , a ) . p ( x , ci, i d , f llcc(G) /R cano( X_ des 5, on montre composantes aue ccnnexes la catégorie de 11CC ). ) , qui PF - élargissent ftcut cemme la loi crès", au §4« la llcctG) ) . 'Vr et b Définissons tout d'abord ces lois (ainsi que d'autres, aussi "naturelles", dont on verra l'utilité plus l o i n ) , Définition 1 : Si 1'on a : « x > # • a on pose successivement : - PF) 87 < v # S. L a c a t é g o r i e des composantes connexes est f(x,y,a,/?) = f = s(x,a.s(y,/3>) , b = b f i.a) ,y) 88 i (x,y,a,/?) »(/î.s(x,a) ,y) 5. - La c a t é g o r i e PF30:,y,a„/?) f3:, a ) , s < y , / ? > ) = +(s(x.a),5(y,/?)) , **# s3(x,y?oi,/?) = 5 ( s ( x , a ) , s ( y , / î ) ) , *\# b3<;:,y,a,/?) , = b < s < ; < . a ) , s < y , /?> ) est une LCC , comme représenté ci—dessous : a PF vertu de s s ,s (Remarquons ft = s < s ( x , a ) ..s(y.,?)) PF f s et (p ) ) : PF • ) /> • - ! - i - > # X 2 que : PF( e ± . \ ± , e 2 - X 2 ) Rob PF< e x - e 2 ) f R o b PFis'^sp f(e' e') Rfl -F , » 1 Rfl une LCC , 2 b,=> &&—zigzags 2-ziçzags f~\ %_ 1 de : -* c X * cas assure de qu'on peut toujours longueurs différentes à des #^-zigzags de longueurs égales). On a alors le diagramme ci-dessous (obtenu grâce à l'axiome (f) : PF 1 f 2 nd ^l -> • A PF(e ,e ) • 1" f < e 2 i'e2> W^a'»? .id PF ci-dessous Rfl b3 » PF Rob *\t «\# P Onr e uav e . l e J** PF2 ) Rfl f ( x , a . s < y ? / ? ) ) (en v e r t u On o b t i e n t ainsi d u lemme que 1 et car f• < ly on a si x v -. • < > • idV alors • yid on a PF # v: « alors on a : *Vr *\r *V dom(f et codam = codcm(x) R ob codom(y) Montrons maintenant que les lois sont compatibles awee les relations PF , f . s de connexion et b (entre objets et entre flèches). Pour ce faire, on commence oar une SLiccession de lemmes. Lemme 4 : Si l9on a : 95 5. alors La c a t é g o r i e des composantes connexes e s t unw LCC a ft a.' p' PF(x,y,a./?) Rob PF b(x.y,a./?) Rfl b ( x . y . a ' , ft' ) . on a : , , Preuve. On a : f . f î ? t ( y , / ? , / ? ' , a , a ' ) ) On o b t i s r t ainsi que : fm • autrement alors dit* z" si l'on a on a PF PF Rob PF Rfl f h'reuve. Le lemme 5 a s s L i r e même, que que PF< ; : , ^ . z " ) PF Rob Pha • >or s l'on a : x R f l x' et y Rfl y' * codom(x) R ob codom(v) Cet donc alors codom(x') R ob codam(v') } * on a : PF(x,y,a.f?) R o b PF (x ' , y' ,a' *ft' ) , f(x,y,ot,/?) Rfl f (x' ,y' ,a' ,ft' ) * s(x,y,a,/?) Rfl s (x' ,y' ,a' ,/?' ) , b(x,y,a,/?) Rfl b (x ' , v' ,a' ,/?' ) . Cette proposition 4, qui est tout à fait essentielle, peut être qualifiée, comme précédemment, de proposi tion de contournement. Cette proposition exprime que, si. a priori, il possible n'est pas (notamment en raison du "trou central") de faire directement "alisser oar connexité" le lax-produit fibre PF composantes \a' ft' connexes { -f # x y w on pose successivement : - p> f « ci—dessous : PF(/?.s) , v - w ) < x , v , v , w , a,/?,^,6.£:,C) p 2 p(f?.s . s< w. f ( y , ft) > ) ... ^ < x , y , v . w . a,ft,rfà.£.^'> p p ( s < x , a ) , s < y , ^ ? ) , s< v , -F < x . a ) ) , s < w. f < y . ,?> ) ) r P F ( s ( x , a ) , s ( y , / î ) ) -, s> s< v , f < x , o 0 ) :f(v,-f(x,a)) i f > s s 3 •F w w (Les flèches, dont q u ' e l l e s sont dans Par souci aussi il est indiqué dans cette définition 31 , y s o n t en v e r t u de l ' a x i o m e d'homogénéiser les notations, nous (hf) ) . noterons : P < X , y , V,W,Ol, Etablissons ft^YnÔn^n tout Ç) = d'abord suite. Lemme 9 z Si l*on a : 108 P± < << J Y ? v , W , Ol, ft, Y ? <5 ? ^ ? C > deux lemmes Lit il es pour - la 5. La c a t é g o r i e des composantes connexes est une LCC X 4 alors 4 2 on a : p ( e± . \ 1 , e 2 • X 2 , e 3 . X 3 , e 4 - X 4 ) R fL p < e ± , e 2 , X ± . e 3 , X 2 . e 4 ) Preuve. Le diagramme ci-dessous (obtenu grâce aLix axiomes o(e PFi^ 4 -e 2 -X 3 ,e 3 ,X ,X 3? 4* -X 4 1 1 3 -\ 2 e ) 2 4 —. p(e =- 1 .\ 1 .e r 2 .\ 2 2 2 ) 4 ) 4 S P F < e -X - e , e 1 id! ,e 3 , e ^ 4 PF PF RfL p< s ;- , e ; - , e ; - , e ; - > Preuive. Il suffit (en résultats dans raison de le de 2 - z i g z a g s cas l'axiome (=^,=)) d'établir les simples, i.e. la dans s i t u a t i o n SLÛvante : /~T~^ Le diagramme ci-dessous (obtenu grâce à l'axiome établit alors le résLiltat voulu : 110 (pfL,p)) S. La c a t é g o r i e des composantes connexes est une LCC p < e ; > e 2 > e 3 ' e ; > PF P F ( e ' . e ' ) >p„, PFve? p P F ( e " . e " ) 1 4 2 Fin de la preuve. Etablissons maintenant relatives à la loi Lemme 11 : Si l'on P* n D les (et aux lois premières p2 et propriétés o3 ) . a es m • •n <- w alors on a : p p ( s < x , a ) , s ( y , /?) , s < v , f < x , o 0 ) , s ( w . f ( v . / ? ) ) ) ^ \p ( a , s < x , o t ) - s ( v , f ( x , a ) ) , s ( y , / ? ) - s < w , f ( y , / ? ) ) ) p , s ( v , f < x , a ) ) . s ( w , f ( y , / ? ) ) ) (en r a i s o n d u lemme 10 e t des axiomes (c3ne±) et (cSne2) ) Rfl o ( x , a . s < y , / ? ) , f < x , a ) . s ( v , f ( x , a ) ) , s ( w , f ( y , / ? ) ) ) (en r a i s o n dui lemme 9 e t car f(x,a) <= 3t ) Rfl p ( x , a . s < y , / ? ) , v . f ( v , f < x , o 0 ) , s < w , f < v , f ? ) ) ) (en r a i s o n du lemme 10 e t des axiomes Rfl D ( x , a . s ( y , / ? ) , v , s < w , f (en raison d u lemme 9 e t car = p ( x , y , v , w , a , / ? , ^ , 6 , ^ , Ç) Par conséquent, on a o b t e n u étant et (c3ne2) ) (Y,/?))) f£ C LCC a & ïï\ w alors que il existe des /lèches x * v * v et w telles : N/ V x Rfl x , V y Rfl y , V v Rfl v , w Rfl w et V **» p) (en v e r t u dLi lemme 10 e t des axiomes Rfl et (cSne 2 ) ) p(x,y,v,f(y,id)-s(s)) (en v e r t u du lemme 10 e t des axiomes (c3ne ± ) et (c3ne2) ) Rfl o < x , y , v , s < w , i d ) > (en v e r t u du lemme 9 e t c a r f • alors # <- on a : 114 w La c a t é g o r i e des composantes connexes est une LCC dom(p(x .y?v,w.a,/9,^.<5.^,Ç)> Rob PF ) , s : a : a.s . f < y , / 3 ) ) On a a l o r s = w . : p R (t2)) que Fin de la preuve. l'on : n p, C) Preuve. On a : p < x , y , v , w , a , / ? , / , 6 . ^ : . C) = o(x,a-s) R f l p < x , a - s ( y , / ? ) , v , o < y , / ? , w, i d ) ) ( e n v e r t t i d u lemme 9 e t car pc) f ( f ( y , / ? ) , f < y , / ? ' ) ) , v . c f < y , w,/?,/?' ) ) d u lemme 9 e t car f' - m", w) Rfl o(x , y, m", w, id. id , 77' .i d.id,id) Le lemme 12 permet alors de conclure. Fin de la preuve. x • •~ e t cÊonc, si les /lèches m et m' véri/ient m R fl m' , alors on a : < y — ont même codomaine p dit* idl- m conclure. preuve. Lemme 19 : Si autrement de « a l9on si # n ZL • a : "lid • idF" * - > "I77 • 120 id id, <- • R fl p • -> # _ • « v on a : o<77-z",y,m,n) Rfl p<7j' -z",y,m,n) Preuve. On établit ce lemme en s'appuyant sur les lemmes 13 et 13, comme on avait établi le lemme lemmes 14 et 12. Fin de la oreLive. Lemme 20 : Si l'on a : 121 15 en s'appuyant sur les 5. La c a t é g o r i e d e s composantes c o n n e x e s e s t une LCC 1 i" -7 " n -* • *.* tf 23 ©' 1' et donc* si* d'une part* codomaine et véri/ient /lèches 1 et domaines de z les /lèches z Rfl z' ont 1' et pour et z' z et et si* d autre codomaines véri/ient ont même part* les ti/s les z' 9 respec 1 Rfl 1' * alors on a : p(z,y,l.n) Rfl o.z",y.s • -* • jr a r > • *..£! ^ ^ Preuve. En raison du lemme 11, il est équivalent de prouver eue : p2(x, y, v, w,a,/?,^,6,^:,C) Rfi p2 W • 6' autrement dit* C si l'on a x R,fl et y v Rfl v' et w F^fl w' * R fl v' , codom(x) Rob codom(v) , dom(x) Rob codom(v) Cet donc et dom(y) Rob codom(w) , : cadom(x') Rob codam(y') , d o m < x ' ) R o b codoffl(v') et d o m ( y ' ) R o b c o d o m ( w ' ) J>, aLors on a : p< x , y, v, w, a,/?, ^, 6, <£. Ç ) R fl p dans le premier dessin oui suit, il est cependant possible de le faire oar un chemin détourné comme le suggère le deuxième dessin oui suit : 126 5. La c a t é g o r i e des composantes 127 connexes est une LCC S. La c a t é g o r i e des composantes 128 connexes est une LCC 3. La c a t é g o r i e des composantes c o n n e x e s e s t une LCC Nous terminons maintenant l'étude de la loi o par la proposition ci— desso'us qui concerne sa "restriction", o . Proposition 10 : La loi relation R p est compatible avec ta fl • Preuve. Cette proposition exactement comme se déduit des la proposition propositions 5 du déduisait des propositions 2 et 4 (§4). Fin de la preuve. 129 7 et 9. paragraphe 4 se 5. La c a t é g o r i e des composantes connexes est une LCC 5-3. La structure de LCC Par souci d'homogénéiser les notations, nous posons maintenant : - s i x € Fl (llcc(G) ) : d) Il existe donc des flèches de 31 ) et une flèche x" telles que a , a' , Y telles aue : 130 x Rfl x' . et y9 (éléments 5. La c a t é g o r i e des composantes CX CX 4 ^ à Ù d(x) jd où (a,/?) » connexions {y ^6) et Carbitrai codom(x) et rement codom(y) , et codom(w) Si x e Fl(C) , alors sont (^?Ç) on respectivement choisies} dam(x) pose Cet entre et cela des les objets codom(v) , dom(y) a bien un sens} a bien un : d ators on a : p = p(x,y,v,w) Si x a t o r s on a : et = PF ators on dom s < x . v » a. /?) 2 • ' • Or on a : x - f1(x,y,a,/?) = x -f T) = codom(v) et dom est une LCC d'établir GU= : f < x , y , a . /?) . D < x , y , v . w, a , /?, y, 6 , _:. Ç ) R f l v . f ( v , 6 ) . f ( x . y . s ( v , 6 ) , y . _7 . = < -J , Ç" ) . ex. f?) Posons v = y-s assure alors que : L'axiome f ( x, x) . dC x) = i d . La seconde égalité se démontre de manière analogue. Fin de la preuve. Proposition 20 : Si x > y , v , w > m , n <= Fl CC) t e 11 es _ que : _ _ _ _ _ sont _ codom(x) = codom(y) , dom (/J.V) des connexions entre objets, comme représenté ci-dessous : T sf7.s) (en v e r t u dui lemme 2 e t de l ' a x i o m e <(pc) )) Rfl pc .pc assure que : p< x , y, v. w) • p< x • v, v • w. m, n) = D(x,a.s , f < y , / ? > ) . p c ( w , s ( n , f ( w , Ç) ) - f ( v , / ? ) ) (en v e r t u de l'axiome ((pc) ) puisaue f(v./?) p c ( w , s < n , f ) - f < y , / ? > ) {car = s(-T.5) *- s Rfl s<<ÊT.s s< x , a ) .ft.s< x , a ) ) (en vertu de la proposition 1 5 ) . Et on a d'autre oart (en vertu de la proposition 15 encore) : d(y.x) = d) = d Fin de la preuve. Proposition 22 : Si v * r <== Fl (C) sont telles que : ccdcm . Preuve. Soit (a,/?) une connexion entre comme représenté ci-dessous : codom(x) et codcm et comme V -> • # vu, on a s(x,a) = ex x RfL e x et et On a a l o r s d ' u n e p a r t - ft a Notons < s(y,/?) y Rfl e y = ey . Ainsi déjà . : p< x . y , f < x , y) , s ( x , y) ) = p< i Ç . i Ç , f < x , y) . s< x , v ) ) = p A' On a donc : avec _ _ _ _ f £ ^ = ^ et si S. La c a t é g o r i e des composantes connexes est une LCC (en vertu, de la proposition 9 (§£•} et de la proposition 15) = id (dom (x ) ^ (en vertu, de l'axiome (hf) * = Id(B) . L'aLitre égalité se prouve de manière analogue. Fin de la preuve. Il est immédiat (en vertu proposition 15) aue : Proposition 24 : de l'axiome 'cte.D et de la cte(T) = Td(T) . Enfin, il reste à étsblir aue : Proposition 25 : Si x A' On a donc : avec B7" = B et £^=^ cte*Â).x = cte'ÂM.x = cte(A').x (en vertu de la proposition 15) = cte(A')-x (en vertu de la proposition 9 du paragraphe 4) = cteiB 7 ) (en vertu de l'axiome (cteFl) et de la proposition 15) 145 si 5. La c a t é g o r i e des composantes connexes est une LCC = cte(B> . Fin de la preuve. On conclut de la définition 3 et des proocsi ti cr-s 16 à 25 aue les lois cte PF , f , s (, b ). a . un d . et définissent bien une struicture de LCC sur la catégorie € = ____E_________/R (définie dans le paragraphe 4) et ou'ainsi le point (ii) du théorème (§2) est établi: désormais cette LCC des composantes connexes sera donc notée : = llcc(G)/P Le f o n c t e L i r "composantes connexes" aui q u o t i e n t : cano(C) : llcc(G) » i.e. le foncteur > llcc(G) / passage = C est un homomorphisme de LLCC en raison de la proposition 15 (pour les les lois dont il n'y est pas propriétés voulues sont trivialement fait mention. vérifiées): désormais ce foncteLir sera donc noté : > 11 ce (G) >/Q = . cano(G) : llcc( f. b ) . s (. propositions 1 et parce aue les sont représentées o. 6 d , assurent un que le vérifie le point (ix) du théorème (§2). 146 lois de LCC (cf {par les lois PF . et cte ) cu^ les foncteur cano(G) «5. à. Liberté d e La LCC d e s c o m p o s a n t e s connexes Liberté de la LCC des composantes connexes Nous reprenons paragraphe 2. ici. entre Proposition : La catégorie autres. localement les notations du cartésienne = llcc(G) yn est librement engendrée Crelativement sous-jacent" au par /oncteur © : (LCC Preuive. Par définition même, (relativement sous-jacent" structures > G G © ) . Par "transi ti vite des > QJLCC ) . C'est le orienté est librement engendrée par est librement au G = lec(G) . au foncteur IL© : ILILCC = llcc(G) s orienté "graphe llcc(G) libres", graphe d'oubli ilcc(G) A G le poLir donc d'établir engendrée "LLCC llcc(G) sous-jacente" ce que nous (future) oar aue allons flèche faire, canon i aue d'adjonction, de 1'homomorphisme de LLCC : > •:€> = llcc(G) >/ cano(G) : llcc(G) /P défini dans les paragraohes 4 et 5. Pour ce faire, on se donne un homomorphisme (quelconque) de LLCC : OH : llcc(G) > <Œ)> où <Œ)> est une LCC et on doit prouver qu'il existe alors un unique homomorphisme de LCC : > <Œ)> ÛH : < c > vérifiant : 147 ©. Liberté de la L C C des composantes QH.cano'G) comme r e p r é s e n t é oar le connexes = OH . diagramme ci-dessous : OJLCC l l c c ( G ) /^ = <- /P (dit Si autrement, un effet, (1) et (2) tel on d o i t OH l'égalité prouver existe, llcc(G) cano(G) que OH p a s s e au qu.otisnt). il est nécessairement DH-cano(G) = (H équivaut a : A e Ob(llccCG)) ÔH<Â) = QH , on a dans existe bien. lice (G) représentent le même : A' a or B (en vertu de la proposition 1 (§2)> et on a ainsi : 148 ©. Liberté de l a LCC d e s composantes connexes 0H sont les icentitès; = QH , on a dans _\.._ les flèches : en effet, 11 ce (G) liée(G) î représentent : t£\ ;_f B' (en v e r t u de l a p r o p o s i t i o n e t on a a i n s i 2 (§2)) : 0H de <Œ>> e s t = 0H ÔHCy-x") étant temps, . alors aue. 0H C On a a l o r s dans <Œ)> 0H(x) -» 0H de et fonct OH ) - ô. Liberté d e l a LCC d e s c o m p o s a n t e s ( connexes f • • < 1 que 1 ' o n a d a n s : Z • l i c e (G) : v K On a 7< «S. ''•> f < x , a ) > a * ftY "F < v . ft\ .. -•" alors 0 H < f < x , y ) ) = DH(f> (comme VLI c i - d e s s u s p u i s a u e c* . ft «s 31 ) = f > ation de . OH à analogue. Prouvons maintenant On SLippose donc • aue OH commute à l a que l ' o n a d a n s v > • x > • 151 < '"C> : v - # < loi w 6. Liberté c'est-à—dire d e lai LCC d e s c o m p o s a n t e s eue l ' o n a dans connexes llcc( i) B> " s(v.''cï) ! -F(v,<5) ; _ 3 (où l ' o n a p o s é On a a l o r s ) ;'(;<'. et')'"] >-F(x.cO n ; * r's'Cy.y?')" r"'s.' fs T T .j L. st *(w.Ç) •:• & * n ÏÏI v = j^.s(v,6) *^ W w w = £.s(w.Ç> >. : D H < p ( K . y . VyW) ) = D H ( a ( s < x , a > , s ( y , / ? ) , s< v , -f ( x , c 0 ) , s ( â . - F < v . fi) ) ) ) ( e n v e r t u du lemme 11 d u o a r a g r a o h e 5 ) = QH(p( s < x , a ) , s < y , / ? > . s < v , - f < x . a > ) , s < w , - f < y , / ? ) ) ) ) = p ( 0 H ( s ( x . a ) ) , W ( s ( y . / ? ) ) ,QH(s( v , - F ( x , c O ) ) . I H ( s ( w. f ( y . / ? ) ) ) ) = p) (comme v u c i - d e s s u s p u i s q u e a , (3 . f ( x , a ) . f(y,f?) e A 5 = p([HOO ,QH(y) .QH(}"s(v.,<5)) , ( H ( £ . s ( w , 0 > ) = p(CH . Q H ( s ( w . O > ) = p ( t H < x ) , ( H < y ) , D H < s < v , 6 ) ) , [ H ( s ( w,Ç) ) ) (car ^ . £ € ^t ) = p(QH(x) , 0 H ( y ) , [ H ( v ) . 0 H ( w ) ) (comme vu ci-dessus ouisque 6 , Ç "= ^ > = p(QH(x) ,ÎÏÏ(y) .W(v) .,frl(w)) . Comme la commutation de IH aux lois "cte" est évidente à montrer, nous avons ainsi prouvé c^us 152 ô. OH est bien auoaravant Liberté de la I.CC des composantes un q.ril et ncus avions v'u OH.-zano(G) = DH st air il est homamoronisme vérifie de LCZ connexes uniaue à la vérifier. Fin de la oreuve. Nous avons établi, par point (iii; du téorème cette dernière Drcoositior. 1= (§2) et oreuve de ce théorème. 153 nous avens donc achevé la TABLE INTRODUCTION 1. 2. .. ., CATEGORIES LAX-LOCALEMENT-CARTESIENNES (LLCC) 3. : 3. P D, -*3 LA SUFFISANTE COMPLETUDE CONNEXE DES LLCC SUR LES LCC , 3. PREUVES DE SIMPLIFIABILITE DES ZIGZAGS D. 53 4. LA CATEGORIE DES COMPOSANTES CONNEXES p. 65 5. LA CATEGORIE DES COMPOSANTES CONNEXES EST o. 37 UNE LCC 6. LIBERTE DE LA LCC DES COMPOSANTES CONNEXES ,. o. 1*7