D IAGRAMMES R. G UITART C. L AIR Limites et co-limites pour représenter les formules Diagrammes, tome 7 (1982), exp. no 4, p. GL1-GL24 © Université Paris 7, UER math., 1982, 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, Vol 0 7 , 1982, LIMITES ET CO-LIMITES POUR REPRESENTER LES FORMULES R. Guitart et C. Lair Introduction» Soit L un langage classique et T une théorie du pre- mier ordre classique, décrite dans le langage de L • Nous établissons au §1 que les groupoïdes respectifs des interprétations ensemblistes de L et des modèles de T sont des groupoïdes esquissables au sens de C, Ehresmann. En particulier, ceci signifie que les modèles de T sont des struc- tures esquissables. En théorie usuelle des modèles, si l'on sait évidemment définir canoniquement les isomorphismes entre modèles de T , on ne possède pas de définition générale des homomorphismes entre ces modèles (sauf à particulariser T , par exemple en supposant qu'elle est algébrique = équationnelle). Nous montrons au §1 que de l'esquissabilité des modèles de T résul- tent des procédés systématiques de définition (et donc d'étude) des homomorphismes entre ces modèles. Ce point de vue est celui de (R.M.S.S.): les morphismes d'une catégorie de modèles sont, eux-aussi, des structures qu'il convient donc d'esquisser également. Ainsi, une catégorie de modèlesest esquissable à l'aide d'une co-catégorie interne à la catégorie des esquisses. Les intèrpètations ensemblistes d'un langage L sont esquissables. Les interprétations ensemblistes des formules GL 2 classiques écrites avec L le sont également; par des sur- esquisses de l'esquisse décrivant L • Une combinaison boo- léenne de ces formules possède donc une esquisse qui est une "combinaison booléenne" des sur-esquisses précédentes. Nous établissons au §2 qu'une telle situation se systématises la catégorie des "sur-esquisses" (appelées précisément esquisses au §2) d'une esquisse donnée //L// //W/- - jouant le rôle d'un langage de base - possède au moins un calcul fonctoriel booléen (ou propositionnel). Par réalisations (i. e. par interprétations) ensemblistes, ces calculs fonctoriels booléens fournissent? - le calcul booléen classique (intersection, complémentaire) sur les groupoïdes d'isomorphismes entre les structures ainsi esquissées, - un calcul "booléen" non classique sur les catégories d'homomorphismes entre ces structures esquissées. Au §3 nous donnons d'autres démonstrations des résutats obtenus aux §§1 et 2 et quelques précisions techniques. Cependant, il convient de noter qu'on y ébauche une procédure de traduction entres - les systèmes de ré-écriture d'une formule classique en une formule équivalente de forme donnée, - certains calculs fonctoriels - i. e 0 certaines logiques sur la catégorie des esquisses. Le §0 est consacré à des rappels de terminologie et notations, 0, Terminologie, Notations. On dit que //£// = (S^, TF, H ) est une esquisse (mixte) si, et seulement si (voir (E,T,S,A.) )s - £ est un graphe multiplicatif petit, - 3P est un ensemble de cônes projectifs de bases petites, dis- GL 3 t ingués dans - H S_ , est un ensemble de cônes inductifs de bases petites, dis- tingués dans £ , Lorsque l'ensemble des cônes inductifs distingués est vide, on dit qu'il s'agit d'une esquisse projective que l'on note alors, plus simplement, Si HS_H /S/ , est une esquisse, on notera les esquisses telles que IP' => IP et Enfin, une esquisse telle que On dit que -Rs S vers > S^ H' ^ H , CS,0,0) sera identifiée à S • //R // s //£ // HS^II sation de ///S/ // = (S^,ff',H') > //S/ // est une réali- //S_' // si, et seulement sis est un foncteur, - l'image par R de tout cône distingué de cône distingué de //lS' // • //£// est un Une réalisation saiVre^ esquisses projectives sera notée, plus simplement, /Et/s /S/ > /S>V , Esquisses et réalisations entre esquisses sont les objets et les morphismes de la catégorie des esquisses notée Soit //sy/ sation de Esq . une esquisse. On appelle simplement réali- //£// , et l'on note F? //£// > Ens , tout foncteur F s S^ > Ens transformant les cônes distin- gués de //£// en des limites de On note réal(//:S//) la classe de toutes les réalisations de Ens • //£// • On désigne par Réal(//S_//) la sous-catégorie pleine S de Ens— dont les objets sont ces réalisations. Enfin, on désigne par GrRéal( //£// ) le sous-groupoïde, plein, saturé par isomorphismes, de Ens— dont la classe d'objets est réal(//!3//) $ c'est donc aussi un sous-groupoïde, plein, saturé par isomorphismes, de Réal(//£//), Supposons que c //£//» //¾// > //¾// d > //¾// k GL 4 est une co-catégorie (resp. un co-groupoïde) interne à Esq 3 on en déduit une catégorie (resp, un groupoïde) ensemblistes réal(c) réal(k) - (réal(//S3//). réal(//£//)! r é a K / ^ / / ) J_ réal(//S 2 //) > Ens ), signifie, dualement, que le cône suivant est distingué même si la flèche en question n'est pas un monomorphisme dans le graphe multiplicatif sous-jacent à l'esquisse (mais elle doit donc être réalisée en un mono de - si Ens ) , I_ est une petite catégorie, le symbole lim S = S signifie que le cône inductif considéré est distingué dans l'esquisse décrite, même s'il n'est pas limite inductive dans le graphe multiplicatif sous-jacent à l'esquisse utilisée (cependant, il doit être réalisé en une limite inductive de Ens ) , GL 6 - dualement, si I est une petite catégorie, le symbole lim S = S représente un couple de f.f' = Id = Id . et f'.f 1, Esquissabilité des groupoïdes et des catégories de modèles de théories du premier ordre classique. Supposons que L = ( v >( F n ) n ç N '^Wo^ (au sens de (E,D,L,M,)) ayant variables et, pour tout V e S t u n lan &age pour ensemble (infini) de n€N , ayant F (resp, R ) pour ensemble de symboles fonctionnels (resp, relationnels) à n places. Le groupoïde des bijections entre ensembles opère, évidemment, sur la classe int(L) des interprétations (enssmblistes) de L , Il en résulte un groupoïde d'hypermorphismes, noté Grlnt(L) et appelé groupoïde canonique des interprétations de L . Dans ces conditions, nous avons s Proposition 1, Le groupoïde canonique des interprétations d'un langage est un groupoïde naturellement esquissable. Preuve, Il suffit d'utiliser l'esquisse projective /S_/ briè- GL 7 vement décrite ci-dessous s n < s s < < G_ r (où que nÇN et r parcourt Supposons, de nouveau, que L est un langage et,de plus, 0 , f parcourt F est une formule booléenne de R . // L , i. e. une combinai- son booléenne (finitaire) de formules atomiques ne contenant que les seules variables x.., ,,, , x (où p€N ), Le groupoïde des bijections ensemblistes opère sur la classe int(G) des interprétations de graphe Q c E P ) de per mor phi sme s, noté I = (E,0) (de support E et 9 . Il en résulte un groupoïde d'hy- Grlnt(9) et appelé groupoïde canonique des interprétations de 0 , Il est facile de construire une sur-esquisse //¾ // de /S / , contenant en particulier un monomorphisme distingué go > sp G > , de sorte que toute réalisation F s //S- // > Ens s'identifie à une interprétation —6 I » (F (S),F (G)) et inversement. Autrement dit, on a; Proposition 2. Le groupoïde canonique des interprétations d'une formule booléenne est un groupoïde naturellement esquissable. Supposons, encore, que que a L est un langage et, de surcroit, est une formule classique, i, e, une formule du premier ordre, de longueur finie, écrite avec un nombre fini de quantificateurs. Le groupoïde des bijections ensemblistes opère, bien entendu, sur la classe mod(tf) des modèles de cf , i, e, des intèrprè- GL 8 tations de L qui satisfont 0 • Il en résulte un groupoïde d'hypermorphismes, noté GrMod(a) et appelé le groupoïde canonique des modèles de a . Dans ces conditions, montrons que s Proposition 3, Le groupoïde canonique des modèles d'une formule classique est un groupoïde naturellement esquissable. Preuve, La formule C est équivalente à une formule clas- sique prénexe, i, e, pouvant s'écrireg où \fx1 3 x^ V x 3 ... n€N et G 3x2n 6(xl5 ,., fX^) f est une formule booléenne. Il suffit, alors, d'utiliser la sur-esquisse //S // de //SA // , brièvement décrite ci-dessous s G >- 2n *3> S J P~> 2n-l 2n Y,2n-1 -> S P + P* *2n-l 2n-l •< P* *2n-l ^2n-l „2n-2 = » p + P* 2n-2 2n-2 P 2 >- -< P' r 2n-2 = P 3 + Y* 3 ^P3 = P 2 T+ - S . // GL 9 Supposons toujours que que T L est un langage et, maintenant, est une théorie du premier ordre classique, i, e, un ensemble de formules classiques de L0 Le groupoïde des bijections ensemblistes opère encore sur la classe mod(T) des modèles de T , i, e, des interprétations de satisfaisant toutes les formules appartenant à T , On L appelle donc groupoïde canonique des modèles de T et on note GrMod(T) le groupoïde d'hypermorphismes qui résulte de cette opération. Dès lors, nous avons? Théorème 1, Le groupoïde canonique des modèles d'une théorie du premier ordre classique est un groupoïde naturellement esquissable. Preuve, Il suffit de considérer l'esquisse mixte me amalgammée au-dessus de //S // , som- /S T / , dans la catégorie Esq , des —"L esquisses //¾// f quand a parcourt Notons que les esquisses T , // /^/ , //¾// t //¾// ou //¾^ ne sont pas, a priori, les seules qui permettent d'esquisser naturellement les groupoïdes canoniques Grlnt(L) , Grlnt(9) , GrMod(cr) , GrMod(T) . Remarquons aussi que, dès lors que l'on sait esquisser naturellement, à l'aide d'une esquisse //^// $ les groupoïdes canoni- aues précédents, on dispose d'un moyen systématique pour définir des types d*isomorphismes (resp, d'homomorphismes) - non nécessairement canoniques - entre interprétations ou modèles de 0 , c ou T s ce sont les morphismes des groupoïdes (resp, des catégories) réal( //£//) , où (resp, une co-catégorie) de esquisse L , Esq //$_/! est un co-groupoïde dont l'objet des objet est 1' //£//• 2, Combinaisons booléennes d'esquisses. Dans toute la suite de ce §2 , nous supposons que est une esquisse fixée. //L// GL 10 On d i t que //L// > //S// //R// est une esquisse de langage - le foncteur > / / / S / // //Idg// //L// si, et Seulement sis GrRéal(//R//): GrRéal( //S // ) > GrRéal(//L//) est une équivalence, (on pourrait imposer la condition plus fortes - Réal(//R//)s Réal(//S//) > Réal(//L//) est une équi- valence, mais nous n'en avons pas l'utilité technique ici? on notera, cependant, que c'est bien cette dernière condition qui est vérifiée dans la pratique courante cars //L// = /L/ - et //S_// = /S/ //R//* /R/ s /L/ sont purement projectives, -> /S/ et ///S/ // sont construi- tes à partir de la donnée de formules internes à Réal(/L/) s ce sont justement les cônes inductifs distingués de ///S/ // qui ont pour images, par le plongement de Yoneda S°P > Réal(/S/) Viei -> S f t ) T - T c * J6J ) distingués dans ///S/ // — II S II \ //s- // GL 12 - pour tout c€C e t tout - pour tout c'ÇC' - pour tout c€C , o n a ICI , o n a e t tout J€J , o n a m,s c - pour tout c'ÇC' , on a - q . s = s.q et - i.e = s et s .s =s,m c = s , s'f,s'=s', , c m ' f . s ' t = s',m't , q',s* = s.q' , p..,S = p 2 «d = IcL, , I l e s t immédiat de constater que l a r é a l i s a t i o n //R'//S nyi > //S//C > //S'// //R// induit bien une équivalence entre les groupoïdes et GrRéal(//L//) GrRéal(//S' / / ) . Pour obtenir ///£'/ // , il suffit alors de distinguer a comme épi. On conclut facilement en constatant qu'une réalisation F? / / / S ' / / / (qui transforme nécessairement transformer s bien un élément F(c') Si > a Ens en une surjection) ne peut en une bijection. En conséquence, il existe c de C ou c' de C' tel que F(c) ou n'est pas une limite, // (///£.///).-T le groupoïde est une famille de GrRéal(///^.///) valent à un sous-groupoïde G, //L//-esquisses, est, pour chaque iÇI , qui- de saturé GrRéal(//L//) par isomorphismes. L'intersection de ces sous-groupoïdes est encore un sous-groupoïde de GrRéal(//L//) saturé par isomor- phismes. Nous poserons 0 G i€I = A GrRéal(///S ///) iei et nous l'appellerons groupoïde conjonction canonique des groupoïdes de réalisations de la famille Montrons, maintenant, que s ( ///£. / // ). — , GL 13 Proposition 5. Le groupoïde conjonction canonique des groupoïdes de réalisations d'une famille de //L//-esquisses est un groupoïde naturellement esquissable. Preuve, Il suffit d'utiliser la //L//-esquisse finie comme suit: ///S/ // dé- - la sous-esquisse //S// de ///S/ // est la somme amalgammée, au-dessus de //L// , dans la catégorie Esq , des //S. // représentée ci-dessous: ^7 II h " //R. IL > IIS H IH-ff " / / / S / // ll\ll //R// * ll\ll.ll\ll est la somme amalgammée, au-dessus de la catégorie Esq , des //L// , dans /IIS^I II représentée ci-dessous: I//SJ II //Id. II.III.IL /II. Il -> / / / S V / / 111**1 H (on constate que ceci définit bien une esquisse de langage nyi t //L// . ,HlL—> fis H jr^-j-, > ///SV //« ///S/ // ///RV// * //Ids//.//R// car le foncteur "graphe multiplicatif sous-jacent" commute aux sommes amalgammées). // Supposonst maintenant^ que: - P((x.). < . < ) est une formule purement booléenne, i. e. est écrite à l*aide des variables symboles "1 et A > - (///15.///)1 < * < est x., ... , x " ^ f a m i l l e de et des seuls //L//-esquisses. GL 14 Chacun des groupoïdes sous-groupoïde de GrRéal( //AS. / //) est équivalent à ton GrRéal(//L//) , saturé par isomorphismes, auquel nous l'identifions. Dans ces conditions, nous notons P((GrRéal(///Si/ / / ) ^ < ^ < ) le sous-groupoïde de GrRéal(//L//), saturé par isomorphismes, dont les objets sont les réalisations F: //L// > Ens P((F Ç réal(///£./ /f^i telles que soit vraie la proposition < -< )• Ce sous-groupoïde est alors appelé groupoïde canonique d'interprétation de lisations de la famille P par les réa~ • ( ///jS. / // )-, < . < Des propositions 4 et 5 résulte immédiatement s Théorème 2. Le groupoïde canonique d'interprétation d'une formule purement booléenne par les réalisations d'une famille de //L //-esquisses est un groupoïde naturellement esquissable. Les constructions utilisées dans les démonstrations précédentes et la "combinaison booléenne" de ces constructions que l'on utilise pour établir le théorème 2 fournissent, à partir des //L//-esquisses initialement donnée s, d'autres //L//esquisses que nous pouvons noter respectivement: -V//S/// , A ///S./// et P((///^/ / / ) 1 < 1 < n ) . Ainsi, sont définis des opérateurs sur la classe //L//-esq des //L//-esquisses. Ils se prolongent, évidemment, en autant de foncteurs sur la catégorie -que l'on définit facilement //L//-Esq des //L//-esquisses s 1 : //L//-Esq > //L//-Esq , j*. : (//L^-Esq) 1 > //L//-Esq , P : (//L//-Esq)n > //L//-Esq , On dispose donc d'un calcul fonctoriel booléen (ou proposition-* nel) sur la catégorie des //L//-esquisses. Remarquons qu'un tel calcul n'est pas unique, au même titre GL 15 que la //L//-esquisse 1///S/// (resp. Aj. Il/S^lll ) précédente n'est pas, en général, la seule telle que: GrRéaK "1 ///S/ / / ) ^ 1 GrRéal( ///S/ // ) (resp. GrRéaK ^ ///^/ //) ~ ^ GrRéaK ///^/ //) ). Il y aurait donc lieu d'analyser chacun de ces calculs fonctoriels et de les comparer. Notons qu'un système naturel (en //L//) de calculs fonctoriels booléens sur les catégories varie dans //L//-Esq (quand //L// Esq ) permet de définir un calcul booléen (ou propositionnel) sur les catégories esquissables. Supposons, en effet, que s liyix -> //v > -> "h.H IIJ^/I est une co-catégorie interne à Esq . Alors, on appelle 11%II" cocatégorie interne à Esq un diagramme commutâtifs Util + Ilh " llh.ll •» //L3// Util V 1> //¾ // Ilh II //*// > //¾ // IIUSII V l/ltlfl \V : IIIS^I H my ii , lf/S2/l/ vérifiant s - chaque ligne est une co-catégorie interne à - chaque colonne 1 < p< 3 est une Esq , //L //-esquisse. Dans ces conditions: - si / / / # / // est une //£//-co-catégorie interne à Esq , on GL 16 appelle négation de la catégorie esquissable et l'on note réal( 1 ///$/ "I réal( /fl$J II) * //) la catégorie esquissable (qui n'est pas, en général, "la catégorie complémentaire de - si réal(///£///) , réal( ///S/ //) (///£.///).— dans est une famille de réal( fit //)"), //jL//-co-catégories internes à Esq , on appelle conjonction des catégories es** quissables (réal( ///^///)) i Ç I > et l'on note la catégorie esquissable réal( A ///£. / //) .*. réal(///^///), (qui n'est pas, M en général, " l ' i n t e r s e c t i o n des catégories réal(111$.! / / ) ), 3 , Compléments. Montrons en quoi le calcul f o n c t o r i e l booléen exhibé au §2 n ' e s t pas unique. Pour ce f a i r e , e x p l i c i t o n s , par exemple, une autre "V HlSjllt T///S/// //L//-esquisse v é r i f i a n t encore s GrRéaK V // / S / // ) ^ -\ GrRéaK / / / S / // ) • On y parvient immédiatement en reprenant l a preuve de l a proposition 4 et en s u b s t i t u a n t , l o r s de l a construction de à l a sous-esquisse //S" // //S* / / , c e l l e brièvement d é c r i t e par le diagramme et les conditions ci-dessous s (U + U) x (U + U) T U T (TxT)=T+T' U GL 17 - q-i«d = q2«d = IcL, p^.S = Po-â = IcL , c.s^ « c.s^ = Id.. , , Donnons, maintenant, un exemple d'application des résultats du §2 , en particulier de celui de la proposition 4 f Supposons que L est une catégorie petite et que c = (pT$ G > GT)T-T de base discrète 1^ . On dit (voir (F.A,U.C.) ) qu'un fonc- teur > Ens Fs L est un cône projectif de valide c si, et seulement sis (» c ) V f s G — > F 3 I€I 3 gs G x On note alors dant c et val(c) > F (resp, ~\GrVal(c) ) poïde plein, saturé par isomorphismes, de classe d'objets est val(c) dans (g.P][ = f ) . la classe des objets de GrVal(c) val(c) Ens— , Ens— vali- le sous-grou- Ens— dont la (resp, le complémentaire de Ob(Ens—) ) , Dans ces conditions, nous avons? Proposition 6. Les groupoïdes GrVal(c) e£ "1 GrVal(c) sont des groupoïdes naturellement esquissables. Preuve. A tout objet Fs L catégorie d'hypermorphismes rr(F)? H(F) > L > Ens H(F) de Ens— associons sa et notons le foncteur canonique de projection. On sait que le plongement de Yoneda Y s Lop > Ens— est dense. Autrement dit, on as F = lira (H(F)° P > L°P —*> ir(F)°P ~ Y Notons S p la sous-catégorie pleine de Ens— > En*£ dont les objets sont s - les Y(L) , quand - sommet du cône G - les GT L , quand Désignons par /S L , c , I / est objet de est objet de 1^ • l'esquisse projective obtenue en dis- GL 18 tinguant dans - G= S lim (H(G) < - l e s l i m i t e s p r o j e c t i v e s canoniques? GT = > L - TT(G) lim (H(GT) <— > S , ^° RQ > L > S TT(G T ) R^ 1 o , R sL > S est la restriction de Y o p . o — —co Notons S le graphe multiplicatif obtenu en adjoignant à S s - un cône inductif "c = (p s G- • • • • > G ) - _ , de même base op — que c , - une flèche h s G > G telle que p .h = p , pour où tout objet I de 1^ . Désignons par //S // la sur-esquisse de /S / obtenue en —c —co distinguant également le cône inductif c , On en déduit une réalisations //R//i L ~ >/S /R / -° /« 0 > US H . ~° o Si ///S / // est la sur-esquisse de //S // obtenue en distinguant de plus h comme épi, il est alors clair que GrVal(c) *£ GrRéaK///S ///) —c (voir aussi (C.M.C.F.)). De plus, on constate immédiatement que; L > US //R// H > Il/S IH ~* //Id s // -* —c est bien une L-esquisse. On conclut donc par application de la proposition 4, Les constructions précédentes sont encore valables si on substitue à la catégorie petite L une esquisse projective /L/ (car on dispose encore d'un "plongement de Yoneda" L — > Réal(/L/) qui est toujours dense)g à tout cône projectif - i. e. à toute formule interne - c de Réal(/L/) GL 19 est donc associée une /L/-esquisse > IIS^H /L/ > HISJII . Plus généralement, si C est un ensemble de cônes projectifs à bases discrètes dans Réal(/L/) , on lui associe une /L/esquisse dite externe g /L/ > HISçl H . > //¾ // Elle s'obtient par somme amalgammée au-dessus de /L/ , dans la catégorie Esq , des esquisses respectives //S // et —c ///S / // quand c parcourt C • Dans ces conditions, les opérateurs négation 1 et disjonction £* sur les /L/-esquisses externes se déduisent l'un de l'autre. En effet, on as - - i« IHSc /// = 1(3i i 1 ^ < + "lit11? /L/ i€I ///Sj// = "^ V IH ) f "^i IIISIJ C' c: C II f si l'on pose "^ C' * 0 ///W// = ( ^ + ///S / / / ) + /L/ "° ( /L/ c€C-C' + ///S///) /L/ "* , cÇC' (où + /L/ désigne l'opération de somme amalgammée au-dessus de /L/ dans la catégorie Esq ) . Notons, enfin, qu'à toute esquisse associée une /L/-esquisse externe /y //L// est canoniquement >*• //¾ // t e l l e que l e s c a t é g o r i e s Réal( H/SJ > IIISJ u //) et , où C' Réal(//L//) soient équivalentes s - i l s u f f i t de poser C « Y(C') cônes d i s t i n g u é s de //L// et YÎ L o p e s t l'ensemble des >Réal(/L/) est GL ÏO le plongement de Yoneda. On peut démontrer la proposition 3 d'une autre manière que celle présentée au §1. On sait (voir (CY.A.L, )) que toute formule classique d'un langage L est élément air ement équivalente à une formule de la formes (D V Xj^ 3 X2 V x 3 ... 3 ¾ D est de la formes où i < z D(x1, ... ,X2n) , i j < PjL j J ' où les A. les sont des formules atomiques. Pour prouver la propo- B. sont des conjonctions de formules atomiques et sition 3 , il suffit donc de le faire pour des formules classiques de la forme (1). Soit /£ / l'esquisse projective associée (comme dans la preuve de la proposition 1) au langage L . Il est montré en (I.F.O.F.) que le groupoïde canonique des modèles GrMod(tf) d'une formule a de la forme (1) est équivalent au sous-groupoïde plein, saturé par isomorphismes, de Réal(/£L/) ayant pour objets ceux de Réal(/SL/) validant ion certain arbre . Pour établir la proposition 3, il suffit donc de prouver qu'un tel sous-groupoïde est naturellement esquissable, en précisant ce que l'on entend (en (I.F.O.F.)) par validation d'un arbre. Notons M l'ensemble des mots finis, non vides, s'écrivant m = m ^ ••• m (on pose alors z = long m ) grâce à l'al- phabet ÏT = {1,2, ... ,n, ,., } . Munissons M de l'ordre défini comme suitÏ - m < m' si, et seulement sis + long m < long m' , + pour tout i < long m , on a m. < m' . On appelle alors arbre fini toute partie finie A de M , sta- GL 21 ble par induction, i. e. vérifiants - " m < m' dans M et m' appartient à A ,f implique " m appartient à A " . A tout arbre fini A , on associe un graphe orienté, noté A , défini comme suit s - ses objets sont les éléments de A , - ses flèches sont les • > mn s sm mn M + m appartient à A , + n appartient à iNH , + le concaténé à A . tels que s mn de m et n appartient Un arbre (fini) de Réal(/S T /) est alors un homomorphisme de graphes orientés as A objet > Ens de Réal(/S T /) valide F s /S T / > Réal(/S T /) • On dit qu'un l'arbre a si, et seulement si, il existe une stratégie gagnante pour le joueur J , dans le jeu à deux joueurs JQ et J-. dé- fini comme suit s - au premier coup, J.. choisit un f-. s a(l) = a, - au deuxième coup, J que s + le mot choisit un couple ln 2 & F , (ru,f 2 ) tel appartient à A , + f 2 8 "in, > F + f 2*a(sln2) = fl ' • • . • - au p coup, J , «, choisit un couple ' p mod 2 (n ,f ) tel p' p que s + le mot liun 3 ... n .n appartient à A , GL 22 + f s a. > F, p J.n2«..n + fp v ,a(sT ) = fp-1-,' , ln^,..n 2 p - le premier joueur qui ne peut jouer a perdu. Montrons donc que le sous-groupoïde, plein, saturé par isomorphismes, noté GrVal(a) , de Réal(/S T /) dont les objets —JL sont ceux qui valident un arbre fini a est naturellement esquissable. Pour faire court, nous ne le prouvons que dans le cas particulier suivant (le cas général se traitant de manière analogue)? A z 1 — > 11 ^ S > 112 -i^-^ lll l'image de A par as A x ^ _ > Réal(/S,/) étant notées x ll > aii > 1121 x 112 > ^ 1121 ^> a i i n ^ 1 1 a lll (et Y s S L ° P > Réal(/S / ) désignant le ••plongement" de Yoneda). A tout objet F de Réal(/S /) est associée une catégorie d'hypermorphismes H(F) et un foncteur canonique de projection TT(F)S H(F) > S T tels ques F = lim —> Notons /SJ (H(F)° P > ST°P P Réal(/ST/) ) . Y "L l'esquisse projective obtenue comme suit s - S est la sous-catégorie pleine de Réal(/S T /) dont les objets sont s GL 2i + les Y(S) , si S est objet de £, , + les a , si m est élément de A , m - les cônes projectifs distingués de /Sj sont s + les cônes projectifs images par Y op s ST > S des cônes projectifs dis-HL — tingués de /SL/ , + les limites projectives canoniques ->S) a m = lim(H(a) > S -L y op m ^ m f m si m est élément de A • Nous complétons alors /S/ en une sur-esquisse //£' // en lui adjoignant le diagramme et les conditions suivantes s ^ll où l'on as e = x^.h.p^. » x--.l'.p2 . On vérifie bien alors que GrRéaK//S///) ^ GrVal(a), Compte tenu des remarques et constructions précédentes, et avec une terminologie évidente, ceci établit que s Théorème 3. Les groupoïdes naturellement esquissables (i. e. de la forme GrRéaK//S//) ) sont des groupoïdes canoniques de validation d'un ensemble de cônes projectifs à bases diacrètes - formules internes = arbres de hauteur 1 (donnés GL 24 dans Réal(/S/)) et inversement. De même, tout groupoïde na- turellement esquissable est un groupoïde canonique de validation d'un ensemble d'arbres finis et inversement. Bibliographie. (C.M.C.F.) R. Guitart et C. Lair, Calcul syntaxique des modèles et calcul des formules internes, Diagrammes 4 , Paris (1980), (C.Y.A.L.) L. Henkin, J, Monk et A. Tarski, Cylindric algebras, Part I , North-Holland (1971). (E.D.L.M.) G. Kreisel et J.-L. Krivine, Eléments de logique mathématique, Dunod, Paris (1967), (E.G,C.E.) C, Lair, Etude générale de la catégorie des esquisses, Esquisses Mathématiques 23, Paris (1975), (E,T,S,A,) C. Ehresmann, Esquisses et types de structures algébriques, Bul. Instit. Polit., Iaçi XIV (1968). (F.A.U.C) H. Andréka et I. Németi, Formulas and ultraproducts in catégories, Beit. zur Alg, und Geom. 8 (1979). (I,F,0.F.) H. Andréka et I. Németi, Injectivity in catégories to represent ail first order formulas I , Dem. Math. XII-3 (1979). (R.M.S.S.) R. Guitart et C. Lair, Critères de rigidification des morphismes souples entre structures internes, Diagrammes 5, Paris (1981).