Estudo de caso: o que é necessário para formular e provar o argumento do objeto pequeno de Quillen no ZFC?
Estou ficando um pouco perdido com a questão interessante de Peter Scholze sobre como remover a dependência de universos dos teoremas na teoria das categorias. Em particular, estou sendo forçado a admitir que realmente não sei quando a substituição está sendo invocada, muito menos quando é invocada "de uma maneira essencial". Portanto, gostaria de trabalhar com um exemplo razoavelmente concreto do fenômeno. Eu entendo que a substituição deve "realmente" ser pensada como o axioma que permite a recursão transfinita. Minha sensação é que a teoria das categorias tende a não usar a recursão de uma forma pesada (embora, mais do que outros ramos da matemática, ela tenha muitas definições que, pelo menos prima facie, têm complexidade de Levy não trivial. Por exemplo, eu acho que o Fórmula$\phi(x,y,z,p,q)$ dizendo que o conjunto $z$ e funções $p: z \to x$ e $q: z \to y$ são um produto categórico dos conjuntos $x,y$ é sintaticamente $\Pi_1$, e a declaração de que produtos binários existem na categoria de conjuntos é sintaticamente $\Pi_3$ (ignorando quantificadores limitados, é claro)).
O seguinte teorema é, eu acho, uma das notáveis exceções à categoria teórica-não-uso-de-recursão:
Teorema [Quillen] "O argumento do objeto pequeno": Let$\mathcal C$ seja uma categoria apresentável localmente, e deixe $I \subseteq Mor \mathcal C$ser um pequeno conjunto de morfismos. Deixar$\mathcal L \subseteq Mor \mathcal C$ ser a classe de retraídos de compostos transfinitos de cobase-mudanças de coprodutos de morfismos em $I$, e deixar $\mathcal R \subseteq Mor \mathcal C$ compreendem aqueles morfismos fracamente ortogonais à direita aos morfismos de $I$. Então$(\mathcal L, \mathcal R)$é um sistema de fatoração fraco em$\mathcal C$.
Para obter a prova, consulte o nlab . Basicamente, as fatorações são construídas por recursão transfinita. A recursão parece "essencial" para mim porque novos dados são introduzidos em cada estágio da construção.
Formalização:
Eu acho que este teorema e sua prova são diretamente formalizáveis em MK, onde a distinção "pequeno / grande" da teoria da categoria é interpretada como a distinção "conjunto / classe" de MK. Não me sinto qualificado para comentar se a prova funciona em NBG, mas a afirmação pelo menos faz sentido diretamente.
Quando se trata de formalizar em ZFC, temos escolhas a fazer em relação à distinção entre pequeno e grande porte:
Uma opção é introduzir um "universo" $V_\kappa$(que, se estivermos realmente tentando trabalhar no ZFC, será um tipo de universo mais fraco do que o normal). Iremos interpretar "pequeno" como significando "em$V_\kappa$". Não vamos considerar" objetos verdadeiramente grandes "- tudo sobre o que falarmos será um conjunto - em particular, cada categoria sobre a qual falamos terá o tamanho de um conjunto, mesmo que não seja" pequeno "por si só. interpretar "categoria apresentável localmente" como significando "$\kappa$-cocomplete, localmente $\kappa$-pequena categoria com um forte $\kappa$-pequeno, $\lambda$- gerador apresentável para algum $\lambda < \kappa$"(Não sei se faz diferença dizer isso $V_\kappa$ pensa $\lambda$ é um cardeal regular).
Outra opção é não introduzir nenhum universo e apenas interpretar "pequeno" como "tamanho definido". Nesse caso, qualquer objeto "grande" sobre o qual falamos deve ser definível a partir de pequenos parâmetros. Portanto, definimos uma categoria para incluir uma classe de objetos definíveis por parâmetros, uma classe de morfismos definíveis por parâmetros, etc. Isso pode parecer restritivo, mas funcionará bem no caso apresentável localmente, uma vez que podemos definir uma categoria apresentável localmente$\mathcal C$ a ser definido, em relação aos parâmetros $(\lambda, \mathcal C_\lambda)$ (Onde $\lambda$ é um cardeal regular e $\mathcal C_\lambda$ é um pequeno $\lambda$-cocomplete categoria), como a categoria de $\lambda$-Ind objetos em $\mathcal C_\lambda$.
Agora, para o teorema em questão, a abordagem (2) parece mais limpa porque a "tradução" necessária é direta e, uma vez feita, a prova original deve funcionar sem modificação. Acho que as principais desvantagens de (2) vêm em outro lugar. Por exemplo, provavelmente será uma questão delicada formular teoremas sobre a categoria de categorias localmente apresentáveis. Em geral, haverá vários teoremas sobre categorias que têm formulações e provas conceituais claras quando as categorias envolvidas são pequenas, mas que requerem modificações técnicas irritantes quando as categorias envolvidas são grandes. É por essas razões que abordagens mais como (1) tendem a ser favorecidas para projetos teóricos de categorias em grande escala.
Então, vamos supor que estamos seguindo a abordagem (1). A questão então se torna:
Questão 1: Exatamente que tipo de universo precisamos para formular e provar o teorema acima seguindo a abordagem (1)?
Pergunta 2: Quantos universos têm a garantia de existência do ZFC?
Presumivelmente, a resposta à pergunta 2 será que existem muitos desses universos - o suficiente para que possamos fazer coisas como, dada uma categoria, passar para um universo grande o suficiente para torná-la pequena e invocar o teorema para esse universo .
Pergunta 3: Até que ponto no meio do mato devemos ir para responder às perguntas 1 e 2?
Precisamos analisar a prova do Teorema de maneira profunda? Existe uma rubrica fácil de critérios que nos permite dar uma olhada na prova e, para 99% dos teoremas como este, dizer facilmente que ela "passa" sem nos aprofundar muito nas coisas? Ou existe algum metateorema formal ao qual possamos recorrer, de modo que até mesmo um computador possa verificar se as coisas estão bem?
Respostas
O comentário de Jacob Lurie dá uma resposta à questão 1. Ou seja, assumindo que as estimativas que dei em meu comentário estão corretas, a fim de formular e provar o teorema, será suficiente supor que
- $\kappa$ é regular
e essa
- para cada $\mu < \kappa$, existe $\rho < \kappa$ de tal modo que $\mu \ll \rho$ (significa que $\mu' < \mu, \rho' < \rho \Rightarrow (\rho')^{\mu'} < \rho$)
Talvez esta propriedade de $\kappa$pode ser visto como uma "forma" de substituição. Mas, realmente, o que temos são duas condições$\kappa$ que são puramente teóricas de conjuntos, em vez de metamatemáticas, de modo que a resposta à Questão 1 é algo muito mais claro do que eu supunha.
Isso nos permite abordar a questão 2. Presumivelmente, o resultado é que o ZFC prova que há muitos e muitos $\kappa$ satisfazendo as duas condições acima.
Quando se trata da pergunta 3, parece que, nesta abordagem, precisamos de fato nos aprofundar na prova. Na verdade, parece que, para realizar essa abordagem, devemos adicionar algum conteúdo matemático genuíno à prova e, de fato, provar uma afirmação mais forte. As outras questões tornam-se então
Em geral, será possível "construtivar" "a maioria" dos teoremas da teoria das categorias dessa maneira, ou outras questões aparecerão no curso do projeto "teoria das categorias ZFC-ify"?
Se a resposta para (1) for "sim" (ou se geralmente for "não" e restringirmos nossa atenção aos casos em que é "sim"), então "quanto trabalho extra" esse projeto realmente representaria?
Meu palpite é que a resposta para (1) é que, quando se trata do uso de recursão transfinita na teoria das categorias, normalmente acontece que o uso de substituição pode ser eliminado de maneira semelhante a esta, mas que mais importante, eu perdi o ponto: como Jacob Lurie argumenta em resposta à pergunta de Peter Scholze, os problemas mais espinhosos com a teoria das categorias de ZFC não têm a ver com recursão transfinita, mas sim com ser capaz de ir e voltar livremente entre "grandes categorias "e" pequenas categorias "de várias maneiras.
Meu palpite é que a resposta para (2) é que para a "maioria" dos usos da recursão transfinita na teoria das categorias, deveria ser bastante simples "construtivá-los" para que se encaixassem em um "universo infantil" com as propriedades acima ou algo semelhante, e que com apenas um pouco de prática, pode-se desenvolver a capacidade de verificar quase à primeira vista se é possível, embora ainda com base em teorema por teorema. Mas eu adoraria ser provado que estou errado e mostrar um teorema na teoria das categorias em que esse tipo de abordagem falha!
Finalmente, isso deixa em aberto a questão de saber se existe uma maneira "mais automática" de fazer tudo isso - talvez com uma conclusão mais fraca do que "nosso universo não precisa satisfazer nenhuma forma de substituição".