D IAGRAMMES R. G UITART Carrés exacts et carrés déductifs Diagrammes, tome 6 (1981), exp. no 2, p. G1-G17 © Université Paris 7, UER math., 1981, 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, Volt 6 , 1981 • CARPES EXACTS El CARRES DEDUCTIFS ^ R. Guitart 1. But, En 197 8 (voir {4} ) j'ai introduit les carrés exacts dans les 2-catégories et montré leur utilité dans le cas spécial de (voir CAT . Depuis, en diverses occasions {6} ) , jfai indiqué brièvement pourquoi ces carrés exacts jouent,au niveau de la théorie générale des modèles, le rôle joué par l'équivalence logique " < > " dans le calcul propositionnel. Je me propose ici de présenter ensemble les arguments en ce sens, ceux déjà donnés ailleurs et quelques nouveaux. Cela me conduira à isoler un nouveau concept destiné à jouer, au niveau de la théorie générale des modèles, le rôle joué par l'implication logique " > " dans le cal- cul propositionnels il s'agit du concept de carré déductif. A partir de l'idée de carré déductif, il est très aisé de définir les preuves. Une théorie axiomatique est alors une 2-catégorie où l'on distingue certains chemins-zigzags (les axiomes) et où l'on se donne certains carrés dits déductif s (les règles de déductions). Les théorèmes sont les zigzags terminaux de preuves partant d'axiomes. Exposé donné au Séminaire de Catégories de l'Université Paris 7 en automne 1981. G 2 2. L'idée de travailler dans les catégories additives avec les carrés exacts plutôt qu'avec les suites exactes remonte à Lambek, MacLane, Puppe et une bonne partie de ce qui peut être fait est exposée dans Hilton (en {8} ), Sur l'usage des carrés exacts dans les catégories non additives et le lien avec le problème du plongement de la catégorie envisagée dans diverses catégories à involutions, je renvoie le lecteur à Grandis (en {2} ) où d'autres ré- férences (Calenko et Conte, par exemple) sont indiquées. Le succès de ce point de vue réside dans l'observationclé suivante: on peut obtenir le composé de deux relationsspans A < X > B et B < Y > C sous la forme * A où X Y B b est n'importe quel carré exact (voir Guitart [3}, p. 35 et {6} , p. 22 ) . Par suite, l'étude des lois de formation des carrés exacts dans une catégorie de la forme de C° P Ens— C Ens— permet de connaître le calcul des relations op et donc la logique déductive de ce topos. Mais, comme on sait que les logiques des catégories cop Ens^- "sont" la sémantique naturelle de la logique intuitioniste, on voit que la méthode des carrés exacts se trouve, de fait, plus étendue que l'intuitionisme. L'intuitionisme est, en quelque sorte, la partie discrète ou 1-dimensionnelle, de la logique exacte fibrée introduite en {6} comme une par- tie principale de la logique catégorique. La logique exacte fibrée sur une catégorie C est l'étude des lois de G 3 formation des carrés exacts dans les 2-catégories C° P , CAT— Fib(£) , JD^(£) » CAT/£ ... (la deuxième partie principale de la logique catégorique sur fibrées sur £ est l'étude des monades C , i. e. des monades dans 3, Les carrés exacts dans C° P ... CAT/C ) . CAT— CAT , dans les 2-catégories représentables ou munies de Yoneda-structures ont été introduits par Guitart {4} et, depuis, la théorie s'est développée dans Van den Bril {lo} et {il}, dans Guitart {6} , dans Guitart-Lair {7} (dans le cas de CAT , voir ici des rappels et compléments au §12). Une première raison du succès de ces carrés exacts 2-dimensionnels est qu'effectivement à peu près tout ce que 1' on fait dans CAT (e. g. carrés commas et co-commas, fonc- teurs riches, opaques, cc-pleinement fidèles, limites et extensions absolues, adjonctions partielles et adjonctions, extensions de Kan ponctuelles) est directement et naturellement exprimable en termes de carrés exacts. Une deuxième raison est que, dans le cas de CAT , la com- position des pro-foncteurs vus comme bi-fibrations se fait encore en tenant comte de l'observation-clé du §2 . 4. Toute formule du 1 er ordre peut s'écrire par des conditions de continuité et de co-continuité (Guitart-Lair, à paraître) et de telles conditions s'expriment encore par des exactitudes de carrés dans CAT , de sorte que l'étude de la validité des formules et la théorie de la déduction de formules-théorèmes à partir de formules-axiomes reviennent, en principe, à des problèmes de la logique exacte. En G 4 particulier, les règles usuelles de déduction (principe de la contraposition, modus ponens) doivent s'exprimer sous forme de principes de constructions de carrés exacts. C'est bien le cas, comme on dit en {6} et {7} , avec les rè- gles de modélisation, de syntactisation, d'extension exacte (mod , syn , ex*ex ). Pour réaliser la portée d'une règle comme ex.ex , il suffit de savoir qu'elle induit directe- ment les théorèmes de Mac-Donald et Deleanu-Hilton sur 1' extension de Kan de théories cohomologiques et K-théories. Pour plus de détails sur la logique exacte, je renvoie à {6} . 5. Que la théorie de la déduction soit transformable (§4) en la théorie de la construction de carrés exacts, cela revient à dire, puisque (§2) les carrés exacts sont les éléments servant à décrire les compositions des relations, que la déduction est l'étude de la catégorie des relations et, particulièrement, la détermination des triplets de relations Rs X -4—>Y , S; Y —\—>Z , Ts X —4—>Z tels que S o R = T . Comme dans le cas de ENS la composition de R fait par union de sous-objets de et S se Z , la théorie de la dé- duction se définit encore comme la recherche de la structure des objets "de sous-objets" dère que PZ est le treillis complet libre sur étant valable dans ante de PZ . En général, on consi- ENS Z (ceci ou un topos comme catégorie ambi- Z ). J'ai indiqué que la structure de si être analysée comme extenseur (voir {5} En tout état de cause, la structure de PZ PZ peut aus- et le §7 ). est d'être une P-algèbre libre, et sera donc décrite quand on connaîtra la structure de P • J'ai proposé en {6} d'élucider cette struc- G 5 ture comme celle dr univers algébrique qui est assez forte er pour "faire" toutes les mathématiques du 1 ordre et assez souple pour être valide quand la catégorie ambiante est un topos ou bien une catégorie d'ensembles flous. 6. Puisque le fond du problème avec PZ est de faire la théorie de la déduction (§5), Lambek-Scott en proposé de comprendre un ensemble E PZ {9} ont comme un ensemble déductif, i. e. muni d'une relation de déduction I- cz ( 9 . E) x E fin satisfaisant l e s axiomes 1 x {x} i - , A i- y {x} V- y A U {x} l— y Si (L, < ) ... H , xn} H 7. Si £ tive y , {y} x = y pars y ssi V/ x i i y SSi V X. i E V X. i J , on peut définir une ex- G 6 tension de ^ f ) = Si £ f le long de J h pars -I7->PJ-Fh-*PI Pf -> PE est un topos ou les ensembles flous, e Ex -S> E satisfait alors les axiomes d'extenseurs. Si E a une structure d'extension, il a une structure de déduction, i. e. on peut définir ->E) (f: I ->E) (gs J si, et seulement si, il existe: I <- où Ex (k) « f 8. Dans K" . V -> .X prod. fib. a comma b * > (ENS^)OPh-£-) exact d ex, -> Y \k > (CAT/S_)op ££. V = ex. (CAT/S)° P lim v> -> (ENS^)° P On a que -> J w (a.b.c) est exact ssi v: £ï°P (ENS-) (ENS^) O P ,a.b.c (7-V) est exact, ce que < - h(S)F 1 = l'on pouvait écrire F fr=c lim g > g , ("dialectique" entre modèle abstrait/formule concrète , d'une part, et modèle déployé/formule abstraite , d'autre part). G 7 Il s'agit là d'un exemple important de mise en place d'un réseau exact (voir {4} ) , un réseau plan de carrés étant dit exact si, en le complétant "aux places vides" par de petits carrés exacts, le grand carré final obtenu est luimême exact. Le calcul des carrés exacts est envisageable aussi comme X calcul d'échanges entre 2-fractions droites s.t et 2X fractions gauches u .v et le calcul des réseaux exacts correspond à des échanges d'ordre supérieur, comme par ex- X X X X emples Si/tj* ^ 2 ^ 2 ^ ul o V i , u 2 #v 2 • Comme exemple, soit le réseau ( p l e i n ) complété ( p o i n t i l l é s ) s w si le carré extérieur (pleins et pointillés) est exact, i. e. si le réseau (traits pleins) est exact, alors on a une modification exacte du chemin (a,b,c,d,e,f) vers le chemin (g,h,i,j,k,l) décrite par la séquences (a,b,c,d,e,f) f (a,b',c',d ,e',f) > (a,b',c',d,e,f) > (a,b',u,v,e',f) (a.b1.u,f.e'.v) > (x.h.g,w.k.l) - (g,h,x,w,k,l) - -> (g,h,i,j,k,l) . > > G 8 En général, une modification exacte est à voir comme une preuve "stricte" de la relation représentée par le chemin (g>h,i,jfk,l) chemin à partir de la relation représentée par le (a,b,c,d,e,f). La "théorie des preuves" dans CAT peut être vue, de ce point de vue, comme l'étude des commutations de limites dans ENS s une preuve est un arbre avec l'indication, à chaque n œ u d , d'une règle de commutation de limites dans du 1 ENS . Les règles de la logique ordre classique (manipulation des quantificateurs, calcul des propositions) sont effectivement de cette nature. Très particulièrement, si P et positions, on montre que > Q par application des P < Q sont des pro- règles de commutation comme (si a' = ~t a " aAb < > l(a'N/b')" et b' = ~\ b ) , toutes ces règles étant réunies dans l'énoncés " Si P est une proposition, sa forme normale disjonc- tive équivaut à sa forme normale conjonctive (et équivaut à P elle-même) ". 9. Il y a une adjonction du type syntaxe-sémantique entre les théories d'exactitude et les théories de relations. Pour préciser cela, on se place dans une catégorie £ (la généralisation aux 2-catégories est aisée) et on considères 1 ) . La catégorie Po£ E oC de l'ensemble , dont les objets sont les parties des carrés commutatifs de £ et dont les morphismes sont les inclusions, 2 ) . La catégorie PMI£ des pro-monades involutives sur £ G 9 dont les objets sont les (Ls £ > R_ , I) , où un foncteur bijectif sur les objets et I L est est une involu- IÎ R > R°P sant fixes les objets et vérifiant I .1 * Id ), et dont les morphismes sont les foncteurs Hs R tion sur R que H.L = (i. e. L' un foncteur et I'.H = > R' tels H.I . On définit, alors, un foncteur en associant à lais- Exs PMIC -> P o c (L,I) l'ensemble des carrés commutâtifs . > . s V u qui, de plus, "anti-commutent dans R " i. e. satisfont Ls.ILt = ILu.Lv • Le foncteur Ex admet un adjoint à gauche Res P D C ~> PMIC que l'on peut décrire comme suit. a). On désigne par Ch(£) la catégorie libre des chemins de £ , dont les objets sont ceux de £ phismes de lesquels A à B sont les X- = A , X sont objets de C = B et (X..,...,X $f..,...,f ) pour et, pour tout f. sX. i et dont les mor- i i < n , les ou bien •^Vi :>X. (la composition de ces morphismes se 1 1+1 faisant alors par simple juxtaposition). b). On désigne par sur £ Zz(£) la catégorie à involution libre dont les objets sont ceux de £ phismes de A vers tels que,pour tout B et dont les mor- sont les zigzags (i. e. les chemins) i < n , f. et f. - ne soient pas composables (la composition s'effectuant par juxtaposition, G 10 suivie si nécessaire de réduction en composant s'ils sont composables f ainsi, de ï! et f Zz(£) est un quotient Ch(£) ). c). Enfin, supposons donnée E c n £ , On définit comme catégorie quotient de Ch(£) par l'équivalence en- gendrée par les règles suivantes? (i). on peut, dans un chemin, remplacer un -> Y -> Z i+1 -> Z par î+l i (ii). on peut, dans un chemin, remplacer un f. s X —•—> Y par un -> K -> Y u tel que v.u = f. , (iii). on peut, dans un chemin, remplacer un X <- > Z f i+l par un X > K Y (R,D " ) est immédiate. On voit alors que les Re(E)-algèbres sont précisément les E-extenseurs. 10. De nombreuses classes tant d'un pseudo-foncteur C op E sont construites en par-> Cat , tel que, pour tout G 12 objet X de £ , la catégorie SX soit pensée comme "ca- tégorie des sous-objets formels de X " . On définit alors E c Q C S comme les carrés commutâtifs dont les images par dans dans Cat soient exactes (i. e. soient anti-commutâtifs BIM => Cat). En particulier, si S = Sub s £ > Cat , avec Sub(X) = Catégorie des sous-objets de X , la théorie des relations Re(E ) qui en résulte est le calcul des foncteurs entre les SubX , SubY ... qui sont représentables par un chemin dans £ . En associant à tout chemin gramme c la limite projective du dia- c , on détermine, pourvu que les carrés pull-backs soient exacts, une représentation par spans des relations? si C n'a pas de limites projectives convenables, on prend A C° P cette limite dan9 la catégorie £ = Ens— , d'où s /\ > S pan £ . lim * Ch(£) 11. En fait, les modifications exactes sont des preuves "strictes en ce sens que, si dans une preuve ordinaire H • ' •-> A > B > C •••• > T on convient de répéter à chaque étape les hypothèses précédentes dans la conclusion, on obtient une chaine d'équivalences ou modifications exactes de H < > H A A < En travaillant dans "A c " A n B Hs > HA AA B < > ... H A A A ..AT. PZ , cela revient à ne pas utiliser B " et à le remplacer par = A " . " A U B = B " ou par Si, maintenant, les relations sont des chemins, par la voie G 13 des modifications exactes on pourra dire si R < et puis pour R > T il faudra dire qu'il existe tel que R V Q < Q > T . Mais il n'est pas clair comment définir V $ cela revient à définir on définit > S R < > S par R > . Et ensuite, > S et S > R . Ceci conduit à l'idée de carré déductif , qui sont aux car— rés exacts ce que > est à < > , comme je vais le définir au §13. 12. 1). Dans la 2-catégorie consite (voir CAT , un carré exact {4} ) en quatre foncteurs et une transformation naturelle ^ s S, T, U > V U.S » et V T -> Y r X V > B \k U tels que, dans BIM, | S H T° /v> *> U° B V , ou encore tels que les AJ ^ X Y ( A ) : £(X,SA)xY(TA,Y) -> B(UX,VY)s (m,n) \—> Vn.fA.Um induisent un isomorphismes 1 X,Y' A (X SA)xY(TA,Y) J *' ^j -> B(UX,VY) . 2). En plus des exemples de {4} aussi (voir est exact ssi pour toute exten- {4} ) que 1 rappelés au §3, rappelons sion de Kan ponctuelle ("pointwise Kan extension") dans CATs > B A G 14 la figure composée est encore une extension de Kan ponctuelle. 3 ) . B o u m et Cordier ont montré en {1} que la même proprié- té de préservation des extensions ponctuelles est encore vraie dans BIM et ils en déduisent qu'un carré exact est la situa- tion la plus générale qui donne lieu à une factorisation -> Y ^/l V H, -> B, X *v u y -> KI n\ KIIT. où ITC et E ^ à S et sont les monades de co-densité associées v V . 4 ) . On peut aussi voir un carré exact position ternaire généralisée de B , comme une décom- à cause de l'exemple suivant• Soit E, D et M des sous-catégories de B^ et soit catégorie ayant pour objets les morphismes de phismes les carrés commutâtifs D A la et pour mor- G 15 où u et v sont inversibles. Alors (E,D,M) est une dé- composition ternaire de B ssi le carré est exact, si l'on pose vd = d . 5). Un carré 4* est sous-exact (resp. sur-exact) ssi, pour tout couple (X,Y) d'objets de XxY , f X , Y eSt in ~ jectif (resp. surjectlf). Etant donné en f ^ un carré quelconque, il peut se décomposer = i 8 s , avec tive de € (voir 6 exact, | la structure multiplica- {>}> §1.5), i sous-exact et s sur-exact. Ce résultat est une version 2-dimensionnelle de la notion 1-dimensionnelle de décomposition des morphismes en épimono. 13. Soit donnée une 2-catégorie £ munie d'une classe TE de carrés réputés "exacts" (par exemple, les carrés exacts au sens de voir {4} ) et soit H , ou au sens de K H o p , au sens de M ... une classe de morphismes de £ appe- lés "comparaisons canoniques" (par exemple, les monos de £ , ou les épis de dans S , ou les morphismes de £ ayant un adjoint (S . . . ) . Avec les notations du §9, on pose: G 16 Définition. Un carré sera dit EHK-déductif s ' i l ( i ) une m o d i f i c a t i o n existes IE-exacte X de X <- en -> Y S' ( i i ) une m o d i f i c a t i o n T' IE-exacte X< k; A' , g, B' U' (iii) un morphisme (S,T) de (U,V) en >Y V ~> B' de K tel que k.X = p,. La 2-catégorie REL ^ R (£) a pour objets ceux de C ,a pour morphismes les éléments de R e ( E ) , appelés relations, et ses 2-morphismes sont engendrés par les carrés lE-K-dé- ductifs et seront appelés preuves. Cette procédure de description de la 2-catégorie des relations améliore celle que j'avais fournie au §3 de {4}. Bibliographie. Cl} D. Bourn et J. M. Cordier, Distributeurs et théorie de la forme, Cah. de Top. et Géom. Diff. XXI-2 (1^80) pp. 161-189. {2} M. Grandis, Symétrisations de catégories et factorisations quaternaires, Atti délia Accademia Nazionale dei Lincei, Série VIII, Vol. XIV, Fasc. 5, Roma, 1977. G 17 {3} R. Guitart, Monades involutives complémentées, Cah. de Top. et Géom. Diff. XVI-1 (1975), pp. 17-101. {4} R. Guitart, Relations et carrés exacts, Ann. Se. Math. Québec, Vol. IV-2 (1980), pp. 103-125. {5} R. Guitart, Extenseurs, Diagrammes, Vol. 3 (1980). {6} R. Guitart, Qu'est-ce que la logique dans une catéeme gorie ? , 3 Colloque sur les catégories dédié à Charles Ehresmann, Amiens, Juillet 1980 (à paraître dans les Cah. de Top. et Géom. Diff. XXIII). {7} R. Guitart et C. Lair, Calcul syntaxique des modèles et calcul des formules internes, Diagrammes, Vol. 4 (1980), pp. GL 1 - GL 106 . £8} P. Hilton, Correspondances and exact squares, Proc. of the Conf. on Cat. Alg. La Jolla, Springer, 1966. {9) J. Lambek et F. J. Scott, Algebraic aspects of topos eme theory, 3 Colloque sur les catégories dédié à Charles Ehresmann, Amiens, Juillet 1980, in Cah. de Top. et Géom. Diff. XXII-2 (1980), pp. 129-140. £lo} L. Van den Bril, Carrés exacts de Hilton dans des contextes non abéliens, Ann. Se. Math. Québec, Vol. IV-2 (1980). {il} L. Van den Bril, Exactitude dans les Yoneda-strutures, 3 Colloque sur les catégories dédié à Charles Ehresmann, Amiens, Juillet 1980 (à paraître dans les Cah. de Top. et Géom. Diff. XXIII).