最近、カートメル／ヴォエヴォドスキーのC-システム（「C-システム、分裂ディスプレイクラス、カートメルツリー構造」参照）に興味を持っています。で、次の論文を眺めてみました。
- [Voe14-15]
- Title: A C-system defined by a universe category
- Author: Vladimir Voevodsky
- Submitted: 28 Sep 2014 (v1), 29 Jul 2015 (v3)
- Pages: 33p
- URL: https://arxiv.org/abs/1409.7925
最初の数ページをチラ見しただけなんですが ‥‥ ウーム、感慨深い。
上記論文でヴォエヴォドスキーが定義している“宇宙”は、（ひとつの解釈として）普遍的なグロタンディーク構成だとみなせます。宇宙を備えた圏から作られるC-システムはパルムグレンの複前層の圏（「パルムグレンによる、型理論の複前層モデル」参照）と一致するようです。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\In}{\text{ in }}`$
内容：
ヴォエヴォドスキーの宇宙圏
冒頭で参照したヴォエヴォドスキー論文の "Definition 2.1" において“宇宙構造”が、"Definition 2.6" において“宇宙圏”が定義されています。もちろん、天文学や宇宙物理の話ではありません。
圏 $`\cat{C}`$ 内の対象 $`U`$ と、射 $`p:\widetilde{U} \to U \In \cat{C}`$ がとある性質を満たすとき、$`U`$ を中心とした構造を宇宙構造〈universe structure〉と呼びます。そして、$`(\cat{C}, p, \mrm{pt})`$ が宇宙圏〈universe category〉だとは、$`p`$ が宇宙構造を定義する射で、$`\mrm{pt}`$ が特定された終対象であることです。
ヴォエヴォドスキーは、宇宙圏を公理的に定義しています。いきなり宇宙圏の公理的定義を出されても「はぁ？」という気分になるでしょう。宇宙圏のオフィシャルな公理的定義は後回しにして、宇宙圏の具体例を出します。
$`U \in U'`$ を2つのグロタンディーク宇宙とします。2つのグロタンディーク宇宙から作られた2つの集合圏を次のように書きます。
$`\quad {\bf Set}_U\\
\quad {\bf Set}_{U'}
`$
デフォルトの宇宙を $`U`$ 、デフォルトより一段大きな宇宙を $`U'`$ と考えて、次の略記をします。
$`\quad {\bf Set} := {\bf Set}_U\\
\quad {\bf SET} := {\bf Set}_{U'}
`$
大きな集合圏 $`{\bf SET}`$ は、小さい集合圏の対象達の集合を1つの対象として含みます。つまり、次が成立します。
$`\quad |{\bf Set}| = U \in |{\bf SET}|`$
$`{\bf SET}`$ は、その内部に“宇宙”と呼ぶべき特定の対象を備えています。特定された宇宙対象〈universe object〉 $`U`$ を備えた圏が宇宙圏です。とはいえ、宇宙が宇宙である条件・資格を定義しないことには、「$`U`$ は宇宙である」と言っても説得力がありません。
「圏の対象が宇宙であるとは何だろう？」という問題は、何度か考えたことがあります。ラムダ計算の立場だと、計算的な万能対象〈universal object〉だと言えそうです。
しかし、ヴォエヴォドスキーが採用した宇宙の定義は計算的万能対象とはまったく違ったものでした。付点集合〈pointed set〉から特定された点〈要素〉を忘れる写像の機能・メカニズムに注目したのです。
付点集合の圏を $`{\bf Set}_\bullet`$ とします。$`{\bf Set}_\bullet`$ の対象は、集合 $`X`$ とその要素 $`a`$ のペア $`(X, a)`$ で、射は特定された点〈要素〉を保存する写像です。$`(X, a) \mapsto X`$ という忘却関手があります。忘却関手は $`U`$ と書くのが習慣ですが、今回は宇宙と区別が付かなくなるので、忘却関手を $`P`$ とします。
$`\quad P:{\bf Set}_\bullet \to {\bf Set} \In {\bf CAT}`$
$`P`$ は関手なので、大きな圏達からなるとても大きな2-圏（n-圏の大きさ〈サイズ〉は「変換手意味論とブラケット記法 // n-圏」参照）の1-射ですが、対象部分〈object part〉をとれば、大きな集合達の1-圏の射になります。
$`\quad P_\mrm{obj}: |{\bf Set}_\bullet| \to |{\bf Set}| \In {\bf SET}`$
次のように記号を置き換えます。
$`\quad p: \widetilde{U} \to U \In {\bf SET}\\
\text{Where}\\
\quad p := P_\mrm{obj}\\
\quad \widetilde{U} := |{\bf Set}_\bullet|\\
\quad U = |{\bf Set}|
`$
写像 $`p`$ は付点集合の特定された点を忘れる忘却写像です。
$`p:\widetilde{U} \to U \In {\bf SET}`$ は特筆すべき性質を持ちます。それは、任意の写像 $`f:X \to U \In {\bf SET}`$ に対してプルバック四角形が作れることです。以下の図式の点線・疑問符の部分を埋めることができるのです。
$`\quad \xymatrix{
{?} \ar@{.>}[r] \ar@{.>}[d]
\ar@{}[dr]|{\text{p.b.}}
& \widetilde{U} \ar[d]^p
\\
X \ar[r]_f
& U
}\\
\quad \In {\bf SET}
`$
$`U`$ は小さい集合達のクラス〈大きな集合〉なので、写像 $`f`$ は、集合（小さくないかも知れない）$`X`$ をインデキシング集合とするファミリー〈indexed family of sets〉です。上の図式の疑問符の所を埋める集合は、ファミリー $`f`$ のシグマ型です。
シグマ型も、このブログでよく取り上げている話題です。
シグマ型に関する過去記事をひとつだけ挙げるなら以下(↓)。色々と修正が入って汚いのですが、そのドタバタも含めて参考になるかも知れません。
上の図式の点線・疑問符を埋めたプルバック四角形は次のようになります。
$`\quad \xymatrix{
{\sum_{x\in X}f(x)} \ar[r]^-{f^\uparrow} \ar[d]_{\pi^f}
\ar@{}[dr]|{\text{p.b.}}
& \widetilde{U} \ar[d]^p
\\
X \ar[r]_f
& U
}\\
\quad \In {\bf SET}
`$
ここで：
- $`X`$ ： ファミリーのインデキシング集合（写像の域）
- $`f`$ ： ファミリー（写像）
- $`\sum_{x\in X}f(x)`$ ： ファミリーのシグマ型
- $`\pi^f`$ ： シグマ型の射影、依存ペア $`(x, a) \text{ where }a\in f(x)`$ に、$`x\in X`$ を対応させる。
- $`f^\uparrow`$ ： シグマ型の要素である依存ペア $`(x, a) \text{ where }a\in f(x)`$ に、付点集合 $`(f(x), a)`$ を対応させる写像
このプルバック四角形は、シグマ型の圏論的な特徴付けになっています。それはまた、宇宙構造 $`p:\widetilde{U} \to U`$ の特徴付けでもあります。宇宙構造とは、シグマ型を作り出すメカニズムである、ってことになります。
以上の話を、$`{\bf SET}`$ から $`{\bf CAT}`$ に移して考えると、次のプルバック四角形の議論になります。
$`\quad \xymatrix{
\mrm{el}(D) \ar[r]^-{D^\uparrow} \ar[d]_{\pi^D}
\ar@{}|{\text{p.b.}}
& {{\bf Set}_\bullet} \ar[d]^{P}
\\
\cat{C} \ar[r]_D
& {\bf Set}
}\\
\quad \In {\bf CAT}
`$
ここで：
- $`\cat{C}`$ ： 余前層のベース圏（関手の域）
- $`D`$ ： 余前層（関手、あるいは形状が $`\cat{C}`$ である図式）
- $`\mrm{el}(D)`$ ： 余前層の要素の圏
- $`\pi^D`$ ： 要素の圏の射影（関手）、依存ペア $`(x, a) \text{ where }a\in D(x)`$ に、$`x\in X`$ を対応させる。
- $`D^\uparrow`$ ： 要素の圏の対象である依存ペア $`(x, a) \text{ where }a\in D(x)`$ に、付点集合 $`(D(x), a)`$ を対応させる関手
前層／余前層に対する要素の圏は、グロタンディーク構成の特別なものです。言い方を変えると、要素の圏を一般化するとグロタンディーク構成（の平坦化圏）になります。
10年以上前、宇宙構造の観点はまったくなかったのですが、要素の圏やグロタンディーク構成に伴うプルバック四角形について考えたことはあります。
- 普遍的なグロタンディーク構成？ (2013-02-01)
グロタンディーク構成の普遍性（プルバック四角形を形成すること）が、宇宙の定義に採用されるとは思ってもみなかったですね ‥‥ ウーム、感慨深い。
C-システムとパルムグレンの複前層の圏
前節で出した宇宙構造 $`p:\widetilde{U} \to U \In {\bf CAT}`$ は、具体的な宇宙構造でした。ヴォエヴォドスキーの宇宙構造／宇宙圏の定義は抽象的・公理的です。
圏 $`\cat{C}`$ とそのなかの射 $`p:\widetilde{U} \to U \In \cat{C}`$ （もはや具体的な射ではない）が、任意の（しかし余域は $`U`$ である）射 $`f`$ に対して次のプルバック四角形を作れるなら、$`p`$ は、抽象的・公理的な意味で宇宙構造〈universe structure〉です。
$`\quad \xymatrix{
{?} \ar@{.>}[r] \ar@{.>}[d]
\ar@{}[dr]|{\text{p.b.}}
& \widetilde{U} \ar[d]^p
\\
X \ar[r]_f
& U
}\\
\quad \In \cat{C}
`$
点線・疑問符を埋めたプルバック四角形を、ヴォエヴォドスキーは次のように書いています。
$`\quad \xymatrix{
(X; f) \ar[r]^-{Q(f)} \ar[d]_{p_{X,f}}
\ar@{}[dr]|{\text{p.b.}}
& \widetilde{U} \ar[d]^p
\\
X \ar[r]_f
& U
}`$
前節の具体例と対応させれば、$`(X; f)`$ がシグマ型に対応し、$`p_{x, f}`$ がシグマ型の射影に対応します（[追記]「射影」に関する注意は「型理論に出てくる第一射影と第二射影」参照[/追記]）。しかし、宇宙構造は抽象的・公理的に定義されているので、他の事例もあります。ヴォエヴォドスキーは、群論からの例を出しています。
圏 $`\cat{C}`$ の特定された終対象も添えた $`(\cat{C}, p, \mrm{pt})`$ が抽象的・公理的に定義された宇宙圏〈universe category〉です。$`{\bf 1}`$ を特定された単元集合とすれば、$`({\bf SET}, p, {\bf 1})`$ は宇宙圏の具体例になります。
一般的な宇宙圏 $`(\cat{C}, p, \mrm{pt})`$ に対してヴォエヴォドスキーは、プルバック四角形による $`(X ; f)`$ の構成を繰り返して、次のような対象を定義しています。
$`\quad (X; f_1, \cdots, f_n) := (\cdots ((X; f_1);f_2)\cdots ; f_n)`$
ンッ？ この構成法は ‥‥ パルムグレンの複前層の作り方（「パルムグレンによる、型理論の複前層モデル」参照）と同じじゃないか。
ヴォエヴォドスキー論文の続きをチラ見すると、ヴォエヴォドスキーは宇宙圏からC-システム（「C-システム、分裂ディスプレイクラス、カートメルツリー構造」参照）$`\mrm{CC}(\cat{C}, p)`$ を作っています。宇宙圏から作られたC-システムは、どうやらパルムグレンの複前層の圏と同じ圏のようです。
ヴォエヴォドスキーは、公理的なセッティングでC-システムを構成しているので、その意味でパルムグレンより抽象的・一般的と言えます。しかし一方、パルムグレンは圏と前層から出発しているので、集合とファミリーがベースのヴォエヴォドスキーより複雑なケースを扱っているとも言えます。
セットアップに若干の差があるのですが、ヴォエヴォドスキーもパルムグレンも、ほぼ同じ方法でほぼ同じ構造を定義しています。ヴォエヴォドスキー論文が2014年から2015年、パルムグレン論文(↓)が2013年から2016年、同じ時期で、互いに参照もないので、独立な仕事なのでしょう。‥‥ ウーム、感慨深い。
- [Pal13-16]
- Title: The Grothendieck construction and models for dependent types
- Author: Erik Palmgren
- Date: March 8, 2013; minor editing May 28, 2016
- Pages: 23p
- URL: https://staff.math.su.se/palmgren/iterated_presheaves_and_dependent_types_v8.pdf
悲しい偶然ですが、これらの論文を出した少し後に、ヴォエヴォドスキーもパルムグレンも亡くなっています（ヴォエヴォドスキー 1966-2017、パルムグレン 1963–2019）。残念です。
