Zasada odbicia a wszechświaty
W dyskusjach z teorią kategorii często pojawia się pokusa spojrzenia na kategorię wszystkich grup abelowych lub wszystkich kategorii itp., Co szybko prowadzi do typowych problemów z teorią mnogości. Często unika się ich, używając wszechświatów Grothendiecka. W języku teorii mnogości naprawia się niektórych mocno niedostępnych kardynałów$\kappa$ -- to znaczy że $\kappa$ jest jakimś niezliczonym kardynałem, takim dla wszystkich $\lambda<\kappa$, również $2^\lambda<\kappa$i dla dowolnego zestawu $<\kappa$ wiele zestawów $S_i$ wielkościowy $<\kappa$, również ich związek jest wielkości $<\kappa$. Oznacza to, że scena$V_\kappa\subset V$ z "zestawów o rozmiarze $<\kappa$„sam w sobie jest modelem ZFC - stosując dowolne operacje na zestawach, takie jak przyjmowanie powersetów lub związków zawodowych, nigdy nie możesz wyjść $V_\kappa$. Zbiory te określa się wówczas jako „małe”, a wtedy kategoria małych grup abelowych jest zdecydowanie dobrze zdefiniowana.
Historycznie rzecz biorąc, podejście to po raz pierwszy zastosował Grothendieck; bardziej aktualny tekst założycielski dotyczy pracy Luriego$\infty$-kategorie. Jednak ich użycie zawsze wywoływało pewien sprzeciw, a niektórzy ludzie nie chcieli pozwolić, aby aksjomaty wykraczające poza ZFC wślizgnęły się do ustalonej literatury. Na przykład, myślę, że w pewnym momencie toczyła się długa dyskusja, czy Ostatnie twierdzenie Fermata zostało udowodnione w ZFC, teraz rozstrzygniętym przez McLarty'ego. Niedawno widziałem podobne argumenty dla twierdzeń, których dowody odnoszą się do pracy Luriego. (Osobiście nie mam co do tego silnych uczuć i tak czy inaczej rozumiem argumenty).
Z drugiej strony zawsze było tak, że bliższa analiza wykazała, że jakiekolwiek użycie wszechświatów było w rzeczywistości niepotrzebne. Na przykład projekt stosów nie korzysta ze wszechświatów. Zamiast tego (patrz Tag 000H mówi), skutecznie osłabia to hipotezę$\kappa$ jest silnie niedostępny, dla czegoś w rodzaju mocnego kardynała granicznego o niezliczonej kumulalności, czyli: dla wszystkich $\lambda<\kappa$, jeden ma $2^\lambda<\kappa$i zawsze, gdy masz policzalną kolekcję zestawów$S_i$ wielkościowy $<\kappa$, także związek $S_i$ ma rozmiar $<\kappa$. ZFC łatwo udowadnia istnienie takich$\kappa$, a prawie każdy argument, jaki można sobie wyobrazić w kategorii grup abelowych, działa również w kategorii $\kappa$-małe grupy abelowe dla takich $\kappa$. Jeśli argumentuje się bardziej skomplikowanymi argumentami, można odpowiednio wzmocnić początkową hipotezę$\kappa$. Sam miałem okazję zagrać w tę grę, zobacz sekcję 4 na stronie www.math.uni-bonn.de/people/scholze/EtCohDiamonds.pdf, aby uzyskać wynik. Z tego doświadczenia jestem pewien, że w podobny sposób można przepisać "Teorię wyższego toposu" Luriego, lub jakąkolwiek inną podobną pracę z teorią kategorii, tak aby usunąć wszystkich silnie niedostępnych kardynałów, zastępując ich starannie dobranymi$\kappa$ z właściwościami takimi jak te powyżej.
W rzeczywistości wydaje się, że istnieje twierdzenie ZFC, zasada odbicia (omówiona krótko w znaczniku 000F projektu Stacks), która wydaje się gwarantować, że jest to zawsze możliwe. Mianowicie, dla dowolnego skończonego zbioru formuł teorii mnogości istnieje wystarczająco duży$\kappa$ tak, że z grubsza rzecz biorąc, te formuły się utrzymują $V_\kappa$ wtedy i tylko wtedy, gdy się trzymają $V$. Wydaje się to oznaczać, że dla dowolnego skończonego zbioru formuł można je znaleźć$\kappa$ takie że $V_\kappa$zachowuje się jak wszechświat w odniesieniu do tych formuł, ale proszę, popraw mnie w moim bardzo naiwnym rozumieniu zasady odbicia! (Powiązany fakt jest taki, że ZFC udowadnia spójność dowolnego określonego skończonego fragmentu aksjomatów ZFC.)
Z drugiej strony, każdy podany tekst matematyczny zawiera skończenie wiele formuł (chyba że zawiera „schemat twierdzenia”, co, jak sądzę, zwykle się nie zdarza). Pytanie jest więc sformułowane nieco prowokacyjnie:
Czy zasada refleksji zakłada, że musi istnieć możliwość przepisania Teorii Wyższego Toposu w sposób, który unika używania wszechświatów?
Edycja (28.01.2021): Bardzo dziękuję za wszystkie bardzo pomocne odpowiedzi! Myślę, że mam teraz znacznie jaśniejszy obraz sytuacji, ale nadal nie jestem do końca pewien, jaka jest odpowiedź na to pytanie.
Z tego, co rozumiem, (z grubsza) najlepszym meta-twierdzeniem w tym kierunku jest następujące (wyspecjalizowane w HTT). Przypomnij sobie, że HTT naprawia dwóch mocno niedostępnych kardynałów$\kappa_0$ i $\kappa_1$, robiąc w ten sposób miejsce na małe (w $V_{\kappa_0}$), duży (w $V_{\kappa_1}$) i bardzo duże (w $V$) obiektów. Można więc spróbować odczytać HTT w następującym systemie aksjomatów (jest to zasadniczo jeden z artykułu Fefermana „Teoretyczne podstawy teorii kategorii”, który również został zaproponowany w odpowiedzi Rodrigo Freire'a poniżej).
(i) Zwykłe aksjomaty ZFC
(ii) Dwa inne symbole $\kappa_0$ i $\kappa_1$, z aksjomatami, że są kardynałami, że współmierność $\kappa_0$ jest niepoliczalna i że współmierność $\kappa_1$ jest większy niż $\kappa_0$.
(iii) Schemat aksjomatów, mówiący, że dla każdej formuły $\phi$ teorii mnogości, $\phi\leftrightarrow \phi^{V_{\kappa_0}}$ i $\phi\leftrightarrow \phi^{V_{\kappa_1}}$.
Następnie można zastosować zasadę refleksji, aby pokazać (patrz odpowiedź Rodrigo Freire poniżej, aby uzyskać szkic dowodu):
Twierdzenie. Ten system aksjomatów jest konserwatywny w stosunku do ZFC. Innymi słowy, każde twierdzenie w tym systemie formalnym, które się do niego nie odnosi$\kappa_0$ i $\kappa_1$ jest również twierdzeniem ZFC.
To jest dokładnie taki wniosek, jaki chciałbym mieć.
Zwróć na to uwagę $V_{\kappa_0}$ i $V_{\kappa_1}$ są modelami ZFC, ale (krytycznie!) nie można tego udowodnić w systemie formalnym, ponieważ ZFC nie jest ostatecznie aksjomatyzowalny, a tylko każdy indywidualny aksjomat ZFC jest postulowany przez (iii).
Jedną fajną rzeczą w tym systemie aksjomatów jest to, że wyraźnie dopuszcza okazjonalne argumenty w postaci „udowodniliśmy to twierdzenie dla małych kategorii, ale potem możemy je zastosować również do dużych kategorii”.
Bardziej precyzyjne pytanie brzmi zatem:
Czy argumenty HTT działają w tym formalnym systemie?
Mike Shulman w sekcji 11 dokumentu https://arxiv.org/abs/0810.1279daje bardzo jasny opis tego, jakie są potencjalne problemy. Mianowicie, jeśli masz zestaw$I\in V_{\kappa_0}$ i zestawy $S_i\in V_{\kappa_0}$ dla $i\in I$, nie możesz stwierdzić, że związek $S_i$ jest w $V_{\kappa_0}$. Ten wniosek jest gwarantowany tylko wtedy, gdy funkcja$i\mapsto S_i$ jest również zdefiniowany w $V_{\kappa_0}$ (albo jeśli $I$jest policzalny, przy dodatkowym założeniu niepoliczalnej współliniowości). W praktyce oznacza to, że gdy chce się stwierdzić, że coś jest „małe” (tj$V_{\kappa_0}$), orzeczenie to dotyczy nie tylko przedmiotów, ale także morfizmów itp. Nie jest teraz dla mnie jasne, jak dużym problemem jest to w rzeczywistości, musiałbym się nad tym bardziej zastanowić; Właściwie mógłbym sobie wyobrazić, że dość łatwo jest odczytać HTT, aby spełnić ten formalny system. Shulman mówi, że z tym zastrzeżeniem można udowodnić twierdzenie o funktorze sprzężonym, a jak mówi Lurie w swoich odpowiedziach, argumenty w HTT mają podobną złożoność teorii mnogości. Jednak nadal byłbym zainteresowany oceną, czy odpowiedź na pytanie brzmi „tak, jak napisano”, czy raczej „prawdopodobnie tak, ale trzeba w to trochę się postarać”, czy w rzeczywistości „nie bardzo”. (Mam szczerą nadzieję, że eksperci będą mogli zgodzić się mniej więcej co do tego, gdzie w tym spektrum mieści się odpowiedź.)
Ostatnia uwaga: powyżej założenie „niepoliczalności” można uznać za nieco arbitralne; dlaczego nie pozwolić na nieco większe związki? Jednym ze sposobów rozwiązania tego problemu jest dodanie symbolu$\kappa_{-1}$ z tymi samymi właściwościami i zamiast tego zapytaj, czy współmierność $\kappa_0$ jest większy niż $\kappa_{-1}$. Podobnie, ktoś mógłby chcieć zamienić oprawę$\mathrm{cf} \kappa_1>\kappa_0$ przez nieco mocniejsze wiązanie $\mathrm{cf} \kappa_1>2^{\kappa_0}$mówić. Znowu, jeśli to upraszcza sprawę, można by po prostu wcisnąć inny$\kappa_{1/2}$ pomiędzy, więc to $\mathrm{cf} \kappa_{1/2}>\kappa_0$ i $\mathrm{cf} \kappa_1>\kappa_{1/2}$. W ten sposób nie trzeba się martwić, czy którykolwiek ze „standardowych” obiektów, które pojawiają się w niektórych dowodach, pozostaje policzalnych rozmiarów, czy też nadal można przyjmować okrężnice w$V_{\kappa_1}$ gdy zestawy indeksów nie mają dokładnie rozmiaru ograniczonego przez $\kappa_0$ ale zostały trochę zmanipulowane.
PS: Dopiero teraz znajduję wszystkie odpowiednie poprzednie pytania i odpowiedzi MO. Niektóre bardzo istotne z nich to odpowiedzi Joela Hamkinsa tu i tutaj .
Odpowiedzi
Zamierzam wyjść na kończynę i zasugerować, że książka HTT nigdy nie używa niczego mocniejszego niż zamiennik $\Sigma_{15}$-formuły teorii mnogości. (Tutaj$15$ to losowo wybrana duża liczba, a HTT to losowo wybrana książka matematyczna, która nie dotyczy konkretnie teorii mnogości).
Zastanawiając się nad komentarzem Gabe'a na temat mojej pierwotnej odpowiedzi, myślę, że to, co napisałem, jest mylące, ponieważ łączy w sobie dwa oddzielne (ale powiązane) twierdzenia:
Istnienie silnie niedostępnych kardynałów nie jest tak naprawdę potrzebne w teorii kategorii.
Pełna siła ZFC nie jest tak naprawdę potrzebna w teorii kategorii.
Zgadzam się z obydwoma stwierdzeniami, ale uważam, że najlepszym sposobem na przekonanie kogoś o 1) nie byłoby połączenie 2) z zasadą refleksji: czyli nie należy próbować zastępować użycia mocno niedostępnego kardynała $\kappa$ o jeden, dla którego $V_{\kappa}$ modeluje dużą część ZFC.
Jak widzę, „problemem”, który rozwiązują wszechświaty, jest uzasadnienie połączenia dwóch typów rozumowania:
A) Czasami przydatne jest udowodnienie twierdzeń o małych kategoriach $\mathcal{C}$ poprzez osadzanie ich w „dużych” kategoriach (na przykład za pomocą osadzania Yoneda), które mają fajne dodatkowe cechy: na przykład istnienie ograniczeń i kolimitów.
B) Duże kategorie są również kategoriami, więc każde twierdzenie, które ma zastosowanie do kategorii w ogólności, powinno również odnosić się do dużych kategorii.
Jeśli martwiłeś się tylko o B), wtedy odpowiednia może być zasada refleksji. Wybór kardynała$\kappa$ takie że $V_{\kappa}$ spełnia dużą część ZFC, można przedefiniować „małą kategorię” na oznaczającą „należącą do niej kategorię” $V_{\kappa}$„i„ duża kategoria ”oznacza„ kategorię niekoniecznie należącą do $V_{\kappa}$”i możesz mieć pewność, że wszystkie podstawowe twierdzenia, których możesz chcieć, są słuszne w obu przypadkach.
Ale jeśli martwisz się również A), to niekoniecznie jest pomocne. Powiedzmy, że zaczynasz od kategorii$\mathcal{C}$ należeć do $V_{\kappa}$i chcesz mieć jakąś wersję osadzania Yoneda. Naturalnym przypuszczeniem byłoby osadzenie w kategorii funktorów z$\mathcal{C}^{\mathrm{op}}$ do kategorii zestawów rozmiarów $<\tau$ (lub jakiś równoważny model tego), dla jakiegoś kardynała $\tau$. Pierwsze przypuszczenie jest takie, że powinieneś wziąć$\tau = \kappa$, ale myślę, że to ma tylko sens $\kappa$jest mocno niedostępny (w przeciwnym razie niektóre zestawy Hom będą zbyt duże). W każdym razie gwarantując, że ta konstrukcja ma dobre właściwości, będziesz chciał żądać innych właściwości od kardynała$\tau$. Na przykład, jeśli chcesz, aby ta kategoria presheaveów miała wiele colimitów, będziesz tego chcieć$\tau$mieć dużą współfinalizm. A jeśli zaczniesz się zastanawiać, jakie rodzaje dodatkowych założeń możesz potrzebować, wrócisz do punktu początkowego: zastanawiasz się, jakiego rodzaju szacunki liczności gwarantują, że „wstępne zestawienia zbiorów rozmiarów$< \tau$„są dobrym przybliżeniem do kategorii wszystkich składów wstępnych zbiorów. Zatem zasada refleksji tak naprawdę nie pomaga uniknąć tych problemów.
(Edycja: po napisaniu zdałem sobie sprawę, że poniższy tekst w większości powtarza oryginalny post Petera. Zostawię go tutaj na wypadek, gdyby ktoś uznał go za przydatny.)
Jeśli chcesz rygorystycznej formalizacji w czymś takim jak ZFC, prawdopodobnie najlepszą rzeczą do zrobienia jest całkowite wyeliminowanie dużych kategorii. Zatem B) nie jest problemem. Aby zająć się A), pozwolę sobie zauważyć, że wiele „dużych” kategorii, o których chciałoby się mówić, powstaje w szczególny sposób: zaczynamy od małej kategorii$\mathcal{C}$ który ma już pewne rodzaje kolimitów i formalnie się powiększa $\mathcal{C}$ aby stworzyć większą kategorię $\mathcal{C}^{+}$który ma dowolne ograniczenia (bez zmiany tych, od których zacząłeś). Kategorie, które powstają w ten sposób, są nazywane lokalnie prezentowalnymi i istnieje prosty wzór na$\mathcal{C}^{+}$: to kategoria funktorów $F: \mathcal{C}^{\mathrm{op}} \rightarrow \mathrm{Set}$ które zachowują ograniczenia, od których zacząłeś (czyli kolimity, w których zacząłeś) $\mathcal{C}$).
Teraz, jeśli chcesz naśladować to w świecie małych kategorii, możesz zamiast tego wybrać kardynała $\kappa$ zamiast tego rozważ funktory $F: \mathcal{C}^{\mathrm{op}} \rightarrow \{ \text{Sets of size < $\ kappa$} \}$, co jest odpowiednikiem małej kategorii $\mathcal{C}^{+}_{\kappa}$. Pytanie, które napotkasz, brzmi, czy jest to wystarczająco dobry zamiennik dla dużej kategorii$\mathcal{C}^{+}$powyżej. Na przykład, czy ma wiele ograniczeń i górnych granic? Nierozsądne jest proszenie, aby miał wszystkie okrężnice, ale zamiast tego można zapytać:
P) Czy kategoria $\mathcal{C}^{+}_{\kappa}$ mają colimity indeksowane diagramami rozmiaru $< \kappa$?
Odpowiedź na pytanie Q) brzmi „ogólnie nie, ale tak, jeśli $\kappa$ jest ładnie wybrany. ”Na przykład, jeśli masz nieskończonego kardynała $\lambda$ ograniczające rozmiar $\mathcal{C}$ i liczbę diagramów colimit, od których zaczniesz, to myślę, że możesz zagwarantować (i) biorąc $\kappa = (2^{\lambda})^{+}$ (i kategoria $\mathcal{C}^{+}_{\kappa}$można scharakteryzować za pomocą oczekiwanej właściwości uniwersalnej). Co więcej, aby to udowodnić, nie potrzebujesz żadnej formy wymiany.
Teraz możesz również zadać następujące pytania:
Q ') Czy kategoria $\mathcal{C}^{+}_{\kappa}$ mają ograniczenia indeksowane według diagramów rozmiaru $< \kappa$?
Tutaj odpowiedź będzie zwykle brzmiała „nie”, chyba że $\kappa$jest mocno niedostępny. Ale jeśli interesują Cię tylko granice określonego typu (na przykład, jeśli studiujesz toposy Grothendiecka, możesz być szczególnie zainteresowany ograniczeniami skończonymi), wtedy odpowiedź będzie ponownie „tak, dla$\kappa$ dobrze dobrane. ”I to jest coś, co możesz udowodnić używając bardzo małej ilości ZFC.
Teraz twierdzę, że na podstawie mojego doświadczenia powyższa dyskusja jest reprezentatywna dla rodzaju pytań, na które napotkasz, próbując poradzić sobie z rozróżnieniem między „małymi” i „dużymi” kategoriami (z pewnością reprezentuje sposób, w jaki te rzeczy pojawiły się w mojej książce, o którą zadawano oryginalne pytanie). W praktyce nigdy nie musisz mówić o całości tak dużej kategorii, jak$\mathcal{C}^{+}$; wystarczy zbudować z niego wystarczająco duży kawałek (np$\mathcal{C}^{+}_{\kappa}$) posiadające funkcje, które chcesz zobaczyć, które możesz ustawić, wybierając $\kappa$ ostrożnie.
Uważam, że koncepcyjnie jaśniej jest zignorować kwestię tego, jak rzeczy są sformalizowane w ZFC i frazować rzeczy w kategoriach „dużych” $\mathcal{C}^{+}$, odwołując się do jego „małych” przybliżeń $\mathcal{C}^{+}_{\kappa}$tylko jako pomocnicy w dowodzie (który nieuchronnie jeszcze gdzieś się pojawi!). Przywoływanie „wszechświatów” jest po prostu sposobem na pisanie w ten sposób, a jednocześnie deklaruje deklarację o aksjomatycznej strukturze ZFC i jest zdecydowanie nieistotne.
Chciałbym wspomnieć o czymś, o czym myślę, że nie zostało jeszcze wskazane. Pierwotne pytanie zaczęło się od
W języku teorii mnogości naprawia się niektórych mocno niedostępnych kardynałów $\kappa$... Oznacza to, że scena $𝑉_\kappa\subset 𝑉$ z "zestawów o rozmiarze $<\kappa$„jest modelem ZFC.
Jednak stwierdzenie, że $V_\kappa$ to model ZFC jest znacznie słabszy niż mówienie tego $\kappa$jest niedostępny. W rzeczywistości, jeśli$\kappa$ jest więc niedostępne $\{ \lambda\mid V_\lambda$ to model ZFC $\}$ jest nieruchomy w $\kappa$. Dlatego najmniejsza niedostępna (jeśli taka istnieje) jest znacznie większa niż najmniejsza$\kappa$ takie że $V_\kappa$ modele ZFC.
O ile zasada refleksji jest użyteczna (co, jak wskazały inne odpowiedzi, można przynajmniej kwestionować), jest ona bezpośrednio pomocna tylko w przypadku argumentów, w których istotną właściwością wszechświata Grothendiecka jest to, że jest to model ZFC. Jednak przynajmniej w naiwnym sformułowaniu jest wiele miejsc, w których teoria kategorii używa czegoś więcej. W szczególności używamy faktu, że wszechświat Grothendiecka spełnia funkcję zastępowania drugiego rzędu , co oznacza, że każda funkcja$f:A\to V_\kappa$, gdzie $A \in V_\kappa$ma obraz. Mówiąc, że$V_\kappa$modele ZFC tylko implikuje, że spełnia wymagania wymiany pierwszego rzędu , co pozwala nam tylko stwierdzić, że taki plik$f$ ma obraz, jeśli $f$ można zdefiniować z $V_\kappa$ logiczną formułą.
Uważam, że zamiana drugiego rzędu jest wszechobecna we wszechświecie w teorii kategorii, jak zwykle się formułuje. Na przykład, jeśli${\rm Set}_\kappa$ oznacza kategorię zbiorów w $V_\kappa$, aby to udowodnić ${\rm Set}_\kappa$ jest „kompletny i współkompletny” w naiwnym sensie, że dopuszcza granicę i kolimit dla każdego funktora, którego dziedzina jest mała, potrzebujemy zamiany drugiego rzędu, aby zebrać obrazy takiego funktora w jeden zbiór.
Istnieją sposoby na przeformułowanie teorii kategorii, aby tego uniknąć. Artykuł McLarty'ego robi to w sposób teoretyczny. Kategorycznie spójne podejście polega na zastąpieniu naiwnych „dużych kategorii” (czyli kategorii, których zbiory obiektów i morfizmów mogą nie należeć do$V_\kappa$) z dużym ${\rm Set}_\kappa$- indeksowane kategorie . Ale jest to znacznie bardziej znaczące przeformułowanie, które można wykonać ręcznie.
Jeśli dobrze rozumiem, szukasz oświadczenia formularza:
„Jeśli coś zostało udowodnione w HTT przy użyciu wszechświatów, można to udowodnić bez nich, ograniczając się do niektórych $V_\kappa$ dla $\kappa$ wystarczająco duży"
Rygorystyczną odpowiedzią na to pytanie, jeśli nie mamy więcej informacji na temat HTT, jest to, że nie może być takiego stwierdzenia, jeśli ZFC jest spójne.
Rzeczywiście, jest możliwe, że istnienie wszechświatów jest niespójne (w rzeczywistości nie można udowodnić, że jest spójne), aw takiej sytuacji wszystko można udowodnić za pomocą wszechświatów, a więc takie stwierdzenie sugerowałoby, że wszystko można udowodnić , tj. ZFC jest niespójne.
Jestem trochę niechlujny, jeśli chodzi o to, co można udowodnić w czym itp., Ale główna idea jest tam
Oczywiście wiemy wiele o HTT i jeśli uważnie go przeczytamy, możemy przeanalizować, gdzie używa on wszechświatów i zobaczyć, że w rzeczywistości można je zastąpić przechodnimi modelami zastępowania ZC + aż do $\Sigma_{15}$-formuły, jak wskazuje Jacob. W takim razie, skoro można udowodnić, że takie ładnie zachowane modele (w postaci$V_\kappa$, dla $\kappa$dobrze dobrane), to nie jest problem; a HTT można przepisać bez wszechświatów - ale nie można tego udowodnić bez wiedzy o tym, co jest w HTT.
„Moralne” jest to, że w większości teoretycznych pytań głównego nurtu, wszechświaty są narzędziem oszczędzającym czas, a nie rzeczywistą częścią matematyki.
Dowolne twierdzenie $T$ z $\mathsf{ZFC}$ wynika ze skończonego podzbioru aksjomatów $\mathsf{ZFC}$ lub, aby uprościć, od $\mathsf{ZFC}$ gdzie schemat zastępowania aksjomatów jest ograniczony do $\Sigma_n$ predykaty¹, nazwij to $\mathsf{ZFC}_n$. Teraz$\mathsf{ZFC}$, a dokładniej $\mathsf{ZFC}_{n+1}$dowodzi istnienia arbitralnie dużych kardynałów $\kappa$, mocne granice niepoliczalnej współmierności, takie $V_\kappa$ jest modelem $\mathsf{ZFC}_n$, aw szczególności twierdzenie $T$i takie, że zresztą prawdziwą wartość każdego $\Sigma_n$ instrukcja, z parametrami w $V_\kappa$ jest taki sam w $V_\kappa$jak w (prawdziwym) wszechświecie. Możemy to nazwać$V_\kappa$ „Ograniczone wszechświaty” w tym sensie, że są one zamknięte w ramach większości operacji opartych na teorii mnogości, takich jak przyjmowanie zestawów mocy, z wyjątkiem tego, że zastąpienie musi być policzalne (uwzględnione dla wygody) lub ograniczone do $\Sigma_n$orzec; aw szczególności są zamknięte pod jakimikolwiek stwierdzeniami o istnieniu$T$ robi.
Więc idea polegałaby na zastosowaniu powyższego do spójnika $T$ wszystkich twierdzeń, które uważasz za część Wyższej Teorii Toposu (i wszelkich innych teorii, które są używane jako warunki wstępne) i znajdź odpowiednie $n$. (Właściwie to podejrzewam$n=1$ powinno wystarczyć: byłbym bardzo zdziwiony, gdybym znalazł przypadek zamiany w zwykłej matematyce, która nie wynika z tego $\Sigma_1$-replacement.) Następnie $\mathsf{ZFC}_n$ udowodniłby $T$ (wszystkie twierdzenia teorii) i $\mathsf{ZFC}_{n+1}$ udowodniłoby istnienie nieskończonej ilości ograniczonych wszechświatów, w których można by zastosować teorię.
Oczywiście, aby uniknąć nieskończonej pętli, nie można rozważać tego twierdzenia (twierdzącego o istnieniu nieskończonej ilości$V_\kappa$), aby być częścią teorii, albo musisz przejść do większego $n$.
Aby wyjaśnić to, co może wydawać się logiczną sprzecznością, należy wyjaśnić, że stwierdzenie, że istnienie wielu modeli $\mathsf{ZFC}_n$ można udowodnić w $\mathsf{ZFC}$ dla każdego $n$, ale nie jednolicie (dowód staje się coraz dłuższy, jak $n$ rośnie), więc $n$musi być konkretną liczbą naturalną, powszechnie określaną ilościowo (ok $n$) nie można udowodnić w formacie$\mathsf{ZFC}$. Ale to nie jest problem, o ile twoja teoria jest ustalona i sformułowana w$\mathsf{ZFC}$ (co wymaga, aby sam w sobie nie zawierał takich metateorematów, jak „dla jakiegokolwiek betonu $n$ możemy udowodnić, co następuje $\mathsf{ZFC}$”). Do Ciebie należy więc upewnienie się, że tak jest w przypadku HTT (i jeśli jesteś wystarczająco odważny, znajdź odpowiednie$n$).
(Tylko po to, żeby dać wyobrażenie o tym, jak zaangażowani byli kardynałowie, kardynałowie $\kappa$ takie że $V_\kappa$ jest modelem $\mathsf{ZFC}_1$ są stałymi punktami $\gamma \mapsto \beth_\gamma$funkcjonować. Myślę, że nie ma nadziei na rozsądny opis domeny$\kappa$ takie że $V_\kappa$ jest modelem $\mathsf{ZFC}_n$ do każdego betonu $n\geq 2$. Zobacz także to pytanie .)
- Znaczenie predykatów z co najwyżej $n$ naprzemienne zestawy nieograniczonych kwantyfikatorów, zaczynając od kwantyfikatorów egzystencjalnych, po których następuje wzór z ograniczonymi kwantyfikatorami (znaczenie formy $\forall x\in y$ lub $\exists x\in y$).
OK, spędziłem większość dzisiejszego dnia próbując to rozgryźć, przyglądając się bardziej szczegółowo HTT. To była niezła przejażdżka; Zdecydowanie wielokrotnie zmieniałem swoją perspektywę w trakcie tego procesu. Obecnie wydaje mi się, że odpowiedź brzmi, że HTT, tak jak napisano, można czytać w tym formalnym systemie. (To jest tak, jak w żartach, w których po godzinach ktoś mówi: „Tak, to oczywiste”. Zdecydowanie są miejsca, w których należy wybrać właściwą interpretację, ale jak w każdym tekście matematycznym, tak i tak już jest). Tą odpowiedzią chcę wysunąć argument, że HTT można odczytać w tym formalnym systemie, próbując wyjaśnić trochę, jak interpretować pewne rzeczy w przypadku pojawienia się niejasności i dlaczego uważam, że czytając to w ten sposób, wszystko powinno działać. Ale jest całkiem prawdopodobne, że przeoczyłem coś ważnego, więc popraw mnie!
Jak zauważa Tim Campion, większość wczesnych rzeczy działa bez problemów - w rzeczywistości nawet nie wspomina o wszechświatach. Dopóki nie, wszystko działa$V_{\kappa_0}$, w $V_{\kappa_1}$, i w $V$, a podany schemat aksjomatów gwarantuje nawet, że wszelkie wykonane konstrukcje będą kompatybilne.
Należy zwrócić większą uwagę, gdy dojdzie się do rozdziałów 5 i 6. Spróbuję przedstawić niektóre definicje i propozycje z tych rozdziałów z trzech różnych punktów widzenia.
Klasyczny punkt widzenia ZFC lub (równie konsekwentnie) punkt widzenia teorii von Neumanna - Bernaysa - Gödla (NBG), która dopuszcza klasy oprócz zbiorów, więc możemy mówić o (klasowej) kategorii wszystkich zbiorów $\mathrm{Set}$.
Punkt widzenia HTT, czyli wszechświatów ZFC + Grothendiecka.
Punkt widzenia teorii mnogości Fefermana w formie przedstawionej w pytaniu. (Właściwie nie jestem już pewien, czy naprawdę potrzebuję tych granic współmierności. Ale miło jest wiedzieć, że można je założyć.)
Zauważ, że zadane pytanie zakłada, że naprawdę interesuje nas pierwszy punkt widzenia, a pozostałe tylko o tyle, o ile są wygodą, aby udowodnić coś o pierwszym ustawieniu. Jest to zgodne z treścią rozdziałów 5 i 6: cała teoria przedstawianych kategorii ładnie pasuje do pierwszego kontekstu, również filozoficznie.
OK, więc przypomnij sobie, że to dająca się prezentować kategoria - pozwól mi po prostu trzymać się kategorii zamiast $\infty$-kategorie, różnica jest nieistotna dla naszych obaw - jest kategorią (wielkości klasy) $C$ który dopuszcza wszystkie małe okrężnice i takie, jakie dla zwykłego kardynała $\kappa$, jest jakaś mała kategoria $C_0$ i równoważność $C\cong \mathrm{Ind}_{\kappa}(C_0)$,
to znaczy $C$ uzyskuje się poprzez swobodne łączenie $\kappa$-filtrowane colimits do $C_0$. (W szczególności,$C_0$ jest koniecznie równoważne pełnej podkategorii $\kappa$-kompaktowe obiekty z $C$.) W szczególności kategorie, które można przedstawić, są określane przez niewielką ilość danych. Pomysł jest taki$C$jest tak naprawdę kategorią wszystkich obiektów (zbiorów, grup, cokolwiek). Ten punkt widzenia jest rzeczywiście najwyraźniej wyrażony w 1), podczas gdy w 2) i 3) pojęcie prezentowalności nagle znów zależy od wszechświata i nagle znów zawierają one tylko małe zbiory / grupy /…; pozwólcie mi więc odpowiednio nazwać je małymi - reprezentacyjnymi. Zauważ, że to pojęcie ma sens zarówno w 2), jak i 3) i zależy tylko od$V_{\kappa_0}$. Kategoria „mała do prezentacji” jest wtedy szczególnie mała do zdefiniowania, więc żyje$\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$, gdzie to włączenie jest równością w 2) (ale nie w 3)).
W 2) zwykle definiuje się kategorię „mała do prezentacji” jako specjalny rodzaj dużej kategorii, czyli podejście HTT. Ale tutaj właściwie już jestem trochę zdezorientowany: wydaje się, że istnieją dwa pojęcia funktorów$F: C\to D$: Te, które można zdefiniować w $V_{\kappa_0}$, równoważnie $F\in V_{\kappa_0+1}$ (mianowicie, $V_{\kappa_0+1}$ są dokładnie klasami $V_{\kappa_0}$) lub wszystkie funktory w $V_{\kappa_1}$. Nie wydaje mi się oczywiste, że jakikolwiek funktor$F: C\to D$ w $V_{\kappa_1}$ kłamstwa w $V_{\kappa_0+1}$, tak jak $C$ i $D$ tylko mieszkają $V_{\kappa_0+1}$. Różnica między tymi dwoma pojęciami znika, gdy ograniczymy się do dostępnych funktorów, z których wszystkie są definiowalne. Zauważ, że 1) mówi, że to naprawdę pierwsza kwestia, na której powinniśmy się przejmować! (Przed napisaniem tego posta nie zdawałem sobie sprawy z różnicy.)
W 3) właściwym sposobem postępowania jest użycie perspektywy podyktowanej przez 1), która jest perspektywą „$V_{\kappa_0}$-definiowalne kategorie ”, więc żyją w $\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$. Można je ponownie uznać za$\kappa_1$-małe kategorie. Na początku myślałem, że będzie tutaj zasadnicza różnica między podejściami 2) i 3), ale w rzeczywistości wydaje się, że w obu przypadkach dochodzi się do dwóch różnych pojęć funktorów, które są uzgadniane, gdy ogranicza się do dostępnych funktorów.
Jednym z głównych twierdzeń jest twierdzenie o funktorze sprzężonym: Jeśli $F: C\to D$jest funktorem reprezentowalnych kategorii, który zachowuje wszystkie małe kolimity, a następnie dopuszcza właściwe sprzężenie. Co właściwie oznacza to twierdzenie?
W 1) oznacza to, że istnieje funktor $G: D\to C$ - co w szczególności oznacza, że musi być definiowalne za pomocą formuł, bo tym właśnie są funktory między kategoriami klasowymi - wraz z (definiowalnymi!) transformacjami jednostkowymi i liczebnymi spełniającymi zwykłe warunki.
W 2) jest po prostu rozważenie $C$ i $D$ jako małe, gdy rozważa się je w $V_{\kappa_1}$a następnie potwierdza tam istnienie właściwego łącznika. Bez dalszych informacji wydaje się, że to faktycznie nie daje tego, czego chcieliśmy w 1), a priori$G$(oraz transformacje jednostek i jednostek) wszystkie znajdują się w większym wszechświecie. Ale te informacje można uzyskać, pamiętając o tym$G$ jest faktycznie dostępny (część twierdzenia o funktorze sprzężonym, którego nie opisałem powyżej, ale powinienem zostać uwzględniony), a więc wszystko jest określone na zbiorze.
W 3) chciałoby się ponownie dojść do wyniku 1), ale można spróbować zrobić to jak w 2), najpierw udowadniając istnienie takich danych w $V_{\kappa_1}$ a następnie udowadniając dostępność, uzyskując w ten sposób, że wszystko w nim leży $\mathrm{Def}(V_{\kappa_0})$.
Zobaczmy, jak to się rozgrywa w kilku wczesnych miejscach rozdziału 5, gdzie używane są wszechświaty.
Definicja 5.1.6.2: Let $C$być kategorią, która dopuszcza wszystkie małe okrężnice. Obiekt$X\in C$jest całkowicie zwarty, jeśli funktor$j_X: C\to \widehat{\mathrm{Set}}$ współreprezentowany przez $X$ zachowuje małe okrężnice.
Tutaj $\widehat{\mathrm{Set}}$ to (bardzo duża) kategoria zestawów w $V_{\kappa_1}$. Zinterpretujmy, co ta definicja oznacza w powyższych systemach.
Tutaj $C$jest dowolną kategorią (prawdopodobnie równą klasie). Zwróć uwagę, że szczególnie w HTT „lokalnie mały” nie jest standardową hipotezą, więc pozwala to nawet morfizmom między dwoma obiektami być właściwymi zbiorami. Z tego powodu funktor naprawdę musi się udać$\widehat{\mathrm{Set}}$, i to jest coś, o czym nie możemy rozmawiać w tym miejscu. Należałoby więc przeformułować warunek, aby sprostać temu zarzutowi; nie powinno to być trudne, ale może być trochę nieprzyjemne.
Myślę, że z definicji wynika, że $C$ to dowolna kategoria, w której się znajduje $V_{\kappa_1}$. Jest to ściśle uchwycenie konfiguracji 1) w tym przypadku$C$ jest mały - można go zdefiniować jako pochodzący z 1), a następnie dowolny mały diagram colimit w $C$ jest automatycznie definiowalna jako mała.
Mamy tutaj dwie możliwości: albo tę z 1), albo tę z 2), i podają różne pojęcia. W przypadku konfliktu poprawna jest perspektywa z punktu 1), więc$C$jest mała-definiowalna i prosi się o komutację z kolimitami małych definiowalnych diagramów. Ale podczas gdy w 1) mieliśmy problem z sformułowaniem warunku, wszechświaty w zasięgu 3) oznaczają, że warunek można teraz sformułować: możemy poprosić, aby wymagał małych definiowalnych kolimitów w$C$ do colimits w $\widehat{\mathrm{Set}}$. Tutaj$\widehat{\mathrm{Set}}$ są zestawy $V_{\kappa_1}$.
Tak więc w tym przypadku skutek jest taki, że trzeba być nieco ostrożnym w 3) interpretacji, ale kierując się 1) można podać właściwą definicję; i wtedy system faktycznie pomaga.
Twierdzenie 5.2.6.2: Niech $C$ i $D$być kategoriami. Następnie kategorie$\mathrm{Fun}^L(C,D)$ lewych funktorów sprzężonych z $C$ do $D$, i $\mathrm{Fun}^R(D,C)$ prawych funktorów sprzężonych z $D$ do $C$ są (kanonicznie) sobie równoważne.
Z tej perspektywy ta propozycja ma sens tylko wtedy, gdy $C$ i $D$ są małe, jak inaczej $\mathrm{Fun}(C,D)$jest za duży. (Można rozważyć takie kategorie funktorów, gdy$C$ i $D$są prezentowalne (lub dostępne), ale tylko wtedy, gdy ograniczają się do dostępnych funktorów. Jest to więc dyskusja, która pojawi się później w rozdziale 5.) Zatem stwierdzenie jest wystarczająco jasne, a przedstawiony dowód ma zastosowanie.
Z tej perspektywy myślę, że jest to to samo, co w 1), z tym wyjątkiem, że ten sam wynik można sformułować w innym wszechświecie.
To samo tutaj.
Należy jednak zauważyć, że w obecnym kształcie w 1) tej propozycji nie można (jeszcze) zastosować w przypadku $C$ i $D$są reprezentacyjne. W 2) i 3), (małe-) reprezentacyjne są specjalnymi dużymi kategoriami, do których odnosi się wynik. Zauważ jednak, że wszystkie kategorie funktorów i ich równoważności żyją w większym wszechświecie i nie otrzymujemy żadnych informacji o nich$V_{\kappa_0+1}$ lub $\mathrm{Def}(V_{\kappa_0})$.
Następna propozycja dotyczy kategorii presheaf $\mathcal P(C)=\mathrm{Fun}(C^{\mathrm{op}},\mathrm{Set})$, a dowód jest typowym argumentem obejmującym przejście do większego wszechświata w celu rozwiązania kwestii homotopii-koherencji.
Twierdzenie 5.2.6.3: Niech $f: C\to C'$ być funktorem między małymi kategoriami i niech $G: \mathcal P(C')\to \mathcal P(C)$ być indukowanym funktorem kategorii presheaf indukowanych przez kompozycję z $f$. Następnie$G$ jest dobrze połączony $\mathcal P(f)$.
Tutaj $\mathcal P(f)$ definiuje się jako unikalne małe rozszerzenie zachowujące colimity $f$ (pod osadzeniem Yoneda).
Tutaj mamy dwie kategorie wielkości klasy i funktory między nimi, wszystkie definiowalne (co musi być). Propozycja wymagałaby od nas znalezienia (dających się zdefiniować!) Transformacji jednostek i jednostek, co spowodowałoby, że niektóre diagramy dojeżdżałyby do pracy. Nie wydaje się to zbyt trudne. Ale w$\infty$-kategorie, trudno jest ręcznie zdefiniować funktory, więc tak naprawdę nie jest tak, jak postępuje Lurie!
Tutaj $\mathcal P(C)$ i $\mathcal P(C')$to specjalne duże kategorie. W rzeczywistości Lurie stosuje w dowodzie duże Yoneda. Więc to jest tak naprawdę wytwarzanie jednostek i uzupełnień jednostek tylko w jakimś większym wszechświecie. Jak omówiono powyżej, myślę, że ten dowód w rzeczywistości nie daje tego, czego chcieliśmy w 1)!
Możemy spierać się, tak jak robi to Lurie, tworząc dane w jakimś większym „wszechświecie”. (Edycja: Właściwie, jak wskazuje Tim Campion, należy zrobić minimalny objazd, aby uzasadnić to, co zostało napisane. Zobacz komentarze do jego odpowiedzi.)
Tak więc czytając tę propozycję, w systemie 2) lub 3), należy zaznaczyć w myślach, że stwierdzenie to, jak dotąd udowodniono, jest słabsze, niż można by naiwnie oczekiwać. Ale zostanie to później poprawione, zauważając, że wszystko zależy od niewielkiej ilości danych.
Upshot: Chociaż na początku myślałem, że będzie znacząca różnica między 2) a 3), tak naprawdę myślę, że nie ma (prawie) żadnej. Jedna różnica jest taka$\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$ jest właściwym włączeniem, ale w praktyce sposobem na zagwarantowanie ograniczenia w $V_{\kappa_0+1}$ wydaje się być definiowalny w $V_{\kappa_0}$ (np. udowadniając, że pewne funktory są dostępne).
OK, teraz powiedz mi, dlaczego to nie działa! :-)
Odpowiedź na to pytanie zależy w dużej mierze od tego, czego dokładnie oczekujesz od Teorii Wyższego Toposu, ponieważ wyrażenie wysokiej siły logicznej jest innym celem niż wyrażenie trafnie zunifikowanej struktury logicznej dla geometrii algebraicznej i teorii liczb. Zunifikowane, mocne podstawy ogólnej matematyki kategorialnej to jeden wspaniały cel i wydaje się być celem wielu autorów. W tym celu istotne jest wszystko, co zostało powiedziane w komentarzach i odpowiedziach na to pytanie. Ale trafna praca w geometrii i teorii liczb nie wymaga ogromnej siły logicznej.
Podczas gdy HTT jest bardziej spleciona ze wszechświatami niż SGA, ani HTT, ani SGA nie wykorzystują w rzeczywistości (bardzo silnego) schematu zastępowania. W ten sposób mogą używać „wszechświatów” radykalnie słabszych niż te Grothendiecka. Jako typowy i zasadniczy przykład Grothendieck odwołał się tylko do schematu aksjomatów zastępowania. To jest w jego dość kluczowym dowodzie, że każda kategoria AB5 z agregatem prądotwórczym ma wystarczającą ilość iniekcji. I to użycie wymiany okazuje się być wyeliminowane. Udało się, ale Grothendieck w rzeczywistości nie potrzebował tego, aby uzyskać swój wynik.
Aby rozwinąć wykorzystanie zamiany przez Grothendiecka: Reinhold Baer w latach czterdziestych XX wieku zastosował indukcję pozaskończoną (która wymaga schematu zastępowania aksjomatów), aby udowodnić, że moduły (w dowolnym pierścieniu) mają wystarczającą ilość iniekcji. Świadomie eksplorował nowe techniki dowodowe i uzyskał dobry wynik. Tohoku Grothendiecka rzucił ten dowód w formie pokazującej, że każda kategoria AB5 z małym zestawem generatorów ma wystarczającą ilość iniekcji - a kilka lat później Grothendieck odkrył, że jest to dokładnie to twierdzenie, którego potrzebował do kohomologii toposu. Baer i Grothendieck mieli praktyczne cele, nie byli związani z problemami fundacji, ale obaj też chcieli dobrze założyć fundamenty. I zrobili. Okazuje się jednak, że mogli otrzymać te same twierdzenia, poprawnie, bez zamiany, przez prawie te same dowody, określając na początek wystarczająco duże zbiory funkcji (używając zestawu potęg, ale nie zastępując). Istnieją wyniki, które naprawdę wymagają zastąpienia schematu aksjomatów. Ale te wyniki rzadko pojawiają się poza podstawowymi badaniami.
Wielu ludzi wywodzących się z bardzo różnych punktów widzenia (niektórzy logicy, niektórzy nie lubią logiki) od lat sześćdziesiątych XX wieku zauważyli, że w kontekście geometrii algebraicznej i teorii liczb, duża siła logiczna aksjomatu Grothendiecka jest faktycznie niewykorzystanym produktem ubocznym Pragnienie Grothendiecka dotyczące ujednoliconych ram kohomologii. Można to teraz sprecyzować: cały aparat Grothendiecka, obejmujący nie tylko wyprowadzoną kohomologię funktorów topoz, ale także 2-kategorię toposów i kategorie pochodne, można sformalizować prawie dokładnie w taki sam sposób, jak został sformalizowany przez Grothendiecka, ale siła logiczna znacznie poniżej Zermelo-Fraenkela czy nawet teorii mnogości Zermelo. To samo dotyczy HTT. Możesz go zdobyć bez niedostępnych wszechświatów lub refleksji, o ile nie potrzebujesz ogromnej (i rzadko używanej) siły zastępczej. Dowód nie został faktycznie przedstawiony dla HTT. To było dla zastosowań wszechświatów przez Grothendiecka . Wydaje się jasne, że to samo zadziała w przypadku HTT.
Potrzebna siła logiczna została wyrażona na różne sposoby: teoria typów prostych (z arytmetyką), arytmetyka skończonego porządku, elementarna teoria kategorii zbiorów, ograniczona kwantyfikator teoria zbiorów Zermelo. Mówiąc z grubsza, zakładasz zbiór liczb naturalnych i zakładasz, że każdy zbiór ma zbiór potęg, ale nie zakładasz nieograniczonej iteracji zbiorów potęg. Dość naiwną teorię wszechświatów można uznać za konserwatywną w stosunku do któregokolwiek z nich (sposób, w jaki teoria mnogości Godela-Bernaysa jest konserwatywna w stosunku do ZFC) i adekwatną do całego aparatu dużych struktur szkoły Grothendiecka.
Rozważyłbym konserwatywne rozszerzenie ZFC otrzymane z ZFC poprzez dodanie stałej $\alpha$ oraz następujące aksjomaty:
$\alpha$ jest porządkową ($Ord(\alpha)$).
Zdanie $\phi\leftrightarrow\phi^{V_\alpha}$, dla każdego zdania w języku oryginalnym $\phi$ (schemat aksjomatów).
$V_{\alpha}$ zachowuje się jak $V$(dla wszystkich zdań w języku teorii mnogości). Jeśli potrzebne są dwa (lub więcej) wszechświaty, można dodać kolejną stałą$\beta$ z odpowiednimi aksjomatami i aksjomatem $\alpha<\beta$.
Dowód na to, że powstała teoria jest konserwatywna w stosunku do ZFC, jest łatwy.
Zakładać, że $\phi$ można udowodnić na podstawie nowych aksjomatów (aksjomaty używające $\alpha$), w którym $\phi$jest w języku oryginalnym. Ponieważ każdy dowód jest skończony, istnieje nieskończenie wiele zdań$\phi_1$, ..., $\phi_n$ takie że
$Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}})\rightarrow \phi$
można udowodnić bez żadnych nowych aksjomatów. Dlatego można pomyśleć$\alpha$jako zmienna wolna, a powyższe zdanie można udowodnić w ZFC (twierdzenie o stałych). Od$\alpha$ nie występuje w $\phi$, następująca implikacja jest możliwa do udowodnienia w ZFC ($\exists$-wprowadzenie):
$\exists\alpha(Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}}))\rightarrow \phi$
Teraz zasada odbicia dla ZFC mówi, że poprzednikiem jest twierdzenie ZFC. Z modus ponens udowadnia ZFC$\phi$.
Możesz więc pracować z nowymi aksjomatami i $V_{\alpha}$ zachowuje się jak wszechświat i wszystko, co zostało udowodnione, o czym nie wspomina $\alpha$ można udowodnić już w ZFC.
Pytanie, które pojawiło się w komentarzach, dotyczyło motywacji do zadania pytania. Spróbuję tutaj zająć się tym.
Przede wszystkim chodzi o naukę! Jak wspomniałem w pierwotnym pytaniu, bawiłem się pewnymi „głupimi” kardynalnymi ograniczeniami i dopiero później poznałem zasadę refleksji, więc chciałem zrozumieć, co może zrobić (a czego nie może) i czy może w jakiś sposób automatycznie przenieść dalsze skomplikowane wersje takich szacunków do tej maszyny. Więc to normalna rzecz, kiedy potykasz się w ciemnym pokoju i bardzo chciałbyś, aby pokój był oświetlony! Dziękuję wam wszystkim za pouczające odpowiedzi!
Innym powodem jest to, że ostatnio trochę frustrowało mnie rozwiązanie wszechświatów Grothendiecka. Pozwól mi wyjaśnić.
Bardzo chcę porozmawiać o kategorii wszystkich zbiorów lub wszystkich grup itp. I chcę udowodnić na jej temat twierdzenia. I przynajmniej w wersji von Neumanna-Bernaysa-Gödela (NBG) teorii ZFC, która dopuszcza klasy, jest to całkowicie poprawne pojęcie. Tak więc uważam, że praca w tym układzie jest ontologicznie bardzo przyjemna i bardzo chciałbym, aby twierdzenie o funktorze sprzężonym było twierdzeniem o (prezentowalnych) kategoriach w tym sensie.
Teraz kategorie, które można przedstawić, są określane na podstawie niewielkiej ilości danych, więc zawsze można pracować z tak małą ilością danych i uważnie śledzić ich rozmiary. W rzeczywistości wiele dowodów w HTT wyraźnie śledzi takie względne rozmiary, ale wciąż jest kilka miejsc, w których dobrze jest najpierw przyjrzeć się „szerszemu spojrzeniu” i spojrzeć na te duże kategorie tak, jakby były małe.
Rzeczywiście, twierdzenie o funktorze sprzężonym dotyczy funktorów między dużymi kategoriami i szybko staje się nieprzyjemne, gdy mówi się o tym z poziomu NBG / ZFC. Zauważ, że stwierdzenie twierdzenia o sprzężonym funktorze ma doskonały sens - po prostu prosi, aby wszystkie dane sprzężenia były definiowalne. Ale to trochę paskudne, gdy próbuje się mówić o tych rzeczach „od wewnątrz”. Więc zdecydowanie byłoby miło mieć jakąś meta-teorię, za pomocą której można spierać się o te duże kategorie i udawać, że są one małe. Subtelna kwestia „definiowalności od wewnątrz” może być a priori zagubiona w tej meta-teorii, ale uważam tę kwestię „definiowalności od wewnątrz” za centralną, ponieważ w końcu to, czego chciałem, to twierdzenie o wszystkich zbiorach, więc W porządku, że muszę poświęcić temu trochę uwagi - i żeby oderwać się od puenty, okazuje się, że na tym właśnie polega różnica między pracą z wszechświatami Grothendiecka a pracą z „wszechświatami” Fefermana.
A więc to jest to, do czego służą wszechświaty Grothendiecka: zawsze dają ci większy wszechświat dla każdego wszechświata, w którym obecnie pracujesz. Istnienie wszechświatów Grothendiecka wydaje mi się całkowicie intuicyjne i w rzeczywistości twierdzenie, że ich istnienie wydaje się być równoznaczne z założeniem nieskończony zestaw na pierwszym miejscu: po prostu pozwalasz zebrać wszystko, co już masz, w większą własną całość.
Ale teraz nagle to, o czym myślałem, gdy wszystkie zestawy nazywa się małymi zestawami, a jest też wiele większych zestawów. Więc nawet jeśli udowodnię twierdzenie o funktorze sprzężonym w tym ustawieniu, nie jest to już twierdzenie o funktorach między kategoriami wszystkich zbiorów / grup / ..., ale tylko jeden z funktorów między małymi zbiorami / grupami / .... Więc jeśli pomyśl o tym, nawet we wszechświatach ZFC + Grothendiecka nigdy nie udowodnisz twierdzenia, którego tak naprawdę chciałeś, o kategorii wszystkich zbiorów. (Właściwie do niedawna zakładałem, że twierdzenie o funktorze sprzężonym (for$\infty$-kategorie) to stwierdzenie ZFC, które zostało udowodnione w kategorii „ZFC + Universes”, ale nie jest to do końca poprawne: stwierdzenie, które zostało udowodnione, można sformułować nawet tylko w ZFC + Universes.)
Udowodniono, że jest zgodne z twierdzeniem o funktorze sprzężonym. Mianowicie, zakładając spójność Wszechświatów ZFC +, stworzyłeś teraz model ZFC - model małych zbiorów w twoim modelu Wszechświatów ZFC + - w którym twierdzenie jest prawdziwe. Możesz więc teraz pracować w teorii "ZFC + twierdzenie o funktorze sprzężonym", w której twierdzenie o funktorze sprzężonym można zastosować do kategorii wszystkich zbiorów / grup / ..., ale to zdecydowanie wydaje mi się oszustwo. Nie udowodniłeś nawet, że „ZFC + Wszechświaty + twierdzenie o funktorze sprzężonym” jest spójne! (Otrzymasz to, jeśli zaczniesz od konsystencji nieco większej niż ZFC + Universes, prosząc o$\kappa$ takie że $V_\kappa$spełnia ZFC + Universes. Ponownie, wydaje mi się to całkowicie słusznym założeniem - po prostu kontynuuj.) Ale teraz możesz dostrzec niebezpieczeństwo, że nieumyślnie wspinasz się po drabinie spójności, gdy zaczniesz bezwarunkowo przywoływać coraz więcej twierdzeń udowodnionych również dla małych zbiorów. dla wszystkich zestawów.
Byłoby znacznie przyjemniej, gdybyś wiedział, że we wszechświatach ZFC + Grothendieck wszystko, co udowodniłeś o małych zbiorach, jest również twierdzeniem o całej kategorii otoczenia wszystkich zbiorów. Nie jest to automatyczne, ale możesz dodać to jako schemat aksjomatów. Mike Shulman w sekcji 12 teorii mnogości dla teorii kategorii (arXiv: 0810.1279) omawia ten pomysł (że oznacza ZMC): Uważam, że ontologicznie jest całkiem przyjemny, wydaje mi się również, że ma bardzo prostą aksjomatyzację (nawet prostszą niż ZFC!), ale
a) ten dodatkowy schemat aksjomatów nie jest dla mnie całkowicie oczywisty: dlaczego wszystko , co jest prawdą w małych zbiorach, ma również obowiązywać dla wszystkich zbiorów? (Zwłaszcza jeśli mieliśmy pewne problemy potwierdzający pożądany rezultat w pierwszej kolejności Należy również pamiętać, że to na pewno nie. Nie trzymać za jakiekolwiek pojęcie małych zestawach: Raczej gwarancji schemat aksjomatu, że istnieje pewne pojęcie małych zestawów, dla których ten rodzaj refleksji. Teraz wydaje mi się to trochę wątpliwe, ponieważ na początku nigdy nie chciałem małych zestawów, więc teraz je stawiam, a także proszę, aby nadal odzwierciedlały całe zachowanie wszystkich zestawów. Prawdopodobnie dobrze, ale nie dla mnie oczywiste).
b) siła spójności tego schematu aksjomatów jest znacznie wyższa: jest taka sama, jak konsystencja kardynała Mahlo. Jest to wciąż nisko, jak idą wielcy kardynałowie, ale jest znacznie wyższy niż zwykłe wszechświaty Grothendiecka (które są naprawdę nisko na dole hierarchii).
Jeśli chodzi o a), fakt, że mogliśmy udowodnić spójność twierdzenia o funktorze sprzężonym na podstawie spójności wszechświatów Grothendiecka, wskazuje na właściwy kierunek, ale to samo w sobie nie gwarantuje, że oba razem są spójne. Mogę sobie wyobrazić, że mógłbym przekonać samego siebie, że schemat aksjomatów jest rozsądny, ale z pewnością uważam, że wymaga on znacznie więcej uzasadnienia niż zwykłe wszechświaty Grothendiecka. (Pytanie poboczne: Jak dużych kardynałów można uzasadnić za pomocą idei „umożliwienia zebrania wszystkiego, co już mieliśmy”? Nie jestem pewien, czy jest to całkowicie dobrze zdefiniowane pytanie ... ale dla mnie Wymierny kardynał zdecydowanie nie jest tego rodzaju (ale cieszę się, że mogę zostać poprawiony), ponieważ wydaje się, że zakłada pojawienie się nowych cech kombinatorycznych.)
Innym powodem, dla którego ostatnio byłem nieco niezadowolony ze wszechświatów Grothendiecka, jest to, że chociaż w pewnym sensie chcielibyśmy ich użyć, aby móc zignorować subtelności teorii mnogości, w pewnym sensie wracają, by cię ugryźć, tak jak teraz musisz określić w w którym wszechświecie żyją pewne rzeczy. Czasami może być nawet konieczne określenie kilku różnych wszechświatów dla różnych typów obiektów (pomyśl o snopach na zestawach nieskończonych) i stwierdzam, że szybko robi się to dość brzydkie. Wolałbym, aby wszystkie obiekty żyły razem w jednym wszechświecie.
Tak więc, myśląc o snopach na zestawach profinite, doszedłem do wniosku, że tylko jeden wszechświat jest znacznie bardziej estetyczny i ontologiczny, a to rozwiązanie (zbiory skondensowane) można sformalizować w ZFC bez problemu.
OK, więc twierdzę, że wszechświaty Grothendiecka tak naprawdę nie rozwiązały problemu, który zamierzali rozwiązać, jak np
a) nadal nie pozwalają na udowodnienie twierdzeń o kategorii wszystkich zbiorów / grup / ... (z wyjątkiem wyniku zgodności lub pod silniejszymi dużymi aksjomatami kardynalnymi)
b) pracując z nimi, nadal musisz się martwić kwestiami rozmiaru - twoja kategoria wszystkich zestawów jest teraz podzielona na zestawy różnego rodzaju o różnych rozmiarach (tj. w różnych wszechświatach).
Ponadto zwiększają siłę konsystencji.
Teraz, po tej wspaniałej dyskusji tutaj, myślę, że propozycja Fefermana jest w rzeczywistości znacznie lepsza. Jednakże, jak również skomentował Mike Shulman, uważam, że aksjomaty Fefermana nie opisują żadnego ontologicznie poprawnego świata, ale uważam „wszechświaty” teorii Fefermana jedynie za udogodnienia, aby mówić o dużych kategoriach tak, jakby były małe. Innymi słowy, teoria Fefermana dokładnie przedstawia meta-teorię, w której można spierać się o tak duże kategorie z „zewnątrz”. Ale to teoria, której użyłbym tylko do udowodnienia twierdzenia o ZFC. W porównaniu do wszechświatów Grothendiecka, teoria Fefermana
a) nie pozwalają udowodnić twierdzenia o kategorii wszystkich / grup zestawów / ..., ponieważ wyraźnie zawiera schemat aksjomatu, że wszystkie twierdzenia o małych zestawy są również twierdzenia o wszystkich zestawach.
b) Oczywiście, w ramach dowodu twierdzenia ZFC, które wywołuje pewne nietrywialne kwestie rozmiaru, bardzo mile widziane jest, że teoria pozwala mówić o różnych rozmiarach. Co więcej, robi to w taki sposób, że nadal możesz zastosować wszystkie aksjomaty ZFC do każdego z „wszechświatów”, a także dba o to, aby „za kulisami” przepisać wszystko w kategoriach (potencjalnie niezwykle subtelnych) granic kardynalnych w samym ZFC. Jest to więc język programowania wysokiego poziomu dla argumentów związanych z trudnymi szacunkami kardynalnymi w ZFC.
Ponadto nie zwiększa siły spójności, aw rzeczywistości wszelkie stwierdzenia ZFC udowodnione w tym języku są twierdzeniami ZFC. (Jak przypomniałem powyżej, moglibyśmy również mieć a) + b) z wszechświatami Grothendiecka, ale wtedy doszlibyśmy do spójności kardynała Mahlo.)
Tak więc, rezultat jest taki, że myślę, że wszechświaty Fefermana wykonują znacznie lepszą robotę w rozwiązywaniu problemu dostarczania meta-teorii do „mówienia o dużych kategoriach tak, jakby były małe” niż wszechświaty Grothendiecka.
Pozwólcie, że dodam kilka ostatnich powodów, dla których zadam to pytanie. Myślę, że techniki wyższej kategorii, takie jak te przedstawione w HTT, mają bardzo centralne znaczenie, nie tylko w topologii algebraicznej, w której powstały, ale w całej matematyce. Z pewnością mogę to potwierdzić, jeśli chodzi o teorię liczb i geometrię algebraiczną. Tak więc ich centralne znaczenie jest również ważnym powodem do analizy siły ich spójności.
Czytanie HTT to sprawa bardzo nietrywialna - jest długa i skomplikowana. Niektórzy koledzy z teorii liczb powiedzieli jednak, że jednym z głównych powodów, dla których nie mogli odczytać HTT, jest to , że używa on wszechświatów . Mianowicie, są tak przyzwyczajeni do ZFC (i do sprawdzania z najwyższą starannością!), Że automatycznie spróbują wyeliminować jakiekolwiek użycie wszechświatów w argumentacji. Teraz w SGA, przynajmniej jeśli byłbyś zainteresowany tylko zastosowaniami do etale kohomologii rozsądnych schematów, było to coś, co możesz zrobić ręcznie - na przykład po prostu dodaj kilka założeń policzalności, aby uczynić rzeczy małymi. Jednak w HTT nie widzę żadnego sposobu, aby ktoś był w stanie wprowadzić kardynalne granice, gdy będziesz czytać dalej - argumenty są na to zbyt skomplikowane.
Więc teraz mam nadzieję, że mogę im powiedzieć, że mogą sprawdzić, czy wszystko działa w ZFC i nadal potrafią czytać HTT (zasadniczo) tak, jak napisano, jeśli przeczytają go w teorii mnogości Fefermana. Jeśli sprawdzą dokładnie (co będą), nadal mogą potrzebować wypełnić mały lemat tutaj i trochę dodatkowego argumentu tam - ale i tak musieliby to zrobić, w każdej książce zawierającej ~ 1000 stron, i mogę sobie wyobrazić że mniej niż połowa tych uwag pobocznych dotyczy zastąpienia wszechświatów Grothendiecka „wszechświatami” Fefermana. Jeśli ktokolwiek rzeczywiście podejmie się tego projektu, oczywiście zasługuje na pełne uznanie, jeśli odniesie sukces w tej ważnej pracy!
Zakończę bardzo krótką uwagą na temat tego, co wydaje się być kluczowym punktem w tłumaczeniu teorii Fefermana. Doceniłem kwestię, którą poruszył Tim Campion w swojej odpowiedzi, i teraz widzę, że zostało to również wspomniane w drugiej odpowiedzi Jacoba Lurie. Z grubsza wygląda to następująco. Gdyby$C$ jest kategorią możliwą do zaprezentowania, to jest jakaś mała kategoria $C_0$ takie że $C=\mathrm{Ind}_\kappa(C_0)$
dla jakiegoś zwykłego kardynała $\kappa$, przylegając swobodnie wszystkie małe $\kappa$-filtrowane colimits. To sprawia$C$ naturalnie związek $C_\tau$jest, gdzie $C_\tau$ zbiera tylko pliki $\tau$-mały $\kappa$-filtrowane colimits. Tutaj$\tau$ jest zwykłym kardynałem, takim że $\tau\gg \kappa$. Ta rosnąca struktura$C$ jako związek $C_\tau$ma kluczowe znaczenie w teorii prezentowalnych kategorii, ale poziomy są naprawdę wyliczane przez (pewnych) zwykłych kardynałów $\tau$. Jeśli zwiększysz swój wszechświat, otrzymasz także większą wersję$C'$ z $C$ siebie i we wszechświatach Grothendiecka $C$ jest teraz jedną z ładnych warstw $C'_\tau$ z $C$, gdzie $\tau$jest kardynałem odcinającym poprzedniego wszechświata. Ale we wszechświatach Fefermana to$\tau$nie jest regularne. Może to sprawić, że niektóre argumenty będą bardziej subtelne, ale spodziewałbym się, że zwykle można rozwiązać ten problem, po prostu osadzając$C$ do niektórych $C'_\tau$ z $\tau$ jakiś zwykły kardynał większy niż kardynał odcinający mniejszego wszechświata.
W odpowiedzi na edycję, która sprowadza sprawy do formalnego systemu z udziałem kardynałów $\kappa_{-1} < \kappa_0 < \kappa_{1/2} < \kappa_1$:
Zamierzam pójść na bardziej być może nierozsądną kończynę i przewidzieć, że aby dopasować rozdziały 1-4 do tego formalnego systemu, nie będzie potrzebna żadna prawdziwa arytmetyka kardynalna. Raczej w tej części książki wszystko, co musisz zrobić, to przejść przez i dodać do różnych twierdzeń hipotez w postaci "$X$ jest $\kappa_{-1}$-small ". W końcu ta część książki zajmuje się tak naprawdę tylko małymi przedmiotami, z wyjątkiem kilku szczególnych dużych obiektów, takich jak kategoria małych zbiorów uproszczonych, kategoria małych kategorii uproszczonych itp., itp. Skonstruowane są różne struktury modelowe, ale wierzę, że w każdym przypadku można sobie poradzić, używając argumentu o specjalnym przypadku małego obiektu do generowania kofibracji / acyklicznych kofibracji między obiektami o skończonej reprezentacji, tak że nie jest potrzebna indukcja pozaskończona. Pozornie prostowanie / prostowanie ma wygląd konstrukcji, które mogą wykorzystywać teorię mnogości w poważny sposób, ale zamierzam iść dalej i przewidzieć, że nie stanowią one problemów dla proponowanego systemu formalnego.
Rozdział 5 staje się bardziej irytujący. Uważam, że trzeba będzie dokonać pewnych ostrożnych wyborów dotyczących podstawowych twierdzeń reprezentatywności ($\infty$)-kategorie. Tym, co sprawia, że prezentowalne kategorie zaznaczają, jest to, że pakują one twierdzenie o funktorze sprzężonym w bardzo przejrzysty sposób, ale, jak powiesz, zwykłe twierdzenie o funktorze sprzężonym ma pewne zastrzeżenia w tym ustawieniu. Mogę posunąć się nawet do stwierdzenia, że cały sens myślenia o kategoriach prezentowalnych w pierwszej kolejności jest w tym ustawieniu całkowicie odwrócony. Nie będziesz w stanie udowodnić podstawowych rzeczy, takich jak „kategorie, które można prezentować, są dokładnie dostępnymi lokalizacjami kategorii presheaf”. Przewiduję, że niezależnie od wyborów dotyczących formułowania słabych wersji podstawowych twierdzeń przedstawianych kategorii w tym ustawieniu, na tym ucierpi jakieś zastosowanie lub potencjalne zastosowanie.
Rozdziały 5 i 6 zawierają również pewne twierdzenia dotyczące określonych bardzo dużych kategorii, takich jak $\infty$-kategoria reprezentacyjnych $\infty$-kategorie i $\infty$-kategoria $\infty$-topoi [1]. System wydaje się być taki, że tak naprawdę nie będzie to problemem per se , z wyjątkiem tego, że problemy napotykane w podstawowej teorii prezentowalności będą teraz złożone. Nie będziesz w stanie tego udowodnić$Pr^L$ jest podwójny do $Pr^R$. Nie będziesz w stanie udowodnić twierdzenia Girauda (cóż, definicje i tak będą się zmieniać, więc powinienem wyjaśnić: nie będziesz w stanie udowodnić, że pozostawione dokładne dostępne lokalizacje kategorii presheaf są takie same jak lokalnie małe kategorie spełniające listę warunków kompletności, generacji i dokładności). Więc każde twierdzenie o$\infty$-topoi, którego dowód rozpoczyna się od przypadku presheaf, a następnie lokalizacja będzie musiała zostać całkowicie przemyślana.
Może jestem tutaj poza bazą, ale uważam, że w rozdziałach 5 i 6 wymagana byłaby znaczna dodatkowa praca i prawdziwie nowe pomysły matematyczne, a wynikiem byłaby teoria, która jest znacznie trudniejsza w użyciu.
Z drugiej strony, myślę, że jeśli chcesz ograniczyć uwagę do dużych kategorii, które można zdefiniować na podstawie małych parametrów, to chociaż będziesz tęsknić za piękną umiejętnością powiedzenia „udowodniliśmy to dla małych kategorii, ale teraz możemy to zastosować do dużych jedynki ”, otrzymasz znacznie bardziej użyteczną teorię prezentowalności, bez wychodzenia z ZFC.
[1] W rzeczywistości w zwykłych fundacjach te kategorie są (aż do równoważności) tylko duże i niezbyt duże (a dokładniej, mają $\kappa_0$-wiele obiektów i $\kappa_0$duże domy), ale potrzeba odrobiny pracy, aby to wykazać. Czy tak będzie nadal w tym formalnym systemie? Nie jestem pewny.
EDIT: Długi komentarz w odpowiedzi na Petera SCHOLZE za odpowiedź .
Jedną rzeczą, jaką sobie sprawę , że jeśli$\kappa_0$ nie jest $\beth$-fixed-point, to nie każdy zestaw $V_{\kappa_0}$ ma liczność $<\kappa_0$, aby pomnożyć pojęcia „małości”. Na szczęście myślę, że twój formalny system to potwierdza$V_{\kappa_0}$ ma $\Sigma_1$-replacement, co oznacza, że jest to plik $\beth$-stały punkt. Kryzys zażegnany!
Być może to podejście polegające na systematycznym stosowaniu hipotez definiowalności w ramach „ustawienia wszechświata” będzie wykonalne - łącząc „to, co najlepsze z obu światów”. Jedną fajną rzeczą jest to, że nawet jeśli jawnie używasz hipotez metamatematycznych, wydaje się, że nadal będziesz w stanie stwierdzić i udowodnić te twierdzenia jako pojedyncze twierdzenia, a nie schemat.
Jestem trochę zdezorientowany co do twierdzenia 5.2.6.3 (ostatniego, o którym mówisz, i dziecięcej wersji twierdzenia o sprzężonym funktorze). Przypuszczam, że kategoria presheaf$P(C)$ zostaną zdefiniowane tak, aby obejmowały te funktory $C^{op} \to Spaces$ które leżą $Def(V_{\kappa_0})$. Kiedy przechodzimy do większego wszechświata, przejście jest zwykle dość płynne, ponieważ oczekujemy$P(C)$ aby wszystkie colimity były indeksowane przez $\kappa_0$-małe kategorie - całkowicie naturalna właściwość do pracy $V_{\kappa_1}$. Rzeczywiście, pierwszym krokiem dowodu 5.2.6.3 Luriego jest wykazanie, że lewy sprzężony istnieje, wykorzystując fakt, że$P(C)$ma wszystkie małe okrężnice [2]. Jednak w obecnych warunkach nigdy nie możemy tego założyć$\kappa_0$ jest regularne i dlatego nigdy nie możemy tego założyć $P(C)$ma wszystkie małe okrężnice. Najlepsze, co możemy powiedzieć, to to$V_{\kappa_0}$ myśli $P(C)$ma wszystkie małe okrężnice. Dopóki pracujemy w$V_{\kappa_0}$, ta właściwość jest „tak samo dobra” jak posiadanie wszystkich małych kolimitów. Ale kiedy przejdziemy do$V_{\kappa_1}$nagle musimy pomyśleć o tym, czym jest - właściwością metamatematyczną. Być może później usiądę i spróbuję sprawdzić, czy dowód 5.2.6.3 Luriego będzie działał w tym ustawieniu, ale myślę, że prima facie jest to niejasne.
[2] Dopiero po abstrakcyjnym zweryfikowaniu istnienia w ten sposób pokazuje, że lewy sprzęg musi być wskazanym funktorem. Oczywiście ten manewr jest w rzeczywistości dodatkową komplikacją związaną z$\infty$-Ustawienie kategorialne - w zwykłych kategoriach formuły dla dwóch funktorów można bezpośrednio zweryfikować jako sprzężone, ale w $\infty$-kategorie wzór na lewy sprzężenie nie jest oczywiście funkcyjny.