Caso di studio: cosa serve per formulare e dimostrare l'argomento del piccolo oggetto di Quillen in ZFC?
Mi sto un po 'perdendo per l' interessante domanda di Peter Scholze sulla rimozione della dipendenza dagli universi dai teoremi nella teoria delle categorie. In particolare, sono costretto ad ammettere che non so davvero quando viene invocata la sostituzione, figuriamoci quando viene invocata "in modo essenziale". Quindi vorrei elaborare un esempio ragionevolmente concreto del fenomeno. Capisco che la sostituzione dovrebbe "davvero" essere pensata come l'assioma che consente la ricorsione transfinita. La mia sensazione è che la teoria delle categorie tenda a non usare la ricorsione in modo pesante (sebbene, più di altri rami della matematica, abbia molte definizioni che almeno prima facie hanno una complessità del prelievo non banale. Per esempio, penso che il formula$\phi(x,y,z,p,q)$ dicendo che il set $z$ e funzioni $p: z \to x$ e $q: z \to y$ sono un prodotto categorico degli insiemi $x,y$ è sintatticamente $\Pi_1$e l'affermazione che i prodotti binari esistono nella categoria degli insiemi è sintattica $\Pi_3$ (ignorando i quantificatori limitati ovviamente)).
Il seguente teorema è, penso, una delle eccezioni degne di nota alla teoria-categoria-non-uso-della-ricorsione:
Teorema [Quillen] "L'argomento del piccolo oggetto": Let$\mathcal C$ essere una categoria presentabile a livello locale e lasciare $I \subseteq Mor \mathcal C$essere un piccolo insieme di morfismi. Permettere$\mathcal L \subseteq Mor \mathcal C$ essere la classe di ritratti di compositi transfiniti di cambiamenti cobasi di coprodotti di morfismi in $I$, e lascia $\mathcal R \subseteq Mor \mathcal C$ comprendono quei morfismi debolmente ortogonali ai morphsims di $I$. Poi$(\mathcal L, \mathcal R)$è un debole sistema di fattorizzazione su$\mathcal C$.
Per la prova, vedere il nlab . Fondamentalmente, le fattorizzazioni sono costruite dalla ricorsione transfinita. La ricorsione mi sembra "essenziale" perché nuovi dati vengono introdotti in ogni fase della costruzione.
Formalizzazione:
Penso che questo teorema e la sua dimostrazione siano chiaramente formalizzabili in MK, dove la distinzione "piccolo / grande" teorica di categoria è interpretata come distinzione "insieme / classe" di MK. Non mi sento qualificato per commentare se la dimostrazione funziona in NBG, ma l'affermazione almeno ha senso in modo diretto.
Quando si tratta di formalizzare in ZFC, dobbiamo fare delle scelte per quanto riguarda la distinzione piccolo / grande:
Un'opzione è introdurre un "universo" $V_\kappa$(che, se stiamo effettivamente cercando di lavorare in ZFC, sarà un tipo di universo più debole del solito). Interpreteremo "piccolo" con "in$V_\kappa$Non considereremo "oggetti veramente grandi" - tutto ciò di cui parliamo sarà un set - in particolare, ogni categoria di cui parliamo sarà a grandezza naturale, anche se non "piccola" di per sé. interpreta "categoria presentabile localmente" con "$\kappa$-cocompleto, localmente $\kappa$-categoria piccola con un forte $\kappa$-piccolo, $\lambda$-generatore rappresentabile per alcuni regolari $\lambda < \kappa$"(Non so se dirlo fa differenza $V_\kappa$ pensa $\lambda$ è un cardinale regolare).
Un'altra opzione è quella di non introdurre alcun universo e di interpretare semplicemente "piccolo" nel senso di "dimensione dell'insieme". In questo caso, qualsiasi oggetto "grande" di cui parliamo deve essere definibile da piccoli parametri. Quindi definiamo una categoria che comprenda una classe di oggetti definibile da parametro, una classe di morfismi definibile da parametro, ecc. Questo potrebbe sembrare restrittivo, ma funzionerà bene nel caso presentabile localmente, poiché possiamo definire una categoria presentabile localmente$\mathcal C$ da definire, relativo ai parametri $(\lambda, \mathcal C_\lambda)$ (dove $\lambda$ è un cardinale regolare e $\mathcal C_\lambda$ è un piccolo $\lambda$-cocomplete category), come categoria di $\lambda$-Individuare oggetti $\mathcal C_\lambda$.
Ora, per il teorema in questione, l'approccio (2) sembra più pulito perché la necessaria "traduzione" è semplice e, una volta eseguita, la dimostrazione originale dovrebbe funzionare senza modifiche. Penso che i principali inconvenienti di (2) vengano altrove. Ad esempio, sarà probabilmente una questione delicata formulare teoremi sulla categoria delle categorie presentabili localmente. In generale, ci saranno vari teoremi sulle categorie che hanno formulazioni e dimostrazioni pulite e concettuali quando le categorie coinvolte sono piccole, ma che richiedono fastidiose modifiche tecniche quando le categorie coinvolte sono grandi. È per tali ragioni che approcci più come (1) tendono ad essere favoriti per progetti di teoria delle categorie su larga scala.
Quindi supponiamo di seguire l'approccio (1). La domanda quindi diventa:
Domanda 1: Di che tipo di universo abbiamo bisogno esattamente per formulare e dimostrare il teorema di cui sopra seguendo l'approccio (1)?
Domanda 2: Quanti universi di questo tipo sono garantiti da ZFC?
Presumibilmente, la risposta alla domanda 2 sarà che ci sono molti di questi universi - abbastanza da poter fare cose come, data una categoria, passare a un universo abbastanza grande da rendere piccola quella categoria e invocare il teorema di quell'universo .
Domanda 3: Fino a che punto dobbiamo spingerci tra le erbacce per rispondere alle domande 1 e 2?
Dobbiamo analizzare la dimostrazione del Teorema in modo approfondito? Esiste una facile rubrica di criteri che ci permetta di dare uno sguardo alla dimostrazione e, per il 99% di teoremi come questo, dire facilmente che "passa" senza approfondire troppo le cose? O c'è anche qualche metateorema formale a cui possiamo fare appello in modo tale che anche un computer possa verificare che le cose vadano bene?
Risposte
Il commento di Jacob Lurie dà una risposta alla domanda 1. Vale a dire, supponendo che le stime che ho fornito nel mio commento siano corrette, per formulare e dimostrare il teorema basterà supporre che
- $\kappa$ è regolare
e quello
- per ogni $\mu < \kappa$, lì esiste $\rho < \kappa$ tale che $\mu \ll \rho$ (intendendo che $\mu' < \mu, \rho' < \rho \Rightarrow (\rho')^{\mu'} < \rho$).
Forse questa proprietà di $\kappa$potrebbe essere visto come una "forma" di sostituzione. Ma in realtà, ciò che abbiamo sono due condizioni$\kappa$ che sono puramente teorici degli insiemi piuttosto che metamatematici, così che la risposta alla domanda 1 è qualcosa di molto più pulito di quanto avessi supposto.
Questo ci consente di affrontare la domanda 2. Presumibilmente, il risultato è che ZFC dimostra che ce ne sono molti e molti $\kappa$ soddisfacendo le due condizioni di cui sopra.
Quando si arriva alla domanda 3, sembrerebbe che in questo approccio abbiamo effettivamente bisogno di approfondire la dimostrazione. In effetti, sembra che per attuare questo approccio, dobbiamo aggiungere un contenuto matematico genuino alla dimostrazione e dimostrare effettivamente un'affermazione più forte. Le ulteriori domande poi diventano
In generale sarà possibile "costruttivizzare" la "maggior parte" dei teoremi di teoria delle categorie in questo modo, o altri problemi emergeranno nel corso del progetto "ZFC-ify category theory"?
Se la risposta a (1) è "sì" (o se generalmente è "no" e limitiamo la nostra attenzione ai casi in cui è "sì"), allora "quanto lavoro extra" sarebbe davvero un progetto del genere?
La mia ipotesi è che la risposta a (1) sia che quando si tratta dell'uso della ricorsione transfinita nella teoria delle categorie, sarà in effetti tipicamente il caso che l'uso della sostituzione possa essere eliminato in un modo simile a questo, ma più Soprattutto ho perso il punto: come sostiene Jacob Lurie in risposta alla domanda di Peter Scholze, le questioni più spinose con la teoria delle categorie ZFC non hanno a che fare con la ricorsione transfinita ma piuttosto con la possibilità di andare avanti e indietro liberamente tra "grandi categorie "e" piccole categorie "in vari modi.
La mia ipotesi è che la risposta a (2) sia che per "la maggior parte" degli usi teorici di categoria della ricorsione transfinita, dovrebbe essere piuttosto semplice "costruttivizzarli" in modo che si adattino a un "universo bambino" con le proprietà sopra o qualcosa di simile, e che con un po 'di pratica si potrebbe sviluppare la capacità di verificare quasi a colpo d'occhio che è possibile, anche se sempre su base teorema per teorema. Ma mi piacerebbe essere smentito e mostrato un teorema nella teoria delle categorie in cui questo tipo di approccio fallisce!
Infine, questo lascia aperta la questione se esista un modo "più automatico" di fare tutto questo - forse con una conclusione più debole di "il nostro universo non ha bisogno di soddisfare alcuna forma di sostituzione".