先週の話題を引っぱって、圏のサイズ問題なんですが、圏のサイズを何種類か定義して、それに伴って現れる“圏の圏”に名前を付けておきます。
Uがグロタンディーク宇宙である条件に、ω∈U を含めます。ωは自然数の集合Nと同じです。ωは可算無限基数の意味ですが、Nと思ってかまいません。
ロー〈Zhen Lin Low〉に従って、ω∈U を外した場合はプレ宇宙〈pre-universe〉と呼びます（「グロタンディーク宇宙って何なんだ？」参照）。
「あなたはこの公理を信じますか」で引用したレヴィ〈Paul Blain Levy〉の論文 "Formulating Categorical Concepts using Classes" に（だいたい）従って、圏のサイズを分類します。
Uを単一宇宙公理として、ZFC+UはZFCの公理系に単一宇宙公理Uを加えたものです。
- [U 単一宇宙公理] グロタンディーク宇宙Uが存在する。
VをZFC+Uのモデルとして、単一宇宙公理で存在が保証されたグロタンディーク宇宙Uを固定して考えます。UはZFC（ZFC+Uではない）のモデルになっています。
圏Cの対象の集合|C|と、a, b∈|C| ごとのホムセットC(a, b)達のサイズに条件を付けて、圏を分類します。“圏のサイズ”とは、単独のサイズではなくて、対象集合のサイズとホムセット達のサイズの組み合わせで定義します。
Vの集合xがUに関して小さい（U-小〈U-small〉）とは、x∈U のことだとします（他の定義もありますが）。また、Vの集合yがUに関してクラス（U-クラス〈U-class〉）であるとは、y⊆U のことだとします（他の定義もありますが）。U-クラスであることも、サイズに関する制約とみなせます。
レヴィによる、サイズに基づく圏の分類を表にまとめます。
| Cに関する条件→ | |C|∈U | |C|⊆U | C(a, b)∈U | C(a, b)⊆U |
|---|---|---|---|---|
| 小〈small〉 | ◎ | ○ | ◎ | ○ |
| 局所小〈locally small〉 | - | - | ◎ | ○ |
| 軽〈light〉 | - | ◎ | ◎ | ○ |
| 穏和〈moderate〉 | - | ◎ | - | ◎ |
二重丸'◎'は、定義により成立する条件、丸'○'は定義から導かれる条件です。この定義のまんまで話がスムーズに進むかは定かでないのですが、目安と考えてください。
特定のサイズ条件を満たす圏の全体からなる“圏の圏”は次のように書くことにします。
- CatU -- Uに関して小さい圏〈small categories〉の圏
- CATU-- Uに関して軽い圏〈light categories〉の圏
- ℂATU -- Uに関して穏和な圏〈moderate categories〉の圏
- ℂ𝔸𝕋 -- 無条件な圏の圏
ℂ𝔸𝕋は、外側の大宇宙V内で定義される圏の圏で、Vから見れば小さい圏の圏なので、
- ℂ𝔸𝕋 = CatV
と書けます。上記のように字種・字体を変えて区別*1すれば、小宇宙Uは省略してもかまいません。
- Cat = CatU
- CAT = CATU
- ℂAT = ℂATU
複数の小宇宙〈グロタンディーク宇宙〉を考えているときは、混乱してしまうので単純な省略はできません。
サイズの問題は、（僕が）想像していたより複雑で、ボンヤリ考えているのはやっぱりマズイなと思いました。小さい圏の圏をCatと書くのはよく使われる記法・習慣ですが、大きい圏に関しては、その“大きさ”が分析されてなくて、雰囲気的にCATを使ってしまうこともあるでしょう。少なくとも僕は、あまり考えずに“大きいかも知れない圏の圏”をCATと書いてました。上記のレヴィのCATの意味か、ℂ𝔸𝕋の意味か、あるいは別な小宇宙U'に対するCatU'か、区別してなかったですね。
状況設定をハッキリさせないと、例えば「CATはデカルト閉か？」のような問に答えることができず、安易な推論でしくじりそうです。やっぱり、ボンヤリ・雰囲気はダメですね。
*1:白抜きの太字は黒板文字〈blackboard bold〉と呼ばれます。Unicodeの文字番号は、白抜きC（複素数用） U+2102, 白抜きA U+1D538, 白抜きT U+1D54B です。
