昨日「階層的な圏論的宇宙・楽観的暫定版」において、グロタンディーク宇宙の無限系列 U0, U1, U2, ... があったらいいな、という話を書きました。
圏論の宇宙に関する資料はなかなか見つからないのですが、ロー〈Zhen Lin Low〉の次の論文があります。
- Title: Universes for category theory
- Author: Zhen Lin Low
- Pages: 27p
- URL: https://arxiv.org/abs/1304.5227
集合論と圏論の関係を論じるときは、到達可能圏〈accessible category〉や局所表現可能圏〈locally presentable category〉などの知識が必要になります。ここら辺を僕は避けてきたので、ローの論文は全然読めません。
技術的議論は置いといて（分かんないので）、ロー論文冒頭に出てくる宇宙公理〈universe axiom〉の意味を考えてみます。単に宇宙公理というより、その内容からは、多宇宙公理〈multiverse axiom〉とか入れ子宇宙公理〈nested universes axiom〉と呼ぶのがふさわしいでしょう。
入れ子宇宙を可能とするには、2種の（公理的）集合論が必要です。ひとつは、外の宇宙、あるいは大宇宙を規定する集合論です。これはベース集合論〈base set theory〉と呼びましょう。もうひとつは、圏論のための小宇宙を規定する圏の集合論〈set theory for categories〉です。
ベース集合論としては、ZFC〈Zermelo–Fraenkel + Choice〉集合論が圧倒的によく使われますが、他にも集合論はあります。
- マックレーン集合論〈Mac Lane set theory〉
- モース／ケリー集合論〈Morse–Kelley set theory〉
- フォン・ノイマン／ベルナイス／ゲーデル集合論〈von Neumann–Bernays–Gödel set theory〉
- タルスキー／グロタンディーク集合論〈Tarski–Grothendieck set theory〉
マックレーン集合論に関する短い解説は見当たりませんが、長い（128ページ）論文なら、"The strength of Mac Lane set theory"があります。
圏の集合論は、一人前の集合論というよりは、ベース集合論の宇宙（大宇宙）のなかで、圏論を展開するためのクラスを定義する公理系のことです。通常、この目的にはグロタンディーク宇宙の公理系が使われますが、必要に応じて他のバリアントがあってもいいでしょう。
さて、ベース集合論の宇宙をVとして、VのサブクラスUで圏の集合論の公理を満たすものを圏論の宇宙〈universe for category theory〉、または小宇宙〈small universe〉と呼びましょう。この状況で、宇宙公理（多宇宙公理、入れ子宇宙公理）とは次のものです。
- Vの任意の集合x（x∈V）に対して、x∈Uであって、U∈V である小宇宙Uが存在する。
これは非常に強い公理に思えます。Uが十分に強いなら何でも出来ちゃいそう。
例えば、xとして自然数の集合Nを取ると、Nを要素とする小宇宙U0が取れます。宇宙公理からU0はVの集合なので、U0∈U1 である小宇宙U1が取れます。この過程を続ければ、小宇宙の無限系列が作れて、「階層的な圏論的宇宙・楽観的暫定版」の願望はアッサリとかなえられることになります。
宇宙公理が他の公理と矛盾しないのか、あるいは、宇宙公理は他の公理から導けるのか（実は定理なのか）あたりが問題になります。もちろんこれは、ベース集合論と圏の集合論の取り方に依存します。
仮に、ベース集合論が宇宙公理を満たすとしても、小宇宙の拡張／取り替えなどで圏論側の問題が出てくるから、そう簡単じゃないよ、てのがロー論文の主張のようです。技術的困難や注意事項が色々とありそうですが、しかしそれでも、「階層的な圏論的宇宙・楽観的暫定版」で述べたような楽観主義を否定する根拠はないように思えます。いずれは、入れ子の宇宙を定義して安全に取り扱う処方箋が確立されるんじゃないのかな（と、これも楽観主義）。
