Principio di riflessione vs universi
Nelle discussioni sulla teoria delle categorie, c'è spesso la tentazione di guardare alla categoria di tutti i gruppi abeliani, o di tutte le categorie, ecc., Il che porta rapidamente ai soliti problemi della teoria degli insiemi. Questi vengono spesso evitati utilizzando gli universi di Grothendieck. Nel linguaggio della teoria degli insiemi, si fissa un cardinale fortemente inaccessibile$\kappa$ -- ciò significa che $\kappa$ è un cardinale innumerevole tale che per tutti $\lambda<\kappa$, anche $2^\lambda<\kappa$e per qualsiasi set di $<\kappa$ molti set $S_i$ di dimensioni $<\kappa$, anche la loro unione è di dimensione $<\kappa$. Ciò implica che lo stage$V_\kappa\subset V$ di "insiemi di dimensioni $<\kappa$"è esso stesso un modello di ZFC: applicando una qualsiasi delle operazioni sui set, come prendere gruppi di potenza o sindacati, non puoi mai lasciare $V_\kappa$. Questi insiemi vengono quindi definiti "piccoli", e quindi la categoria dei piccoli gruppi abeliani è decisamente ben definita.
Storicamente, questo approccio è stato utilizzato per la prima volta da Grothendieck; un testo fondamentale più recente è il lavoro di Lurie$\infty$-categorie. Tuttavia, il loro uso ha sempre creato una sorta di contraccolpo, con alcune persone riluttanti a lasciare che gli assiomi oltre ZFC scivolino nella letteratura consolidata. Ad esempio, penso che a un certo punto ci sia stata una lunga discussione se l'Ultimo Teorema di Fermat sia stato dimostrato in ZFC, ora risolto da McLarty. Più recentemente, ho visto argomenti simili emergere per teoremi le cui dimostrazioni si riferiscono al lavoro di Lurie. (Personalmente, non ho forti sentimenti al riguardo e capisco gli argomenti in entrambi i casi.)
D'altra parte, è sempre stato anche il caso che un esame più attento ha rivelato che qualsiasi uso degli universi era in realtà non necessario. Ad esempio, il progetto Stack non utilizza gli universi. Invece, (vedi Tag 000H dire) indebolisce effettivamente l'ipotesi che$\kappa$ è fortemente inaccessibile, a qualcosa come un cardinale limite forte di innumerevoli cofinalità, cioè: per tutti $\lambda<\kappa$, uno ha $2^\lambda<\kappa$e ogni volta che hai una raccolta numerabile di set$S_i$ di dimensioni $<\kappa$, anche l'unione di $S_i$ ha dimensioni $<\kappa$. ZFC dimostra facilmente l'esistenza di tali$\kappa$, e quasi ogni argomento che si potrebbe immaginare di fare nella categoria dei gruppi abeliani funziona effettivamente anche nella categoria dei $\kappa$-piccoli gruppi abeliani per tali $\kappa$. Se si fanno argomenti più complicati, si può di conseguenza rafforzare l'ipotesi iniziale su$\kappa$. Ho avuto occasione di giocare io stesso a questo gioco, vedi la Sezione 4 di www.math.uni-bonn.de/people/scholze/EtCohDiamonds.pdf per il risultato. Da questa esperienza, sono abbastanza sicuro che si possa riscrivere in modo simile la "Higher Topos Theory" di Lurie, o qualsiasi altro lavoro di teoria delle categorie simile, in modo da rimuovere tutti i cardinali fortemente inaccessibili, sostituendoli con$\kappa$ con proprietà come quelle sopra.
In effetti, sembra esserci un teorema di ZFC, il principio di riflessione (discusso brevemente nel Tag 000F del progetto Stacks, per esempio), che sembra garantire che ciò sia sempre possibile. Vale a dire, per ogni dato insieme finito di formule della teoria degli insiemi, ce ne sono alcune sufficientemente grandi$\kappa$ tale che, grosso modo, queste formule mantengono $V_\kappa$ se e solo se resistono $V$. Questo sembra dire che per ogni dato insieme finito di formule, se ne possono trovare alcune$\kappa$ tale che $V_\kappa$si comporta come un universo rispetto a queste formule, ma per favore correggimi nella mia comprensione molto ingenua del principio di riflessione! (Un fatto correlato è che ZFC dimostra la consistenza di un dato frammento finito degli assiomi di ZFC.)
D'altra parte, un dato testo matematico contiene solo un numero finito di formule (a meno che non indichi uno "schema di teorema", cosa che di solito non accade, credo). La domanda è quindi formulata in modo leggermente provocatorio:
Il principio di riflessione implica che deve essere possibile riscrivere la Teoria dei Topos Superiori in un modo che eviti l'uso degli universi?
Modifica (28.01.2021): Grazie mille per tutte le risposte molto utili! Penso di avere un quadro molto più chiaro della situazione ora, ma non sono ancora esattamente sicuro di quale sia la risposta alla domanda.
Da quello che ho capito, (approssimativamente) il miglior meta-teorema in questa direzione è il seguente (specializzato in HTT). Ricorda che HTT risolve due cardinali fortemente inaccessibili$\kappa_0$ e $\kappa_1$, facendo così spazio per piccoli (in $V_{\kappa_0}$), grande (in $V_{\kappa_1}$) e molto grandi (in $V$) oggetti. Si può quindi provare a leggere HTT nel seguente sistema di assiomi (questo è essenzialmente quello dell'articolo di Feferman "Fondamenti di teoria degli insiemi della teoria delle categorie", ed è stato anche proposto nella risposta di Rodrigo Freire sotto).
(i) I soliti assiomi ZFC
(ii) Altri due simboli $\kappa_0$ e $\kappa_1$, con gli assiomi di essere cardinali, di cui la cofinalità $\kappa_0$ è innumerevole e che la cofinalità di $\kappa_1$ è maggiore di $\kappa_0$.
(iii) Uno schema assioma, che lo dica per ogni formula $\phi$ della teoria degli insiemi, $\phi\leftrightarrow \phi^{V_{\kappa_0}}$ e $\phi\leftrightarrow \phi^{V_{\kappa_1}}$.
Quindi il principio di riflessione può essere utilizzato per mostrare (vedere la risposta di Rodrigo Freire di seguito per uno schizzo della dimostrazione):
Teorema. Questo sistema di assiomi è conservativo rispetto a ZFC. In altre parole, qualsiasi teorema in questo sistema formale a cui non si fa riferimento$\kappa_0$ e $\kappa_1$ è anche un teorema di ZFC.
Questa è precisamente la conclusione che vorrei avere.
Notare che $V_{\kappa_0}$ e $V_{\kappa_1}$ sono modelli di ZFC, ma (criticamente!) questo non può essere dimostrato all'interno del sistema formale, poiché ZFC non è finitamente assiomatizzabile, e solo ogni singolo assioma di ZFC è posto da (iii).
Una cosa bella di questo sistema di assiomi è che consente esplicitamente gli argomenti occasionali della forma "abbiamo dimostrato questo teorema per piccole categorie, ma poi possiamo applicarlo anche a grandi categorie".
Una domanda più precisa è quindi:
Gli argomenti di HTT funzionano in questo sistema formale?
Mike Shulman nella sezione 11 di https://arxiv.org/abs/0810.1279fornisce un'esposizione molto chiara di quali siano i potenziali problemi qui. Vale a dire, se hai un set$I\in V_{\kappa_0}$ e set $S_i\in V_{\kappa_0}$ per $i\in I$, non è consentito concludere che l'unione di $S_i$ è dentro $V_{\kappa_0}$. Questa conclusione è garantita solo se la funzione$i\mapsto S_i$ è definito anche in $V_{\kappa_0}$ (o se $I$è numerabile, dal presupposto extra di innumerevoli cofinalità). In pratica, questo significa che quando si vuole affermare che qualcosa è "piccolo" (cioè in$V_{\kappa_0}$), questo giudizio non riguarda solo gli oggetti, ma anche i morfismi ecc. Non mi è chiaro ora quanto sia in realtà un problema, dovrei pensarci di più; Potrei effettivamente immaginare che sia abbastanza facile leggere HTT per soddisfare questo sistema formale. Shulman dice che, con questo avvertimento, il teorema del funtore aggiunto può essere dimostrato e, come dice Lurie nelle sue risposte, gli argomenti in HTT sono di complessità teorica degli insiemi simile. Tuttavia, sarei comunque interessato a un giudizio se la risposta alla domanda è "Sì, come scritto" o piuttosto "Probabilmente sì, ma devi impegnarti" o in effetti "Non proprio". (Spero sinceramente che gli esperti saranno in grado di concordare approssimativamente dove la risposta rientra in questo spettro.)
Un'ultima osservazione: si può trovare l'ipotesi di "non numerabilità" sopra un po 'arbitraria; perché non consentire alcune unioni leggermente più grandi? Un modo per occuparsene è aggiungere un simbolo$\kappa_{-1}$ con le stesse proprietà e chiedi invece che la cofinalità di $\kappa_0$ è maggiore di $\kappa_{-1}$. Allo stesso modo, si potrebbe voler sostituire il limite$\mathrm{cf} \kappa_1>\kappa_0$ da un legame leggermente più forte come $\mathrm{cf} \kappa_1>2^{\kappa_0}$dire. Di nuovo, se semplifica le cose, uno potrebbe semplicemente spremerne un altro$\kappa_{1/2}$ in mezzo, in modo che $\mathrm{cf} \kappa_{1/2}>\kappa_0$ e $\mathrm{cf} \kappa_1>\kappa_{1/2}$. In questo modo non ci si deve preoccupare se qualcuno degli oggetti "standard" che appaiono in alcune dimostrazioni rimane di dimensione numerabile, o se si possono ancora prendere i colimiti$V_{\kappa_1}$ quando i set di indici non hanno esattamente la dimensione delimitata da $\kappa_0$ ma sono stati un po 'manipolati.
PS: Sto trovando solo ora tutte le precedenti domande e risposte relative a MO. Alcuni molto rilevanti sono le risposte di Joel Hamkins qui e qui .
Risposte
Ho intenzione di uscire su un arto e suggerire che il libro HTT non usa mai qualcosa di più forte del sostituto di $\Sigma_{15}$-formule di teoria degli insiemi. (Qui$15$ è un numero elevato scelto a caso e HTT è un libro di matematica scelto a caso che non riguarda specificamente la teoria degli insiemi.)
Riflettendo sul commento di Gabe sulla mia risposta originale, ora penso che ciò che ho scritto sia fuorviante perché fonde due affermazioni separate (ma correlate):
L'esistenza di cardinali fortemente inaccessibili non è realmente necessaria nella teoria delle categorie.
La piena forza di ZFC non è realmente necessaria nella teoria delle categorie.
Sono d'accordo con entrambe queste affermazioni, ma penso che il modo migliore per convincere qualcuno di 1) non sarebbe combinare 2) con un principio di riflessione: cioè, non si dovrebbe cercare di sostituire l'uso di un cardinale fortemente inaccessibile $\kappa$ da uno per cui $V_{\kappa}$ modella gran parte di ZFC.
Per come la vedo io, il "problema" che gli universi risolvono è giustificare la combinazione di due tipi di ragionamento:
A) A volte è utile dimostrare teoremi su piccole categorie $\mathcal{C}$ incorporandoli in categorie "grandi" (ad esempio, utilizzando l'incorporamento di Yoneda) che hanno caratteristiche aggiuntive interessanti: ad esempio, l'esistenza di limiti e colimiti.
B) Le grandi categorie sono anche categorie, quindi qualsiasi teorema che si applica alle categorie in generale dovrebbe applicarsi anche alle grandi categorie.
Se fossi preoccupato solo per B), allora un principio di riflessione potrebbe essere rilevante. Scegliere un cardinale$\kappa$ tale che $V_{\kappa}$ soddisfa una grossa fetta di ZFC, puoi ridefinire "categoria piccola" per indicare "categoria a cui appartiene $V_{\kappa}$"e" categoria grande "per indicare" categoria non necessariamente appartenente $V_{\kappa}$", e puoi essere certo che tutti i teoremi di base che potresti desiderare sono validi in entrambi i casi.
Ma se sei anche preoccupato per A), questo non è necessariamente utile. Supponi di iniziare con una categoria$\mathcal{C}$ appartenente a $V_{\kappa}$e vuoi qualche versione dell'incorporamento di Yoneda. Un'ipotesi naturale sarebbe quella di incorporare nella categoria dei funtori da$\mathcal{C}^{\mathrm{op}}$ alla categoria dei set di dimensioni $<\tau$ (o qualche modello equivalente di esso), per qualche cardinale $\tau$. Una prima ipotesi è che dovresti prendere$\tau = \kappa$, ma penso che questo abbia solo senso $\kappa$è fortemente inaccessibile (altrimenti alcuni set Hom saranno troppo grandi). In ogni caso assicurati che questa costruzione abbia buone proprietà, vorrai richiedere diverse proprietà del cardinale$\tau$. Ad esempio, se vuoi che questa categoria di presine abbia molti colimiti, allora vorrai$\tau$avere una grande cofinalità. E se inizi a pensare a quali tipi di ipotesi aggiuntive potresti dover fare, sei tornato da dove hai iniziato: pensare a quale tipo di stime di cardinalità garantiscono che "preselezioni di insiemi di dimensioni$< \tau$"sono una buona approssimazione alla categoria di tutti i presheaves di set. Quindi il principio di riflessione non ti aiuta davvero a evitare questi problemi.
(Modifica: mi sono reso conto dopo aver scritto che il testo qui sotto sta per lo più ribadendo il post originale di Peter. Ma lo lascio qui nel caso qualcuno lo trovi utile.)
Se vuoi una formalizzazione rigorosa in qualcosa come ZFC, probabilmente la cosa migliore da fare è eliminare del tutto le grandi categorie. Quindi B) è un non problema. Per affrontare A), lasciatemi notare che molte delle "grandi" categorie di cui si vorrebbe parlare sorgono in un modo particolare: si inizia con una piccola categoria$\mathcal{C}$ che ha già certi tipi di colimiti e si allarga formalmente $\mathcal{C}$ per creare una categoria più grande $\mathcal{C}^{+}$che ha colimiti arbitrari (senza cambiare quelli con cui hai iniziato). Le categorie che si presentano in questo modo sono chiamate presentabili localmente e c'è una semplice formula per$\mathcal{C}^{+}$: è la categoria dei funtori $F: \mathcal{C}^{\mathrm{op}} \rightarrow \mathrm{Set}$ che preservano i limiti con cui hai iniziato (cioè i colimit con cui hai iniziato in $\mathcal{C}$).
Ora, se vuoi imitare questo nel mondo delle piccole categorie, potresti invece scegliere un cardinale $\kappa$ e invece contemplare funtori $F: \mathcal{C}^{\mathrm{op}} \rightarrow \{ \text{Sets of size < $\ kappa$} \}$, che è equivalente a una piccola categoria $\mathcal{C}^{+}_{\kappa}$. La domanda che incontri è se questo sia un sostituto abbastanza buono per la grande categoria$\mathcal{C}^{+}$sopra. Ad esempio, ha molti limiti e limiti? Non è ragionevole chiedere che abbia tutti i colimiti, ma potresti invece chiedere quanto segue:
D) Fa la categoria $\mathcal{C}^{+}_{\kappa}$ avere i colimiti indicizzati da diagrammi di dimensione $< \kappa$?
La risposta a Q) è "no in generale, ma sì se $\kappa$ è ben scelto ". Ad esempio, se hai un cardinale infinito $\lambda$ limitando la dimensione di $\mathcal{C}$ e il numero di diagrammi colimit con cui inizi, quindi credo che tu possa garantire (i) prendendo $\kappa = (2^{\lambda})^{+}$ (e la categoria $\mathcal{C}^{+}_{\kappa}$può essere caratterizzato dalla proprietà universale attesa). Inoltre, per dimostrarlo non è necessaria alcuna forma di sostituzione.
Ora potresti anche chiedere quanto segue:
Q ') Fa la categoria $\mathcal{C}^{+}_{\kappa}$ hanno limiti indicizzati da diagrammi di dimensione $< \kappa$?
Qui la risposta sarà solitamente "no" a meno che $\kappa$è fortemente inaccessibile. Ma se sei interessato solo ai limiti di un tipo particolare (ad esempio, se stai studiando Grothendieck topoi, potresti essere particolarmente interessato ai limiti finiti), la risposta sarà di nuovo "sì per$\kappa$ ben scelto ". E questo è qualcosa che puoi provare usando pochissimo ZFC.
Ora la mia affermazione è che, in base alla mia esperienza, la discussione di cui sopra è rappresentativa del tipo di domande che ti imbatterai nel tentativo di navigare nella distinzione tra categorie "piccole" e "grandi" (certamente è rappresentativa del modo in cui queste cose vieni nel mio libro, su cui era posta la domanda originale). In pratica, non hai mai bisogno di parlare della totalità di una grande categoria come$\mathcal{C}^{+}$; è sufficiente per costruirne un pezzo abbastanza grande (come$\mathcal{C}^{+}_{\kappa}$) con le caratteristiche che vuoi vedere, che puoi organizzare scegliendo $\kappa$ accuratamente.
Trovo concettualmente più chiaro ignorare la questione di come le cose sono formalizzate in ZFC e formulare le cose in termini di categoria "grande" $\mathcal{C}^{+}$, rimandando alle sue "piccole" approssimazioni $\mathcal{C}^{+}_{\kappa}$solo come ausiliari in una dimostrazione (che inevitabilmente arriverà ancora da qualche parte!). L'invocazione di "universi" è solo un modo per scrivere in questo modo, pur prestando fede alla struttura assiomatica di ZFC, ed è decisamente inessenziale.
Vorrei menzionare qualcosa che penso non sia stato ancora sottolineato. La domanda originale iniziava con
Nel linguaggio della teoria degli insiemi, si fissa un cardinale fortemente inaccessibile $\kappa$... Ciò implica che il palco $𝑉_\kappa\subset 𝑉$ di "insiemi di dimensioni $<\kappa$"è esso stesso un modello di ZFC.
Tuttavia, l'affermazione che $V_\kappa$ è un modello di ZFC è significativamente più debole di quello che dice $\kappa$è inaccessibile. In effetti, se$\kappa$ è inaccessibile, quindi $\{ \lambda\mid V_\lambda$ è un modello di ZFC $\}$ è fermo in $\kappa$. Quindi, il più piccolo inaccessibile (se ce n'è uno) è molto più grande del più piccolo$\kappa$ tale che $V_\kappa$ modelli ZFC.
Nella misura in cui il principio di riflessione è utile (cosa che, come alcune altre risposte hanno sottolineato, si può almeno mettere in discussione), è direttamente utile solo per argomenti in cui la proprietà rilevante di un universo di Grothendieck è che si tratta di un modello di ZFC. Tuttavia, almeno quando formulata in modo ingenuo, ci sono molti posti in cui la teoria delle categorie usa più di questo. Nello specifico, utilizziamo il fatto che un universo di Grothendieck soddisfa la sostituzione del secondo ordine , il che significa che qualsiasi funzione$f:A\to V_\kappa$, dove $A \in V_\kappa$, ha un'immagine. Dicendo ciò$V_\kappa$i modelli ZFC implica solo che soddisfi la sostituzione del primo ordine , il che ci consente solo di concludere che tale$f$ ha un'immagine se $f$ è definibile da $V_\kappa$ da una formula logica.
Credo che la sostituzione del secondo ordine sia onnipresente nella teoria delle categorie basata sull'universo come di solito formulata. Ad esempio, se${\rm Set}_\kappa$ denota la categoria di insiemi in $V_\kappa$, quindi per dimostrarlo ${\rm Set}_\kappa$ è "completo e cocomplete" nel senso ingenuo che ammette un limite e un colimit per ogni funtore il cui dominio è piccolo, abbiamo bisogno di una sostituzione del secondo ordine per raccogliere le immagini di un tale funtore in un unico insieme.
Ora, ci sono modi per riformulare la teoria delle categorie per evitarlo. L'articolo di McLarty lo fa in alcuni modi teorici degli insiemi. Un approccio categoricamente coerente consiste nel sostituire ingenui "grandi categorie" (ovvero categorie i cui insiemi di oggetti e morfismi potrebbero non appartenere$V_\kappa$) con grande ${\rm Set}_\kappa$- categorie indicizzate . Ma questo è un tipo di riformulazione molto più sostanziale da eseguire manualmente.
Se ho capito bene, stai cercando una dichiarazione del modulo:
"Se qualcosa è stato dimostrato in HTT utilizzando gli universi, può essere dimostrato senza di essi limitandone ad alcuni $V_\kappa$ per $\kappa$ abbastanza grande"
La risposta rigorosa a questa domanda, se non disponiamo di ulteriori informazioni su HTT, è che non può esserci alcuna dichiarazione del genere se ZFC è coerente.
In effetti, è possibile che l'esistenza degli universi sia incoerente (in effetti non è possibile provare che sia coerente), e in quella situazione, qualsiasi cosa può essere dimostrata usando gli universi, e quindi una tale affermazione implicherebbe che qualsiasi cosa può essere dimostrata , ovvero ZFC non è coerente.
Sono un po 'sciatto su ciò che è dimostrabile in cosa ecc. Ma l'idea principale è lì
Certo, sappiamo cose su HTT, e se lo leggiamo attentamente possiamo analizzare dove usa gli universi, e vedere che possono in effetti essere sostituiti con modelli transitivi di sostituzione ZC + fino a $\Sigma_{15}$-formule, come fa notare Jacob. In tal caso, poiché è possibile che esistano modelli così ben educati (della forma$V_\kappa$, per $\kappa$ben scelto), questo non è un problema; e HTT può essere riscritto senza universi, ma ciò non può essere dimostrato senza conoscere cosa c'è in HTT.
La "morale" di questo è che, nella maggior parte delle domande teoriche di categoria mainstream, gli universi sono un dispositivo che fa risparmiare tempo e non una parte effettiva della matematica.
Qualsiasi teorema $T$ di $\mathsf{ZFC}$ segue da un sottoinsieme finito degli assiomi di $\mathsf{ZFC}$ o, per mantenere le cose semplici, da $\mathsf{ZFC}$ dove lo schema dell'assioma della sostituzione è limitato a $\Sigma_n$ predicati¹, chiamiamolo $\mathsf{ZFC}_n$. Adesso$\mathsf{ZFC}$e più precisamente $\mathsf{ZFC}_{n+1}$, prova l'esistenza di cardinali arbitrariamente grandi $\kappa$, forti limiti di innumerevoli cofinalità, tali che $V_\kappa$ è un modello di $\mathsf{ZFC}_n$, e, in particolare, del teorema $T$, e tale che, inoltre, che il valore di verità di qualsiasi $\Sigma_n$ istruzione, con parametri in $V_\kappa$ è lo stesso in $V_\kappa$come nel (vero) universo. Possiamo chiamarli$V_\kappa$ "Universi limitati" in quanto sono chiusi nella maggior parte delle operazioni basate sulla teoria degli insiemi, come prendere gruppi di potenza, tranne per il fatto che la sostituzione deve essere numerabile (inclusa per comodità) o limitata a un $\Sigma_n$predicato; e in particolare, sono chiusi sotto qualunque dichiarazione di esistenza$T$ fa.
Quindi l'idea sarebbe di applicare quanto sopra alla congiunzione $T$ di tutti i teoremi che consideri parte della Higher Topos Theory (e qualunque altra teoria sia usata come prerequisiti) e trovi l'appropriata $n$. (In realtà lo sospetto$n=1$ dovrebbe essere sufficiente: sarei molto sorpreso di trovare un'istanza di sostituzione nella matematica ordinaria che non segue da $\Sigma_1$-sostituzione.) Allora $\mathsf{ZFC}_n$ dimostrerebbe $T$ (tutti i teoremi della teoria) e $\mathsf{ZFC}_{n+1}$ proverebbe l'esistenza di una scorta infinita di universi limitati in cui utilizzare la teoria.
Ovviamente, per evitare un ciclo infinito, non puoi considerare quel teorema (quello che asserisce l'esistenza di una scorta infinita di$V_\kappa$) per far parte della teoria o è necessario passare a una più ampia $n$.
Per spiegare quella che potrebbe sembrare una contraddizione logica, qui, occorre chiarire che l'affermazione che l'esistenza di molti modelli di $\mathsf{ZFC}_n$ può essere provato $\mathsf{ZFC}$ per ogni $n$, ma non in modo uniforme (la dimostrazione diventa sempre più lunga come $n$ cresce), quindi $n$deve essere un numero naturale concreto , il quantificato universalmente (oltre $n$) non è dimostrabile in$\mathsf{ZFC}$. Ma questo non è un problema fintanto che la tua teoria è fissa ed è formulata in$\mathsf{ZFC}$ (il che esige che esso stesso non contenga metateoremi come “per qualsiasi concreto $n$ possiamo provare quanto segue in $\mathsf{ZFC}$"). Quindi sta a te accertarti che questo sia il caso di HTT (e, se sei abbastanza coraggioso, trova l'appropriato$n$).
(Giusto per dare un'idea di come sono coinvolti i tipi di cardinali, i cardinali $\kappa$ tale che $V_\kappa$ è un modello di $\mathsf{ZFC}_1$ sono i punti fissi del $\gamma \mapsto \beth_\gamma$funzione. Non credo ci sia alcuna speranza per una descrizione ragionevole del file$\kappa$ tale che $V_\kappa$ è un modello di $\mathsf{ZFC}_n$ per qualsiasi calcestruzzo $n\geq 2$. Vedi anche questa domanda .)
- Significato predicati con al massimo $n$ serie alternate di quantificatori illimitati, a partire da quantificatori esistenziali, seguiti da formula con quantificatori limitati (significato della forma $\forall x\in y$ o $\exists x\in y$).
OK, ho passato gran parte della giornata a cercare di capirlo guardando effettivamente in dettaglio HTT. È stato un bel viaggio; Ho decisamente cambiato la mia prospettiva più volte nel processo. Attualmente, mi sembra che la risposta sia che HTT, come scritto, può essere letto in questo sistema formale. (Quindi questo è come nella barzelletta in cui dopo l'orario di chiusura qualcuno dice "Sì, è ovvio." Ci sono sicuramente punti in cui deve essere scelta la corretta interpretazione, ma come in ogni testo matematico, è già così comunque.) Quindi con questa risposta, voglio avanzare un argomento che HTT può essere letto in questo sistema formale, cercando di spiegare un po 'come interpretare certe cose nel caso in cui possano sorgere ambiguità, e perché penso che leggendolo in questo modo tutto dovrebbe funzionare. Ma è abbastanza probabile che abbia trascurato qualcosa di importante, quindi per favore correggimi!
Come nota Tim Campion, la maggior parte delle prime cose funziona senza problemi - in effetti, non menziona nemmeno gli universi. Finché non funziona, tutto funziona$V_{\kappa_0}$, nel $V_{\kappa_1}$e in $V$, e lo schema dell'assioma dato garantisce anche che tutte le costruzioni realizzate saranno compatibili.
Bisogna prestare maggiore attenzione quando si raggiungono i capitoli 5 e 6. Vorrei provare a presentare alcune definizioni e proposizioni di questi capitoli da tre diversi punti di vista.
Il punto di vista classico ZFC, o (equiconsistentemente) quello della teoria di von Neumann - Bernays - Gödel (NBG), che consente classi oltre agli insiemi, quindi possiamo parlare della categoria (classificata) di tutti gli insiemi $\mathrm{Set}$.
Il punto di vista di HTT, ovvero gli universi ZFC + Grothendieck.
Il punto di vista della teoria degli insiemi di Feferman, nella forma indicata nella domanda. (In realtà, non sono più sicuro di aver davvero bisogno di questi limiti di cofinalità. Ma è bello sapere che possono essere assunti.)
Si noti che la domanda posta presume che si sia realmente interessati al primo punto di vista, e agli altri solo nella misura in cui sono convenienze per provare qualcosa sul primo contesto. Ciò è in linea con i contenuti dei capitoli 5 e 6: l'intera teoria delle categorie presentabili si adatta perfettamente alla prima impostazione, anche filosoficamente.
OK, quindi ricorda che una categoria presentabile - fammi restare solo con le categorie invece di $\infty$-categorie, la differenza non è essenziale per le nostre preoccupazioni - è una categoria (a misura di classe) $C$ che ammette tutti i colimiti piccoli, e tale che per qualche cardinale regolare $\kappa$, c'è una piccola categoria $C_0$ e un'equivalenza $C\cong \mathrm{Ind}_{\kappa}(C_0)$,
cioè $C$ si ottiene accostando liberamente $\kappa$-filtrato colimits a $C_0$. (In particolare,$C_0$ è necessariamente equivalente alla sottocategoria completa di $\kappa$-oggetti compatti di $C$.) In particolare, le categorie presentabili sono determinate da una piccola quantità di dati. Inoltre, l'idea è quella$C$è davvero la categoria di tutti gli oggetti (insiemi, gruppi, qualunque cosa). Questo punto di vista è davvero articolato più chiaramente in 1), mentre in 2) e 3) la nozione di presentabilità improvvisamente dipende di nuovo dall'universo, e improvvisamente contengono di nuovo solo piccoli insiemi / gruppi / ...; permettetemi quindi di chiamarli di conseguenza piccoli presentabili. Nota che questa nozione ha senso sia in 2) che in 3), e dipende solo da$V_{\kappa_0}$. Una categoria piccola presentabile è quindi in particolare piccola definibile, quindi vive$\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$, dove questa inclusione è un'uguaglianza in 2) (ma non in 3)).
In 2), di solito si definisce una categoria piccolo-presentabile come un tipo speciale di categoria grande, che è l'approccio di HTT. Ma qui in realtà sto già diventando un po 'confuso: sembrano esserci due nozioni di funtori$F: C\to D$: Quelli definibili in $V_{\kappa_0}$, equivalentemente $F\in V_{\kappa_0+1}$ (vale a dire, $V_{\kappa_0+1}$ sono esattamente le classi di $V_{\kappa_0}$), o tutti i funtori in $V_{\kappa_1}$. Non mi sembra ovvio che qualsiasi funtore$F: C\to D$ nel $V_{\kappa_1}$ si trova in $V_{\kappa_0+1}$, come $C$ e $D$ se stessi vivono solo in $V_{\kappa_0+1}$. La differenza tra queste due nozioni scompare quando ci si limita a funtori accessibili, che sono tutti definibili. Nota che 1) dice che è davvero la prima idea di cui dovremmo preoccuparci! (Prima di scrivere questo post, non ero a conoscenza della differenza.)
In 3), il modo corretto di procedere è utilizzare la prospettiva dettata da 1), che è quella di "$V_{\kappa_0}$-categorie definibili ", quindi vivono in $\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$. Si possono ancora considerare questi come$\kappa_1$-piccole categorie. All'inizio pensavo che qui ci sarebbe stata una differenza sostanziale tra gli approcci di 2) e 3), ma in realtà sembra che in entrambi i casi si arrivi a due diverse nozioni di funtori, che si riconciliano una volta che ci si limita ai funtori accessibili.
Uno dei teoremi principali è il teorema del funtore aggiunto: If $F: C\to D$è un funtore di categorie presentabili che conserva tutti i piccoli colimiti, quindi ammette un aggiunto corretto. Cosa significa in realtà questo teorema?
In 1), significa che c'è un funtore $G: D\to C$ - il che in particolare significa che deve essere definibile mediante formule, poiché questo è ciò che sono i funtori tra le categorie a dimensione di classe - insieme alle trasformazioni di unità e di conteggio (definibili!) che soddisfano le condizioni usuali.
In 2), si tratta semplicemente di $C$ e $D$ come piccolo se considerato in $V_{\kappa_1}$e poi afferma l'esistenza del diritto ivi aggiunto. Senza ulteriori informazioni, questo in realtà non sembra dare ciò che volevamo in 1), a priori$G$(e le trasformazioni di unità e paese) si trovano tutte nell'universo più grande. Ma questa informazione può essere ottenuta ricordandola$G$ è effettivamente accessibile (una parte del teorema del funtore aggiunto che ho omesso di dichiarare sopra, ma dovrebbe essere incluso), e quindi tutto è determinato su un insieme.
In 3), si vorrebbe di nuovo arrivare al risultato di 1), ma si può provare a farlo come in 2) provando prima l'esistenza di tali dati in $V_{\kappa_1}$ e poi dimostrando l'accessibilità, cedendo così che tutto sta dentro $\mathrm{Def}(V_{\kappa_0})$.
Vediamo come si svolge in un paio di primi punti del Capitolo 5 in cui vengono usati gli universi.
Definizione 5.1.6.2: Let $C$essere una categoria che ammette tutti i piccoli colimiti. Un oggetto$X\in C$è completamente compatto se il funtore$j_X: C\to \widehat{\mathrm{Set}}$ copresentato da $X$ conserva piccoli colimiti.
Qui $\widehat{\mathrm{Set}}$ è la categoria (molto ampia) di set in $V_{\kappa_1}$. Interpretiamo il significato di questa definizione nei sistemi di cui sopra.
Qui $C$è una qualsiasi categoria (possibilmente delle dimensioni di una classe). Si noti che, specialmente in HTT, "localmente piccolo" non è un'ipotesi standard, quindi questo consente anche ai morfismi tra due oggetti di essere insiemi appropriati. Per questo motivo, il funtore deve davvero andare a$\widehat{\mathrm{Set}}$, e questo è qualcosa di cui non possiamo parlare in questo contesto. Quindi si dovrebbe riformulare la condizione per soddisfare questa obiezione; questo non dovrebbe essere difficile, ma potrebbe essere un po 'sgradevole.
Penso che sia implicito nella definizione che $C$ è qualsiasi categoria in cui si trova $V_{\kappa_1}$. Questo è rigorosamente catturare la configurazione di 1) in quella if$C$ è piccolo definibile come proveniente da 1), quindi qualsiasi piccolo diagramma colimit in $C$ è automaticamente definibile in piccole dimensioni.
Qui abbiamo due scelte: o quella da 1) o quella da 2), e danno nozioni diverse. In caso di conflitto la prospettiva da 1) è quella corretta, quindi$C$è definibile in piccolo, e si richiede la commutazione con colimiti di diagrammi definibili in piccolo. Ma mentre in 1) abbiamo avuto problemi a formulare la condizione, gli universi a portata di mano in 3) significano che la condizione ora può essere formulata: possiamo chiedere che ci vogliono piccoli colimiti definibili in$C$ a colimiti in $\widehat{\mathrm{Set}}$. Qui$\widehat{\mathrm{Set}}$ sono gli insiemi $V_{\kappa_1}$.
Quindi, in questo caso, il risultato è che bisogna stare un po 'cauti in 3) sull'interpretazione, ma guidati da 1) si può dare la giusta definizione; e poi il sistema aiuta davvero.
Proposizione 5.2.6.2: Let $C$ e $D$essere categorie. Poi le categorie$\mathrm{Fun}^L(C,D)$ di funtori aggiunti a sinistra da $C$ per $D$, e $\mathrm{Fun}^R(D,C)$ di funtori aggiunti di destra da $D$ per $C$ sono (canonicamente) equivalenti tra loro.
In questa prospettiva, questa proposizione ha davvero senso solo quando $C$ e $D$ sono piccoli, come altrimenti $\mathrm{Fun}(C,D)$è troppo grande. (Si vogliono considerare tali categorie di funtori quando$C$ e $D$sono presentabili (o accessibili), ma solo quando sono limitati ai funtori accessibili. Quindi questa è una discussione che apparirà più avanti nel Capitolo 5.) Quindi l'affermazione è abbastanza chiara e la prova fornita si applica.
In questa prospettiva, penso che sia la stessa di 1), tranne per il fatto che si può anche formulare lo stesso risultato in un universo diverso.
Anch'io.
Si noti tuttavia che così com'è, in 1) questa proposizione non può (ancora) essere applicata nel caso $C$ e $D$sono presentabili. In 2) e 3), quelli (piccoli) presentabili sono categorie speciali grandi, a cui si applica il risultato. Si noti tuttavia che le categorie del funtore e la loro equivalenza vivono tutte in un universo più grande e non otteniamo informazioni su di esse che si trovano in entrambi$V_{\kappa_0+1}$ o $\mathrm{Def}(V_{\kappa_0})$.
La proposizione successiva prende in considerazione la categoria del presheaf $\mathcal P(C)=\mathrm{Fun}(C^{\mathrm{op}},\mathrm{Set})$, e la dimostrazione è un tipico argomento che coinvolge il passaggio a un universo più ampio per risolvere i problemi di coerenza omotopica.
Proposizione 5.2.6.3: Let $f: C\to C'$ essere un funtore tra piccole categorie e lascia $G: \mathcal P(C')\to \mathcal P(C)$ essere il funtore indotto delle categorie presheaf indotte dalla composizione con $f$. Poi$G$ è giusto aggiunto a $\mathcal P(f)$.
Qui $\mathcal P(f)$ è definita come l'unica piccola estensione che preserva i colimit di $f$ (sotto l'incorporamento di Yoneda).
Qui, abbiamo due categorie a dimensione di classe e funtori tra di loro, tutti definibili (come deve essere). La proposizione ci chiederebbe di trovare (definibili!) Trasformazioni di unità e paesi, facendo commutare alcuni diagrammi. Non sembra troppo difficile. Ma in$\infty$-categorie, è notoriamente difficile definire i funtori a mano, quindi non è così che procede Lurie!
Qui $\mathcal P(C)$ e $\mathcal P(C')$sono categorie speciali di grandi dimensioni. Lurie infatti applica la grande incorporazione di Yoneda nella dimostrazione. Quindi questo sta davvero producendo le aggiunte di unità e contatori solo in un universo più grande. Come discusso in precedenza, penso che questa prova in realtà non dia ciò che volevamo in 1)!
Possiamo sostenere come Lurie fa per produrre i dati in un "universo" più ampio. (Modifica: in realtà, come sottolinea Tim Campion, è necessario fare una deviazione minima per giustificare ciò che è scritto. Vedi i commenti alla sua risposta.)
Quindi, quando si legge questa proposizione, in entrambi i sistemi 2) o 3), si dovrebbe fare un segno mentale che finora l'affermazione dimostrata è più debole di quanto si potrebbe ingenuamente sperare. Ma questo viene corretto in seguito, osservando che tutto è determinato da una piccola quantità di dati.
Risultato: mentre all'inizio pensavo che ci sarebbe stata una differenza sostanziale tra 2) e 3), in realtà penso che non ce ne sia (quasi) nessuna. Una differenza è questa$\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$ è una corretta inclusione, ma in pratica il modo per garantire il contenimento in $V_{\kappa_0+1}$ sembra essere quello di dimostrare la definibilità in $V_{\kappa_0}$ (ad esempio, dimostrando che alcuni funtori sono accessibili).
OK, ora dimmi perché non funziona! :-)
Rispondere a questa domanda dipende fortemente da ciò che si vuole dalla teoria dei topi superiori, perché esprimere un'elevata forza logica è un obiettivo diverso dall'esprimere un quadro logico opportunamente unificato per la geometria algebrica e la teoria dei numeri. Solide basi unificate per la matematica categorica generale sono un ottimo obiettivo e sembrano essere l'obiettivo di molti collaboratori qui. Per questo obiettivo tutto ciò che viene detto nei commenti e nelle risposte a questa domanda è rilevante. Ma un lavoro appropriato in geometria e teoria dei numeri non richiede una grande forza logica.
Sebbene HTT sia più intrecciato con gli universi rispetto a SGA, né HTT né SGA fanno un uso reale dello schema (molto forte) assioma della sostituzione. Così possono usare "universi" radicalmente più deboli di quelli di Grothendieck. Come esempio tipico e pertinente, Grothendieck ha fatto un solo appello allo schema dell'assioma della sostituzione. Questo è nella sua prova abbastanza cruciale che ogni categoria AB5 con un gruppo elettrogeno ha abbastanza iniettori. E questo utilizzo della sostituzione risulta essere eliminabile. Ha funzionato, ma Grothendieck in realtà non ne aveva bisogno per ottenere il suo risultato.
Per espandere l'uso della sostituzione da parte di Grothendieck: Reinhold Baer negli anni '40 usò l'induzione transfinita (che richiede lo schema dell'assioma della sostituzione) per dimostrare che i moduli (su un dato anello) hanno abbastanza iniettivi. Stava esplorando consapevolmente nuove tecniche di dimostrazione e ha ottenuto un buon risultato. Il Tohoku di Grothendieck ha lanciato quella prova in una forma che mostra che ogni categoria AB5 con un piccolo set di generatori ha abbastanza iniettori - e pochi anni dopo Grothendieck ha scoperto che questo era esattamente il teorema di cui aveva bisogno per la coomologia del topos. Baer e Grothendieck avevano entrambi obiettivi pratici, non legati alle preoccupazioni delle fondamenta, ma entrambi volevano anche ottenere le basi giuste. E lo hanno fatto. Ma si scopre che avrebbero potuto ottenere quegli stessi teoremi, correttamente, senza sostituzione, con quasi le stesse dimostrazioni, specificando set di funzioni abbastanza grandi per cominciare (usando il set di alimentazione, ma non la sostituzione). Ci sono risultati che richiedono veramente lo schema dell'assioma di sostituzione. Ma questi risultati si verificano raramente al di fuori della ricerca fondamentale.
Molte persone provenienti da angolazioni molto diverse (alcuni logici, alcuni non gradiscono la logica) dagli anni '60 hanno osservato che nel contesto della geometria algebrica e della teoria dei numeri, l'elevata forza logica dell'assioma dell'universo di Grothendieck, è un sottoprodotto in realtà inutilizzato di Il desiderio di Grothendieck di un quadro unificato per la coomologia. Ciò può ora essere reso abbastanza preciso: l'intero apparato di Grothendieck, inclusa non solo la coomologia del funtore derivato dei topos ma la 2-categoria dei topos e le categorie derivate, può essere formalizzato quasi esattamente nello stesso modo in cui è stato formalizzato da Grothendieck, ma a forza logica molto al di sotto della teoria degli insiemi di Zermelo-Fraenkel o addirittura di Zermelo. Lo stesso vale per HTT. Puoi ottenerlo senza universi inaccessibili o riflessi fintanto che non hai bisogno della vasta (e usata raramente) forza del rimpiazzo. La prova non è stata effettivamente data per HTT. È stato per gli usi degli universi di Grothendieck . Sembra chiaro che lo stesso funzionerà per HTT.
La forza logica necessaria è stata espressa in modi indifferenti: Teoria dei tipi semplici (con aritmetica), Aritmetica degli ordini finiti, Teoria elementare della categoria degli insiemi, Teoria degli insiemi del quantificatore delimitato di Zermelo. In parole povere, si pone un insieme di numeri naturali e si ipotizza che ogni set abbia un set di potenze, ma non si ipotizza l'iterazione illimitata dei set di potenze. Una teoria degli universi abbastanza ingenua può essere considerata conservativa rispetto a uno qualsiasi di questi (il modo in cui la teoria degli insiemi di Godel-Bernays è conservativa rispetto a ZFC) e adeguata a tutto l'apparato di grandi strutture della scuola di Grothendieck.
Considererei un'estensione conservativa di ZFC ottenuta da ZFC mediante l'addizione di una costante $\alpha$ e i seguenti assiomi:
$\alpha$ è un ordinale ($Ord(\alpha)$).
La frase $\phi\leftrightarrow\phi^{V_\alpha}$, per ogni frase nella lingua originale $\phi$ (schema assioma).
$V_{\alpha}$ si comporta come $V$(per tutte le frasi nel linguaggio della teoria degli insiemi). Se sono necessari due (o più) universi, uno può aggiungere un'altra costante$\beta$ con gli assiomi corrispondenti e l'assioma $\alpha<\beta$.
La prova che la teoria risultante è conservativa rispetto a ZFC è facile.
Assumilo $\phi$ è dimostrabile dai nuovi assiomi (assiomi usando $\alpha$), in quale $\phi$è nella lingua originale. Poiché ogni dimostrazione è finita, ci sono finitamente molte frasi$\phi_1$, ..., $\phi_n$ tale che
$Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}})\rightarrow \phi$
è dimostrabile senza nuovi assiomi. Pertanto, si può pensare$\alpha$come variabile libera e la frase precedente è dimostrabile in ZFC (teorema sulle costanti). Da$\alpha$ non si verifica in $\phi$, la seguente implicazione è dimostrabile in ZFC ($\exists$-introduzione):
$\exists\alpha(Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}}))\rightarrow \phi$
Ora, il principio di riflessione per ZFC dice che l'antecedente è un teorema ZFC. Da modus ponens, ZFC lo dimostra$\phi$.
Quindi puoi lavorare con i nuovi assiomi e $V_{\alpha}$ si comporta come un universo, e tutto ciò che è dimostrato che non lo menziona $\alpha$ può essere provato già in ZFC.
Una domanda che è emersa nei commenti riguardava la motivazione per porre la domanda. Vorrei provare ad affrontare questo problema qui.
Innanzitutto, si tratta di imparare! Come ho menzionato nella domanda originale, mi sono divertito con alcuni limiti cardinali "stupidi", e solo in seguito ho imparato a conoscere il principio di riflessione, quindi volevo capire cosa può fare (e cosa non può fare) e se può in qualche modo relegare automaticamente qualsiasi ulteriore versione complicata di tali stime in questa macchina. Quindi è la solita cosa in cui inciampi in una stanza buia e vorresti che la stanza fosse illuminata! Quindi, grazie a tutti voi per le risposte illuminanti!
Un altro motivo è che recentemente sono stato un po 'frustrato dalla soluzione degli universi di Grothendieck al problema in questione. Lasciatemi spiegare.
Voglio davvero parlare della categoria di tutti gli insiemi, o di tutti i gruppi, ecc., E voglio dimostrare dei teoremi al riguardo. E, almeno nella versione von Neumann-Bernays-Gödel (NBG) della teoria ZFC che consente le classi, questa è una nozione perfettamente valida. Quindi trovo ontologicamente molto piacevole lavorare in questo contesto, e mi piacerebbe molto che il teorema del funtore aggiunto fosse un teorema sulle categorie (presentabili) in quel senso.
Ora le categorie presentabili sono determinate da una piccola quantità di dati, quindi si può sempre lavorare con questa piccola quantità di dati e tenere traccia delle dimensioni relative. In effetti, molte dimostrazioni in HTT tengono esplicitamente traccia di tali dimensioni relative, ma ci sono ancora alcuni punti in cui è bello prima dare una "visione più ampia" e guardare queste grandi categorie come se fossero piccole.
In effetti, il teorema del funtore aggiunto riguarda i funtori tra grandi categorie, e diventa rapidamente sgradevole parlarne dall'interno di NBG / ZFC. Nota che l'affermazione del teorema del funtore aggiunto ha perfettamente senso: chiede solo che tutti i dati dell'aggiunta siano definibili. Ma è un po 'brutto cercare di parlare di queste cose da "dentro". Quindi sarebbe sicuramente bello avere una sorta di meta-teoria che usi per discutere di queste grandi categorie e fingere che siano piccole. La sottile questione della "definibilità dall'interno" può essere persa a priori in questa meta-teoria, ma considero centrale questa questione della "definibilità dall'interno", perché dopo tutto quello che volevo era un teorema su tutti gli insiemi, quindi io ' Va bene dover prestare un po 'di attenzione ad esso - e, per togliere la battuta finale, si scopre che questa è precisamente la differenza tra lavorare con gli universi di Grothendieck e lavorare con gli "universi" di Feferman.
Quindi questo è ciò a cui servono gli universi di Grothendieck: ti danno sempre un universo più grande per qualsiasi universo in cui stai attualmente lavorando. Trovo l'esistenza degli universi di Grothendieck completamente intuitiva, e in effetti ipotizzare la loro esistenza sembra completamente alla pari con il postulare un set infinito in primo luogo: stai solo permettendo di raccogliere tutto ciò che già hai in una sua entità più grande.
Ma ora all'improvviso ciò a cui pensavo come tutte le espansioni sono chiamate le espansioni piccole , e ci sono anche molte espansioni più grandi. Quindi, anche se dimostri un teorema del funtore aggiunto in questa impostazione, non è più un teorema sui funtori tra le categorie di tutti gli insiemi / gruppi / ..., ma solo uno dei funtori tra piccoli insiemi / gruppi / .... Quindi se tu pensaci, anche negli universi ZFC + Grothendieck, non proverai mai quel teorema che effettivamente volevi, sulla categoria di tutti gli insiemi. (In realtà, fino a tempi molto recenti, ho assunto che il teorema del funtore aggiunto (per$\infty$-categories) è un'affermazione di ZFC che è stata dimostrata sotto "ZFC + Universes", ma non è del tutto esatto: l'affermazione che è stata dimostrata può anche essere formulata solo in ZFC + Universes.)
Ciò che è stato dimostrato è che è coerente che vale il teorema del funtore aggiunto. Vale a dire, assumendo la consistenza degli universi ZFC +, ora hai prodotto un modello di ZFC - quello dei piccoli insiemi nel tuo modello di universi ZFC + - in cui il teorema è vero. Quindi ora potresti lavorare sulla teoria "ZFC + il teorema del funtore aggiunto", in cui il teorema del funtore aggiunto può essere applicato alla categoria di tutti gli insiemi / gruppi / ..., ma questo mi sembra decisamente un inganno. Non hai nemmeno dimostrato che "ZFC + Universi + teorema del funtore aggiunto" è coerente! (Lo otterrai se inizi con la consistenza di un po 'più di ZFC + Universes, chiedendo$\kappa$ tale che $V_\kappa$soddisfa gli universi ZFC +. Di nuovo, mi sembra un presupposto del tutto equo - continua ad andare avanti.) Ma ora potresti arrivare a vedere il pericolo di salire inavvertitamente la scala della coerenza mentre inizi implicitamente a invocare sempre più teoremi dimostrati anche per piccoli insiemi per tutti i set.
Sarebbe molto più bello se sapessi che, negli universi ZFC + Grothendieck, tutto ciò che hai dimostrato sugli insiemi piccoli è anche un teorema sull'intera categoria ambientale di tutti gli insiemi. Questo non è automatico, ma puoi aggiungerlo come schema di assiomi. Mike Shulman nella sezione 12 della teoria degli insiemi per la teoria delle categorie (arXiv: 0810.1279) discute questa idea (che denota ZMC): la trovo ontologicamente abbastanza piacevole, sembra anche avere un'assiomatizzazione molto semplice (anche più semplice di ZFC!), ma
a) questo schema di assiomi aggiuntivo non è del tutto ovvio per me: perché tutto ciò che è vero in piccoli insiemi dovrebbe valere anche per tutti gli insiemi? (Soprattutto se abbiamo avuto qualche problema dimostrando il risultato desiderato in primo luogo Si noti inoltre che sicuramente non. Non tenere per qualsiasi nozione di piccoli set: Piuttosto, le garanzie schema di assiomi che ci sia una certa nozione di piccoli set per la quale questo tipo di riflessione vale. Ora questo mi sembra un po 'dubbioso perché in primo luogo non ho mai voluto set piccoli, quindi ora li sto postulando e chiedo anche che riflettano ancora l'intero comportamento di tutti i set. Probabilmente va bene, ma non evidente per me.)
b) la forza di coerenza di questo schema assioma è notevolmente più alta: è la stessa della coerenza di un cardinale Mahlo. Questo è ancora basso come fanno i grandi cardinali, ma è molto molto più alto dei semplici universi di Grothendieck (che sono davvero bassi nella parte inferiore della gerarchia).
Per quanto riguarda a), il fatto che potremmo provare la coerenza del teorema del funtore aggiunto dalla consistenza degli universi di Grothendieck punta nella giusta direzione, ma questo non garantisce di per sé che i due insieme siano coerenti. Posso immaginare che potrei convincermi che lo schema dell'assioma è ragionevole, ma di certo penso che abbia bisogno di molte più giustificazioni rispetto ai semplici universi di Grothendieck. (Domanda a margine: quanto sono grandi i grandi cardinali che si possono giustificare usando l'idea di "permettere di raccogliere tutto quello che già avevamo"? Non sono sicuro che questa sia una domanda del tutto ben definita ... ma per me, una cardinale misurabile non è sicuramente di quel tipo (ma sono felice di essere corretto), poiché sembra postulare l'emergere di nuove caratteristiche combinatorie.)
Un altro motivo per cui recentemente sono diventato un po 'scontento degli universi di Grothendieck è che mentre in un certo senso vorremmo usarli per poter ignorare le sottigliezze della teoria degli insiemi, in qualche modo tornano a morderti, come ora devi specificare in in quale universo vivono certe cose. A volte, potresti anche dover specificare diversi universi diversi per diversi tipi di oggetti (pensa ai fasci su set profiniti), e trovo che diventa rapidamente piuttosto brutto. Preferirei di gran lunga che tutti gli oggetti vivessero insieme in un universo.
Quindi, mentre pensavo ai fasci su set profiniti, sono arrivato a trovare la soluzione con un solo universo molto più esteticamente e ontologicamente gradevole, e questa soluzione (set condensati) può essere formalizzata in ZFC senza problemi.
OK, quindi affermo che gli universi di Grothendieck non hanno davvero risolto il problema che si proponevano di risolvere, come
a) non ti permettono ancora di dimostrare teoremi sulla categoria di tutti gli insiemi / gruppi / ... (eccetto come risultato di coerenza, o sotto assiomi cardinali grandi e più forti)
b) lavorando con loro, devi ancora preoccuparti dei problemi di dimensione: la tua categoria di tutti i set ora viene stratificata in set di tutti i tipi di dimensioni diverse (cioè in universi diversi).
Inoltre, aumentano anche la forza della consistenza.
Ora, dopo questa meravigliosa discussione qui, penso che la proposta di Feferman sia effettivamente molto migliore. Tuttavia, come ha commentato anche Mike Shulman, considero gli assiomi di Feferman non come una descrizione di un mondo ontologicamente corretto, ma considero gli "universi" della teoria di Feferman semplicemente come comodità, per parlare di grandi categorie come se fossero piccole. In altre parole, la teoria di Feferman ti fornisce esattamente una meta-teoria in cui discutere su categorie così ampie dall'esterno. Ma è una teoria che userei sempre e solo per dare una dimostrazione di un teorema di ZFC. Confrontando gli universi di Grothendieck, la teoria di Feferman
a) non consentono di dimostrare teoremi sulla categoria di tutti gli insiemi / gruppi / ..., perché include in modo esplicito uno schema assioma che tutti i teoremi sui piccoli insiemi sono anche teoremi sui tutti i set.
b) Naturalmente, all'interno di una dimostrazione di un teorema di ZFC che invoca alcuni problemi di dimensioni non banali, è molto positivo che la teoria ti permetta di parlare di varie dimensioni. Inoltre, lo fa in un modo in cui è ancora possibile applicare tutti gli assiomi di ZFC a ciascuno degli "universi", e si occupa anche "dietro le quinte" di come riscrivere tutto in termini di limiti cardinali (potenzialmente estremamente sottili) nella stessa ZFC. Quindi è come un linguaggio di programmazione di alto livello per argomenti che implicano stime cardinali difficili in ZFC.
Inoltre, non aumenta la forza della coerenza, e infatti tutte le affermazioni di ZFC dimostrate in questo linguaggio sono teoremi di ZFC. (Come ho ricordato sopra, potremmo anche avere a) + b) con gli universi di Grothendieck, ma poi arriveremmo alla consistenza di un cardinale Mahlo.)
Quindi, il risultato è che penso che gli universi di Feferman facciano un lavoro molto migliore nel risolvere il problema di fornire una meta-teoria per "parlare di grandi categorie come se fossero piccole" rispetto agli universi di Grothendieck.
Vorrei aggiungere alcune ragioni finali per porre la domanda. Penso che le tecniche di categoria superiore come quelle esposte in HTT siano di fondamentale importanza, non solo nella topologia algebrica in cui hanno avuto origine, ma in tutta la matematica. Posso certamente attestarlo per quanto riguarda la teoria dei numeri e la geometria algebrica. Quindi la loro centralità è anche un motivo importante per analizzare la loro forza di coerenza.
Leggere HTT non è una questione banale: è lunga e complicata. Alcuni colleghi di teoria dei numeri hanno tuttavia affermato che uno dei motivi principali per cui non potevano leggere HTT è che utilizza gli universi . Vale a dire, sono così abituati allo ZFC (e al controllo con estrema cura!) Che cercheranno automaticamente di eliminare qualsiasi uso di universi in una discussione. Ora in SGA, almeno se fossi interessato solo alle applicazioni alla coomologia etale di schemi ragionevoli, questo era qualcosa che potresti farlo a mano - per esempio, aggiungi solo alcuni presupposti di numerabilità per rendere le cose piccole. Tuttavia, in HTT non vedo alcun modo in cui qualcuno sarà in grado di inserire limiti cardinali mentre leggi - gli argomenti sono troppo complessi per questo.
Quindi ora spero di poter dire loro che possono controllare che tutto funzioni in ZFC e che possono ancora leggere HTT (essenzialmente) come scritto, se lo leggono nella teoria degli insiemi di Feferman. Se controllano attentamente (cosa che faranno), potrebbero ancora aver bisogno di compilare un piccolo lemma qui e qualche piccolo argomento extra lì - ma dovrebbero farlo comunque, in qualsiasi libro di ~ 1000 pagine, e potrei immaginare che meno della metà di queste osservazioni secondarie ha a che fare con la sostituzione degli universi di Grothendieck con gli "universi" di Feferman. Qualcuno dovrebbe effettivamente intraprendere quel progetto, ovviamente merita tutto il merito se riesce in questo importante lavoro!
Vorrei concludere con una brevissima nota su quello che sembra essere il punto saliente chiave nella traduzione della teoria di Feferman. Compresi il punto sollevato da Tim Campion nella sua risposta, e ora vedo che questo è stato menzionato anche nella seconda risposta di Jacob Lurie. Approssimativamente, è il seguente. Se$C$ è una categoria presentabile, poi c'è una piccola categoria $C_0$ tale che $C=\mathrm{Ind}_\kappa(C_0)$
per qualche cardinale regolare $\kappa$, confinante liberamente tutto piccolo $\kappa$-colimiti filtrati. Questo fa$C$ naturalmente un'unione di $C_\tau$è, dove $C_\tau$ raccoglie solo i file $\tau$-piccolo $\kappa$-colimiti filtrati. Qui$\tau$ è un cardinale regolare tale che $\tau\gg \kappa$. Questa struttura crescente di$C$ come unione di $C_\tau$è centrale nella teoria delle categorie presentabili, ma i livelli sono realmente enumerati da (certi) cardinali regolari $\tau$. Se aumenti il tuo universo, ottieni anche una versione più grande$C'$ di $C$ stesso e negli universi di Grothendieck $C$ ora è uno dei bei livelli $C'_\tau$ di $C$, dove $\tau$è il cardinale di esclusione dell'universo precedente. Ma negli universi di Feferman, questo$\tau$non è regolare. Questo potrebbe rendere alcuni argomenti più sottili, ma mi aspetto che di solito si possa risolvere questo problema semplicemente incorporandoli$C$ in alcuni $C'_\tau$ con $\tau$ un cardinale regolare più grande del cardinale di separazione dell'universo più piccolo.
In risposta alla modifica che inchioda le cose a un sistema formale che coinvolge i cardinali $\kappa_{-1} < \kappa_0 < \kappa_{1/2} < \kappa_1$:
Esprimerò un aspetto forse più sconsiderato e prevedo che per adattare i capitoli 1-4 a questo sistema formale, non sarà necessaria alcuna reale aritmetica cardinale. Piuttosto, per questa parte del libro, tutto ciò che dovrai fare è esaminare e aggiungere a varie affermazioni di teoremi ipotesi della forma "$X$ è $\kappa_{-1}$-small ". Dopo tutto, questa parte del libro tratta solo di piccoli oggetti, con l'eccezione di alcuni particolari oggetti di grandi dimensioni come la categoria dei piccoli insiemi simpliciali, la categoria delle piccole categorie simpliciali, ecc. e cose come categorie di sezioni. Sono costruite varie strutture modello, ma credo che in ogni caso si possa cavarsela usando il caso speciale dell'argomento piccolo oggetto per generare cofibrazioni / cofibrazioni acicliche tra oggetti finitamente presentabili, in modo che non sia necessaria alcuna induzione transfinita. A prima vista, il raddrizzamento / svincolo ha l'aspetto di costruzioni che potrebbero utilizzare seriamente la teoria degli insiemi, ma andrò avanti e prevedo che non presentano problemi al sistema formale proposto.
Il capitolo 5 diventa più fastidioso. Credo che bisognerà fare alcune scelte attente sui teoremi di base del presentabile ($\infty$) -categorie. Ciò che rende le categorie presentabili valide è che impacchettano il teorema del funtore aggiunto in modo molto pulito, ma come dici tu, il teorema del funtore aggiunto ordinario viene fornito con avvertenze in questa impostazione. Potrei arrivare a dire che il punto centrale di pensare alle categorie presentabili in primo luogo è completamente annullato in questo contesto. Non sarai in grado di dimostrare cose di base come "le categorie presentabili sono precisamente le localizzazioni accessibili di categorie pre-fasce". Prevedo che qualunque scelta venga fatta sulla formulazione di versioni deboli dei teoremi fondamentali delle categorie presentabili in questo contesto, ci sarà qualche applicazione o potenziale applicazione che ne risente.
I capitoli 5 e 6 contengono anche alcuni teoremi su particolari categorie molto grandi come il $\infty$-categoria di presentabile $\infty$-categorie e il $\infty$-categoria di $\infty$-topoi [1]. Il sistema sembra essere tale che questo non sarà davvero un problema di per sé , tranne per il fatto che i problemi incontrati nella teoria di base della presentabilità saranno ora aggravati. Non sarai in grado di dimostrarlo$Pr^L$ è doppio con $Pr^R$. Non sarai in grado di dimostrare il teorema di Giraud (beh, le definizioni saranno in ogni caso in continuo mutamento, quindi dovrei chiarire: non sarai in grado di dimostrare che le localizzazioni esatte a sinistra delle categorie preheaf sono le stesse di localmente piccole categorie che soddisfano un elenco di condizioni di completezza, generazione e esattezza). Quindi qualsiasi teorema su$\infty$-topoi la cui dimostrazione procede partendo dal caso presheaf e poi localizzando dovrà essere completamente ripensata.
Forse sono fuori base qui, ma credo che per i capitoli 5 e 6 sarebbero necessari un lavoro extra significativo e idee matematiche veramente nuove, e il risultato sarebbe una teoria che è sostanzialmente più difficile da usare.
Al contrario, penso che se sei disposto a limitare l'attenzione a grandi categorie definibili da piccoli parametri, anche se ti mancherà la bella capacità di dire "lo abbiamo dimostrato per le piccole categorie ma ora possiamo applicarlo a grandi quelli ", ti ritroverai con una teoria della presentabilità molto più utilizzabile, senza lasciare ZFC.
[1] In realtà, nelle basi usuali queste categorie sono (fino all'equivalenza) solo grandi e non molto grandi (più precisamente, hanno $\kappa_0$-molti oggetti e $\kappa_0$-sized homs), ma è necessario un minimo di lavoro per dimostrarlo. Sarà ancora così in questo sistema formale? Non sono sicuro.
EDIT: Un lungo commento in risposta a Peter Scholze risposta .
Una cosa che ho appena capito è che se$\kappa_0$ non è un $\beth$-punto fisso, quindi non tutti i set in $V_{\kappa_0}$ ha cardinalità $<\kappa_0$, in modo che le nozioni di "piccolezza" si moltiplichino. Fortunatamente, penso che il tuo sistema formale lo dimostri$V_{\kappa_0}$ ha $\Sigma_1$-sostituzione, il che implica che si tratta di un file $\beth$-Punto fisso. Crisi scongiurata!
Forse questo approccio di utilizzare sistematicamente ipotesi di definibilità all'interno di un "universo" sarà realizzabile - combinando il "meglio di entrambi i mondi". Una cosa carina è che anche se stai usando esplicitamente ipotesi metamatematiche, sembrerebbe che sarai ancora in grado di affermare e dimostrare questi teoremi come singoli teoremi piuttosto che come schemi.
Sono un po 'confuso riguardo alla Proposizione 5.2.6.3 (l'ultima di cui parli e una versione per bambini del teorema del funtore aggiunto). Presumo che la categoria presheaf$P(C)$ sarà definito per comprendere quei funtori $C^{op} \to Spaces$ che si trovano in $Def(V_{\kappa_0})$. Quando passiamo a un universo più grande, la transizione di solito è piuttosto fluida, perché ci aspettiamo$P(C)$ per avere tutti i colimit indicizzati da $\kappa_0$-piccole categorie: una proprietà perfettamente naturale con cui lavorare $V_{\kappa_1}$. In effetti, il primo passo della dimostrazione di Lurie del 5.2.6.3 è mostrare che esiste un aggiunto sinistro usando il fatto che$P(C)$ha tutti i colimiti piccoli [2]. Tuttavia, nell'attuale contesto non possiamo mai supporlo$\kappa_0$ è regolare, e quindi non possiamo mai supporlo $P(C)$ha tutti i colimiti piccoli. Il meglio che possiamo dire è questo$V_{\kappa_0}$ pensa $P(C)$ha tutti i colimiti piccoli. Finché ci stiamo lavorando$V_{\kappa_0}$, questa proprietà è "altrettanto buona" di avere tutti i colimit piccoli. Ma quando passiamo a$V_{\kappa_1}$, improvvisamente dobbiamo pensarci per quello che è: una proprietà metamatematica. Forse più tardi mi siederò e proverò a vedere se la dimostrazione di Lurie della 5.2.6.3 può essere fatta funzionare in questa impostazione, ma penso che prima facie non sia chiaro.
[2] Solo dopo aver verificato l'esistenza astrattamente in questo modo mostra che l'aggiunto sinistro deve essere il funtore indicato. Naturalmente, questa manovra è in realtà un'ulteriore complicazione che viene fornita con il$\infty$-impostazione categoriale - nelle categorie ordinarie le formule per i due funtori possono essere verificate direttamente per essere aggiunte, ma in $\infty$-categorie la formula per l'aggiunto sinistro non è ovviamente funtoria.