Principe de réflexion vs univers
Dans les discussions sur la théorie des catégories, il y a souvent la tentation de regarder la catégorie de tous les groupes abéliens, ou de toutes les catégories, etc., ce qui conduit rapidement aux problèmes habituels de la théorie des ensembles. Ceux-ci sont souvent évités en utilisant les univers Grothendieck. En langage de la théorie des ensembles, on corrige des cardinaux fortement inaccessibles$\kappa$ -- cela signifie que $\kappa$ est un cardinal indénombrable tel que pour tous $\lambda<\kappa$, également $2^\lambda<\kappa$, et pour tout ensemble de $<\kappa$ de nombreux ensembles $S_i$ de taille $<\kappa$, aussi leur union est de taille $<\kappa$. Cela implique que la scène$V_\kappa\subset V$ de "ensembles de taille $<\kappa$"est en soi un modèle de ZFC - en appliquant l'une des opérations sur les décors, comme prendre des ensembles de pouvoirs ou des unions, vous ne pouvez jamais quitter $V_\kappa$. Ces ensembles sont alors appelés «petits», puis la catégorie des petits groupes abéliens est définitivement bien définie.
Historiquement, cette approche a été utilisée pour la première fois par Grothendieck; un texte fondateur plus récent est le travail de Lurie sur$\infty$-catégories. Cependant, leur utilisation a toujours créé un certain contrecoup, certaines personnes ne voulant pas laisser des axiomes au-delà de ZFC glisser dans la littérature établie. Par exemple, je pense qu'à un moment donné, il y a eu une longue discussion pour savoir si le dernier théorème de Fermat a été prouvé dans ZFC, maintenant réglé par McLarty. Plus récemment, j'ai vu des arguments similaires se présenter pour des théorèmes dont les preuves se réfèrent aux travaux de Lurie. (Personnellement, je n'ai pas de sentiments forts à ce sujet et je comprends les arguments de toute façon.)
D'un autre côté, il a également toujours été le cas qu'une inspection plus approfondie a révélé que toute utilisation d'univers était en fait inutile. Par exemple, le projet Stacks n'utilise pas d'univers. Au lieu de cela, (voir Tag 000H dire) cela affaiblit effectivement l'hypothèse selon laquelle$\kappa$ est fortement inaccessible, à quelque chose comme un cardinal limite forte de cofinalité indénombrable, c'est-à-dire: pour tous $\lambda<\kappa$, on a $2^\lambda<\kappa$, et chaque fois que vous avez une collection dénombrable d'ensembles$S_i$ de taille $<\kappa$, aussi l'union de la $S_i$ a la taille $<\kappa$. ZFC prouve facilement l'existence d'un tel$\kappa$, et presque tous les arguments que l'on pourrait envisager de faire dans la catégorie des groupes abéliens fonctionnent aussi dans la catégorie des $\kappa$-petits groupes abéliens pour de tels $\kappa$. Si l'on fait des arguments plus compliqués, on peut en conséquence renforcer l'hypothèse initiale sur$\kappa$. J'ai eu l'occasion de jouer à ce jeu moi-même, voir la section 4 de www.math.uni-bonn.de/people/scholze/EtCohDiamonds.pdf pour le résultat. De cette expérience, je suis à peu près sûr que l'on peut réécrire de la même manière "Higher Topos Theory" de Lurie, ou tout autre travail similaire sur la théorie des catégories, de manière à supprimer tous les cardinaux fortement inaccessibles, en les remplaçant par des$\kappa$ avec des propriétés telles que celles ci-dessus.
En fait, il semble y avoir un théorème de ZFC, le principe de réflexion (discuté brièvement dans Tag 000F du projet Stacks, par exemple), qui semble garantir que cela est toujours possible. À savoir, pour tout ensemble fini donné de formules de la théorie des ensembles, il existe des$\kappa$ de telle sorte que, grosso modo, ces formules tiennent $V_\kappa$ si et seulement s'ils tiennent $V$. Cela semble dire que pour tout ensemble fini donné de formules, on peut trouver$\kappa$ tel que $V_\kappa$se comporte comme un univers vis-à-vis de ces formules, mais corrigez-moi s'il vous plaît dans ma compréhension très naïve du principe de réflexion! (Un fait connexe est que ZFC prouve la cohérence de tout fragment fini donné des axiomes de ZFC.)
D'un autre côté, tout texte mathématique donné ne contient qu'un nombre fini de formules (à moins qu'il n'énonce un "schéma de théorème", ce qui n'arrive généralement pas je crois). La question est donc formulée de manière légèrement provocante:
Le principe de réflexion implique-t-il qu'il doit être possible de réécrire la théorie des topos supérieurs d'une manière qui évite l'utilisation d'univers?
Edit (28.01.2021): Merci beaucoup pour toutes les réponses très utiles! Je pense avoir une image beaucoup plus claire de la situation maintenant, mais je ne sais toujours pas exactement quelle est la réponse à la question.
D'après ce que je comprends, (à peu près) le meilleur méta-théorème dans ce sens est le suivant (spécialisé en HTT). Rappelons que HTT corrige deux cardinaux fortement inaccessibles$\kappa_0$ et $\kappa_1$, faisant ainsi place aux petits (en $V_{\kappa_0}$), grand (en $V_{\kappa_1}$) et très grande (en $V$) objets. On peut alors essayer de lire HTT dans le système d'axiomes suivant (c'est essentiellement celui de l'article de Feferman "Fondements théoriques des ensembles de la théorie des catégories", et a également été proposé dans la réponse de Rodrigo Freire ci-dessous).
(i) Les axiomes habituels de ZFC
(ii) Deux autres symboles $\kappa_0$ et $\kappa_1$, avec les axiomes qu'ils sont cardinaux, que la cofinalité de $\kappa_0$ est indénombrable, et que la cofinalité de $\kappa_1$ est plus grand que $\kappa_0$.
(iii) Un schéma d'axiome, disant que pour chaque formule $\phi$ de la théorie des ensembles, $\phi\leftrightarrow \phi^{V_{\kappa_0}}$ et $\phi\leftrightarrow \phi^{V_{\kappa_1}}$.
Ensuite, le principe de réflexion peut être utilisé pour montrer (voir la réponse de Rodrigo Freire ci-dessous pour une esquisse de la preuve):
Théorème. Ce système d'axiomes est conservateur par rapport à ZFC. En d'autres termes, tout théorème de ce système formel qui ne fait pas référence à$\kappa_0$ et $\kappa_1$ est également un théorème de ZFC.
C'est précisément la conclusion que j'aimerais avoir.
Noter que $V_{\kappa_0}$ et $V_{\kappa_1}$ sont des modèles de ZFC, mais (de façon critique!) cela ne peut pas être prouvé à l'intérieur du système formel, car ZFC n'est pas finement axiomatisable, et seul chaque axiome individuel de ZFC est posé par (iii).
Une bonne chose à propos de ce système d'axiomes est qu'il permet explicitement les arguments occasionnels de la forme "nous avons prouvé ce théorème pour les petites catégories, mais ensuite nous pouvons aussi l'appliquer aux grandes catégories".
Une question plus précise est alors:
Les arguments de HTT fonctionnent-ils dans ce système formel?
Mike Shulman dans la section 11 de https://arxiv.org/abs/0810.1279donne une exposition très claire de ce qu'est le problème potentiel ici. À savoir, si vous avez un ensemble$I\in V_{\kappa_0}$ et ensembles $S_i\in V_{\kappa_0}$ pour $i\in I$, vous n'êtes pas autorisé à conclure que l'union des $S_i$ est dans $V_{\kappa_0}$. Cette conclusion n'est garantie que si la fonction$i\mapsto S_i$ est également défini dans $V_{\kappa_0}$ (ou si $I$est dénombrable, par l'hypothèse supplémentaire d'une cofinalité indénombrable). En pratique, cela signifie que lorsque l'on veut affirmer que quelque chose est "petit" (c'est-à-dire en$V_{\kappa_0}$), ce jugement ne concerne pas seulement les objets, mais aussi les morphismes, etc. Je ne sais pas maintenant à quel point il s'agit d'un problème, je devrais y réfléchir davantage; J'imagine en fait qu'il est assez facile de lire HTT pour répondre à ce système formel. Shulman dit qu'avec cette mise en garde, le théorème du foncteur adjoint peut être prouvé, et comme le dit Lurie dans ses réponses, les arguments en HTT sont d'une complexité similaire en théorie des ensembles. Cependant, je serais toujours intéressé par un jugement pour savoir si la réponse à la question est "Oui, tel qu'écrit" ou plutôt "Probablement oui, mais vous devez faire des efforts" ou en fait "Pas vraiment". (J'espère sincèrement que les experts seront en mesure de s'entendre à peu près sur où se situe la réponse dans ce spectre.)
Une dernière remarque: on peut trouver l'hypothèse "indénombrable" ci-dessus un peu arbitraire; pourquoi ne pas autoriser des syndicats légèrement plus importants? Une façon de résoudre ce problème consiste à ajouter un symbole$\kappa_{-1}$ avec les mêmes propriétés, et demandez à la place que la cofinalité de $\kappa_0$ est plus grand que $\kappa_{-1}$. De même, on pourrait vouloir remplacer la borne$\mathrm{cf} \kappa_1>\kappa_0$ par un bond légèrement plus fort comme $\mathrm{cf} \kappa_1>2^{\kappa_0}$dire. Encore une fois, si cela simplifie les choses, on pourrait alors simplement en presser un autre$\kappa_{1/2}$ entre les deux, de sorte que $\mathrm{cf} \kappa_{1/2}>\kappa_0$ et $\mathrm{cf} \kappa_1>\kappa_{1/2}$. De cette façon, on n'a pas à se soucier de savoir si l'un des objets "standard" qui apparaissent dans certaines épreuves reste de taille dénombrable, ou si l'on peut encore prendre des colimites dans$V_{\kappa_1}$ lorsque les ensembles d'index ne sont pas exactement de taille délimitée par $\kappa_0$ mais ont été un peu manipulés.
PS: Je ne trouve que maintenant toutes les questions et réponses pertinentes de MO précédentes. Certaines réponses très pertinentes sont les réponses de Joel Hamkins ici et ici .
Réponses
Je vais sortir sur une branche et suggérer que le livre HTT n'utilise jamais rien de plus fort que le remplacement pour $\Sigma_{15}$-formules de théorie des ensembles. (Ici$15$ est un grand nombre choisi au hasard, et HTT est un livre de mathématiques choisi au hasard qui ne traite pas spécifiquement de la théorie des ensembles.)
En réfléchissant au commentaire de Gabe sur ma réponse initiale, je pense maintenant que ce que j'ai écrit est trompeur car il confond deux affirmations distinctes (mais liées):
L'existence de cardinaux fortement inaccessibles n'est pas vraiment nécessaire dans la théorie des catégories.
La pleine puissance de ZFC n'est pas vraiment nécessaire dans la théorie des catégories.
Je suis d'accord avec ces deux affirmations, mais je pense que le meilleur moyen de convaincre quelqu'un de 1) ne serait pas de combiner 2) avec un principe de réflexion: c'est-à-dire qu'il ne faut pas essayer de remplacer l'utilisation d'un cardinal fortement inaccessible $\kappa$ par un pour lequel $V_{\kappa}$ modélise une grande partie de ZFC.
Selon moi, le «problème» que résolvent les univers est de justifier la combinaison de deux types de raisonnement:
A) Il est parfois utile de prouver des théorèmes sur les petites catégories $\mathcal{C}$ en les intégrant dans de "grandes" catégories (par exemple, en utilisant l'incorporation Yoneda) qui ont de belles fonctionnalités supplémentaires: par exemple, l'existence de limites et de colimites.
B) Les grandes catégories sont aussi des catégories, donc tout théorème qui s'applique aux catégories en général devrait également s'appliquer aux grandes catégories.
Si vous ne vous inquiétez que de B), alors un principe de réflexion pourrait être pertinent. Choisir un cardinal$\kappa$ tel que $V_{\kappa}$ satisfait une grande partie de ZFC, vous pouvez redéfinir «petite catégorie» pour signifier «catégorie appartenant à $V_{\kappa}$"et" grande catégorie "pour signifier" catégorie n'appartenant pas nécessairement à $V_{\kappa}$", et vous pouvez être sûr que tous les théorèmes de base que vous pourriez souhaiter sont valides dans les deux cas.
Mais si vous vous inquiétez également de A), cela n'est pas nécessairement utile. Disons que vous commencez par une catégorie$\mathcal{C}$ appartenir à $V_{\kappa}$, et vous voulez une version de l'intégration Yoneda. Une hypothèse naturelle serait d'intégrer dans la catégorie des foncteurs de$\mathcal{C}^{\mathrm{op}}$ à la catégorie des ensembles de taille $<\tau$ (ou un modèle équivalent de celui-ci), pour certains cardinal $\tau$. Une première estimation est que vous devriez prendre$\tau = \kappa$, mais je pense que cela n'a de sens $\kappa$est fortement inaccessible (sinon certains ensembles Hom seront trop gros). Dans tous les cas, garantissez que cette construction a de bonnes propriétés, vous allez vouloir exiger différentes propriétés du cardinal$\tau$. Par exemple, si vous voulez que cette catégorie de pré-poussoirs ait beaucoup de colimites, alors vous allez vouloir$\tau$d'avoir une grande cofinalité. Et si vous commencez à réfléchir aux types d'hypothèses supplémentaires que vous pourriez avoir besoin de faire, vous revenez là où vous avez commencé: en réfléchissant au type d'estimations de cardinalité garantissent que "présomment des ensembles de taille$< \tau$"sont une bonne approximation de la catégorie de tous les pré-séries d'ensembles. Le principe de réflexion ne vous aide donc pas vraiment à éviter ces problèmes.
(Edit: j'ai réalisé après avoir écrit que le texte ci-dessous réitère principalement le message original de Peter. Mais je le laisserai ici au cas où quelqu'un le trouverait utile.)
Si vous voulez une formalisation rigoureuse dans quelque chose comme ZFC, la meilleure chose à faire est probablement de supprimer complètement les grandes catégories. Alors B) n'est pas un problème. Pour traiter de A), permettez-moi de faire remarquer que beaucoup des «grandes» catégories dont on aimerait parler se présentent d'une manière particulière: on commence par une petite catégorie$\mathcal{C}$ qui a déjà certains types de colimites, et agrandit formellement $\mathcal{C}$ pour faire une plus grande catégorie $\mathcal{C}^{+}$qui a des colimites arbitraires (sans changer celles avec lesquelles vous avez commencé). Les catégories qui se présentent de cette manière sont appelées localement présentables , et il existe une formule simple pour$\mathcal{C}^{+}$: c'est la catégorie des foncteurs $F: \mathcal{C}^{\mathrm{op}} \rightarrow \mathrm{Set}$ qui préservent les limites avec lesquelles vous avez commencé (c'est-à-dire les colimites avec lesquelles vous avez commencé $\mathcal{C}$).
Maintenant, si vous voulez imiter cela dans le monde des petites catégories, vous pouvez à la place choisir un cardinal $\kappa$ et contemplez plutôt les foncteurs $F: \mathcal{C}^{\mathrm{op}} \rightarrow \{ \text{Sets of size < $\kappa$} \}$, ce qui équivaut à une petite catégorie $\mathcal{C}^{+}_{\kappa}$. La question que vous rencontrez est de savoir si c'est un remplacement suffisant pour la grande catégorie$\mathcal{C}^{+}$dessus. Par exemple, a-t-il beaucoup de limites et de colimites? Il est déraisonnable de lui demander d'avoir toutes les colimites, mais vous pouvez plutôt demander ce qui suit:
Q) La catégorie $\mathcal{C}^{+}_{\kappa}$ avoir des colimites indexées par des diagrammes de taille $< \kappa$?
La réponse à Q) est "non en général, mais oui si $\kappa$ est bien choisi ". Par exemple, si vous avez un cardinal infini $\lambda$ délimitant la taille de $\mathcal{C}$ et le nombre de diagrammes colimit avec lesquels vous commencez, alors je crois que vous pouvez garantir (i) en prenant $\kappa = (2^{\lambda})^{+}$ (et la catégorie $\mathcal{C}^{+}_{\kappa}$peut être caractérisée par la propriété universelle attendue). De plus, pour le prouver, vous n'avez besoin d'aucune forme de remplacement.
Maintenant, vous pouvez également demander ce qui suit:
Q ') La catégorie $\mathcal{C}^{+}_{\kappa}$ avoir des limites indexées par des diagrammes de taille $< \kappa$?
Ici, la réponse sera généralement "non" à moins que $\kappa$est fortement inaccessible. Mais si vous ne vous intéressez qu'aux limites d'un type particulier (par exemple, si vous étudiez le topoi de Grothendieck, vous pourriez être particulièrement intéressé par les limites finies), alors la réponse sera à nouveau "oui pour$\kappa$ bien choisi ". Et c'est quelque chose que vous pouvez prouver en utilisant très peu de ZFC.
Maintenant, je prétends que, sur la base de mon expérience, la discussion ci-dessus est représentative du type de questions que vous rencontrerez en essayant de naviguer dans la distinction entre les catégories "petites" et "grandes" (c'est certainement représentatif de la façon dont ces choses dans mon livre, sur lequel la question initiale posait). En pratique, vous n'avez jamais besoin de parler de l' intégralité d'une grande catégorie comme$\mathcal{C}^{+}$; il suffit d'en construire un morceau assez grand (comme$\mathcal{C}^{+}_{\kappa}$) ayant les fonctionnalités que vous souhaitez voir, que vous pouvez organiser en choisissant $\kappa$ soigneusement.
Je trouve conceptuellement plus clair d'ignorer la question de savoir comment les choses sont formalisées dans ZFC et de formuler les choses en termes de «grande» catégorie $\mathcal{C}^{+}$, renvoyant à ses "petites" approximations $\mathcal{C}^{+}_{\kappa}$seulement comme auxiliaires dans une preuve (qui apparaîtra inévitablement encore quelque part!). L'invocation des «univers» est juste une façon d'écrire comme ça tout en faisant toujours du bout des lèvres le cadre axiomatique de ZFC, et c'est définitivement inessentiel.
J'aimerais mentionner quelque chose qui, je pense, n'a pas encore été signalé. La question initiale a commencé par
En langage de la théorie des ensembles, on corrige des cardinaux fortement inaccessibles $\kappa$... Cela implique que la scène $𝑉_\kappa\subset 𝑉$ de "ensembles de taille $<\kappa$"est lui-même un modèle de ZFC.
Cependant, l'affirmation selon laquelle $V_\kappa$ est un modèle de ZFC est nettement plus faible que de dire que $\kappa$est inaccessible. En fait, si$\kappa$ est inaccessible, alors $\{ \lambda\mid V_\lambda$ est un modèle de ZFC $\}$ est stationnaire dans $\kappa$. Par conséquent, le plus petit inaccessible (s'il y en a un) est beaucoup plus grand que le plus petit$\kappa$ tel que $V_\kappa$ modèles ZFC.
Dans la mesure où le principe de réflexion est utile (ce que, comme d'autres réponses l'ont souligné, on peut au moins remettre en question), il n'est directement utile que pour les arguments dans lesquels la propriété pertinente d'un univers de Grothendieck est qu'il s'agit d'un modèle de ZFC. Cependant, au moins lorsqu'elle est formulée naïvement, il existe de nombreux endroits où la théorie des catégories utilise plus que cela. Plus précisément, nous utilisons le fait qu'un univers de Grothendieck satisfait le remplacement de second ordre , ce qui signifie que toute fonction$f:A\to V_\kappa$, où $A \in V_\kappa$, a une image. Dire que$V_\kappa$modèles ZFC implique seulement qu'il satisfait le remplacement du premier ordre , ce qui nous permet seulement de conclure qu'un tel$f$ a une image si $f$ est définissable à partir de $V_\kappa$ par une formule logique.
Je crois que le remplacement de second ordre est omniprésent dans la théorie des catégories basée sur l'univers telle qu'elle est habituellement formulée. Par exemple, si${\rm Set}_\kappa$ désigne la catégorie d'ensembles dans $V_\kappa$, puis pour prouver que ${\rm Set}_\kappa$ est "complet et cocomplet" dans le sens naïf qu'il admet une limite et une colimite pour tout foncteur dont le domaine est petit, nous avons besoin d'un remplacement de second ordre pour rassembler les images d'un tel foncteur en un seul ensemble.
Maintenant, il existe des moyens de reformuler la théorie des catégories pour éviter cela. L'article de McLarty le fait de certaines manières théoriques des ensembles. Une approche catégoriquement cohérente consiste à remplacer les «grandes catégories» naïves (c'est-à-dire les catégories dont les ensembles d'objets et de morphismes peuvent ne pas appartenir à$V_\kappa$) avec grand ${\rm Set}_\kappa$- catégories indexées . Mais c'est une sorte de reformulation beaucoup plus substantielle à effectuer à la main.
Si je comprends bien, vous recherchez une déclaration du formulaire:
"Si quelque chose a été prouvé en HTT en utilisant des univers, il peut être prouvé sans eux en se limitant à certains $V_\kappa$ pour $\kappa$ assez large"
La réponse rigoureuse à cela, si nous n'avons pas plus d'informations sur HTT, est qu'il ne peut y avoir une telle déclaration si ZFC est cohérent.
En effet, il est possible que l'existence d'univers soit incohérente (en fait il n'est pas possible de prouver qu'elle est cohérente), et dans cette situation, tout peut être prouvé en utilisant des univers, et donc une telle déclaration impliquerait que tout peut être prouvé. , c'est à dire ZFC est incohérent.
Je suis un peu négligent sur ce qui peut être prouvé dans quoi, etc. mais l'idée principale est là
Bien sûr, nous savons des choses sur HTT, et si nous le lisons attentivement, nous pouvons analyser où il utilise les univers, et voir qu'ils peuvent en fait être remplacés par des modèles transitifs de remplacement ZC + jusqu'à $\Sigma_{15}$-formules, comme le souligne Jacob. Dans ce cas, puisqu'il existe de manière prouvée de tels modèles bien comportés (de la forme$V_\kappa$, pour $\kappa$bien choisi), ce n'est pas un problème; et HTT peut être réécrit sans univers - mais cela ne peut pas être prouvé sans savoir ce qu'il y a dans HTT.
La "morale" de ceci est que, dans la plupart des questions théoriques des catégories traditionnelles, les univers sont un dispositif qui permet de gagner du temps, et non une partie réelle des mathématiques.
Tout théorème $T$ de $\mathsf{ZFC}$ découle d'un sous-ensemble fini des axiomes de $\mathsf{ZFC}$ ou, pour garder les choses simples, de $\mathsf{ZFC}$ où le schéma d'axiome de remplacement est limité à $\Sigma_n$ prédicats¹, appelez ça $\mathsf{ZFC}_n$. À présent$\mathsf{ZFC}$, et plus précisément $\mathsf{ZFC}_{n+1}$, prouve l'existence de cardinaux arbitrairement grands $\kappa$, de fortes limites de cofinalité indénombrable, telles que $V_\kappa$ est un modèle de $\mathsf{ZFC}_n$, et, en particulier, du théorème $T$, et de telle sorte que, de plus, la valeur de vérité de tout $\Sigma_n$ instruction, avec des paramètres dans $V_\kappa$ est la même chose dans $V_\kappa$comme dans le (vrai) univers. Nous pouvons les appeler$V_\kappa$ «Univers limités» en ce sens qu'ils sont fermés sous la plupart des opérations de la théorie des ensembles, comme prendre des ensembles de pouvoirs, sauf que le remplacement doit être soit dénombrable (inclus par commodité), soit limité à un $\Sigma_n$prédicat; et en particulier, ils sont fermés sous toutes les déclarations d'existence$T$ fait du.
L'idée serait donc d'appliquer ce qui précède à la conjonction $T$ de tous les théorèmes que vous considérez comme faisant partie de la théorie des topos supérieurs (et de toutes les autres théories utilisées comme prérequis) et trouvez les $n$. (Je soupçonne en fait que$n=1$ devrait suffire: je serais très surpris de trouver une instance de remplacement en mathématiques ordinaires qui ne découle pas de $\Sigma_1$-replacement.) Puis $\mathsf{ZFC}_n$ prouverait $T$ (tous les théorèmes de la théorie) et $\mathsf{ZFC}_{n+1}$ prouverait l'existence d'une offre infinie d'univers limités dans lesquels utiliser la théorie.
Bien sûr, pour éviter une boucle infinie, vous ne pouvez pas considérer ce théorème (celui affirmant l'existence d'un approvisionnement sans fin de$V_\kappa$) pour faire partie de la théorie, ou vous devez passer à un $n$.
Pour expliquer ce qui peut sembler une contradiction logique, il faut ici préciser que l'affirmation selon laquelle l'existence de nombreux modèles de $\mathsf{ZFC}_n$ peut être prouvé dans $\mathsf{ZFC}$ pour chaque $n$, mais pas uniformément (la preuve devient de plus en plus longue à mesure que $n$ grandit), donc $n$doit être un nombre naturel concret , le quantifié universellement (sur $n$) n'est pas prouvable dans$\mathsf{ZFC}$. Mais ce n'est pas un problème tant que votre théorie est fixe et formulée en$\mathsf{ZFC}$ (qui exige qu'il ne contienne pas lui-même des métathéorèmes tels que «pour tout $n$ nous pouvons prouver ce qui suit dans $\mathsf{ZFC}$”). C'est donc à vous de vérifier que c'est bien le cas pour HTT (et, si vous êtes assez courageux, trouvez le bon$n$).
(Juste pour donner une idée de la façon dont les types de cardinaux impliqués, les cardinaux $\kappa$ tel que $V_\kappa$ est un modèle de $\mathsf{ZFC}_1$ sont les points fixes du $\gamma \mapsto \beth_\gamma$une fonction. Je ne pense pas qu'il y ait aucun espoir pour une description raisonnable de la$\kappa$ tel que $V_\kappa$ est un modèle de $\mathsf{ZFC}_n$ pour tout béton $n\geq 2$. Voir aussi cette question .)
- Signification des prédicats avec au plus $n$ des ensembles alternés de quantificateurs non bornés, commençant par des quantificateurs existentiels, suivis d'une formule avec des quantificateurs bornés (signification de la forme $\forall x\in y$ ou alors $\exists x\in y$).
OK, j'ai passé une grande partie de la journée à essayer de comprendre cela en regardant en détail HTT. Cela a été une véritable aventure; J'ai définitivement changé ma perspective à plusieurs reprises au cours du processus. Actuellement, il me semble que la réponse est que HTT, tel qu'il est écrit, peut être lu dans ce système formel. (Donc, c'est comme dans la blague où, après les heures, quelqu'un dit "Oui, c'est évident." Il y a certainement des points où l'interprétation correcte doit être choisie, mais comme dans tout texte mathématique, c'est déjà le cas de toute façon.) Donc avec cette réponse, je veux avancer un argument selon lequel HTT peut être lu dans ce système formel, en essayant d'expliquer un peu comment interpréter certaines choses au cas où une ambiguïté pourrait survenir, et pourquoi je pense que la lecture de cette façon tout devrait fonctionner. Mais il est assez probable que j'ai oublié quelque chose d'important, alors corrigez-moi s'il vous plaît!
Comme le note Tim Campion, la plupart des premiers éléments fonctionnent sans problème - en fait, ils ne mentionnent même pas les univers. Tant que ce n'est pas le cas, tout fonctionne en$V_{\kappa_0}$, dans $V_{\kappa_1}$, et en $V$, et le schéma d'axiome donné garantit même que toutes les constructions faites seront compatibles.
Il faut être plus attentif quand on atteint les chapitres 5 et 6. Je vais essayer de présenter quelques définitions et propositions de ces chapitres à partir de trois points de vue différents.
Le point de vue classique de ZFC, ou (de manière équivoque) celui de la théorie de von Neumann - Bernays - Gödel (NBG), qui autorise les classes en plus des ensembles, nous pouvons donc parler de la catégorie (de la taille de la classe) de tous les ensembles $\mathrm{Set}$.
Le point de vue de HTT, qui sont les univers ZFC + Grothendieck.
Le point de vue de la théorie des ensembles de Feferman, sous la forme énoncée dans la question. (En fait, je ne sais plus si j'ai vraiment besoin de ces limites de cofinalité. Mais il est bon de savoir qu'elles peuvent être supposées.)
Notez que la question posée suppose que l'on s'intéresse vraiment au premier point de vue, et aux autres uniquement dans la mesure où ils sont des commodités pour prouver quelque chose sur le premier cadre. Cela s'aligne avec le contenu des chapitres 5 et 6: toute la théorie des catégories présentables s'intègre parfaitement dans le premier contexte, aussi philosophiquement.
OK, alors rappelez-vous qu'une catégorie présentable - permettez-moi de m'en tenir aux catégories au lieu de $\infty$-catégories, la différence n'est pas essentielle pour nos préoccupations - est une catégorie (de la taille d'une classe) $C$ qui admet toutes les petites colimites, et de telle sorte que pour certains cardinaux réguliers $\kappa$, il y a une petite catégorie $C_0$ et une équivalence $C\cong \mathrm{Ind}_{\kappa}(C_0)$,
c'est à dire $C$ s'obtient en joignant librement $\kappa$-colimites filtrées à $C_0$. (En particulier,$C_0$ équivaut nécessairement à la sous-catégorie complète de $\kappa$-objets compacts de $C$.) En particulier, les catégories présentables sont déterminées par une petite quantité de données. De plus, l'idée est que$C$est vraiment la catégorie de tous les objets (ensembles, groupes, peu importe). Ce point de vue est vraiment le plus clairement articulé en 1), tandis qu'en 2) et 3) la notion de présentabilité dépend à nouveau de l'univers, et du coup ils ne contiennent à nouveau que de petits ensembles / groupes / ...; permettez-moi donc de les appeler en conséquence petits-présentables. Notez que cette notion a un sens à la fois dans 2) et 3), et elle ne dépend que de$V_{\kappa_0}$. Une catégorie small-presentable est alors en particulier small-definable, donc vit dans$\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$, où cette inclusion est une égalité en 2) (mais pas en 3)).
Dans 2), on définirait généralement une petite catégorie présentable comme un type spécial de grande catégorie, ce qui est l'approche de HTT. Mais ici, je suis déjà en train de devenir un peu confus: il semble y avoir deux notions de foncteurs$F: C\to D$: Ceux définissables dans $V_{\kappa_0}$, de manière équivalente $F\in V_{\kappa_0+1}$ (à savoir, $V_{\kappa_0+1}$ sont exactement les classes de $V_{\kappa_0}$), ou tous les foncteurs de $V_{\kappa_1}$. Il ne me semble pas évident qu'un foncteur$F: C\to D$ dans $V_{\kappa_1}$ réside dans $V_{\kappa_0+1}$, comme $C$ et $D$ eux-mêmes ne vivent que dans $V_{\kappa_0+1}$. La différence entre ces deux notions disparaît lorsqu'on se limite aux foncteurs accessibles, tous définissables. Notez que 1) dit que c'est vraiment la première notion dont nous devrions nous soucier! (Avant d'écrire ce post, je n'étais pas au courant de la différence.)
En 3), la bonne manière de procéder est d'utiliser la perspective dictée par 1), qui est celle de "$V_{\kappa_0}$-catégories définissables ", donc ils vivent dans $\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$. On peut à nouveau les considérer comme$\kappa_1$-petites catégories. Au début je pensais qu'il y aurait ici une différence substantielle entre les approches de 2) et 3), mais en fait il semble que dans les deux cas on arrive à deux notions différentes de foncteurs, qui se réconcilient une fois qu'on se limite aux foncteurs accessibles.
L'un des principaux théorèmes est le théorème du foncteur adjoint: Si $F: C\to D$est un foncteur de catégories présentables qui préserve toutes les petites colimites, puis il admet un adjoint à droite. Que signifie réellement ce théorème?
En 1), cela signifie qu'il y a un foncteur $G: D\to C$ - ce qui signifie en particulier qu'il doit être définissable par des formules, car c'est ce que sont les foncteurs entre catégories de taille de classe - ainsi que des transformations d'unité et de comptage (définissables!) satisfaisant aux conditions habituelles.
En 2), on concerne simplement $C$ et $D$ comme étant petit quand on le considère $V_{\kappa_1}$et y affirme alors l'existence de l'adjoint de droite. Sans plus d'informations, cela ne semble en fait pas donner ce que nous voulions en 1), comme a priori$G$(et les transformations d'unité et de pays) se trouvent toutes dans l'univers plus large. Mais cette information peut être obtenue en se rappelant que$G$ est en fait accessible (une partie du théorème du foncteur adjoint que j'ai omis de déclarer ci-dessus, mais devrait être incluse), et donc tout est déterminé sur un ensemble.
En 3), on aimerait à nouveau arriver au résultat de 1), mais on peut essayer de le faire comme en 2) en prouvant d'abord l'existence de telles données dans $V_{\kappa_1}$ puis prouvant l'accessibilité, cédant ainsi que tout réside dans $\mathrm{Def}(V_{\kappa_0})$.
Voyons comment cela se produit dans quelques premiers endroits du chapitre 5 où les univers sont utilisés.
Définition 5.1.6.2: Soit $C$être une catégorie qui admet toutes les petites colimites. Un objet$X\in C$est complètement compact si le foncteur$j_X: C\to \widehat{\mathrm{Set}}$ coprésenté par $X$ préserve les petites colimites.
Ici $\widehat{\mathrm{Set}}$ est la (très grande) catégorie d'ensembles dans $V_{\kappa_1}$. Interprétons ce que cette définition signifie dans les systèmes ci-dessus.
Ici $C$est une catégorie (peut-être de la taille d'une classe). Notez que, en particulier en HTT, «localement petit» n'est pas une hypothèse standard, donc cela permet même aux morphismes entre deux objets d'être des ensembles appropriés. Pour cette raison, le foncteur doit vraiment aller à$\widehat{\mathrm{Set}}$, et c'est quelque chose dont nous ne pouvons pas parler dans ce contexte. Il faudrait donc reformuler la condition pour répondre à cette objection; cela ne devrait pas être difficile, mais peut être un peu désagréable.
Je pense qu'il est implicite dans la définition que $C$ est une catégorie qui appartient à $V_{\kappa_1}$. Il s'agit de capturer strictement la configuration de 1) en ce que si$C$ est petit-définissable comme venant de 1), alors tout petit diagramme de colimite dans $C$ est automatiquement définissable en petit.
Ici, nous avons deux choix: soit celui de 1) ou celui de 2), et ils donnent des notions différentes. En cas de conflit, la perspective de 1) est la bonne, donc$C$est petit-définissable, et on demande la commutation avec des colimites de petits diagrammes définissables. Mais alors que dans 1) nous avons eu du mal à formuler la condition, les univers à portée de main dans 3) signifient que la condition peut maintenant être formulée: nous pouvons demander qu'elle prenne de petites colimites définissables en$C$ aux colimites dans $\widehat{\mathrm{Set}}$. Ici$\widehat{\mathrm{Set}}$ sont les ensembles dans $V_{\kappa_1}$.
Donc dans ce cas, le résultat est qu'il faut être un peu prudent dans 3) sur l'interprétation, mais guidé par 1) on peut donner la bonne définition; et puis le système aide réellement.
Proposition 5.2.6.2: Soit $C$ et $D$être des catégories. Puis les catégories$\mathrm{Fun}^L(C,D)$ des foncteurs adjoints à gauche de $C$ à $D$, et $\mathrm{Fun}^R(D,C)$ des foncteurs adjoints à droite de $D$ à $C$ sont (canoniquement) équivalents les uns aux autres.
Dans cette perspective, cette proposition n'a vraiment de sens que lorsque $C$ et $D$ sont petits, comme autrement $\mathrm{Fun}(C,D)$est trop grand. (On veut considérer de telles catégories de foncteurs quand$C$ et $D$sont présentables (ou accessibles), mais uniquement en se limitant à des foncteurs accessibles. C'est donc une discussion qui apparaîtra plus tard dans le chapitre 5.) Alors la déclaration est assez claire, et la preuve donnée s'applique.
Dans cette perspective, je pense que c'est la même chose qu'en 1), sauf qu'on peut aussi formuler le même résultat dans un univers différent.
Pareil ici.
Notez cependant qu'en l'état, en 1) cette proposition ne peut pas (encore) être appliquée au cas où $C$ et $D$sont présentables. En 2) et 3), les (petits) présentables sont des grandes catégories spéciales auxquelles le résultat s'applique. Notez cependant que les catégories de foncteurs et leur équivalence vivent toutes dans un univers plus vaste, et nous n'obtenons aucune information à leur sujet.$V_{\kappa_0+1}$ ou alors $\mathrm{Def}(V_{\kappa_0})$.
La proposition suivante considère la catégorie pré-feuilles $\mathcal P(C)=\mathrm{Fun}(C^{\mathrm{op}},\mathrm{Set})$, et la preuve est un argument typique impliquant le passage à un univers plus large pour résoudre les problèmes d'homotopie-cohérence.
Proposition 5.2.6.3: Soit $f: C\to C'$ être un foncteur entre les petites catégories et laisser $G: \mathcal P(C')\to \mathcal P(C)$ être le foncteur induit des catégories pré-feuilles induites par la composition avec $f$. Puis$G$ est juste adjoint de $\mathcal P(f)$.
Ici $\mathcal P(f)$ est définie comme étant la petite extension unique préservant les colimites de $f$ (sous l'intégration Yoneda).
Ici, nous avons deux catégories et foncteurs de la taille d'une classe entre eux, tous définissables (comme il se doit). La proposition nous demanderait de trouver (définissables!) Des transformations d'unité et de compte, faisant basculer certains diagrammes. Cela ne semble pas trop difficile. Mais en$\infty$-catégories, il est notoirement difficile de définir les foncteurs à la main, donc ce n'est pas vraiment ainsi que Lurie procède!
Ici $\mathcal P(C)$ et $\mathcal P(C')$sont des grandes catégories spéciales. Lurie applique en fait la grande incorporation de Yoneda dans la preuve. Donc, cela ne produit vraiment les adjonctions d'unité et de pays que dans un univers plus vaste. Comme discuté ci-dessus, je pense que cette preuve ne donne pas réellement ce que nous voulions en 1)!
Nous pouvons argumenter comme le fait Lurie pour produire les données dans un «univers» plus large. (Edit: En fait, comme le souligne Tim Campion, il faut faire un petit détour pour justifier ce qui est écrit. Voir les commentaires à sa réponse.)
Ainsi, lors de la lecture de cette proposition, dans le système 2) ou 3), on devrait faire un marqueur mental que jusqu'à présent l'énoncé prouvé est plus faible que ce que l'on pourrait naïvement espérer. Mais cela est corrigé plus tard, en observant que tout est déterminé par une petite quantité de données.
Upshot: Alors qu'au début je pensais qu'il y aurait une différence substantielle entre 2) et 3), je pense en fait qu'il n'y en a (presque) pas. Une différence est que$\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$ est une bonne inclusion, mais dans la pratique, le moyen de garantir le confinement dans $V_{\kappa_0+1}$ semble être de prouver la définissabilité dans $V_{\kappa_0}$ (par exemple, en prouvant que certains foncteurs sont accessibles).
OK, dites-moi maintenant pourquoi cela ne fonctionne pas! :-)
Répondre à cette question dépend fortement de ce que vous attendez exactement de la théorie des topos supérieurs, car exprimer une force logique élevée est un objectif différent de celui d'exprimer un cadre logique parfaitement unifié pour la géométrie algébrique et la théorie des nombres. Des bases solides et unifiées pour les mathématiques catégorielles générales sont un bon objectif, et semblent être le but de nombreux contributeurs ici. Pour cet objectif, tout ce qui est dit dans les commentaires et les réponses à cette question est pertinent. Mais un travail approprié en géométrie et en théorie des nombres n'exige pas une grande force logique.
Alors que HTT est plus étroitement lié aux univers que SGA, ni HTT ni SGA n'utilisent réellement le schéma d'axiome (très fort) du remplacement. Ainsi, ils peuvent utiliser des «univers» radicalement plus faibles que ceux de Grothendieck. À titre d'exemple typique et pertinent, Grothendieck a fait un seul appel au schéma axiomatique du remplacement. C'est dans sa preuve tout à fait cruciale que chaque catégorie AB5 avec un groupe électrogène a suffisamment d'injectifs. Et cette utilisation du remplacement s'avère éliminable. Cela a fonctionné, mais Grothendieck n'en avait pas vraiment besoin pour obtenir son résultat.
Pour développer l'utilisation du remplacement par Grothendieck: Reinhold Baer dans les années 1940 a utilisé l'induction transfinie (qui nécessite le schéma axiome du remplacement) pour prouver que les modules (sur un anneau donné) ont suffisamment d'injectifs. Il explorait consciemment de nouvelles techniques de preuve et a obtenu un bon résultat. Tohoku de Grothendieck a présenté cette preuve sous une forme montrant que chaque catégorie AB5 avec un petit ensemble de générateurs a suffisamment d'injectifs - et quelques années plus tard, Grothendieck a découvert que c'était exactement le théorème dont il avait besoin pour la cohomologie des topos. Baer et Grothendieck avaient tous deux des objectifs pratiques, non liés aux préoccupations des fondations, mais tous deux voulaient également créer de bonnes fondations. Et ils l'ont fait. Mais il s'avère qu'ils auraient pu obtenir ces mêmes théorèmes, correctement, sans remplacement, par à peu près les mêmes preuves, en spécifiant des ensembles de fonctions suffisamment grands pour commencer (en utilisant le jeu de puissance, mais pas le remplacement). Il y a des résultats qui nécessitent véritablement le schéma d'axiomes de remplacement. Mais ces résultats se produisent rarement en dehors de la recherche fondamentale.
Beaucoup de gens venant d'angles très différents (certains logiciens, certains n'aiment pas la logique) depuis les années 1960 ont remarqué que dans le contexte de la géométrie algébrique et de la théorie des nombres, la grande force logique de l'axiome de l'univers de Grothendieck est un sous-produit inutilisé de Le désir de Grothendieck d'un cadre unifié pour la cohomologie. Cela peut maintenant être rendu assez précis: l'ensemble de l'appareil de Grothendieck, y compris non seulement la cohomologie de foncteurs dérivés des topos, mais la catégorie 2 des toposes, et les catégories dérivées, peut être formalisé presque exactement de la même manière qu'il a été formalisé par Grothendieck, mais à force logique bien en dessous de Zermelo-Fraenkel ou même de la théorie des ensembles de Zermelo. La même chose est vraie pour HTT. Vous pouvez l'obtenir sans univers inaccessibles ni réflexion tant que vous n'avez pas besoin de la grande force (et rarement utilisée) du remplacement. La preuve n'a pas été réellement donnée pour HTT. C'était pour les utilisations des univers de Grothendieck . Il semble clair que la même chose fonctionnera pour HTT.
La force logique nécessaire a été exprimée de différentes manières: théorie des types simples (avec arithmétique), arithmétique d'ordre fini, théorie élémentaire de la catégorie des ensembles, théorie des ensembles de Zermelo quantificateurs bornés. En gros, vous posez un ensemble de nombres naturels, et vous posez que chaque ensemble a un ensemble de puissances, mais vous ne posez pas d'itération illimitée d'ensembles de puissances. Une théorie assez naïve des univers peut être donnée conservatrice sur n'importe lequel de ces derniers (la façon dont la théorie des ensembles de Godel-Bernays est conservatrice sur ZFC) et adéquate à tout le grand appareil de structure de l'école de Grothendieck.
Je considérerais une extension conservatrice de ZFC obtenue à partir de ZFC par l'adition d'une constante $\alpha$ et les axiomes suivants:
$\alpha$ est un ordinal ($Ord(\alpha)$).
La phrase $\phi\leftrightarrow\phi^{V_\alpha}$, pour chaque phrase dans la langue d'origine $\phi$ (schéma d'axiomes).
$V_{\alpha}$ se comporte comme $V$(pour toutes les phrases dans le langage de la théorie des ensembles). Si deux univers (ou plus) sont nécessaires, on peut ajouter une autre constante$\beta$ avec les axiomes correspondants et l'axiome $\alpha<\beta$.
La preuve que la théorie qui en résulte est conservatrice sur ZFC est facile.
Suppose que $\phi$ est prouvable à partir des nouveaux axiomes (axiomes utilisant $\alpha$), dans lequel $\phi$est dans la langue d'origine. Puisque toute preuve est finie, il y a un nombre fini de phrases$\phi_1$, ..., $\phi_n$ tel que
$Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}})\rightarrow \phi$
est prouvable sans aucun nouvel axiome. Par conséquent, on peut penser à$\alpha$comme une variable libre et la phrase ci-dessus est prouvable dans ZFC (théorème sur les constantes). Depuis$\alpha$ ne se produit pas dans $\phi$, l'implication suivante est prouvable dans ZFC ($\exists$-introduction):
$\exists\alpha(Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}}))\rightarrow \phi$
Maintenant, le principe de réflexion pour ZFC dit que l'antécédent est un théorème ZFC. De modus ponens, ZFC prouve$\phi$.
Ainsi, vous pouvez travailler avec les nouveaux axiomes et $V_{\alpha}$ se comporte comme un univers, et tout ce qui est prouvé qui ne mentionne pas $\alpha$ peut être prouvé déjà dans ZFC.
Une question qui a été soulevée dans les commentaires portait sur la motivation pour poser la question. Permettez-moi d’aborder cette question ici.
Avant tout, il s'agit d'apprendre! Comme je l'ai mentionné dans la question initiale, je me suis amusé avec des limites cardinales «stupides», et je n'ai appris que plus tard le principe de réflexion, donc je voulais comprendre ce qu'il peut faire (et ce qu'il ne peut pas faire), et si je peut en quelque sorte automatiquement reléguer toute autre version compliquée de telles estimations dans cette machine. C'est donc la chose habituelle où vous trébuchez dans une pièce sombre et que vous aimeriez beaucoup que la pièce soit éclairée! Alors, merci à vous tous pour les réponses éclairantes!
Une autre raison est que récemment, j'ai été un peu frustré par la solution des univers Grothendieck au problème actuel. Laisse-moi expliquer.
Je veux vraiment parler de la catégorie de tous les ensembles, ou de tous les groupes, etc., et je veux prouver des théorèmes à ce sujet. Et, au moins dans la version von Neumann-Bernays-Gödel (NBG) de la théorie ZFC qui autorise les classes, c'est une notion parfaitement valide. Je trouve donc ontologiquement très agréable de travailler dans ce contexte, et j'aimerais beaucoup que le théorème du foncteur adjoint soit un théorème sur les catégories (présentables) dans ce sens.
Désormais, les catégories présentables sont déterminées par une petite quantité de données, de sorte que l'on peut toujours travailler avec cette petite quantité de données et suivre attentivement les tailles relatives. En fait, de nombreuses preuves en HTT gardent explicitement une trace de ces tailles relatives, mais il y a encore quelques endroits où il est agréable d'aborder une «vue plus large» et de regarder ces grandes catégories comme si elles étaient petites.
En effet, le théorème du foncteur adjoint concerne les foncteurs entre grandes catégories, et il devient vite désagréable d'en parler depuis NBG / ZFC. Notez que l'énoncé du théorème du foncteur adjoint a un sens parfait - il demande simplement que toutes les données de l'adjonction soient définissables. Mais c'est un peu méchant d'essayer de parler de ces choses «de l'intérieur». Ce serait donc bien d'avoir une sorte de méta-théorie pour argumenter sur ces grandes catégories et faire semblant qu'elles sont petites. La question subtile de la «définissabilité de l'intérieur» est peut-être a priori perdue dans cette méta-théorie, mais je considère cette question de la «définissabilité de l'intérieur» comme centrale, car après tout ce que je voulais était un théorème sur tous les ensembles, alors je ' Je suis d'accord pour avoir à y prêter un peu d'attention - et, pour enlever la punchline, il s'avère que c'est précisément la différence entre travailler avec les univers de Grothendieck et travailler avec les «univers» de Feferman.
C'est donc à cela que servent les univers de Grothendieck: ils vous donnent toujours un univers plus grand pour n'importe quel univers dans lequel vous travaillez actuellement. Je trouve que l'existence des univers de Grothendieck est complètement intuitive, et en fait, postuler leur existence semble tout à fait comparable à la position d'un ensemble infini en premier lieu: vous permettez simplement de rassembler tout ce que vous avez déjà dans une entité plus grande.
Mais maintenant, tout à coup, ce à quoi je pensais que tous les ensembles s'appellent les petits ensembles, et il y a aussi de nombreux ensembles plus grands. Donc même si je prouve un théorème de foncteur adjoint dans ce cadre, ce n'est plus un théorème sur les foncteurs entre catégories de tous les ensembles / groupes / ..., mais seulement un des foncteurs entre petits ensembles / groupes / .... Donc si vous pensez-y, même dans les univers ZFC + Grothendieck, vous ne prouverez jamais le théorème que vous vouliez réellement, sur la catégorie de tous les ensembles. (En fait, jusqu'à très récemment, j'ai supposé que le théorème du foncteur adjoint (pour$\infty$-categories) est une déclaration de ZFC qui a été prouvée sous "ZFC + Universes", mais ce n'est pas tout à fait vrai: la déclaration qui a été prouvée ne peut même être formulée que dans les univers ZFC +.)
Ce qui a été prouvé, c'est qu'il est cohérent que le théorème du foncteur adjoint est vrai . À savoir, en supposant la cohérence des univers ZFC +, vous avez maintenant produit un modèle de ZFC - celui des petits ensembles dans votre modèle des univers ZFC + - dans lequel le théorème est vrai. Donc, vous pouvez maintenant travailler dans la théorie "ZFC + le théorème du foncteur adjoint", dans laquelle le théorème du foncteur adjoint peut être appliqué à la catégorie de tous les ensembles / groupes / ..., mais cela me semble définitivement une triche. Vous n'avez même pas prouvé que "ZFC + Univers + le théorème du foncteur adjoint" est cohérent! (Vous obtiendrez cela si vous commencez avec la cohérence d'un peu plus d'univers ZFC +, en demandant$\kappa$ tel que $V_\kappa$satisfait les univers ZFC +. Encore une fois, cela me semble être une hypothèse tout à fait juste - continuez simplement.) Mais maintenant, vous pourriez voir le danger de gravir par inadvertance l'échelle de cohérence alors que vous commencez implicitement à invoquer de plus en plus de théorèmes prouvés pour les petits ensembles également pour tous les ensembles.
Ce serait bien mieux si vous saviez que, dans les univers ZFC + Grothendieck, tout ce que vous avez prouvé sur les petits ensembles est aussi un théorème sur toute la catégorie ambiante de tous les ensembles. Ce n'est pas automatique, mais vous pouvez l'ajouter en tant que schéma d'axiome. Mike Shulman dans la section 12 de la théorie des ensembles pour la théorie des catégories (arXiv: 0810.1279) discute de cette idée (qu'il désigne ZMC): je la trouve ontologiquement assez plaisante, elle semble aussi avoir une axiomatisation très simple (encore plus simple que ZFC!), mais
a) ce schéma d'axiome supplémentaire ne me paraît pas tout à fait évident: pourquoi tout ce qui est vrai dans les petits ensembles devrait-il aussi s'appliquer à tous les ensembles? (Surtout si nous avons eu des problèmes prouvant le résultat souhaité en premier lieu Aussi, notez qu'il ne certainement. Pas tenir pour toute notion de petits ensembles: Au contraire, les garanties de schéma axiome qu'il ya une notion de petits ensembles pour lesquels ce genre de réflexion tient. Maintenant, cela me semble un peu douteux car en premier lieu je n'ai jamais voulu de petits ensembles, alors maintenant je les pose, et je demande également qu'ils reflètent toujours l'ensemble du comportement de tous les ensembles. Probablement bien, mais pas cela va de soi pour moi.)
b) la force de cohérence de ce schéma d'axiome est considérablement plus élevée: c'est la même chose que la cohérence d'un cardinal Mahlo. C'est toujours aussi bas que les grands cardinaux, mais c'est beaucoup plus élevé que les simples univers de Grothendieck (qui sont vraiment bas au bas de la hiérarchie).
En ce qui concerne a), le fait que nous puissions prouver la cohérence du théorème du foncteur adjoint à partir de la cohérence des univers de Grothendieck pointe dans la bonne direction, mais cela ne garantit pas en soi que les deux ensemble sont cohérents. Je peux imaginer que je pourrais me convaincre que le schéma d'axiome est raisonnable, mais je pense certainement qu'il a besoin de beaucoup plus de justification que de simples univers de Grothendieck. (Question secondaire: Quelle est la taille des grands cardinaux que l'on peut justifier en utilisant l'idée de "permettre de rassembler tout ce que nous avions déjà"? Je ne sais pas si c'est une question complètement bien définie ... mais pour moi, une le cardinal mesurable n'est certainement pas de ce genre (mais je suis heureux d'être corrigé), car il semble postuler l'émergence de nouvelles caractéristiques combinatoires.)
Une autre raison pour laquelle j'ai récemment été un peu mécontent des univers de Grothendieck est que, même si, dans un certain sens, nous aimerions les utiliser pour pouvoir ignorer les subtilités de la théorie des ensembles, d'une certaine manière, ils reviennent pour vous mordre, comme maintenant vous devez le spécifier dans dans quel univers vivent certaines choses. Parfois, vous devrez peut-être même spécifier plusieurs univers différents pour différents types d'objets (pensez aux gerbes sur des ensembles profinis), et je trouve que cela devient rapidement assez moche. Je préférerais de loin que tous les objets vivent ensemble dans un seul univers.
Ainsi, en pensant aux faisceaux sur des ensembles profinis, je suis arrivé à trouver la solution avec un seul univers beaucoup plus esthétiquement et ontologiquement agréable, et cette solution (ensembles condensés) peut être formalisée en ZFC sans problème.
OK, donc je prétends que les univers de Grothendieck n'ont pas vraiment résolu le problème qu'ils se proposaient de résoudre, car
a) ils ne vous permettent toujours pas de prouver des théorèmes sur la catégorie de tous les ensembles / groupes / ... (sauf comme résultat de cohérence, ou sous de grands axiomes cardinaux plus forts)
b) en travaillant avec eux, vous devez toujours vous soucier des problèmes de taille - votre catégorie de tous les ensembles est maintenant stratifiée en ensembles de toutes sortes de tailles différentes (c'est-à-dire dans des univers différents).
De plus, ils augmentent également la force de consistance.
Maintenant, après cette merveilleuse discussion ici, je pense que la proposition de Feferman est en fait bien meilleure. Cependant, comme l'a également commenté Mike Shulman, je ne considère pas les axiomes de Feferman comme décrivant un monde ontologiquement correct, mais je considère les «univers» de la théorie de Feferman simplement comme des commodités, afin de parler de grandes catégories comme si elles étaient petites. En d'autres termes, la théorie de Feferman vous donne exactement une méta-théorie dans laquelle discuter de ces grandes catégories de «l'extérieur». Mais c'est une théorie que je n'utiliserais jamais que pour donner une preuve d'un théorème de ZFC. Comparée aux univers de Grothendieck, la théorie de Feferman
a) ne vous permettent de démontrer des théorèmes de la catégorie de tous les ensembles / groupes / ..., car il inclut explicitement un schéma d'axiome que tous les théorèmes de petits ensembles sont également théorèmes sur tous les jeux.
b) Bien sûr, dans une preuve d'un théorème de ZFC qui invoque des problèmes de taille non triviaux, il est très bienvenu que la théorie vous permette de parler de différentes tailles. De plus, il le fait d'une manière où vous pouvez toujours appliquer tous les axiomes de ZFC à chacun des "univers", et prend également soin "dans les coulisses" de la façon de tout réécrire en termes de limites cardinales (potentiellement extrêmement subtiles) dans ZFC lui-même. C'est donc comme un langage de programmation de haut niveau pour les arguments impliquant des estimations cardinales difficiles dans ZFC.
De plus, cela n'augmente pas la force de cohérence, et en fait toutes les déclarations de ZFC prouvées dans ce langage sont des théorèmes de ZFC. (Comme je l'ai rappelé ci-dessus, nous pourrions également avoir a) + b) avec les univers Grothendieck, mais nous atteindrions alors la cohérence d'un cardinal Mahlo.)
Donc, le résultat est que je pense que les univers de Feferman font un bien meilleur travail pour résoudre le problème de fournir une méta-théorie pour "parler de grandes catégories comme si elles étaient petites" que les univers de Grothendieck.
Permettez-moi d'ajouter quelques raisons finales pour poser la question. Je pense que les techniques de catégories supérieures telles que celles présentées dans HTT sont d'une importance très centrale, non seulement dans la topologie algébrique d'où elles sont originaires, mais dans toutes les mathématiques. Je peux certainement en témoigner en ce qui concerne la théorie des nombres et la géométrie algébrique. Leur centralité est donc également une raison importante pour analyser leur force de cohérence.
La lecture de HTT est une question très non triviale - c'est long et compliqué. Certains collègues de la théorie des nombres ont cependant dit que l'une des principales raisons pour lesquelles ils ne pouvaient pas lire HTT est qu'il utilise des univers . A savoir, ils sont tellement habitués à ZFC (et à vérifier avec un soin extrême!) Qu'ils essaieront automatiquement d'éliminer toute utilisation d'univers dans un argument. Maintenant, dans SGA, du moins si vous n'étiez intéressé que par des applications pour étaler la cohomologie de schémas raisonnables, c'était quelque chose que vous pouviez à la main - par exemple, ajoutez simplement quelques hypothèses de comptabilité pour rendre les choses petites. Cependant, en HTT, je ne vois aucun moyen que quelqu'un puisse mettre des limites cardinales au fur et à mesure que vous lisez - les arguments sont beaucoup trop complexes pour cela.
Alors maintenant, j'espère pouvoir leur dire qu'ils peuvent vérifier que tout fonctionne dans ZFC, et qu'ils peuvent toujours lire HTT (essentiellement) comme écrit, s'ils le lisent dans la théorie des ensembles de Feferman. S'ils vérifient soigneusement (ce qu'ils feront), ils auront peut-être encore besoin de remplir un petit lemme ici et un petit argument supplémentaire là-bas - mais ils devraient le faire de toute façon, dans n'importe quel livre d'environ 1000 pages, et j'imagine que moins de la moitié de ces remarques secondaires ont à voir avec le remplacement des univers de Grothendieck par les «univers» de Feferman. Si quelqu'un entreprend réellement ce projet, il mérite bien sûr tout le mérite s'il réussit ce travail important!
Permettez-moi de terminer par une très brève note sur ce qui semble être le point saillant clé de la traduction de la théorie de Feferman. J'en suis venu à apprécier le point soulevé par Tim Campion dans sa réponse, et je vois maintenant que cela a également été mentionné dans la deuxième réponse de Jacob Lurie. En gros, c'est le suivant. Si$C$ est une catégorie présentable, alors il y a une petite catégorie $C_0$ tel que $C=\mathrm{Ind}_\kappa(C_0)$
pour un cardinal régulier $\kappa$, attenant librement tous les petits $\kappa$-colimites filtrées. Cela fait$C$ naturellement une union de $C_\tau$'s, où $C_\tau$ ne recueille que le $\tau$-petit $\kappa$-colimites filtrées. Ici$\tau$ est un cardinal régulier tel que $\tau\gg \kappa$. Cette structure croissante de$C$ comme union de $C_\tau$'s est central dans la théorie des catégories présentables, mais les niveaux sont réellement énumérés par (certains) cardinaux réguliers $\tau$. Si vous augmentez votre univers, vous obtenez également une version plus grande$C'$ de $C$ lui-même, et dans les univers de Grothendieck $C$ est maintenant l'une des belles couches $C'_\tau$ de $C$, où $\tau$est le cardinal de coupure de l'univers précédent. Mais dans les univers de Feferman, ce$\tau$n'est pas régulier. Cela peut rendre certains arguments plus subtils, mais je m'attendrais à ce que l'on puisse généralement résoudre ce problème en intégrant simplement$C$ dans certains $C'_\tau$ avec $\tau$ un cardinal régulier plus grand que le cardinal de coupure du petit univers.
En réponse à l'édition qui cloue les choses à un système formel impliquant des cardinaux $\kappa_{-1} < \kappa_0 < \kappa_{1/2} < \kappa_1$:
Je vais sortir sur une branche peut-être plus malavisée et prédire que pour intégrer les chapitres 1 à 4 dans ce système formel, aucune véritable arithmétique cardinale ne sera nécessaire. Au contraire, pour cette partie du livre, tout ce que vous aurez à faire est de passer en revue et d'ajouter à diverses déclarations de théorèmes des hypothèses de la forme "$X$ est $\kappa_{-1}$-small ". Après tout, cette partie du livre ne traite en réalité que des petits objets, à l'exception de quelques grands objets particuliers comme la catégorie des petits ensembles simplicial, la catégorie des petites catégories simplicial, etc., et des choses comme Différentes structures de modèle sont construites, mais je crois que dans chaque cas, on peut se débrouiller en utilisant le cas particulier de l'argument petit objet pour générer des cofibrations / cofibrations acycliques entre des objets finiment présentables, de sorte qu'aucune induction transfinie n'est nécessaire. À première vue, le redressement / le redressement a l'apparence de constructions qui pourraient utiliser la théorie des ensembles de manière sérieuse, mais je vais aller de l'avant et prédire qu'elles ne posent aucun problème au système formel proposé.
Le chapitre 5 devient plus ennuyeux. Je crois qu'il faudra faire des choix prudents sur les théorèmes de base de présentable ($\infty$) -catégories. Ce qui rend les catégories présentables cochées, c'est qu'elles empaquetent très proprement le théorème du foncteur adjoint, mais comme vous le dites, le théorème du foncteur adjoint ordinaire est livré avec des mises en garde dans ce contexte. Je pourrais aller jusqu'à dire que tout l'intérêt de la réflexion sur les catégories présentables en premier lieu est complètement annulé dans ce contexte. Vous ne serez pas en mesure de prouver des choses de base comme "les catégories présentables sont précisément les localisations accessibles des catégories pré-feuilles". Je prédis que quels que soient les choix qui seront faits concernant la formulation de versions faibles des théorèmes de base des catégories présentables dans ce contexte, il y aura une application ou une application potentielle qui en souffrira.
Les chapitres 5 et 6 contiennent également des théorèmes sur des catégories très importantes telles que $\infty$-catégorie de présentable $\infty$-catégories et les $\infty$-catégorie de $\infty$-topoi [1]. Le système semble être tel que ce ne sera pas vraiment un problème en soi , sauf que les problèmes rencontrés dans la théorie de la présentabilité de base seront maintenant aggravés. Tu ne pourras pas le prouver$Pr^L$ est double pour $Pr^R$. Vous ne serez pas en mesure de prouver le théorème de Giraud (enfin, les définitions vont changer de toute façon, donc je devrais clarifier: vous ne serez pas en mesure de prouver que les localisations accessibles exactes des catégories pré-feuilles sont les mêmes que localement petites catégories satisfaisant une liste de conditions d'exhaustivité, de génération et d'exactitude). Donc, tout théorème sur$\infty$-topoi dont la preuve procède en commençant par le cas pré-feuille puis en localisant devra être complètement repensé.
Peut-être que je suis hors de la base ici, mais je crois qu'un travail supplémentaire significatif et des idées mathématiques véritablement nouvelles seraient nécessaires pour les chapitres 5 et 6, et le résultat serait une théorie qui est beaucoup plus difficile à utiliser.
En revanche, je pense que si vous êtes prêt à limiter votre attention aux grandes catégories qui sont définissables à partir de petits paramètres, bien que vous manquiez la belle capacité de dire "nous l'avons prouvé pour les petites catégories, mais maintenant nous pouvons l'appliquer aux grandes ceux », vous vous retrouverez avec une théorie de la présentabilité beaucoup plus utilisable, sans quitter ZFC.
[1] En fait, dans les fondations habituelles, ces catégories ne sont (jusqu'à l'équivalence) que grandes et pas très grandes (plus précisément, elles sont $\kappa_0$-de nombreux objets et $\kappa_0$-sized homs), mais un minimum de travail est nécessaire pour le montrer. Cela sera-t-il toujours le cas dans ce système formel? Je ne suis pas sûr.
EDIT: Un long commentaire en réponse à Peter Scholze réponse .
Une chose que je viens de réaliser est que si$\kappa_0$ n'est pas un $\beth$-fixed-point, alors pas tous les ensembles dans $V_{\kappa_0}$ a la cardinalité $<\kappa_0$, de sorte que les notions de «petitesse» se multiplient. Heureusement, je pense que votre système formel prouve que$V_{\kappa_0}$ possède $\Sigma_1$-replacement, ce qui implique qu'il s'agit d'un $\beth$-un point fixe. Crise évitée!
Peut-être cette approche consistant à utiliser systématiquement des hypothèses de définissabilité dans un «cadre d'univers» sera-t-elle réalisable - combinant le «meilleur des deux mondes». Une bonne chose est que même si vous utilisez explicitement des hypothèses métamathématiques, il semblerait que vous puissiez toujours énoncer et prouver ces théorèmes comme des théorèmes uniques plutôt que comme des schémas.
Je suis un peu confus au sujet de la proposition 5.2.6.3 (la dernière dont vous discutez, et une version bébé du théorème du foncteur adjoint). Je présume que la catégorie présheaf$P(C)$ sera défini comme comprenant ces foncteurs $C^{op} \to Spaces$ qui se trouvent dans $Def(V_{\kappa_0})$. Lorsque nous passons à un univers plus large, la transition est généralement assez transparente, car nous nous attendons à$P(C)$ pour avoir tous les colimits indexés par $\kappa_0$-petites catégories - une propriété parfaitement naturelle avec laquelle travailler $V_{\kappa_1}$. En effet, la première étape de la démonstration de Lurie de 5.2.6.3 est de montrer qu'un adjoint de gauche existe en utilisant le fait que$P(C)$a toutes les petites colimites [2]. Cependant, dans le contexte actuel, nous ne pouvons jamais supposer que$\kappa_0$ est régulier, et par conséquent nous ne pouvons jamais supposer que $P(C)$a tous les petits colimits. Le mieux que l'on puisse dire, c'est que$V_{\kappa_0}$ pense $P(C)$a tous les petits colimits. Tant que nous travaillons dans$V_{\kappa_0}$, cette propriété est "tout aussi bonne" que d'avoir en fait toutes les petites colimites. Mais quand nous passons à$V_{\kappa_1}$, tout à coup, nous devons y penser pour ce qu'il est - une propriété métamathématique. Peut-être que plus tard, je vais m'asseoir et essayer de voir si la preuve de Lurie de 5.2.6.3 peut fonctionner dans ce contexte, mais je pense que, à première vue, ce n'est pas clair.
[2] Ce n'est qu'après avoir vérifié l'existence de manière abstraite de cette manière qu'il montre que l'adjoint de gauche doit être le foncteur indiqué. Bien sûr, cette manœuvre est en fait une complication supplémentaire qui accompagne le$\infty$-catégorie - dans les catégories ordinaires, les formules pour les deux foncteurs peuvent être directement vérifiées comme étant adjointes, mais en $\infty$-catégories la formule de l'adjoint de gauche n'est pas évidemment fonctionnelle.