Simon Henry (Collège de France), Théorie homotopique des types et modèles algébriques pour les infinis catégories et groupoïdes

Programme

Résumé

Dans son manuscrit “À la poursuite des champs” Grothendieck propose une définition “d'infini-groupoïde” ainsi qu'une notion d'équivalence entre eux et conjecture que la catégorie homotopique est équivalente à sa catégorie des infini-groupoïdes “à équivalence près”.

Cette conjecture (l'hypothèse d'homotopie) est toujours un problème ouvert, et il y a de très nombreuses questions basiques concernant cette notion d'infini-groupoïdes qui restent sans réponse. Pour cette raison, on préfère généralement utiliser les ensembles simpliciaux et les complexes de Kan pour définir la notion d'infini-groupoïde et servir de point de départ pour la théorie des catégories supérieures.

Cela dit l'apparition de la théorie homotopique des types nous donne de nouvelles motivations pour s'intéresser à cette notion d'infini-groupoïdes : tout d'abord n'importe quel type en théorie homotopique des types porte une structure d'infini-groupoïde au sens Grothendieck, ensuite, si la théorie des types est censée être la logique interne de certaines infini-catégories, il s'agit à priori d'infini-catégories globulaires, i.e. d'un genre plus proche de la définition de Grothendieck que des versions simpliciales. Enfin, on sait internaliser en théorie des types la définition d'infini-groupoïdes de Grothendieck, alors qu'on est très loin de savoir faire de même pour les approches simpliciales.

Dans cet exposé je vais présenter une nouvelle famille de définitions de la notion d'infini-groupoïde qui sont inspirées à la fois de celle de Grothendieck et de la théorie homotopique des types. Elles conservent certaines des bonnes propriétés de la définition de Grothendieck, mais échappent aux problèmes de celle-ci. On sait en particulier prouver l'analogue de l'hypothèse d'homotopie pour cette définition.

On énoncera aussi une conjecture technique précise, d'apparence simple, qui impliquerait que la définition de Grothendieck est un cas particulier de la nôtre, et qui donc impliquerait aussi l'hypothèse d'homotopie et résoudrait une partie des problèmes ouverts concernant la définition de Grothendieck.