Dans cet exposé, je propose une méthode nouvelle pour introduire la notion de preuve mathématique formelle. Contrairement à ce qui est habituellement proposé, à savoir une introduction basée sur un postulat, comme par exemple le postulat de la correspondance de Curry-Howard, cette méthode ne suppose aucun postulat. Elle n'utilise que des faits que les mathématiciens, et en particulier les mathématiciens non logiciens, admettent sans discussion, parce que ce sont des mécanismes qu'ils utilisent tous les jours. Comme la méthode ne suppose aucune syntaxe a priori pour les preuves, la définition des preuves que je vais donner est un cadre général qui pourrait a priori accommoder différentes syntaxes de preuves. Toutefois on verra, qu'à condition de ne pas introduire de choses inutiles dans le langage, et au variations syntaxiques superficielle près, il n'y a essentiellement qu'un seul langage de preuve possible. On verra quelques exemples de preuves formelles. La méthode met aussi immédiatement en évidence l'existence d'un opérateur de choix et d'un opérateur de description. Ceci m'amènera aussi (si le temps imparti le permet) à discuter de l'axiome du choix et de son rapport au langage ainsi mis en évidence.

La diagonale ensembliste d’un polytope a le défaut rédhibitoire de ne pas être cellulaire: son image n’est pas une union de cellules. Notre but sera ici de développer une théorie générale, basée sur la méthode introduite par N. Masuda, H. Thomas, A. Tonks et B. Vallette, afin de comprendre et de manipuler les approximations cellulaires de la diagonale d’un polytope quelconque. Cette théorie nous permettra d’attaquer le problème de l’approximation cellulaire de la diagonale des opéraèdres, une famille de polytopes allant des associaèdres aux permutoèdres, et qui code les opérades à homotopie près. Nous obtiendrons ainsi une formule explicite pour le produit tensoriel de deux telles opérades, aux propriétés combinatoires intéressantes.

Référence: https://arxiv.org/abs/2110.14062

Le foncteur nerf permet d'associer à toute petite catégorie un type d'homotopie, donnant lieu à une théorie de l'homotopie des petites catégories, développée par Quillen, Thomason et Grothendieck. Pour généraliser cette théorie aux catégories supérieures, on a besoin d'un analogue supérieur au foncteur nerf. Or il existe plein de tels foncteurs!

Le but de cet exposé, basé sur un article en collaboration avec Georges Maltsiniotis, sera d'expliquer des généralités sur la comparaison de foncteurs nerf et de montrer que pour les n-catégories strictes le nerf multi-simplicial, le nerf cellulaire et le nerf de Street sont tous équivalents.

Une courte première partie de cet exposé sera de nature épistémologique. Il s'agira de situer la question, existence et légitimité du problème : esquisses versus algèbres graphiques. L'intrusion de la structure de catégorie dans l'univers structuraliste de Bourbaki du siècle dernier est venue perturber cet univers au moins par deux aspects. Je ne suis pas concerné ici par celui qui parle des fondements. Le second, objet de cet exposé, est celui de la structure même des catégories et de leurs multiples dérivés. Deux conceptions de ces structures, géométriques et/ou algébriques, conduisent à certains clivages dans leurs traitements. Je rappellerai les définitions associées aux deux points de vue : 1) Les esquisses d'Ehresmann introduites en 1966, lesquelles ont fait l'objet de nombreux travaux par certains de ses élèves pendant plusieurs décennies. 2) Les algèbres graphiques introduites par moi en 1981 (voir lien ci-dessous). Je précise que la juste formule n'est pas d'opposer les esquisses aux algèbres graphiques, mais les esquisses aux théories algébriques graphiques (on est au niveaux des théories).

http://www.numdam.org/item/CTGDC_1981__22_3_249_0.pdf

Travail mené conjointement avec Eric Finster et Matthieu Sozeau (https://arxiv.org/abs/2105.00024).

La théorie des types de Martin-Löf peut être vue comme une fondation des mathématiques. Il a été montré que certains de ses modèles validaient une interprétation homotopique des types, ce qui a motivé une nouvelle ligne de développement de celle-ci nommée théorie des types homotopiques.

Dans cette théorie, les types ne sont pas vus comme de simples ensembles car ils ont une structure d'infini-groupoïde non-triviale conférée par leurs types identité. D'où l'idée de formaliser des résultats d'algèbre supérieure en exploitant la structure supérieure des types. Néanmoins, décrire celle-ci de façon interne reste une question ouverte. C'est à dire que l'on peut énoncer des propositions concernant des infini-groupoïdes arbitraires mais que l'on ne sait pas construire une large classe d'infini-groupoïdes, en particulier ceux dont la structure supérieure n'est pas triviale ou tronquée à partir d'une certaine dimension.

Nous proposons une approche consistant à étendre la théorie des types avec un univers de monades polynomiales satisfaisant leurs lois de façon définitionnelle. Cela nous permet de présenter les types et leur structure supérieure, et ainsi d'internaliser un certain nombre de résultats dont le fait que les types sont des infini-groupoïdes.

Étant donnée une catégorie avec une notion d'homotopie, par exemple une catégorie relative, la notion de dérivateur introduite par Grothendieck permet de décrire les catégories de diagrammes à homotopie près, et les relations fonctorielles qu'elles entretiennent.

Dans cet exposé, nous étudierons comment le prédérivateur associé à une telle catégorie relative se restreint en un objet simplicial dans la catégorie CAT des catégories (non nécessairement petites). Cet objet simplicial peut être vu comme un “nerf homotopique” qui décrit les chemins de longueurs n dans la catégorie d'origine, vus à homotopie près.

Partant de ces observations, nous montrerons que dans le cas d'une catégorie de modèle, l'objet simplicial satisfait une condition de Segal, et définit pour cette raison une double catégorie. Cette double catégorie peut être vue comme combinant en une seule structure la catégorie de modèle d'origine (horizontalement) et sa catégorie homotopique (verticalement).

Nous montrons aussi que la construction précédente est compatible avec la structure de dérivateur établie par Cisinski pour un prédérivateur associé à une catégorie de modèle : on obtient ainsi un nouveau dérivateur prenant ses valeurs dans la catégorie DblCAT des doubles catégories plutôt que dans CAT.

En théorie de l'homotopie, l'omniprésence de la catégorie des ensembles simpliciaux semble lui donner un rôle particulier. Parmi les raisons de sa popularité, on peut citer au moins trois propriétés essentielles : (1) Les ensembles simpliciaux modélisent les types d'homotopie (Milnor), (2) Les groupes internes aux ensembles simpliciaux modélisent les types d'homotopie pointés connexes (Kan), (3) Les groupes abéliens internes aux ensembles simpliciaux modélisent les “types d'homologie”, autrement dit la théorie de l'homotopie des complexes de chaînes en degrés positifs (Dold-Kan-Puppe).

En fait, la propriété (2) admet même la généralisation suivante due a Joyal et Tierney :

(4) Les groupoïdes internes aux ensembles simpliciaux modélisent les types d'homotopie.

Il est alors naturel de se demander s'il existe d'autres catégories de préfaisceaux qui admettent les mêmes propriétés, et qui sont donc, en un certain sens, aussi “bonnes” que la catégorie des ensembles simpliciaux pour faire de la théorie de l'homotopie. Dans Pursuing Stacks, Grothendieck développe la théorie des catégories tests, qui sont, très grossièrement parlant, les petites catégories A tels que les préfaisceaux sur A satisfont à l'analogue de la propriété (1) énoncée plus haut. Le constat est clair : la catégorie des simplexes est loin d'être la seule à satisfaire cette propriété et les catégories tests sont légion.

Dans cet exposé, je présenterai mes travaux récents portant sur la théorie des “catégories tests au sens des groupoïdes”, variation de la théorie des catégories tests de Grothendieck et qui sont, grossièrement parlant, les petites catégories A tels que les préfaisceaux sur A satisfont à l'analogue de la propriété (4) énoncée plus haut. Un des résultats importants que je présenterai est :

Une (petite) catégorie est test si et seulement si elle est test au sens des groupoïdes.

Outre le fait qu'il permet de déduire de nombreux nouveaux modèles des types d'homotopie, ce résultat non trivial permet de renforcer, une fois de plus, la pertinence de la notion de catégorie test.

Si le temps me le permet, je terminerai l'exposé par des généralisations conjecturales de cette théorie des “catégories test au sens des groupoïdes”, qui visent notamment à remplacer les groupoïdes par des n-groupoïdes (faibles).

Une catégorie localement présentable peut parfois être décrite comme la catégorie des modèles (dans Ens) d'une théorie algébrique à types (ou sortes) dépendants. Nous en avons vu un exemple (présenté par T. Benjamin) lors d'une séance précédente : la catégorie des omega-catégories faibles du cohérateur de Batanin-Leinster.

Il est naturel de se demander quelles structures algébriques admettent une telle description et si l'on peut les reconnaître « dans la nature ». Dans cet exposé je répondrai à cette question.

Plus précisément, je montrerai que :

1. Les signatures de types dépendants correspondent exactement aux catégories directes localement finies. (Cette description est due à Makkai et porte le nom de “simple category” dans ses travaux sur les FOLDS.)

2. Si C est une catégorie directe localement finie (telle que celles des globes, des semi-simplexes, ou des opétopes), alors les contextes de variables typées par C sont exactement les complexes cellulaires finis dans [C^op, Ens]. (N.B. : La catégorie C étant directe, les préfaisceaux sur C admettent un modèle cellulaire donné par les inclusions de bords de représentables.)

3. La catégorie des « théories algébriques typées par une signature C » est équivalente à celle des monades finitaires sur [C^op, Ens].

4. La catégorie des modèles dans Ens d'une théorie algébrique typée par C est équivalente à la catégorie des algèbres de la monade finitaire correspondante.

On en déduit (parmi d'autres) les exemples des théories algébriques à types dépendants des oméga-catégories et oméga-groupoïdes (strictes et faibles), des opérades colorées (planaires), des ensembles opétopiques, et des combinades (sur les arbres planaires) de Loday. Je les expliquerai.

5. Enfin, je montrerai un résultat un peu surprenant : les théories algébriques à types dépendants sont aussi expressives que les théories essentiellement algébriques ou les esquisses projectives. Autrement dit, toute catégorie localement finiment présentable est la catégorie des modèles dans Ens d'une théorie algébrique à types dépendants.

Ce dernier peut aussi être vu comme conséquence de la version non-homotopique d'un résultat de Cisinski permettant de calculer les extensions de Kan à droite homotopique des préfaisceaux à valeurs dans une catégorie de modèles par passage aux préfaisceaux sur des catégories directes (localement finies).

Il est bien connu que le nerf d'une catégorie C est toujours une quasi-catégorie, et qu'il est un complexe de Kan si et seulement si C est un groupoïde. Le foncteur nerf de Street, entre la catégorie des petites oméga-catégories et celle des ensembles simpliciaux peut être vu comme une généralisation du nerf catégorique. Il est alors naturel de se demander si on peut, de façon analogue au cas catégorique, caractériser les oméga-catégories dont le nerf de Street est un complexe de Kan (resp. une quasi-catégorie). La réponse est affirmative : cela correspond au oméga-catégories dont les n-cellules sont faiblement inversibles pour n>0 (resp. n>1).

Dans cet exposé, après des rappels sur les oméga-catégories, nous présenterons une preuve de ce fait. Si le temps le permet, nous présenterons une généralisation aux ensembles compliciaux.

Cet exposé est basé sur le papier suivant : arxiv.org/abs/2102.04281

Les omega-catégories faibles, comme toutes les structures supérieures, sont délicates a définir et a manipuler. La raison est qu'elles ont de la structure dans toutes les dimensions, et que cette structure est cohérente: pour chaque dimension, les bonnes propriétés vérifiées par la structure dans cette dimension sont encodées par des éléments de dimension supérieure. La conséquence est qu'au fur et à mesure que l'on monte en dimension, les éléments présents deviennent de plus en plus riches et complexes a décrire. Ainsi, les définitions possibles de ces structures s'appuient sur des schémas d'axiomes, permettant de générer l'infinité d'opérations et de cohérences en toute dimensions, et ces schémas d'axiomes sont eux-mêmes encodés dans des structures algébriques adéquates, comme une opérade globulaire (définition due a Batanin et Leinster) ou une catégorie avec certaines colimites (définition due a Grothendieck et Maltsiniotis). Plus récemment, Finster et Mimram ont proposé une définition des omega-catégories faibles en encodant ces schémas d'axiomes dans une théorie des types, CaTT. Dans cet exposé, je vais présenter la theorie CaTT et m'appuyer sur cette formulation pour présenter formellement les omega-categories faibles. Je vais ensuite faire une démonstration d'un assistant de preuve pour les oméga-categories faibles que j'ai implementé en m'appuyant sur cette théorie des types et discuter des possibilités de cet outil, ainsi que des améliorations que j'y ai apportées. Je vais finalement esquisser une comparaison entre CaTT et la définition de Grothendieck-Maltsiniotis des omega-catégories faibles.