Fallstudie: Was braucht es, um Quillens Argument für kleine Objekte in ZFC zu formulieren und zu beweisen?
Ich verliere mich ein wenig über Peter Scholzes interessante Frage, wie man die Abhängigkeit von Universen aus Theoremen der Kategorietheorie entfernen kann. Insbesondere muss ich zugeben, dass ich nicht wirklich weiß, wann der Ersatz aufgerufen wird, egal wann er "auf wesentliche Weise" aufgerufen wird. Daher möchte ich ein einigermaßen konkretes Beispiel für dieses Phänomen durcharbeiten. Ich verstehe, dass das Ersetzen "wirklich" als das Axiom angesehen werden sollte, das eine transfinite Rekursion ermöglicht. Meiner Meinung nach tendiert die Kategorietheorie dazu, die Rekursion nicht in hohem Maße zu verwenden (obwohl sie mehr als andere Zweige der Mathematik viele Definitionen enthält, die zumindest auf den ersten Blick eine nicht triviale Komplexität der Abgabe aufweisen Formel$\phi(x,y,z,p,q)$ sagen, dass das Set $z$ und Funktionen $p: z \to x$ und $q: z \to y$ sind ein kategorisches Produkt der Sets $x,y$ ist syntaktisch $\Pi_1$und die Aussage, dass binäre Produkte in der Kategorie der Mengen existieren, ist syntaktisch $\Pi_3$ (Ignorieren von begrenzten Quantifizierern natürlich)).
Der folgende Satz ist meiner Meinung nach eine der bemerkenswerten Ausnahmen von der kategorietheoretischen Nichtverwendung der Rekursion:
Satz [Quillen] "Das Argument des kleinen Objekts": Let$\mathcal C$ eine lokal präsentierbare Kategorie sein und lassen $I \subseteq Mor \mathcal C$eine kleine Menge von Morphismen sein. Lassen$\mathcal L \subseteq Mor \mathcal C$ sei die Klasse der Rückzüge von transfiniten Kompositen von Cobase-Veränderungen von Nebenprodukten von Morphismen in $I$, und lass $\mathcal R \subseteq Mor \mathcal C$ umfassen diese Morphismen schwach rechts orthogonal zu den Morphsims von $I$. Dann$(\mathcal L, \mathcal R)$ist ein schwaches Faktorisierungssystem auf$\mathcal C$.
Den Beweis finden Sie im nlab . Grundsätzlich werden Faktorisierungen durch transfinite Rekursion konstruiert. Die Rekursion erscheint mir "wesentlich", da in jeder Bauphase neue Daten eingeführt werden.
Formalisierung:
Ich denke, dieser Satz und sein Beweis sind in MK einfach zu formalisieren, wo die kategorietheoretische Unterscheidung "klein / groß" als MKs Unterscheidung "Menge / Klasse" interpretiert wird. Ich fühle mich nicht qualifiziert zu kommentieren, ob der Beweis in NBG funktioniert, aber die Aussage macht zumindest unkompliziert Sinn.
Wenn es um die Formalisierung in ZFC geht, müssen wir hinsichtlich der kleinen / großen Unterscheidung Entscheidungen treffen:
Eine Möglichkeit besteht darin, ein "Universum" einzuführen. $V_\kappa$(was, wenn wir tatsächlich versuchen, in ZFC zu arbeiten, eine schwächere Art von Universum sein wird als gewöhnlich). Wir werden "klein" als "in" interpretieren$V_\kappa$". Wir werden" wirklich große Objekte "nicht berücksichtigen - alles, worüber wir sprechen, wird eine Menge sein - insbesondere wird jede Kategorie, über die wir sprechen, eine bestimmte Größe haben, auch wenn sie per se nicht" klein "ist. Wir werden es tun interpretiere "lokal präsentierbare Kategorie" als "$\kappa$-cocomplete, lokal $\kappa$-kleine Kategorie mit einem starken $\kappa$-klein, $\lambda$-präsentierbarer Generator für einige regelmäßige $\lambda < \kappa$"(Ich weiß nicht, ob es einen Unterschied macht, das zu sagen $V_\kappa$ denkt $\lambda$ ist ein regulärer Kardinal).
Eine andere Möglichkeit besteht darin, kein Universum einzuführen und "klein" einfach als "set-size" zu interpretieren. In diesem Fall muss jedes "große" Objekt, über das wir sprechen, aus kleinen Parametern definierbar sein. Wir definieren also eine Kategorie, die eine durch Parameter definierbare Klasse von Objekten, eine durch Parameter definierbare Klasse von Morphismen usw. umfasst. Dies mag restriktiv erscheinen, funktioniert jedoch im lokal darstellbaren Fall gut, da wir eine lokal darstellbare Kategorie definieren können$\mathcal C$ relativ zu den Parametern definiert werden $(\lambda, \mathcal C_\lambda)$ (wo $\lambda$ ist ein regulärer Kardinal und $\mathcal C_\lambda$ ist ein kleiner $\lambda$-cocomplete Kategorie), als die Kategorie von $\lambda$-Ind Objekte in $\mathcal C_\lambda$.
Für den vorliegenden Satz scheint Ansatz (2) sauberer zu sein, da die notwendige "Übersetzung" unkompliziert ist und der ursprüngliche Beweis ohne Modifikation funktionieren sollte. Ich denke, die Hauptnachteile von (2) kommen woanders hin. Zum Beispiel wird es wahrscheinlich eine heikle Angelegenheit sein, Sätze über die Kategorie lokal präsentierbarer Kategorien zu formulieren. Im Allgemeinen wird es verschiedene Theoreme über Kategorien geben, die saubere, konzeptionelle Formulierungen und Beweise haben, wenn die beteiligten Kategorien klein sind, die aber ärgerliche technische Änderungen erfordern, wenn die beteiligten Kategorien groß sind. Aus solchen Gründen werden Ansätze wie (1) eher für große kategorietheoretische Projekte bevorzugt.
Nehmen wir also an, wir folgen dem Ansatz (1). Die Frage wird dann:
Frage 1: Welche Art von Universum brauchen wir genau, um den obigen Satz nach dem folgenden Ansatz (1) zu formulieren und zu beweisen?
Frage 2: Wie viele solcher Universen gibt es bei ZFC garantiert?
Vermutlich wird die Antwort auf Frage 2 sein, dass es viele solcher Universen gibt - genug, um Dinge wie eine bestimmte Kategorie zu tun, an ein Universum zu übergeben, das groß genug ist, um diese Kategorie klein zu machen und den Satz für dieses Universum aufzurufen .
Frage 3: Wie weit müssen wir ins Unkraut gehen, um die Fragen 1 und 2 zu beantworten?
Müssen wir den Beweis des Satzes gründlich analysieren? Gibt es eine einfache Rubrik von Kriterien, die es uns ermöglicht, einen Blick auf den Beweis zu werfen und für 99% der Sätze wie diesen leicht zu sagen, dass er "bestanden" wird, ohne sich zu sehr mit Dingen zu befassen? Oder gibt es sogar ein formales Metatheorem, an das wir uns wenden können, sodass sogar ein Computer überprüfen kann, ob alles in Ordnung ist?
Antworten
Jacob Luries Kommentar gibt eine Antwort auf Frage 1. Unter der Annahme, dass die Schätzungen, die ich in meinem Kommentar gegeben habe, korrekt sind, reicht es aus, dies anzunehmen, um den Satz zu formulieren und zu beweisen
- $\kappa$ ist regelmäßig
und das
- für jeden $\mu < \kappa$gibt es $\rho < \kappa$ so dass $\mu \ll \rho$ (bedeutet, dass $\mu' < \mu, \rho' < \rho \Rightarrow (\rho')^{\mu'} < \rho$).
Vielleicht diese Eigenschaft von $\kappa$könnte als "Form" des Ersatzes angesehen werden. Aber wir haben wirklich zwei Bedingungen$\kappa$ die eher rein satztheoretisch als metamathematisch sind, so dass die Antwort auf Frage 1 viel sauberer ist, als ich angenommen hatte.
Dies ermöglicht es uns, Frage 2 zu beantworten. Vermutlich ist das Ergebnis, dass ZFC beweist, dass es sehr viele gibt $\kappa$ Erfüllung der beiden oben genannten Bedingungen.
Wenn es um Frage 3 geht, scheint es, dass wir bei diesem Ansatz tatsächlich ziemlich tief in den Beweis eintauchen müssen. Tatsächlich scheint es, dass wir, um diesen Ansatz durchzuführen, dem Beweis einen echten mathematischen Inhalt hinzufügen und tatsächlich eine stärkere Aussage beweisen müssen. Die weiteren Fragen werden dann
Wird es im Allgemeinen möglich sein, "die meisten" kategorietheoretischen Theoreme auf diese Weise zu "konstruieren", oder werden im Verlauf des Projekts "ZFC-ify-Kategorietheorie" andere Probleme auftauchen?
Wenn die Antwort auf (1) "Ja" lautet (oder wenn es im Allgemeinen "Nein" ist und wir unsere Aufmerksamkeit auf die Fälle beschränken, in denen es "Ja" ist), dann wäre "wie viel zusätzliche Arbeit" ein solches Projekt wirklich?
Ich vermute, dass die Antwort auf (1) lautet, dass bei der Verwendung der transfiniten Rekursion in der Kategorietheorie in der Tat in der Regel die Verwendung von Ersatz auf ähnliche Weise beseitigt werden kann, jedoch mehr Wichtig ist, dass ich den Punkt übersehen habe: Wie Jacob Lurie als Antwort auf die Frage von Peter Scholze argumentiert , haben die schwierigeren Probleme mit der ZFC-ifying-Kategorietheorie nicht mit der transfiniten Rekursion zu tun, sondern mit der Möglichkeit, frei zwischen "großen Kategorien" hin und her zu wechseln "und" kleine Kategorien "auf verschiedene Weise.
Ich vermute, dass die Antwort auf (2) lautet, dass es für "die meisten" kategorietheoretischen Verwendungen der transfiniten Rekursion eigentlich ziemlich einfach sein sollte, sie so zu "konstruieren", dass sie in ein "Babyuniversum" mit den Eigenschaften über oder passen etwas Ähnliches, und dass man mit ein wenig Übung die Fähigkeit entwickeln könnte, fast auf einen Blick zu überprüfen, ob es möglich ist, wenn auch immer noch Satz für Satz. Aber ich würde gerne als falsch erwiesen werden und einen Satz in der Kategorietheorie zeigen, bei dem ein solcher Ansatz fehlschlägt!
Schließlich bleibt die Frage offen, ob es einen "automatischeren" Weg gibt, dies alles zu tun - vielleicht mit einer schwächeren Schlussfolgerung als "unser Universum muss überhaupt keine Form von Ersatz befriedigen".