Princípio de reflexão vs universos
Em discussões teóricas de categorias, freqüentemente há a tentação de olhar para a categoria de todos os grupos abelianos, ou de todas as categorias, etc., o que rapidamente leva aos problemas usuais da teoria dos conjuntos. Freqüentemente, eles são evitados usando universos de Grothendieck. Na linguagem da teoria dos conjuntos, corrige-se alguns pontos cardeais fortemente inacessíveis$\kappa$ -- Isso significa que $\kappa$ é algum cardeal incontável que, para todos $\lambda<\kappa$, tb $2^\lambda<\kappa$, e para qualquer conjunto de $<\kappa$ muitos conjuntos $S_i$ do tamanho $<\kappa$, também a união deles é de tamanho $<\kappa$. Isso implica que o estágio$V_\kappa\subset V$ de "conjuntos de tamanho $<\kappa$"é em si um modelo de ZFC - ao aplicar qualquer uma das operações em conjuntos, como tomar conjuntos de poderes ou uniões, você nunca pode sair $V_\kappa$. Esses conjuntos são então denominados "pequenos", e então a categoria de pequenos grupos abelianos é definitivamente bem definida.
Historicamente, essa abordagem foi usada pela primeira vez por Grothendieck; um texto fundamental mais recente é o trabalho de Lurie sobre$\infty$-categorias. No entanto, seu uso sempre criou um certo retrocesso, com algumas pessoas relutantes em permitir que axiomas além do ZFC caiam na literatura estabelecida. Por exemplo, acho que em algum momento houve uma longa discussão se o Último Teorema de Fermat foi provado no ZFC, agora estabelecido por McLarty. Mais recentemente, vi argumentos semelhantes surgindo para teoremas cujas provas se referem ao trabalho de Lurie. (Pessoalmente, não tenho sentimentos fortes sobre isso e entendo os argumentos de qualquer maneira.)
Por outro lado, também sempre aconteceu que um exame mais detalhado revelou que qualquer uso de universos era de fato desnecessário. Por exemplo, o Stacks Project não usa universos. Em vez disso, (ver Tag 000H dizer) efetivamente enfraquece a hipótese de que$\kappa$ é fortemente inacessível, a algo como um cardeal limite forte de cofinalidade incontável, ou seja: para todos $\lambda<\kappa$, um tem $2^\lambda<\kappa$, e sempre que você tiver uma coleção contável de conjuntos$S_i$ do tamanho $<\kappa$, também a união do $S_i$ tem tamanho $<\kappa$. ZFC prova facilmente a existência de tais$\kappa$, e quase todos os argumentos que alguém possa imaginar fazer na categoria de grupos abelianos, na verdade também funcionam na categoria de $\kappa$-pequenos grupos abelianos para tal $\kappa$. Se alguém fizer argumentos mais complicados, pode-se, portanto, fortalecer a hipótese inicial sobre$\kappa$. Tive a oportunidade de jogar este jogo sozinho, consulte a Seção 4 de www.math.uni-bonn.de/people/scholze/EtCohDiamonds.pdf para o resultado. A partir dessa experiência, tenho certeza de que se pode reescrever de forma semelhante a "Teoria do Topos Superior" de Lurie, ou qualquer outro trabalho teórico-categórico semelhante, de forma a remover todos os cardeais fortemente inacessíveis, substituindo-os por cuidadosamente escolhidos$\kappa$ com propriedades como as acima.
Na verdade, parece haver um teorema de ZFC, o princípio de reflexão (discutido brevemente no Tag 000F do projeto Stacks, por exemplo), que parece garantir que isso seja sempre possível. Ou seja, para qualquer dado conjunto finito de fórmulas da teoria dos conjuntos, há alguns suficientemente grandes$\kappa$ de modo que, grosso modo, essas fórmulas se sustentam $V_\kappa$ se e somente se eles segurarem $V$. Isso parece dizer que, para qualquer conjunto finito de fórmulas, pode-se encontrar alguns$\kappa$ de tal modo que $V_\kappa$se comporta como um universo em relação a essas fórmulas, mas, por favor, corrija-me em minha compreensão muito ingênua do princípio de reflexão! (Um fato relacionado é que ZFC prova a consistência de qualquer dado fragmento finito dos axiomas de ZFC.)
Por outro lado, qualquer texto matemático contém apenas um número finito de fórmulas (a menos que exponha um "esquema de teorema", o que geralmente não acontece, creio eu). A questão é, portanto, formulada de forma ligeiramente provocativa:
O princípio da reflexão implica que deve ser possível reescrever a Teoria do Topos Superior de uma forma que evite o uso de universos?
Edit (28.01.2021): Muito obrigado por todas as respostas muito úteis! Acho que tenho uma imagem muito mais clara da situação agora, mas ainda não tenho certeza de qual é a resposta para a pergunta.
Pelo que entendi, (aproximadamente) o melhor metateorema nessa direção é o seguinte (especializado em HTT). Lembre-se de que o HTT corrige dois cardeais fortemente inacessíveis$\kappa_0$ e $\kappa_1$, abrindo espaço para pequenos (em $V_{\kappa_0}$), grande (em $V_{\kappa_1}$), e muito grande (em $V$) objetos. Pode-se então tentar ler HTT no seguinte sistema de axiomas (este é essencialmente aquele do artigo de Feferman "Fundamentos teóricos dos conjuntos da teoria das categorias", e também foi proposto na resposta de Rodrigo Freire a seguir).
(i) Os axiomas ZFC usuais
(ii) Dois outros símbolos $\kappa_0$ e $\kappa_1$, com os axiomas de que são cardeais, que a cofinalidade de $\kappa_0$ é incontável, e que a cofinalidade de $\kappa_1$ é maior que $\kappa_0$.
(Iii) Um esquema axiomático, dizendo que para cada fórmula $\phi$ da teoria dos conjuntos, $\phi\leftrightarrow \phi^{V_{\kappa_0}}$ e $\phi\leftrightarrow \phi^{V_{\kappa_1}}$.
Então, o princípio da reflexão pode ser usado para mostrar (veja a resposta de Rodrigo Freire abaixo para um esboço da prova):
Teorema. Este sistema axioma é conservador em relação ao ZFC. Em outras palavras, qualquer teorema neste sistema formal que não se refere a$\kappa_0$ e $\kappa_1$ também é um teorema de ZFC.
Essa é exatamente a conclusão que eu gostaria de ter.
Observe que $V_{\kappa_0}$ e $V_{\kappa_1}$ são modelos de ZFC, mas (criticamente!) isso não pode ser provado dentro do sistema formal, pois ZFC não é finitamente axiomatizável, e apenas cada axioma individual de ZFC é postulado por (iii).
Uma coisa boa sobre esse sistema de axiomas é que ele permite explicitamente os argumentos ocasionais da forma "provamos esse teorema para categorias pequenas, mas também podemos aplicá-lo a categorias grandes".
Uma pergunta mais precisa é então:
Os argumentos do HTT funcionam neste sistema formal?
Mike Shulman na Seção 11 do https://arxiv.org/abs/0810.1279dá uma exposição muito clara de qual é o problema potencial aqui. Ou seja, se você tiver um conjunto$I\in V_{\kappa_0}$ e conjuntos $S_i\in V_{\kappa_0}$ para $i\in I$, você não tem permissão para concluir que a união do $S_i$ é em $V_{\kappa_0}$. Esta conclusão só é garantida se a função$i\mapsto S_i$ também é definido em $V_{\kappa_0}$ (ou se $I$é contável, pela suposição extra de cofinalidade incontável). Na prática, isso significa que quando se quer afirmar que algo é "pequeno" (ou seja, em$V_{\kappa_0}$), esse julgamento pertence não apenas a objetos, mas também a morfismos etc. Não está claro para mim agora o quanto isso é realmente um problema, eu teria que pensar mais sobre isso; Eu posso realmente imaginar que é muito fácil ler HTT para atender a esse sistema formal. Shulman diz que, com essa ressalva, o teorema do functor adjunto pode ser provado e, como diz Lurie em suas respostas, os argumentos em HTT são de complexidade teórica de conjuntos semelhante. No entanto, ainda estou interessado em saber se a resposta à pergunta é "Sim, conforme está escrito" ou "Provavelmente sim, mas você precisa se esforçar" ou, na verdade, "Na verdade, não". (Eu sinceramente espero que os especialistas consigam chegar a um consenso sobre onde a resposta se encaixa nesse espectro.)
Uma observação final: pode-se achar a suposição de "incontabilidade" acima um pouco arbitrária; por que não permitir alguns sindicatos ligeiramente maiores? Uma maneira de cuidar disso é adicionar um símbolo$\kappa_{-1}$ com as mesmas propriedades e, em vez disso, pedir que a cofinalidade de $\kappa_0$ é maior que $\kappa_{-1}$. Da mesma forma, pode-se querer substituir o limite$\mathrm{cf} \kappa_1>\kappa_0$ por um limite ligeiramente mais forte como $\mathrm{cf} \kappa_1>2^{\kappa_0}$dizer. Novamente, se simplifica as coisas, pode-se então apenas apertar outro$\kappa_{1/2}$ no meio, de modo que $\mathrm{cf} \kappa_{1/2}>\kappa_0$ e $\mathrm{cf} \kappa_1>\kappa_{1/2}$. Desta forma, não é necessário se preocupar se algum dos objetos "padrão" que aparecem em algumas provas permanece de tamanho contável, ou se ainda se pode tomar colimites em$V_{\kappa_1}$ quando os conjuntos de índices não são exatamente do tamanho limitado por $\kappa_0$ mas foram um pouco manipulados.
PS: Só agora estou encontrando todas as perguntas e respostas relevantes do MO anterior. Algumas respostas muito relevantes são as respostas de Joel Hamkins aqui e aqui .
Respostas
Eu vou arriscar e sugerir que o livro HTT nunca usa nada mais forte do que substituto para $\Sigma_{15}$-fórmulas da teoria dos conjuntos. (Aqui$15$ é um grande número escolhido aleatoriamente e HTT é um livro de matemática escolhido aleatoriamente que não trata especificamente da teoria dos conjuntos.)
Refletindo sobre o comentário de Gabe sobre minha resposta original, agora acho que o que escrevi é enganoso porque confunde duas afirmações separadas (mas relacionadas):
A existência de cardeais fortemente inacessíveis não é realmente necessária na teoria das categorias.
A força total do ZFC não é realmente necessária na teoria da categoria.
Concordo com ambas as afirmações, mas acho que a melhor maneira de convencer alguém de 1) não seria combinar 2) com um princípio de reflexão: isto é, não se deve tentar substituir o uso de um cardeal fortemente inacessível $\kappa$ por um pelo qual $V_{\kappa}$ modela uma grande parte do ZFC.
A meu ver, o "problema" que os universos resolvem é justificar a combinação de dois tipos de raciocínio:
A) Às vezes é útil provar teoremas sobre pequenas categorias $\mathcal{C}$ incorporando-os em categorias "grandes" (por exemplo, usando a incorporação de Yoneda) que possuem recursos adicionais interessantes: por exemplo, a existência de limites e colimites.
B) Grandes categorias também são categorias, portanto, qualquer teorema que se aplique a categorias em geral também deve se aplicar a grandes categorias.
Se você estava preocupado apenas com B), um princípio de reflexão poderia ser relevante. Escolhendo um cardeal$\kappa$ de tal modo que $V_{\kappa}$ satisfaz uma grande parte do ZFC, você pode redefinir "pequena categoria" para significar "categoria pertencente a $V_{\kappa}$"e" categoria grande "significam" categoria não necessariamente pertencente a $V_{\kappa}$", e você pode ter certeza de que todos os teoremas básicos que deseja são válidos em ambos os casos.
Mas se você também estiver preocupado com A), isso não será necessariamente útil. Digamos que você comece com uma categoria$\mathcal{C}$ pertencendo à $V_{\kappa}$, e você deseja alguma versão da incorporação de Yoneda. Uma suposição natural seria incorporar na categoria de functores de$\mathcal{C}^{\mathrm{op}}$ para a categoria de conjuntos de tamanho $<\tau$ (ou algum modelo equivalente dele), para algum cardeal $\tau$. Um primeiro palpite é que você deve pegar$\tau = \kappa$, mas acho que isso só faz sentido $\kappa$é fortemente inacessível (caso contrário, alguns conjuntos de Hom serão muito grandes). Em qualquer caso garanta que esta construção tem boas propriedades, você vai querer exigir diferentes propriedades do cardeal$\tau$. Por exemplo, se você quiser que esta categoria de pré-céus tenha muitos colimites, então você vai querer$\tau$para ter grande cofinalidade. E se você começar a pensar sobre que tipos de suposições adicionais você pode precisar fazer, você está de volta ao ponto de partida: pensando sobre que tipo de estimativas de cardinalidade garantem que "pré-variações de conjuntos de tamanho$< \tau$"são uma boa aproximação da categoria de todos os pré-escalões de conjuntos. Portanto, o princípio de reflexão não ajuda você a evitar esses problemas.
(Editar: depois de escrever, percebi que o texto abaixo está basicamente reiterando a postagem original de Peter. Mas vou deixá-lo aqui, caso alguém o considere útil.)
Se você deseja uma formalização rigorosa em algo como ZFC, provavelmente a melhor coisa a fazer é eliminar totalmente as grandes categorias. Portanto, B) não é um problema. Para lidar com A), deixe-me observar que muitas das "grandes" categorias sobre as quais gostaríamos de falar surgem de uma maneira particular: começa-se com uma pequena categoria$\mathcal{C}$ que já tem certos tipos de colimites, e formalmente amplia $\mathcal{C}$ para fazer uma categoria maior $\mathcal{C}^{+}$que tem colimites arbitrários (sem alterar aqueles com os quais você começou). As categorias que surgem desta forma são chamadas localmente apresentáveis , e há uma fórmula simples para$\mathcal{C}^{+}$: é a categoria de functores $F: \mathcal{C}^{\mathrm{op}} \rightarrow \mathrm{Set}$ que preservam os limites com os quais você começou (isto é, os colimites com os quais você começou em $\mathcal{C}$)
Agora, se você quiser imitar isso no mundo das pequenas categorias, você pode escolher algum cardeal $\kappa$ e em vez disso, contemple functores $F: \mathcal{C}^{\mathrm{op}} \rightarrow \{ \text{Sets of size < $\ kappa$} \}$, que é equivalente a uma pequena categoria $\mathcal{C}^{+}_{\kappa}$. A questão que você encontra é se este é um substituto bom o suficiente para a grande categoria$\mathcal{C}^{+}$acima de. Por exemplo, ele tem muitos limites e colimites? Não é razoável pedir que ele tenha todos os colimites, mas você pode perguntar o seguinte:
Q) A categoria $\mathcal{C}^{+}_{\kappa}$ têm colimites indexados por diagramas de tamanho $< \kappa$?
A resposta a Q) é "não em geral, mas sim se $\kappa$ é bem escolhido ". Por exemplo, se você tiver algum cardinal infinito $\lambda$ limitando o tamanho de $\mathcal{C}$ e o número de diagramas de colimites com os quais você começa, então acredito que você pode garantir (i) tomando $\kappa = (2^{\lambda})^{+}$ (e a categoria $\mathcal{C}^{+}_{\kappa}$pode ser caracterizada pela propriedade universal esperada). Além disso, para provar isso você não precisa de nenhuma forma de substituição.
Agora você também pode perguntar o seguinte:
Q ') A categoria $\mathcal{C}^{+}_{\kappa}$ têm limites indexados por diagramas de tamanho $< \kappa$?
Aqui, a resposta geralmente será "não", a menos que $\kappa$é fortemente inacessível. Mas se você estiver interessado apenas em limites de um tipo específico (por exemplo, se estiver estudando topoi de Grothendieck, você pode estar especialmente interessado em limites finitos), então a resposta será novamente "sim para$\kappa$ bem escolhido ". E isso você pode provar usando muito pouco do ZFC.
Agora, minha afirmação é que, com base na minha experiência, a discussão acima é representativa do tipo de perguntas que você encontrará ao tentar navegar na distinção entre categorias "pequenas" e "grandes" (certamente é representativo da maneira como essas coisas aparecer no meu livro, sobre o qual a pergunta original foi feita). Na prática, você nunca precisa falar sobre a totalidade de uma grande categoria como$\mathcal{C}^{+}$; é o suficiente para construir um pedaço grande o suficiente dele (como$\mathcal{C}^{+}_{\kappa}$) tendo os recursos que você deseja ver, que você pode organizar escolhendo $\kappa$ cuidadosamente.
Acho que é conceitualmente mais claro ignorar a questão de como as coisas são formalizadas no ZFC e formular as coisas em termos da categoria "grande" $\mathcal{C}^{+}$, referindo-se às suas "pequenas" aproximações $\mathcal{C}^{+}_{\kappa}$apenas como auxiliares em uma prova (que inevitavelmente ainda aparecerá em algum lugar!). A invocação de "universos" é apenas uma maneira de escrever assim, ao mesmo tempo em que elogia a estrutura axiomática do ZFC, e é definitivamente não essencial.
Gostaria de mencionar algo que acho que ainda não foi apontado. A pergunta original começou com
Na linguagem da teoria dos conjuntos, corrige-se alguns pontos cardeais fortemente inacessíveis $\kappa$... Isso implica que o estágio $𝑉_\kappa\subset 𝑉$ de "conjuntos de tamanho $<\kappa$"é em si um modelo de ZFC.
No entanto, a declaração de que $V_\kappa$ é um modelo de ZFC é significativamente mais fraco do que dizer que $\kappa$está inacessível. Na verdade, se$\kappa$ é inacessível, então $\{ \lambda\mid V_\lambda$ é um modelo de ZFC $\}$ está estacionário em $\kappa$. Portanto, o menor inacessível (se houver) é muito maior do que o menor$\kappa$ de tal modo que $V_\kappa$ modelos ZFC.
Na medida em que o princípio de reflexão é útil (o que, como algumas outras respostas apontaram, pode-se ao menos questionar), ele só é diretamente útil para argumentos nos quais a propriedade relevante de um universo de Grothendieck é ser um modelo de ZFC. No entanto, pelo menos quando formulada ingenuamente, há muitos lugares onde a teoria das categorias usa mais do que isso. Especificamente, usamos o fato de que um universo de Grothendieck satisfaz a substituição de segunda ordem , o que significa que qualquer função$f:A\to V_\kappa$, Onde $A \in V_\kappa$, tem uma imagem. Dizendo isso$V_\kappa$modelos ZFC apenas implica que satisfaz a substituição de primeira ordem , o que apenas nos permite concluir que tal$f$ tem uma imagem se $f$ é definível de $V_\kappa$ por uma fórmula lógica.
Eu acredito que a substituição de segunda ordem é onipresente na teoria das categorias baseada no universo, como geralmente formulada. Por exemplo, se${\rm Set}_\kappa$ denota a categoria de conjuntos em $V_\kappa$, então para provar que ${\rm Set}_\kappa$ é "completo e cocompleto" no sentido ingênuo de que admite um limite e colimite para qualquer functor cujo domínio seja pequeno, precisamos de substituição de segunda ordem para coletar as imagens de tal functor em um único conjunto.
Agora, existem maneiras de reformular a teoria das categorias para evitar isso. O artigo de McLarty faz isso de algumas maneiras da teoria dos conjuntos. Uma abordagem categoricamente consistente é substituir ingênuas "grandes categorias" (categorias de significado cujos conjuntos de objetos e morfismos podem não pertencer a$V_\kappa$) com grande ${\rm Set}_\kappa$- categorias indexadas . Mas esse é um tipo de reformulação muito mais substancial para executar manualmente.
Se bem entendi, você está atrás de uma declaração do formulário:
"Se algo foi provado em HTT usando universos, pode ser provado sem eles, restringindo-se a alguns $V_\kappa$ para $\kappa$ grande o suficiente"
A resposta rigorosa para isso, se não tivermos mais informações sobre o HTT, é que não pode haver tal declaração se o ZFC for consistente.
Na verdade, é possível que a existência de universos seja inconsistente (na verdade não é possível provar que é consistente), e nessa situação, qualquer coisa pode ser provada usando universos, e assim tal afirmação implicaria que qualquer coisa pode ser provada , ou seja, ZFC é inconsistente.
Estou sendo um pouco descuidado sobre o que pode ser provado em quê, etc., mas a ideia principal está aí
Claro, sabemos coisas sobre HTT, e se lermos cuidadosamente podemos analisar onde ele usa universos, e ver que eles podem de fato ser substituídos por modelos transitivos de substituição ZC + até $\Sigma_{15}$-fórmulas, como Jacob aponta. Nesse caso, uma vez que provavelmente existem tais modelos bem comportados (da forma$V_\kappa$, para $\kappa$bem escolhido), isso não é um problema; e o HTT pode ser reescrito sem universos - mas isso não pode ser provado sem o conhecimento do que está no HTT.
A "moral" disso é que, na maioria das questões teóricas das categorias principais, os universos são um dispositivo que economiza tempo, e não uma parte real da matemática.
Qualquer teorema $T$ de $\mathsf{ZFC}$ segue de um subconjunto finito dos axiomas de $\mathsf{ZFC}$ ou, para manter as coisas simples, de $\mathsf{ZFC}$ onde o esquema de axioma de substituição é restrito a $\Sigma_n$ predicados¹, chame isso $\mathsf{ZFC}_n$. Agora$\mathsf{ZFC}$, e mais precisamente $\mathsf{ZFC}_{n+1}$, prova a existência de cardeais arbitrariamente grandes $\kappa$, limites fortes de cofinalidade incontável, de tal forma que $V_\kappa$ é um modelo de $\mathsf{ZFC}_n$, e, em particular, do teorema $T$, e de modo que, além disso, o valor de verdade de qualquer $\Sigma_n$ declaração, com parâmetros em $V_\kappa$ é o mesmo em $V_\kappa$como no (verdadeiro) universo. Podemos chamá-los$V_\kappa$ "Universos limitados" no sentido de que eles são fechados sob a maioria das operações teóricas de conjuntos, como conjuntos de poderes, exceto que a substituição precisa ser contável (incluída por conveniência) ou restrita a um $\Sigma_n$predicado; e, em particular, eles são fechados sob quaisquer declarações de existência$T$ faz.
Portanto, a ideia seria aplicar o que precede à conjunção $T$ de todos os teoremas que você considera fazer parte da Teoria Topos Superior (e quaisquer outras teorias são usadas como pré-requisitos) e encontre o apropriado $n$. (Eu realmente suspeito que$n=1$ deve ser suficiente: eu ficaria muito surpreso em encontrar um exemplo de substituição na matemática comum que não decorre de $\Sigma_1$-substituição.) Então $\mathsf{ZFC}_n$ provaria $T$ (todos os teoremas da teoria) e $\mathsf{ZFC}_{n+1}$ provaria a existência de um suprimento infinito de universos limitados nos quais usar a teoria.
Claro, para evitar um loop infinito, você não pode considerar esse teorema (aquele que afirma a existência de um suprimento infinito de$V_\kappa$) para fazer parte da teoria, ou você precisa mudar para uma $n$.
Para explicar o que pode parecer uma contradição lógica, aqui, deve ser esclarecido que a afirmação de que a existência de muitos modelos de $\mathsf{ZFC}_n$ pode ser provado em $\mathsf{ZFC}$ para cada $n$, mas não uniformemente (a prova fica cada vez mais longa à medida que $n$ cresce), então $n$deve ser um número natural concreto , o universalmente quantificado (sobre $n$) declaração não pode ser provada em$\mathsf{ZFC}$. Mas isso não é um problema, desde que sua teoria seja fixada e formulada em$\mathsf{ZFC}$ (o que exige que ele não contenha, por si só, metateoremas como "para qualquer concreto $n$ podemos provar o seguinte em $\mathsf{ZFC}$”). Portanto, cabe a você verificar se este é o caso do HTT (e, se você for corajoso o suficiente, encontre o apropriado$n$)
(Apenas para dar uma ideia de como os tipos de cardeais envolvidos, os cardeais $\kappa$ de tal modo que $V_\kappa$ é um modelo de $\mathsf{ZFC}_1$ são os pontos fixos do $\gamma \mapsto \beth_\gamma$função. Eu não acho que haja qualquer esperança de uma descrição razoável do$\kappa$ de tal modo que $V_\kappa$ é um modelo de $\mathsf{ZFC}_n$ para qualquer concreto $n\geq 2$. Veja também esta questão .)
- Significado predicados com no máximo $n$ conjuntos alternados de quantificadores ilimitados, começando com quantificadores existenciais, seguidos por fórmula com quantificadores limitados (significado da forma $\forall x\in y$ ou $\exists x\in y$)
OK, passei grande parte do dia tentando descobrir isso olhando em detalhes no HTT. Foi um passeio e tanto; Eu definitivamente mudei minha perspectiva várias vezes no processo. Atualmente, parece-me que a resposta é que o HTT, da forma como está escrito, pode ser lido neste sistema formal. (É como na piada em que depois do expediente alguém diz "Sim, é óbvio". Definitivamente, há pontos em que a interpretação correta deve ser escolhida, mas, como em qualquer texto matemático, esse já é o caso de qualquer maneira.) com essa resposta, quero avançar um argumento de que HTT pode ser lido neste sistema formal, tentando explicar um pouco como interpretar certas coisas no caso de surgir ambigüidade, e por que acho que lendo desta forma tudo deve funcionar. Mas é bastante provável que eu tenha esquecido algo importante, então, por favor, me corrija!
Como observa Tim Campion, a maioria das primeiras coisas funciona sem problemas - na verdade, nem mesmo menciona universos. Enquanto isso não acontecer, tudo funciona em$V_{\kappa_0}$, dentro $V_{\kappa_1}$, e em $V$, e o esquema de axioma fornecido garante até mesmo que quaisquer construções feitas serão compatíveis.
É preciso prestar mais atenção ao chegar aos Capítulos 5 e 6. Deixe-me tentar apresentar algumas definições e proposições desses capítulos a partir de três pontos de vista diferentes.
O ponto de vista clássico do ZFC, ou (equiconsistentemente) o da teoria de von Neumann - Bernays - Gödel (NBG), que permite classes além de conjuntos, para que possamos falar sobre a categoria (tamanho de classe) de todos os conjuntos $\mathrm{Set}$.
O ponto de vista do HTT, que é universos ZFC + Grothendieck.
O ponto de vista da teoria dos conjuntos de Feferman, na forma declarada na pergunta. (Na verdade, não tenho mais certeza se realmente preciso desses limites de finalidade. Mas é bom saber que eles podem ser presumidos.)
Observe que a pergunta feita presume que alguém está realmente interessado no primeiro ponto de vista e nos outros apenas na medida em que sejam conveniências para provar algo sobre o primeiro cenário. Isso se alinha com o conteúdo dos Capítulos 5 e 6: toda a teoria das categorias apresentáveis se encaixa perfeitamente no primeiro cenário, também filosoficamente.
OK, então lembre-se de que uma categoria apresentável - deixe-me ficar com as categorias $\infty$-categorias, a diferença não é essencial para nossas preocupações - é uma categoria (do tamanho da classe) $C$ que admite todos os pequenos colimites, e de tal forma que para alguns cardeais regulares $\kappa$, há uma pequena categoria $C_0$ e uma equivalência $C\cong \mathrm{Ind}_{\kappa}(C_0)$,
ie $C$ é obtido por livremente adjacente $\kappa$-colimites filtrados para $C_0$. (Em particular,$C_0$ é necessariamente equivalente à subcategoria completa de $\kappa$-objetos compactos de $C$.) Em particular, as categorias apresentáveis são determinadas por uma pequena quantidade de dados. Além disso, a ideia é que$C$é realmente a categoria de todos os objetos (conjuntos, grupos, qualquer coisa). Este ponto de vista é realmente mais claramente articulado em 1), enquanto em 2) e 3) a noção de apresentabilidade de repente depende novamente do universo, e de repente eles estão novamente contendo apenas pequenos conjuntos / grupos / ...; deixe-me então chamá-los de apresentáveis pequenos. Observe que essa noção faz sentido em 2) e 3), e depende apenas de$V_{\kappa_0}$. Uma categoria pequena apresentável é então, em particular, pequena definível, então vive em$\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$, onde esta inclusão é uma igualdade em 2) (mas não em 3)).
Em 2), normalmente se definiria uma categoria pequena e apresentável como um tipo especial de categoria grande, que é a abordagem de HTT. Mas aqui eu já estou ficando um pouco confuso: parece haver duas noções de functores$F: C\to D$: Os que podem ser definidos em $V_{\kappa_0}$, equivalentemente $F\in V_{\kappa_0+1}$ (nomeadamente, $V_{\kappa_0+1}$ são exatamente as classes de $V_{\kappa_0}$), ou todos os functores em $V_{\kappa_1}$. Não me parece óbvio que qualquer functor$F: C\to D$ dentro $V_{\kappa_1}$ encontra-se em $V_{\kappa_0+1}$, como $C$ e $D$ eles próprios só vivem em $V_{\kappa_0+1}$. A diferença entre essas duas noções desaparece quando se restringe a functores acessíveis, todos os quais são definíveis. Observe que 1) diz que é realmente a primeira noção com a qual devemos nos preocupar! (Antes de escrever este post, eu não estava ciente da diferença.)
Em 3), a maneira adequada de proceder é usar a perspectiva ditada por 1), que é a de "$V_{\kappa_0}$-categorias definíveis ", para que vivam em $\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$. Pode-se novamente considerá-los como$\kappa_1$-pequenas categorias. A princípio pensei que haveria uma diferença substancial aqui entre as abordagens de 2) e 3), mas na verdade parece que em ambos os casos chegamos a duas noções diferentes de functores, que são reconciliadas quando nos restringimos a functores acessíveis.
Um dos principais teoremas é o teorema do functor adjunto: Se $F: C\to D$é um functor de categorias apresentáveis que preserva todos os pequenos colimites, então admite um adjunto direito. O que esse teorema realmente significa?
Em 1), significa que há um functor $G: D\to C$ - o que em particular significa que deve ser definível por fórmulas, já que é isso que functores entre categorias de tamanho de classe são - junto com unidades (definíveis!) e transformações de contagem que satisfazem as condições usuais.
Em 2), trata-se simplesmente de $C$ e $D$ como sendo pequeno quando considerado em $V_{\kappa_1}$e então afirma a existência do adjunto certo ali. Sem mais informações, isso realmente não parece dar o que queríamos em 1), como a priori$G$(e as transformações de unidade e contagem) estão todas no universo maior. Mas esta informação pode ser obtida lembrando que$G$ está realmente acessível (uma parte do teorema do functor adjunto que omiti de declarar acima, mas deve ser incluído) e, portanto, tudo é determinado em um conjunto.
Em 3), alguém gostaria de obter novamente o resultado de 1), mas pode tentar fazer isso como em 2) provando primeiro a existência de tais dados em $V_{\kappa_1}$ e, em seguida, comprovando a acessibilidade, garantindo que tudo está em $\mathrm{Def}(V_{\kappa_0})$.
Vejamos como isso se desenrola em alguns dos primeiros lugares no Capítulo 5, onde os universos são usados.
Definição 5.1.6.2: Let $C$ser uma categoria que admite todos os pequenos colimites. Um objeto$X\in C$é completamente compacto se o functor$j_X: C\to \widehat{\mathrm{Set}}$ copresentado por $X$ preserva pequenos colimites.
Aqui $\widehat{\mathrm{Set}}$ é a (muito grande) categoria de conjuntos em $V_{\kappa_1}$. Vamos interpretar o que essa definição significa nos sistemas acima.
Aqui $C$é qualquer categoria (possivelmente do tamanho da classe). Observe que, especialmente em HTT, "localmente pequeno" não é uma hipótese padrão, então isso permite que mesmo morfismos entre dois objetos sejam conjuntos adequados. Por esta razão, o functor realmente tem que ir para$\widehat{\mathrm{Set}}$, e isso é algo sobre o qual não podemos falar neste cenário. Portanto, seria necessário reformular a condição para atender a essa objeção; isso não deve ser difícil, mas pode ser um pouco desagradável.
Acho que está implícito na definição que $C$ é qualquer categoria que se encontra em $V_{\kappa_1}$. Isso captura estritamente a configuração de 1) em que se$C$ é pequeno definível como vindo de 1), então qualquer pequeno diagrama colimit em $C$ é automaticamente pequeno definível.
Aqui, temos duas opções: ou a de 1) ou a de 2), e elas fornecem noções diferentes. Em caso de conflito, a perspectiva de 1) é a correta, então$C$é pequeno definível, e pede-se a comutação com colimits de pequenos diagramas definíveis. Mas, enquanto em 1) tivemos problemas para formular a condição, os universos em mãos em 3) significam que a condição agora pode ser formulada: podemos pedir que leve pequenos colimites definíveis em$C$ para colimites em $\widehat{\mathrm{Set}}$. Aqui$\widehat{\mathrm{Set}}$ são os conjuntos em $V_{\kappa_1}$.
Portanto, neste caso, o resultado é que é preciso ter um pouco de cuidado em 3) na interpretação, mas guiado por 1) pode-se dar a definição correta; e então o sistema realmente ajuda.
Proposição 5.2.6.2: Let $C$ e $D$ser categorias. Então as categorias$\mathrm{Fun}^L(C,D)$ de functores adjuntos à esquerda de $C$ para $D$, e $\mathrm{Fun}^R(D,C)$ de functores adjuntos direitos de $D$ para $C$ são (canonicamente) equivalentes um ao outro.
Nesta perspectiva, esta proposição só faz sentido quando $C$ e $D$ são pequenos, caso contrário $\mathrm{Fun}(C,D)$é muito grande. (Deve-se considerar tais categorias de functor quando$C$ e $D$são apresentáveis (ou acessíveis), mas apenas quando restringidos a functores acessíveis. Portanto, essa é uma discussão que apareceria mais tarde no Capítulo 5.) Então, a afirmação é clara o suficiente e a prova fornecida se aplica.
Nessa perspectiva, acho que é o mesmo que em 1), exceto que também se pode formular o mesmo resultado em um universo diferente.
Mesmo aqui.
Observe, no entanto, que tal como está, em 1) esta proposição não pode (ainda) ser aplicada no caso $C$ e $D$são apresentáveis. Em 2) e 3), os (pequenos-) apresentáveis são categorias grandes especiais, às quais o resultado se aplica. Observe, no entanto, que as categorias de functor e sua equivalência estão todas vivendo em um universo maior, e não obtemos nenhuma informação delas em qualquer$V_{\kappa_0+1}$ ou $\mathrm{Def}(V_{\kappa_0})$.
A próxima proposição considera a categoria pré-capa $\mathcal P(C)=\mathrm{Fun}(C^{\mathrm{op}},\mathrm{Set})$, e a prova é um argumento típico envolvendo a passagem para um universo maior para resolver questões de homotopia-coerência.
Proposição 5.2.6.3: Let $f: C\to C'$ seja um functor entre pequenas categorias e deixe $G: \mathcal P(C')\to \mathcal P(C)$ ser o functor induzido de categorias de pré-capa induzida por composição com $f$. Então$G$ é certo adjacente a $\mathcal P(f)$.
Aqui $\mathcal P(f)$ é definida para ser a única extensão preservadora de colimites pequena de $f$ (sob a incorporação de Yoneda).
Aqui, temos duas categorias de tamanho de classe e functores entre eles, todos definíveis (como devem ser). A proposição nos pediria para encontrar (definíveis!) Transformações de unidade e contagem, fazendo alguns diagramas comutarem. Isso não parece muito difícil. Mas em$\infty$-categorias, é notoriamente difícil definir functores manualmente, então não é assim que Lurie procede!
Aqui $\mathcal P(C)$ e $\mathcal P(C')$são grandes categorias especiais. Lurie, de fato, aplica a grande incorporação de Yoneda na prova. Portanto, isso está realmente produzindo os adjuntos de unidade e contagem apenas em algum universo maior. Conforme discutido acima, acho que essa prova não dá realmente o que queríamos em 1)!
Podemos argumentar como Lurie faz para produzir os dados em algum "universo" maior. (Edit: Na verdade, como Tim Campion aponta, é preciso fazer um desvio mínimo para justificar o que está escrito. Veja os comentários à sua resposta.)
Portanto, ao ler esta proposição, no sistema 2) ou 3), deve-se fazer um marcador mental de que, até agora, a declaração provada é mais fraca do que se poderia ingenuamente esperar. Mas isso é corrigido posteriormente, observando que tudo é determinado por uma pequena quantidade de dados.
Conclusão: embora no início eu achasse que haveria uma diferença substancial entre 2) e 3), na verdade acho que não há (quase) nenhuma. Uma diferença é que$\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$ é uma inclusão adequada, mas na prática a forma de garantir a contenção em $V_{\kappa_0+1}$ parece ser para provar definibilidade em $V_{\kappa_0}$ (por exemplo, provando que certos functores estão acessíveis).
OK, agora me diga por que isso não funciona! :-)
A resposta a esta pergunta depende fortemente do que você deseja exatamente da Teoria Topos Superior, porque expressar alta força lógica é um objetivo diferente de expressar uma estrutura lógica unificada de maneira apropriada para a geometria algébrica e a teoria dos números. Fundamentos sólidos unificados para a matemática categórica geral são um objetivo excelente e parecem ser o objetivo de muitos colaboradores aqui. Para esse objetivo, tudo o que é dito nos comentários e nas respostas a esta pergunta é relevante. Mas o trabalho adequado em geometria e teoria dos números não exige uma grande força lógica.
Embora o HTT esteja mais entrelaçado com os universos do que o SGA, nem o HTT nem o SGA fazem uso real do (muito forte) esquema de axioma de substituição. Assim, eles podem usar "universos" radicalmente mais fracos do que os de Grothendieck. Como um exemplo típico e pertinente, Grothendieck fez apenas um apelo ao esquema de axioma da substituição. Essa é sua prova crucial de que cada categoria AB5 com um conjunto gerador tem injetores suficientes. E esse uso de substituição acaba sendo eliminável. Funcionou, mas Grothendieck realmente não precisava disso para obter o resultado.
Para expandir o uso de substituição de Grothendieck: Reinhold Baer na década de 1940 usou indução transfinita (que requer o esquema de axioma de substituição) para provar que os módulos (em qualquer anel) têm injetores suficientes. Ele estava explorando conscientemente novas técnicas de prova e obteve um bom resultado. Tohoku de Grothendieck lançou essa prova em uma forma mostrando que cada categoria AB5 com um pequeno conjunto de geradores tem injetores suficientes - e alguns anos depois Grothendieck descobriu que este era exatamente o teorema de que ele precisava para cohomologia topos. Baer e Grothendieck tinham objetivos práticos, não vinculados a preocupações com as fundações, mas ambos queriam fazer as fundações certas também. E eles fizeram. Mas acontece que eles poderiam ter obtido esses mesmos teoremas, corretamente, sem substituição, por quase as mesmas provas, especificando conjuntos de funções grandes o suficiente para começar (usando conjunto de potência, mas não substituição). Existem resultados que realmente requerem o esquema de axioma de substituição. Mas esses resultados raramente ocorrem fora da pesquisa básica.
Muitas pessoas vindas de ângulos muito diferentes (alguns lógicos, alguns não gostando da lógica) desde a década de 1960 observaram que, no contexto da geometria algébrica e teoria dos números, a alta força lógica do axioma do universo de Grothendieck é um subproduto realmente não utilizado O desejo de Grothendieck por uma estrutura unificada para a cohomologia. Isso agora pode ser bastante preciso: todo o aparato de Grothendieck, incluindo não apenas a co-homologia functor derivada de toposes, mas a 2-categoria de toposes e categorias derivadas, pode ser formalizado quase exatamente da mesma maneira como foi formalizado por Grothendieck, mas em força lógica muito abaixo de Zermelo-Fraenkel ou mesmo da teoria dos conjuntos de Zermelo. O mesmo é verdade para HTT. Você pode obtê-lo sem universos inacessíveis ou reflexo, desde que não precise da vasta (e raramente usada) força de substituição. A prova não foi realmente fornecida para o HTT. Foi pelo uso que Grothendieck fez dos universos . Parece claro que o mesmo funcionará para HTT.
A força lógica necessária foi expressa de maneiras indiferentes: Teoria dos Tipos Simples (com aritmética), Aritmética de Ordem Finita, Teoria Elementar da Categoria de Conjuntos, Teoria dos Conjuntos do Quantificador Limitado de Zermelo. Resumindo, você postula um conjunto de números naturais e que cada conjunto tem um conjunto de potência, mas não pressupõe iteração ilimitada de conjuntos de potência. Uma teoria dos universos bastante ingênua pode ser considerada conservadora em relação a qualquer um deles (da mesma forma que a teoria dos conjuntos de Gõdel-Bernays é conservadora em relação a ZFC) e adequada a todo o aparato de grande estrutura da escola de Grothendieck.
Eu consideraria uma extensão conservadora de ZFC obtida a partir de ZFC pela adição de uma constante $\alpha$ e os seguintes axiomas:
$\alpha$ é um ordinal ($Ord(\alpha)$)
A sentença $\phi\leftrightarrow\phi^{V_\alpha}$, para cada frase no idioma original $\phi$ (esquema de axioma).
$V_{\alpha}$ se comporta como $V$(para todas as sentenças na linguagem da teoria dos conjuntos). Se dois (ou mais) universos são necessários, pode-se adicionar outra constante$\beta$ com os axiomas correspondentes, e o axioma $\alpha<\beta$.
A prova de que a teoria resultante é conservadora em relação ao ZFC é fácil.
Assuma isso $\phi$ é demonstrável a partir dos novos axiomas (axiomas usando $\alpha$), no qual $\phi$está no idioma original. Uma vez que qualquer prova é finita, existem infinitas sentenças$\phi_1$, ..., $\phi_n$ de tal modo que
$Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}})\rightarrow \phi$
é demonstrável sem quaisquer novos axiomas. Portanto, pode-se pensar em$\alpha$como uma variável livre e a sentença acima é demonstrável em ZFC (teorema sobre constantes). Desde a$\alpha$ não ocorre em $\phi$, a seguinte implicação pode ser provada em ZFC ($\exists$-introdução):
$\exists\alpha(Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}}))\rightarrow \phi$
Agora, o princípio de reflexão para ZFC diz que o antecedente é um teorema de ZFC. Do modus ponens, ZFC prova$\phi$.
Então você pode trabalhar com os novos axiomas e $V_{\alpha}$ se comporta como um universo, e tudo o que é provado que não menciona $\alpha$ já pode ser comprovado no ZFC.
Uma pergunta que surgiu nos comentários foi sobre a motivação para fazer a pergunta. Deixe-me tentar resolver isso aqui.
Acima de tudo, trata-se de aprender! Como mencionei na pergunta original, eu mesmo brinquei com alguns limites cardeais "estúpidos" e só mais tarde aprendi sobre o princípio de reflexão, então eu queria entender o que ele pode fazer (e o que não pode), e se eu pode de alguma forma relegar automaticamente quaisquer outras versões complicadas de tais estimativas para esta máquina. Portanto, é comum você estar apenas tropeçando em uma sala escura e gostaria muito que a sala fosse iluminada! Portanto, obrigado a todos pelas respostas esclarecedoras!
Outra razão é que recentemente fiquei um pouco frustrado com a solução dos universos de Grothendieck para o problema em questão. Deixe-me explicar.
Eu quero muito falar sobre a categoria de todos os conjuntos, ou todos os grupos, etc., e quero provar teoremas sobre isso. E, pelo menos na versão de von Neumann-Bernays-Gödel (NBG) da teoria ZFC que permite aulas, esta é uma noção perfeitamente válida. Portanto, acho ontologicamente muito agradável trabalhar neste cenário, e gostaria muito que o teorema do functor adjunto fosse um teorema sobre categorias (apresentáveis) nesse sentido.
Agora, as categorias apresentáveis são determinadas por uma pequena quantidade de dados, portanto, sempre se pode trabalhar com essa pequena quantidade de dados e manter um controle cuidadoso dos tamanhos relativos. Na verdade, muitas provas em HTT explicitamente controlam tais tamanhos relativos, mas ainda existem alguns pontos onde é bom primeiro ter uma "visão mais ampla" e olhar para essas categorias grandes como se fossem pequenas.
Na verdade, o teorema do functor adjunto é sobre functores entre grandes categorias, e rapidamente se torna desagradável falar sobre isso de dentro do NBG / ZFC. Observe que o enunciado do teorema do functor adjunto faz sentido - ele apenas pede que todos os dados da adjunção sejam definíveis. Mas é um pouco desagradável tentar falar dessas coisas "de dentro". Portanto, seria definitivamente bom ter algum tipo de metateoria usando a qual argumentar sobre essas grandes categorias e fingir que são pequenas. A sutil questão da "definibilidade de dentro" pode ser a priori perdida nesta metateoria, mas considero essa questão da "definibilidade de dentro" como central, porque afinal o que eu queria era um teorema sobre todos os conjuntos, então eu ' estou bem em ter que prestar um pouco de atenção a isso - e, para acabar com a piada, verifica-se que essa é precisamente a diferença entre trabalhar com universos de Grothendieck e trabalhar com os "universos" de Feferman.
Portanto, é para isso que os universos de Grothendieck existem: eles sempre dão a você um universo maior para qualquer universo em que você esteja trabalhando no momento. Acho a existência dos universos de Grothendieck completamente intuitiva e, de fato, postular sua existência parece completamente equivalente a postular conjunto infinito em primeiro lugar: Você está apenas permitindo reunir tudo o que já possui em uma entidade maior por si só.
Mas agora, de repente, o que eu costumava pensar como todos os conjuntos são chamados de conjuntos pequenos , e também existem muitos conjuntos maiores. Portanto, mesmo que eu prove um teorema do functor adjunto nesta configuração, não é mais um teorema sobre functores entre categorias de todos os conjuntos / grupos / ..., mas apenas um dos functores entre pequenos conjuntos / grupos / .... Então, se você pense nisso, mesmo em universos ZFC + Grothendieck, você nunca provará aquele teorema que você realmente queria, sobre a categoria de todos os conjuntos. (Na verdade, até muito recentemente, eu assumi que o teorema do functor adjunto (para$\infty$-categories) é uma declaração de ZFC que foi provada sob "ZFC + Universes", mas não está totalmente correta: a declaração que foi provada só pode ser formulada em ZFC + Universes.)
O que foi provado é que é consistente que o teorema do functor adjunto seja válido. Ou seja, assumindo a consistência de universos ZFC +, você agora produziu um modelo de ZFC - aquele de pequenos conjuntos em seu modelo de universos ZFC + - no qual o teorema é verdadeiro. Então você pode agora trabalhar na teoria "ZFC + teorema do functor adjunto", em que o teorema do functor adjunto pode ser aplicado à categoria de todos os conjuntos / grupos / ..., mas isso definitivamente parece uma trapaça para mim. Você nem mesmo provou que "ZFC + Universos + o teorema do functor adjunto" é consistente! (Você obteria isso se começar com a consistência de um pouco mais do que ZFC + Universos, pedindo$\kappa$ de tal modo que $V_\kappa$satisfaz ZFC + Universes. Novamente, isso parece uma suposição completamente justa para mim - apenas continue.) Mas agora você pode começar a ver o perigo de inadvertidamente subir a escada de consistência conforme implicitamente começa a invocar mais e mais teoremas provados para pequenos conjuntos também para todos os conjuntos.
Seria muito melhor se você soubesse que, em universos ZFC + Grothendieck, tudo o que você provou sobre conjuntos pequenos também é um teorema sobre toda a categoria de ambiente de todos os conjuntos. Isso não é automático, mas você pode adicioná-lo como um esquema de axioma. Mike Shulman na seção 12 da teoria dos conjuntos para a teoria das categorias (arXiv: 0810.1279) discute essa ideia (que ele denota ZMC): Eu acho ontologicamente bastante agradável, também parece ter uma axiomatização muito simples (ainda mais simples do que ZFC!), mas
a) este esquema axioma adicional não é completamente autoevidente para mim: por que tudo o que é verdade em pequenos conjuntos também deve valer para todos os conjuntos? (Especialmente se tivemos alguns problemas para provar o resultado desejado em primeiro lugar. Além disso, observe que isso definitivamente não se aplica a qualquer noção de pequenos conjuntos: Em vez disso, o esquema axioma garante que existe alguma noção de pequenos conjuntos para os quais este tipo de reflexão se mantém. Agora, isso parece um pouco duvidoso para mim, pois em primeiro lugar eu nunca quis conjuntos pequenos, então agora estou os postulando, e também peço que eles ainda reflitam todo o comportamento de todos os conjuntos. Provavelmente bem, mas não evidente para mim.)
b) a força de consistência desse esquema axiomático é consideravelmente maior: é a mesma que a consistência de um cardeal Mahlo. Isso ainda é baixo para os grandes cardeais, mas é muito mais alto do que meros universos de Grothendieck (que estão realmente na parte inferior da hierarquia).
Com relação a a), o fato de podermos provar a consistência do teorema do functor adjunto a partir da consistência dos universos de Grothendieck aponta na direção certa, mas isso por si só não garante que os dois juntos sejam consistentes. Posso imaginar que poderia me convencer de que o esquema do axioma é razoável, mas certamente acho que ele precisa de muito mais justificativa do que meros universos de Grothendieck. (Pergunta lateral: Qual o tamanho dos grandes cardeais que se pode justificar usando a ideia de "permitir reunir tudo o que já tínhamos"? Não tenho certeza se esta é uma pergunta completamente bem definida ... mas para mim, uma cardinal mensurável definitivamente não é desse tipo (mas fico feliz em ser corrigido), pois parece postular o surgimento de novos recursos combinatórios.)
Outra razão pela qual recentemente fiquei um pouco infeliz com os universos de Grothendieck é que, embora em certo sentido gostaríamos de usá-los para poder ignorar as sutilezas da teoria dos conjuntos, de certa forma eles voltam para mordê-lo, como agora você tem que especificar em qual universo certas coisas vivem. Às vezes, você pode até ter que especificar vários universos diferentes para diferentes tipos de objetos (pense em feixes em conjuntos profinitos), e eu descobri que rapidamente fica bastante feio. Eu preferiria que todos os objetos vivessem juntos em um universo.
Então, enquanto pensava em feixes em conjuntos profinitos, cheguei a encontrar a solução com apenas um universo muito mais estética e ontologicamente agradável, e esta solução (conjuntos condensados) pode ser formalizada em ZFC sem problemas.
OK, então eu afirmo que os universos de Grothendieck não resolveram realmente o problema que se propuseram resolver, como
a) eles ainda não permitem que você prove teoremas sobre a categoria de todos os conjuntos / grupos / ... (exceto como um resultado de consistência, ou sob grandes axiomas cardinais mais fortes)
b) trabalhando com eles, você ainda precisa se preocupar com questões de tamanho - sua categoria de todos os conjuntos agora vem estratificada em conjuntos de todos os tipos de tamanhos diferentes (ou seja, em universos diferentes).
Além disso, eles também aumentam a força de consistência.
Agora, depois dessa discussão maravilhosa aqui, acho que a proposta de Feferman é na verdade muito melhor. No entanto, como também comentou Mike Shulman, considero os axiomas de Feferman não como descrevendo qualquer mundo ontologicamente correto, mas considero os "universos" da teoria de Feferman meramente como conveniências, a fim de falar sobre grandes categorias como se fossem pequenas. Em outras palavras, a teoria de Feferman fornece exatamente uma metateoria na qual argumentar sobre essas grandes categorias de "fora". Mas é uma teoria que eu usaria apenas para dar uma prova de um teorema de ZFC. Comparando com os universos de Grothendieck, a teoria de Feferman
a) permite que você prove teoremas sobre a categoria de todos os conjuntos / grupos / ..., porque inclui explicitamente um esquema de axioma de que todos os teoremas sobre pequenos conjuntos também são teoremas sobre todos os conjuntos.
b) Claro, dentro de uma prova de um teorema de ZFC que invoca algumas questões de tamanho não triviais, é muito bem-vindo que a teoria permite que você fale sobre vários tamanhos. Além disso, ele faz isso de uma maneira em que você ainda pode aplicar todos os axiomas de ZFC a cada um dos "universos" e também está tomando cuidado "nos bastidores" de como reescrever tudo em termos de limites cardinais (potencialmente extremamente sutis) no próprio ZFC. Portanto, é como uma linguagem de programação de alto nível para argumentos que envolvem estimativas cardinais difíceis no ZFC.
Além disso, não aumenta a força de consistência e, de fato, quaisquer declarações de ZFC provadas nesta linguagem são teoremas de ZFC. (Como recordei acima, também poderíamos ter a) + b) com universos de Grothendieck, mas então atingiríamos a consistência de um cardeal Mahlo.)
Portanto, o resultado é que acho que os universos de Feferman fazem um trabalho muito melhor em resolver o problema de fornecer uma metateoria para "falar sobre grandes categorias como se fossem pequenas" do que os universos de Grothendieck.
Deixe-me acrescentar algumas razões finais para fazer a pergunta. Acho que as técnicas de categorias mais altas, como as apresentadas no HTT, são de importância muito central, não apenas na topologia algébrica onde se originaram, mas em toda a matemática. Posso certamente atestar isso no que diz respeito à teoria dos números e à geometria algébrica. Portanto, sua centralidade também é um motivo importante para analisar sua força de consistência.
Ler o HTT é um assunto nada trivial - é longo e complicado. Alguns colegas da teoria dos números, entretanto, disseram que uma das principais razões pelas quais eles não puderam ler o HTT é que ele usa universos . Ou seja, eles estão tão acostumados a ZFC (e a verificar com extremo cuidado!) Que tentarão automaticamente eliminar qualquer uso de universos em um argumento. Agora, na SGA, pelo menos se você estivesse interessado apenas em aplicativos para etale cohomology de esquemas razoáveis, isso era algo que você poderia manualmente - por exemplo, apenas adicionar algumas suposições de contagem para tornar as coisas pequenas. No entanto, em HTT, não vejo nenhuma maneira de alguém ser capaz de colocar limites cardinais enquanto você lê - os argumentos são muito complexos para isso.
Então, agora eu espero poder dizer a eles que eles podem verificar se tudo funciona no ZFC, e eles ainda podem ler HTT (essencialmente) como escrito, se lerem na teoria dos conjuntos de Feferman. Se eles verificarem cuidadosamente (o que farão), eles ainda podem precisar preencher um pequeno lema aqui e algum pequeno argumento extra ali - mas eles teriam que fazer isso de qualquer maneira, em qualquer livro de ~ 1000 páginas, e eu posso imaginar que menos da metade dessas observações laterais tem a ver com a substituição dos universos de Grothendieck pelos "universos" de Feferman. Se alguém realmente empreender esse projeto, é claro que merece todo o crédito se tiver sucesso neste importante trabalho!
Permitam-me terminar com uma nota muito breve sobre o que parece ser o ponto chave saliente na tradução da teoria de Feferman. Aprendi a apreciar o ponto que Tim Campion levantou em sua resposta, e agora vejo que isso também foi mencionado na segunda resposta de Jacob Lurie. Grosso modo, é o seguinte. Se$C$ é uma categoria apresentável, então há uma pequena categoria $C_0$ de tal modo que $C=\mathrm{Ind}_\kappa(C_0)$
para algum cardeal regular $\kappa$, adjacente livremente a todos os pequenos $\kappa$-colimites filtrados. Isto faz$C$ naturalmente uma união de $C_\tau$de onde $C_\tau$ apenas coleta o $\tau$-pequeno $\kappa$-colimites filtrados. Aqui$\tau$ é um cardeal regular que $\tau\gg \kappa$. Esta estrutura crescente de$C$ como uma união de $C_\tau$é central na teoria das categorias apresentáveis, mas os níveis são realmente enumerados por (certos) cardeais regulares $\tau$. Se você aumentar seu universo, você também obterá uma versão maior$C'$ de $C$ em si, e nos universos de Grothendieck $C$ agora é uma das boas camadas $C'_\tau$ de $C$, Onde $\tau$é o cardeal de corte do universo anterior. Mas nos universos de Feferman, este$\tau$não é regular. Isso pode tornar alguns argumentos mais sutis, mas espero que geralmente se possa resolver esse problema simplesmente incorporando$C$ em alguns $C'_\tau$ com $\tau$ algum cardeal regular maior do que o cardeal de corte do universo menor.
Em resposta à edição que fixa as coisas em um sistema formal envolvendo cardeais $\kappa_{-1} < \kappa_0 < \kappa_{1/2} < \kappa_1$:
Vou sair por um lado talvez mais imprudente e predizer que, para encaixar os capítulos 1-4 nesse sistema formal, nenhuma aritmética cardinal real será necessária. Em vez disso, para esta parte do livro, tudo o que você terá que fazer é seguir e adicionar várias hipóteses de declarações de teoremas da forma "$X$ é $\kappa_{-1}$-pequeno ". Afinal, esta parte do livro realmente trata apenas de objetos pequenos, com exceção de alguns objetos grandes em particular , como a categoria de pequenos conjuntos simpliciais, a categoria de pequenas categorias simpliciais, etc., e coisas como Várias estruturas de modelo são construídas, mas acredito que em cada caso pode-se usar o caso especial do argumento do objeto pequeno para gerar cofibrações / cofibrações acíclicas entre objetos finitamente apresentáveis, de modo que nenhuma indução transfinita seja necessária. Diante disso, endireitar / descomplicar tem a aparência de construções que podem estar usando a teoria dos conjuntos de maneira séria, mas irei em frente e prevejo que elas não apresentam problemas para o sistema formal proposto.
O Capítulo 5 se torna mais irritante. Eu acredito que será necessário fazer algumas escolhas cuidadosas sobre os principais teoremas do apresentável ($\infty$) -categorias. O que torna as categorias apresentáveis marcadas é que elas empacotam o teorema do functor adjunto de forma muito clara, mas, como você diz, o teorema do functor adjunto comum vem com advertências nessa configuração. Eu poderia ir mais longe e dizer que todo o ponto de pensar sobre categorias apresentáveis em primeiro lugar está completamente desfeito neste cenário. Você não será capaz de provar coisas básicas como "categorias apresentáveis são precisamente as localizações acessíveis de categorias pré-capa". Prevejo que, quaisquer que sejam as escolhas feitas sobre a formulação de versões fracas dos teoremas centrais das categorias apresentáveis neste cenário, haverá alguma aplicação ou aplicação potencial que será prejudicada.
Os capítulos 5 e 6 também contêm alguns teoremas sobre categorias particulares muito grandes, como o $\infty$-categoria de apresentável $\infty$-categorias e o $\infty$-categoria de $\infty$-topoi [1]. O sistema parece ser tal que isso não será realmente um problema em si , exceto que os problemas encontrados na teoria básica da apresentabilidade agora serão combinados. Você não será capaz de provar isso$Pr^L$ é dual para $Pr^R$. Você não será capaz de provar o teorema de Giraud (bem, as definições estarão em fluxo de qualquer maneira, então eu devo esclarecer: você não será capaz de provar que localizações exatas e acessíveis de categorias pré-capa são as mesmas que localmente pequenas categorias que satisfaçam uma lista de condições de completude, geração e exatidão). Portanto, qualquer teorema sobre$\infty$-topoi cuja prova prossegue começando com o caso pré-capa e então localizando terá que ser completamente repensada.
Talvez eu esteja errado aqui, mas acredito que um trabalho extra significativo e ideias matemáticas genuinamente novas seriam necessárias para os Capítulos 5 e 6, e o resultado seria uma teoria substancialmente mais difícil de usar.
Por outro lado, acho que se você estiver disposto a restringir a atenção a grandes categorias que podem ser definidas a partir de pequenos parâmetros, embora você esteja perdendo a bela capacidade de dizer "provamos isso para categorias pequenas, mas agora podemos aplicá-lo a grandes ", você vai acabar com uma teoria de apresentabilidade muito mais utilizável, sem sair do ZFC.
[1] Na verdade, em fundações usuais essas categorias são (até a equivalência) apenas grandes e não muito grandes (mais precisamente, elas são $\kappa_0$-muitos objetos e $\kappa_0$-sized homs), mas um pouco de trabalho é necessário para mostrar isso. Esse ainda será o caso neste sistema formal? Não tenho certeza.
EDIT: Um longo comentário em resposta a de Peter Scholze resposta .
Uma coisa que acabei de perceber é que se$\kappa_0$ não é um $\beth$-ponto fixo, então nem todo conjunto em $V_{\kappa_0}$ tem cardinalidade $<\kappa_0$, para que as noções de "pequenez" sejam multiplicadas. Felizmente, acho que seu sistema formal prova que$V_{\kappa_0}$ tem $\Sigma_1$- substituição, o que implica que é um $\beth$-ponto fixo. Crise evitada!
Talvez esta abordagem de usar sistematicamente hipóteses de definibilidade dentro de um "cenário de universo" seja viável - combinando o "melhor dos dois mundos". Uma coisa boa é que, embora você esteja usando explicitamente hipóteses metamatemáticas, parece que ainda será capaz de declarar e provar esses teoremas como teoremas únicos, em vez de esquemas.
Estou um pouco confuso sobre a Proposição 5.2.6.3 (a última que você discute, e uma versão baby do teorema do functor adjunto). Presumo que a categoria pré-capa$P(C)$ será definido para incluir esses functores $C^{op} \to Spaces$ que mentem em $Def(V_{\kappa_0})$. Quando passamos para um universo maior, a transição geralmente é bastante uniforme, porque esperamos$P(C)$ ter todos os colimites indexados por $\kappa_0$- pequenas categorias - uma propriedade perfeitamente natural para trabalhar $V_{\kappa_1}$. Na verdade, a primeira etapa da prova de Lurie de 5.2.6.3 é mostrar que existe um adjunto esquerdo usando o fato de que$P(C)$tem todos os pequenos colimites [2]. No entanto, no cenário atual, nunca podemos assumir que$\kappa_0$ é regular e, portanto, nunca podemos assumir que $P(C)$tem todos os pequenos colimites. O melhor que podemos dizer é que$V_{\kappa_0}$ pensa $P(C)$tem todos os pequenos colimites. Enquanto estivermos trabalhando em$V_{\kappa_0}$, essa propriedade é "tão boa" quanto ter todos os colimites pequenos. Mas quando avançamos para$V_{\kappa_1}$, de repente temos que pensar nisso pelo que é - uma propriedade metamatemática. Talvez mais tarde eu me sente e tente ver se a prova de Lurie do 5.2.6.3 pode funcionar neste cenário, mas acho que à primeira vista não está claro.
[2] Somente depois de verificar a existência abstratamente dessa forma, ele mostra que o adjunto esquerdo deve ser o functor indicado. Claro, esta manobra é na verdade uma complicação adicional que vem com o$\infty$- configuração categórica - em categorias comuns, as fórmulas para os dois functores podem ser verificadas diretamente como adjuntas, mas em $\infty$-categorias a fórmula para o adjunto esquerdo não é obviamente funcional.