Étude de cas: que faut-il pour formuler et prouver l'argument du petit objet de Quillen dans ZFC?
Je suis un peu perdu par la question intéressante de Peter Scholze sur la suppression de la dépendance aux univers des théorèmes de la théorie des catégories. En particulier, je suis obligé d'admettre que je ne sais pas vraiment quand le remplacement est invoqué, encore moins quand il est invoqué «de manière essentielle». J'aimerais donc travailler sur un exemple raisonnablement concret du phénomène. Je comprends que le remplacement devrait "vraiment" être considéré comme l'axiome qui permet une récursion transfinie. Je pense que la théorie des catégories a tendance à ne pas utiliser la récursivité de manière intensive (bien que, plus que d'autres branches des mathématiques, elle comporte de nombreuses définitions qui, au moins à première vue, ont une complexité non triviale. formule$\phi(x,y,z,p,q)$ en disant que l'ensemble $z$ et fonctions $p: z \to x$ et $q: z \to y$ sont un produit catégorique des ensembles $x,y$ est syntaxiquement $\Pi_1$, et la déclaration selon laquelle les produits binaires existent dans la catégorie des ensembles est syntaxiquement $\Pi_3$ (en ignorant les quantificateurs bornés bien sûr)).
Le théorème suivant est, je pense, l'une des exceptions notables à la catégorie-théorique-non-utilisation-de-récursivité:
Théorème [Quillen] "L'argument du petit objet": Soit$\mathcal C$ être une catégorie localement présentable, et laissez $I \subseteq Mor \mathcal C$être un petit ensemble de morphismes. Laisser$\mathcal L \subseteq Mor \mathcal C$ être la classe des rétractations de composites transfinis de cobases-changements de coproduits de morphismes dans $I$, et laissez $\mathcal R \subseteq Mor \mathcal C$ comprennent ces morphismes orthogonaux faiblement droit aux morphsims de $I$. Puis$(\mathcal L, \mathcal R)$est un système de factorisation faible sur$\mathcal C$.
Pour la preuve, voir le nlab . Fondamentalement, les factorisations sont construites par récursivité transfinie. La récursivité me semble "essentielle" car de nouvelles données sont introduites à chaque étape de la construction.
Formalisation:
Je pense que ce théorème et sa preuve sont carrément formalisables dans MK, où la distinction "petit / grand" théorique des catégories est interprétée comme la distinction "ensemble / classe" de MK. Je ne me sens pas qualifié pour dire si la preuve fonctionne dans NBG, mais la déclaration a au moins un sens simple.
Lorsqu'il s'agit de formaliser dans ZFC, nous avons des choix à faire concernant la distinction petit / grand:
Une option consiste à introduire un "univers" $V_\kappa$(qui, si nous essayons réellement de travailler dans ZFC, sera une sorte d'univers plus faible que d'habitude). Nous interpréterons «petit» comme signifiant «dans$V_\kappa$". Nous ne considérerons pas les" objets vraiment grands "- tout ce dont nous parlerons sera un ensemble - en particulier, chaque catégorie dont nous parlons sera de taille définie, même si ce n'est pas" petit "en soi. interpréter "catégorie localement présentable" comme signifiant "$\kappa$-cocomplete, localement $\kappa$-petite catégorie avec une forte $\kappa$-petit, $\lambda$-générateur présentable pour certains réguliers $\lambda < \kappa$"(Je ne sais pas si ça fait une différence de dire ça $V_\kappa$ pense $\lambda$ est un cardinal régulier).
Une autre option est de ne pas introduire d'univers, et d'interpréter simplement «petit» pour signifier «taille d'ensemble». Dans ce cas, tout "gros" objet dont nous parlons doit être définissable à partir de petits paramètres. Nous définissons donc une catégorie pour comprendre une classe d'objets définissables par paramètres, une classe de morphismes définissables par paramètres, etc. Cela peut sembler restrictif, mais cela fonctionnera très bien dans le cas présentable localement, car nous pouvons définir une catégorie présentable localement$\mathcal C$ à définir, par rapport aux paramètres $(\lambda, \mathcal C_\lambda)$ (où $\lambda$ est un cardinal régulier et $\mathcal C_\lambda$ est un petit $\lambda$-cocomplete category), comme catégorie de $\lambda$-Et les objets dans $\mathcal C_\lambda$.
Maintenant, pour le théorème en question, l'approche (2) semble plus propre car la "traduction" nécessaire est simple, et une fois qu'elle est faite, la preuve originale devrait fonctionner sans modification. Je pense que les principaux inconvénients de (2) viennent ailleurs. Par exemple, il sera probablement délicat de formuler des théorèmes sur la catégorie des catégories localement présentables. En général, il y aura divers théorèmes sur les catégories qui ont des formulations et des preuves propres et conceptuelles lorsque les catégories impliquées sont petites, mais qui nécessitent des modifications techniques ennuyeuses lorsque les catégories impliquées sont grandes. C'est pour ces raisons que les approches plus comme (1) ont tendance à être privilégiées pour les projets de théorie des catégories à grande échelle.
Supposons donc que nous suivions l'approche (1). La question devient alors:
Question 1: De quel type d'univers exactement avons-nous besoin pour formuler et prouver le théorème ci-dessus en suivant l'approche (1)?
Question 2: Combien d'univers de ce type sont garantis par ZFC?
Vraisemblablement, la réponse à la question 2 sera qu'il y a beaucoup de tels univers - assez pour que nous puissions faire des choses comme, étant donné une catégorie, passer à un univers suffisamment grand pour rendre cette catégorie petite et invoquer le théorème de cet univers. .
Question 3: Jusqu'où devons-nous aller dans les mauvaises herbes pour répondre aux questions 1 et 2?
Doit-on analyser en profondeur la preuve du théorème? Existe-t-il une rubrique simple de critères qui permet de jeter un coup d'œil sur la preuve et, pour 99% des théorèmes comme celui-ci, de dire facilement qu'elle «passe» sans trop se plonger dans les choses? Ou y a-t-il même un métathéorème formel auquel nous pouvons faire appel pour que même un ordinateur puisse vérifier que tout va bien?
Réponses
Le commentaire de Jacob Lurie donne une réponse à la question 1. À savoir, en supposant que les estimations que j'ai données dans mon commentaire sont correctes, pour formuler et prouver le théorème, il suffira de supposer que
- $\kappa$ est régulier
et cela
- pour chaque $\mu < \kappa$, il existe $\rho < \kappa$ tel que $\mu \ll \rho$ (ce qui signifie que $\mu' < \mu, \rho' < \rho \Rightarrow (\rho')^{\mu'} < \rho$).
Peut-être cette propriété de $\kappa$pourrait être considéré comme une «forme» de remplacement. Mais vraiment, ce que nous avons, ce sont deux conditions sur$\kappa$ qui sont purement théoriques des ensembles plutôt que métamathématiques, de sorte que la réponse à la question 1 est quelque chose de beaucoup plus propre que je ne l'avais supposé.
Cela nous permet de répondre à la question 2. Vraisemblablement, le résultat est que ZFC prouve qu'il y a beaucoup, beaucoup de $\kappa$ satisfaisant les deux conditions ci-dessus.
En ce qui concerne la question 3, il semblerait que dans cette approche, nous devons en fait approfondir la preuve. En fait, il semble que pour mener à bien cette approche, nous devons ajouter un véritable contenu mathématique à la preuve, et en fait prouver une affirmation plus forte. Les autres questions deviennent alors
Sera-t-il généralement possible de «constructiviser» «la plupart» des théorèmes de la théorie des catégories de cette manière, ou d'autres problèmes apparaîtront-ils au cours du projet «théorie des catégories ZFC-ify»?
Si la réponse à (1) est «oui» (ou si c'est généralement «non» et que nous nous limitons aux cas où c'est «oui»), alors «combien de travail supplémentaire» serait vraiment un tel projet?
Je suppose que la réponse à (1) est que lorsqu'il s'agit de l'utilisation de la récursivité transfinie dans la théorie des catégories, il sera en effet généralement le cas que l'utilisation du remplacement peut être éliminée d'une manière similaire à celle-ci, mais que plus ce qui est important, j'ai manqué le point: comme Jacob Lurie le soutient en réponse à la question de Peter Scholze, les problèmes plus épineux avec la théorie des catégories ZFC-ifying ne sont pas à voir avec la récursion transfinie mais plutôt avec la possibilité de faire des allers-retours librement entre les «grandes catégories "et" petites catégories "de diverses manières.
Je suppose que la réponse à (2) est que pour "la plupart" des utilisations théoriques des catégories de la récursivité transfinie, il devrait en fait être assez simple de les "constructiviser" afin qu'elles s'intègrent dans un "univers bébé" avec les propriétés ci-dessus ou quelque chose de similaire, et qu'avec juste un peu de pratique, on pourrait développer la capacité de vérifier presque d'un coup d'œil que c'est possible, bien que toujours sur une base théorème par théorème. Mais j'aimerais avoir tort et montrer un théorème de la théorie des catégories où ce genre d'approche échoue!
Enfin, cela laisse ouverte la question de savoir s'il existe une manière "plus automatique" de faire tout cela - peut-être avec une conclusion plus faible que "notre univers n'a pas besoin de satisfaire une forme de remplacement du tout".