Studium przypadku: co trzeba zrobić, aby sformułować i udowodnić argument małego obiektu Quillena w ZFC?
Trochę gubię się w interesującym pytaniu Petera Scholze o usunięcie zależności od wszechświatów z twierdzeń teorii kategorii. W szczególności jestem zmuszony przyznać, że tak naprawdę nie wiem, kiedy wywoływana jest zamiana, nieważne, kiedy jest ona wywoływana „w zasadniczy sposób”. Chciałbym więc przeanalizować dość konkretny przykład tego zjawiska. Rozumiem, że zastąpienie powinno być „naprawdę” traktowane jako aksjomat, który pozwala na rekurencję pozaskończoną. W moim odczuciu teoria kategorii ma tendencję do nieużywania rekurencji w trudny sposób (chociaż, bardziej niż inne gałęzie matematyki, ma wiele definicji, które przynajmniej prima facie mają nietrywialną złożoność Levy'ego. formuła$\phi(x,y,z,p,q)$ mówiąc, że zestaw $z$ i funkcje $p: z \to x$ i $q: z \to y$ są kategorycznym iloczynem zbiorów $x,y$ jest syntaktycznie $\Pi_1$, a stwierdzenie, że produkty binarne istnieją w kategorii zbiorów, jest składniowe $\Pi_3$ (oczywiście pomijając ograniczone kwantyfikatory)).
Uważam, że następujące twierdzenie jest jednym z godnych uwagi wyjątków od teorii kategorii-teoria rekurencji:
Twierdzenie [Quillen] "Argument małego obiektu": Niech$\mathcal C$ być lokalnie prezentowalną kategorią i niech $I \subseteq Mor \mathcal C$być małym zestawem morfizmów. Pozwolić$\mathcal L \subseteq Mor \mathcal C$ być klasą retrakcji pozaskończonych kompozytów połączonych zmian współproduktów morfizmów w $I$, i pozwól $\mathcal R \subseteq Mor \mathcal C$ zawierają te morfizmy słabo prawostronne do morfizmów $I$. Następnie$(\mathcal L, \mathcal R)$jest osłabiony system faktoryzacji na$\mathcal C$.
Aby uzyskać dowód, zobacz nlab . Zasadniczo faktoryzacje są konstruowane przez rekurencję pozaskończoną. Rekursja wydaje mi się „niezbędna”, ponieważ na każdym etapie konstrukcji wprowadzane są nowe dane.
Formalizowanie:
Myślę, że to twierdzenie i jego dowód są w prosty sposób sformalizowane w MK, gdzie teoretyczne rozróżnienie „małe / duże” według kategorii jest interpretowane jako rozróżnienie „zestaw / klasa” MK. Nie czuję się uprawniony do komentowania, czy dowód działa w NBG, ale stwierdzenie to przynajmniej ma bezpośredni sens.
Jeśli chodzi o formalizowanie w ZFC, mamy do wyboru wybór dotyczący rozróżnienia na małe / duże:
Jedną z opcji jest wprowadzenie „wszechświata” $V_\kappa$(co, jeśli faktycznie próbujemy pracować w ZFC, będzie słabszym rodzajem wszechświata niż zwykle). Będziemy interpretować „małe” jako „w”$V_\kappa$Nie będziemy rozważać „naprawdę dużych obiektów” - wszystko, o czym mówimy, będzie zbiorem - w szczególności każda kategoria, o której mówimy, będzie miała ustalony rozmiar, nawet jeśli nie będzie „mała” per se. interpretować „lokalnie prezentowalną kategorię” jako „$\kappa$-complete, lokalnie $\kappa$-mała kategoria z mocną $\kappa$-mały, $\lambda$-prezentowalny generator dla niektórych zwykłych plików $\lambda < \kappa$„(Nie wiem, czy powiedzenie tego ma znaczenie $V_\kappa$ myśli $\lambda$ jest zwykłym kardynałem).
Inną opcją jest nie wprowadzanie żadnego wszechświata i po prostu zinterpretowanie „małego” jako „rozmiaru zestawu”. W tym przypadku każdy „duży” obiekt, o którym mówimy, musi być definiowalny na podstawie małych parametrów. Więc definiujemy kategorię tak, aby zawierała klasę obiektów definiowaną przez parametr, klasę morfizmów definiowaną przez parametr itp. Może się to wydawać restrykcyjne, ale będzie działać dobrze w przypadku lokalnie prezentowalnym, ponieważ możemy zdefiniować lokalnie prezentowaną kategorię$\mathcal C$ do zdefiniowania w odniesieniu do parametrów $(\lambda, \mathcal C_\lambda)$ (gdzie $\lambda$ jest zwykłym kardynałem i $\mathcal C_\lambda$ jest małe $\lambda$-cocomplete category), jako kategoria $\lambda$-Ind przedmioty w $\mathcal C_\lambda$.
Teraz, dla rozważanego twierdzenia, podejście (2) wydaje się czystsze, ponieważ niezbędne „tłumaczenie” jest proste, a kiedy już zostanie wykonane, oryginalny dowód powinien działać bez modyfikacji. Myślę, że główne wady (2) pojawiają się gdzie indziej. Na przykład prawdopodobnie będzie delikatną sprawą sformułowanie twierdzeń o kategorii lokalnie prezentowalnych kategorii. Ogólnie rzecz biorąc, istnieją różne twierdzenia na temat kategorii, które mają czyste, konceptualne sformułowania i dowody, gdy kategorie są małe, ale które wymagają irytujących modyfikacji technicznych, gdy te kategorie są duże. Z takich powodów w projektach z teorią kategorii na dużą skalę preferowane są podejścia bardziej podobne do (1).
Załóżmy więc, że postępujemy zgodnie z podejściem (1). Pojawia się wtedy pytanie:
Pytanie 1: Dokładnie jakiego rodzaju wszechświata potrzebujemy, aby sformułować i udowodnić powyższe twierdzenie zgodnie z podejściem (1)?
Pytanie 2: Ile takich wszechświatów gwarantuje ZFC?
Przypuszczalnie odpowiedź na pytanie 2 będzie brzmiała, że istnieje wiele takich wszechświatów - wystarczająco dużo, abyśmy mogli zrobić takie rzeczy, jak dana kategoria, przejść do wszechświata wystarczająco dużego, aby uczynić tę kategorię małą i powołać się na twierdzenie dla tego wszechświata .
Pytanie 3: Jak daleko w chwasty musimy się posunąć, aby odpowiedzieć na pytania 1 i 2?
Czy musimy dogłębnie analizować dowód Twierdzenia? Czy istnieje prosta rubryka kryteriów, które pozwalają nam spojrzeć na dowód i w przypadku 99% takich twierdzeń z łatwością stwierdzić, że „przechodzi” bez zbytniego zagłębiania się w rzeczy? A może jest nawet jakieś formalne metateoremat, do którego możemy się odwołać, aby nawet komputer mógł sprawdzić, czy wszystko jest w porządku?
Odpowiedzi
Komentarz Jacoba Lurie daje odpowiedź na pytanie 1. Mianowicie, zakładając, że szacunki, które podałem w moim komentarzu są poprawne, aby sformułować i udowodnić twierdzenie, wystarczy założyć, że
- $\kappa$ jest regularne
i to
- dla każdego $\mu < \kappa$, tam istnieje $\rho < \kappa$ takie że $\mu \ll \rho$ (to znaczy $\mu' < \mu, \rho' < \rho \Rightarrow (\rho')^{\mu'} < \rho$).
Być może ta właściwość $\kappa$może być postrzegane jako „forma” zastąpienia. Ale tak naprawdę mamy tylko dwa warunki$\kappa$ które są czysto teoretyczne, a nie metamatematyczne, więc odpowiedź na pytanie 1 jest znacznie czystsza, niż przypuszczałem.
To pozwala nam odpowiedzieć na pytanie 2. Przypuszczalnie wynik jest taki, że ZFC udowadnia, że jest ich bardzo dużo $\kappa$ spełniające dwa powyższe warunki.
Jeśli chodzi o pytanie 3, wydaje się, że w tym podejściu w rzeczywistości musimy dość głęboko zagłębić się w dowód. W rzeczywistości wydaje się, że aby zastosować to podejście, musimy dodać do dowodu jakąś autentyczną treść matematyczną, a właściwie udowodnić mocniejsze stwierdzenie. Pojawiają się dalsze pytania
Czy generalnie będzie można w ten sposób „konstruktywizować” „większość” twierdzeń teorii kategorii, czy też inne kwestie pojawią się w trakcie projektu „Teoria kategorii ZFC-ify”?
Jeśli odpowiedź na (1) brzmi „tak” (lub jeśli generalnie jest „nie” i ograniczamy naszą uwagę do przypadków, w których jest „tak”), to „ile dodatkowej pracy” naprawdę byłby taki projekt?
Domyślam się, że odpowiedź na (1) jest taka, że jeśli chodzi o użycie rekurencji pozaskończonej w teorii kategorii, to rzeczywiście będzie zazwyczaj tak, że użycie zamiany można wyeliminować w podobny sposób, jak to, ale że więcej co ważne, przegapiłem sedno: jak argumentuje Jacob Lurie w odpowiedzi na pytanie Petera Scholze, bardziej drażliwe problemy z teorią kategorii opartą na ZFC nie mają związku z rekurencją pozaskończoną, ale raczej z możliwością swobodnego przechodzenia między „dużymi kategoriami” „i„ małe kategorie ”na różne sposoby.
Domyślam się, że odpowiedź na (2) jest taka, że dla "większości" teoretycznych zastosowań kategorii rekurencji pozaskończonej powinno być całkiem proste "konstruktywizować" je tak, aby pasowały do "wszechświata dziecka" o właściwościach powyżej lub coś podobnego, i że przy odrobinie praktyki można rozwinąć umiejętność sprawdzenia niemal na pierwszy rzut oka, że jest to możliwe, chociaż wciąż na podstawie twierdzeń po twierdzeniach. Chciałbym jednak udowodnić, że się mylę i pokazać twierdzenie w teorii kategorii, gdzie tego rodzaju podejście zawodzi!
Wreszcie, pozostaje kwestią otwartą, czy istnieje „bardziej automatyczny” sposób na zrobienie tego wszystkiego - być może ze słabszym wnioskiem niż „nasz wszechświat nie musi w ogóle spełniać żadnej formy zastąpienia”.