ケーススタディ：ZFCでQuillenの小さなオブジェクトの議論を定式化して証明するには何が必要ですか？
圏論の定理から宇宙への依存を取り除くことについてのペーター・ショルツェの興味深い質問に少し迷っています。特に、いつ置換が呼び出されるのか本当にわからないことを認めざるを得ません。「本質的な方法で」いつ呼び出されるかは気にしないでください。ですから、この現象のかなり具体的な例を見ていきたいと思います。私は、置換が「本当に」超限帰納法を可能にする公理として考えられるべきであることを理解しています。私の感覚では、圏論は再帰を強力な方法で使用しない傾向があります（ただし、他の数学の分野よりも多くの定義があり、少なくとも一応の複雑さは自明ではありません。たとえば、式$\phi(x,y,z,p,q)$ セットと言って $z$ と機能 $p: z \to x$ そして $q: z \to y$ セットのカテゴリ積です $x,y$ 構文的に $\Pi_1$、および集合の圏にバイナリ積が存在するというステートメントは構文的に $\Pi_3$ （もちろん、有界量化を無視します））。
次の定理は、圏論-非使用-再帰の注目すべき例外の1つだと思います。
定理[キレン]「小さなオブジェクト引数」：みましょう$\mathcal C$ ローカルで提示可能なカテゴリになり、 $I \subseteq Mor \mathcal C$射の小さなセットになります。しましょう$\mathcal L \subseteq Mor \mathcal C$ コベースの超限複合体のリトラクトのクラスである-射の余積の変化 $I$、そして $\mathcal R \subseteq Mor \mathcal C$ の射に弱く右直交する射を含む $I$。その後、$(\mathcal L, \mathcal R)$ある弱い因数分解システム上$\mathcal C$。
証明については、nlabを参照してください。基本的に、因数分解は超限帰納法によって構築されます。構築の各段階で新しいデータが導入されるため、再帰は私には「不可欠」に思えます。
形式化：
この定理とその証明は、圏論的な「小/大」の区別がMKの「集合/クラス」の区別として解釈されるMKで簡単に形式化できると思います。証明がNBGで機能するかどうかについてコメントする資格はないと思いますが、このステートメントは少なくとも簡単に理解できます。
ZFCでの形式化に関しては、大小の区別に関して選択することができます。
1つのオプションは「宇宙」を導入することです $V_\kappa$（これは、実際にZFCで作業しようとしている場合、通常よりも弱い種類の宇宙になります）。「小さい」は「$V_\kappa$「。私たちは「本当に大きなオブジェクト」を考慮しません-私たちが話すすべてがセットになります-特に、私たちが話すすべてのカテゴリは、それ自体が「小さい」でなくても、セットサイズになります。 「ローカルで提示可能なカテゴリ」を「$\kappa$-ローカルでcocomplete $\kappa$-強い小さなカテゴリ $\kappa$-小さい、 $\lambda$-いくつかの定期的なための見栄えの良いジェネレータ $\lambda < \kappa$「（それが違いを生むかどうかはわかりません $V_\kappa$ 考える $\lambda$ 正則基数です）。
もう1つのオプションは、ユニバースを導入せず、「小さい」を「セットサイズ」を意味すると解釈することです。この場合、私たちが話す「大きな」オブジェクトは、小さなパラメータから定義可能でなければなりません。したがって、パラメータで定義可能なオブジェクトのクラス、パラメータで定義可能な射のクラスなどで構成されるカテゴリを定義します。これは制限のように見えるかもしれませんが、ローカルで表示可能なカテゴリを定義できるため、ローカルで表示可能な場合は正常に機能します。$\mathcal C$ パラメータに関連して定義される $(\lambda, \mathcal C_\lambda)$ （どこ $\lambda$ 正則基数であり、 $\mathcal C_\lambda$ 小さいです $\lambda$-cocompleteカテゴリ）、のカテゴリとして $\lambda$-Indオブジェクト $\mathcal C_\lambda$。
さて、手元の定理については、必要な「変換」が簡単であるため、アプローチ（2）はよりクリーンに見えます。一度実行すると、元の証明は変更なしで機能するはずです。（2）の主な欠点は他のところにあると思います。たとえば、ローカルで提示可能なカテゴリのカテゴリに関する定理を定式化することは、おそらく微妙な問題になります。一般に、関連するカテゴリが小さい場合はクリーンで概念的な定式化と証明があり、関連するカテゴリが大きい場合は面倒な技術的変更が必要なカテゴリについては、さまざまな定理があります。（1）のようなアプローチが大規模な圏論的プロジェクトに好まれる傾向があるのはそのような理由のためです。
したがって、アプローチ（1）に従っていると仮定しましょう。その場合、質問は次のようになります。
質問1：アプローチ（1）に従って、上記の定理を定式化して証明するために、正確にどのような宇宙が必要ですか？
質問2：そのような宇宙はZFCによっていくつ存在することが保証されていますか？
おそらく、質問2の答えは、そのようなユニバースがたくさんあるということです-カテゴリが与えられた場合、そのカテゴリを小さくしてそのユニバースの定理を呼び出すのに十分な大きさのユニバースに渡すなどのことができるように十分です。
質問3：質問1と2に答えるには、雑草のどこまで行かなければなりませんか？
定理の証明を深く分析する必要がありますか？証明を一瞥することができる基準の簡単なルーブリックはありますか？このような定理の99％については、物事をあまり深く掘り下げることなく「合格」と簡単に言うことができますか？それとも、コンピューターでさえ問題がないことを確認できるように、私たちがアピールできる正式なメタ定理さえありますか？
回答
ジェイコブ・ルーリーのコメントは質問1に答えます。つまり、私のコメントで与えた見積もりが正しいと仮定すると、定理を定式化して証明するには、次のように仮定するだけで十分です。
- $\kappa$ 定期的です
そしてそれ
- すべてのための $\mu < \kappa$、 が存在します $\rho < \kappa$ そのような $\mu \ll \rho$ （つまり $\mu' < \mu, \rho' < \rho \Rightarrow (\rho')^{\mu'} < \rho$）。
おそらくこのプロパティの $\kappa$交換の「形式」と見なされる場合があります。しかし、実際には、私たちが持っているのは2つの条件です$\kappa$ これは超数学ではなく純粋に集合理論であるため、質問1の答えは私が思っていたよりもはるかにクリーンです。
これにより、質問2に対処できます。おそらく、結果として、ZFCは、たくさんのことがあることを証明します。 $\kappa$ 上記の2つの条件を満たす。
質問3に関しては、このアプローチでは、実際に証拠をかなり深く掘り下げる必要があるように思われます。実際、このアプローチを実行するためには、いくつかの本物の数学的内容を証明に追加し、実際により強力なステートメントを証明する必要があるようです。その後、さらに質問がなります
このようにして「ほとんどの」圏論定理を「構築」することは一般的に可能でしょうか、それとも「ZFC圏論」プロジェクトの過程で他の問題が現れるのでしょうか。
（1）の答えが「はい」である場合（または一般的に「いいえ」であり、「はい」の場合に注意を限定する場合）、そのようなプロジェクトは実際に「どれだけの余分な作業」になるでしょうか。
私の推測では、（1）の答えは、圏論での超限帰納法の使用に関しては、実際、これと同様の方法で置換の使用を排除できる場合が多いということですが、それ以上のことです。重要なことに、私は要点を見逃しました。ジェイコブ・ルーリーがペーター・ショルツェの質問に答えて主張するように、ZFC化圏論の厄介な問題は、超限帰納法ではなく、「大きな圏論」の間を自由に行き来できることです。さまざまな方法で「および「小さなカテゴリ」。
私の推測では、（2）の答えは、超限帰納法の「ほとんど」の圏論的使用については、上記のプロパティを持つ「赤ちゃんの宇宙」に収まるように「構築」するのは実際にはかなり簡単なはずです。似たようなもので、少し練習すれば、定理ごとではありますが、それが可能であることをほぼ一目で確認できるようになります。しかし、私は間違っていることが証明され、この種のアプローチが失敗する圏論の定理を示したいと思います！
最後に、これは、これらすべてを行う「より自動化された」方法があるかどうかを未解決の問題として残します。おそらく、「私たちの宇宙は、いかなる形の置換もまったく満たす必要がない」よりも結論が弱いでしょう。