大きい包括クランの3つの例 - 檜山正幸のキマイラ飼育記 (はてなBlog)

クランやC-システムは、型理論の構文構造の定式化のために案出されたものです。構文構造の定式化には、大きい集合は出てこないので、クランやC-システムは原則的に小さい圏です。しかし、具体例を考える場合には、むしろ大きな圏まで含めたほうが例を作りやすいです。

この記事では、「テレスコープと包括クラン」で述べた包括クランに関して、大きな圏を台とする3つの具体例を構成します。これらの具体例達は相互に深く関係しています。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\u}[1]{\underline{#1}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\In}{\text{ in }}
%\newcommand{\Imp}{\Longrightarrow} % for meta prop
\newcommand{\hyp}{ \text{－} }
\newcommand{\twoto}{\Rightarrow }
`$

内容：

クラン達の圏
包括構造の定義
包括クラン達の圏
例1：集合達の包括クラン
例2：圏達の包括クラン
例3：ファミリー達の包括クラン
3つの具体例の関係

クラン達の圏

クランの定義は、以下の過去記事を参照してください。

クラン、ファイブレーション、スパン

クラン $`\cat{C}`$ を次のように書きます。

$`\quad \cat{C} = (\u{\cat{C}}, \mbf{1}_\cat{C}, \cat{P}_\cat{C})`$

記号の乱用をするときは、台圏 $`\u{\cat{C}}`$ を $`\cat{C}`$ と書きます。下付きの $`{_\cat{C}}`$ は適宜省略します。ファイブレーションクラスを $`\cat{P}`$ と書いているのは、ファイブレーションを射影〈projection〉とも呼ぶからです。ファイブレーションクラス $`\cat{P}`$ は、必要に応じて $`\cat{C}`$（正確には $`\u{\cat{C}}`$）の部分圏とみなします。

$`\cat{C}`$ と $`\cat{D}`$ がクランだとして、関手 $`F:\u{\cat{C}}\to \u{\cat{D}}`$ がクランのあいだの準同型射〈homomorphism〉だとは、次のことだとします。

$`F(\mbf{1}_\cat{C}) = \mbf{1}_\cat{D}`$
$`p \in \cat{P}_\cat{C}`$ ならば $`F(p)\in \cat{P}_\cat{D}`$ である。

クランの準同型射の結合（関手としての結合）は再びクランの準同型射だし、恒等関手はクランの準同型射なので、クラン達と準同型射達は圏を形成します。

ジョイアル〈Andre Joyal〉のオリジナルの定義では、クランは「小さい」とは言ってないようですが、フレイ〈Jonas Frey〉などは明示的に「小さい」を定義に含めています。ここでは、小さいクラン達の圏を $`\mbf{Clan}`$ と書くことにします。大きい（必ずしも小さくない）クラン達の圏は $`\mbf{CLAN}`$ とします。集合圏の上にクラン構造を載せたものは大きいクラン（$`\mbf{CLAN}`$ の対象）になります。

包括構造の定義

ジェイコブス〈Bart Jacobs〉の包括構造〈comprehension structure〉／包括圏〈comprehension category〉は、型理論的圏の鮮やかな定式化ですが、いかんせん抽象的過ぎます。そこで、アンパック（具体的な構成素に分解）して定義を書き下すのですが、そうすると複雑で見通しの悪い定義になります。アンパックの宿命だと言えます。

ジェイコブスの意味での、圏 $`\cat{C}`$ 上の包括構造は次の図式で定義されます。

$`\quad \xymatrix{
\cat{E} \ar[r]^-{\gamma} \ar[d]_\pi
& \mrm{Arr}(\cat{C}) \ar[d]^{\mrm{Cod}}
\\
\cat{C} \ar@{=}[r]
&\cat{C}
}\\
\quad \text{commutative }\In \mrm{CAT}
`$

包括構造の条件〈法則 | 公理〉は次です。

$`\pi : \cat{E}\to \cat{C}`$ は、ファイバー付き圏〈グロタンディーク・ファイブレーション | 圏のファイブレーション〉である。
$`\mrm{Cod} : \mrm{Arr}(\cat{E})\to \cat{C}`$ は、アロー圏〈バンドルの圏 | 可換四角形の圏〉のコドメイン関手である。
関手 $`\gamma : \cat{E} \to \mrm{Arr}(\cat{C})`$ は、デカルト関手〈Cartesian functor〉である。

ファイバー付き圏、デカルト関手、アロー圏などについては、以下の過去記事達（古い順）に説明があります。とりあえず最新の2つの記事（7番, 8番）を読んでみてください（それで十分かも知れない）。

包括構造を備えた圏が包括圏です。記号の乱用で、包括圏とその台圏を同じ記号 $`\cat{C}`$ で表します。包括圏の定義にクラン構造が必須というわけではありません。

包括構造のファイバー付き圏 $`\pi`$ が離散ファイブレーションの場合に、包括圏 $`\cat{C}`$ の定義をアンパックすると、包括圏の構成素は以下の4つになります。$`\sum(\hyp \mid \hyp)`$ は、シグマ型（集合族の総和）を表します。

台圏〈underlying category〉： $`\cat{C}`$ （記号の乱用で、包括圏全体も $`\cat{C}`$ と書く）
エス関手〈ess functor〉： $`\msc{S}_\cat{C}: \cat{C}^\op \to \mbf{Set}\In \mbf{CAT}`$
コンテキスト拡張演算〈context extension operator〉： $`\mrm{CExt}_\cat{C}: \sum(\Gamma\in |\cat{C}| \mid \msc{S}_\cat{C}(\Gamma)) \to |\cat{C}|\In \mbf{SET}`$
標準射影〈canonical projection〉： $`\rho_\cat{C}: \sum(\Gamma\in |\cat{C}| \mid \msc{S}_\cat{C}(\Gamma) ) \to \mrm{Mor}(\cat{C})\In \mbf{SET}`$
標準プルバック四角形〈canonical pullback square〉： $`\mrm{CPBSq}_\cat{C} : \sum( \varphi \in \mrm{Mor}(\cat{C}) \mid \msc{S}_\cat{C}(\mrm{cod}(\varphi))) \to \mrm{Mor}(\mrm{Arr}(\cat{C}))\In \mbf{SET}`$

下付きの $`{_\cat{C}}`$ は適宜省略します。$`\mrm{CExt}(\Gamma, A)`$ は $`\Gamma\cdot A`$ と書きます。$`\rho(\Gamma, A)`$ は $`\rho^{\Gamma, A}`$ と書きます。

これらの構成素達を使った包括圏の定義は、先に述べたように“複雑で見通しの悪い定義”になります。ゴチャゴチャした感じで、人により場合により述べ方の差があります。包括圏を定義する法則〈公理〉達を3つのグループに分けて考えると少しスッキリします。

構成素達の相互関係
デカルト性〈Cartesianess〉
関手性〈functoriality〉

2番目と3番目は、ジェイコブスの定義の $`\gamma`$ がデカルト関手であることに対応します。

構成素達の相互関係を述べるには、可換四角形（アロー圏の射）の各部を次のように呼ぶと約束しましょう。

$`\quad \xymatrix{
\mrm{UpperLeft} \ar[r]^{\mrm{top}} \ar[d]_{\mrm{left}}
&\mrm{UpperRight} \ar[d]^{\mrm{right}}
\\
\mrm{LowerLeft} \ar[r]_{\mrm{bottom}}
&\mrm{LowerRight}
}`$

$`S := \mrm{CPBSq}(\varphi, B)`$ と置いたとき、可換四角形 $`S`$ の各部は次のようになります（箇条書きの下の図も参照）。

$`\mrm{LowerLeft}(S) = \Gamma = \mrm{dom}(\varphi)`$
$`\mrm{LowerRight}(S) = \Delta = \mrm{cod}(\varphi)`$
$`\mrm{UpperRight}(S) = \Delta\cdot B = \mrm{cod}(\varphi)\cdot B`$
$`\mrm{bottom}(S) = \varphi`$
$`\mrm{right}(S) = \rho^{\Delta, B} = \rho^{\mrm{cod}(\varphi), B}`$
$`\mrm{UpperLeft}(S) = \Gamma\cdot (\msc{S}(\varphi)(B) ) = \mrm{dom}(\varphi)\cdot (\msc{S}(\varphi)(B) )`$
$`\mrm{left}(S) = \rho^{\Gamma, \msc{S}(\varphi)(B)} = \rho^{\mrm{dom}(\varphi), \msc{S}(\varphi)(B)}`$

$`\quad \xymatrix{
{\Gamma\cdot (\msc{S}(\varphi)(B) )}\ar[r] \ar[d]_{\rho^{\Gamma, \msc{S}(\varphi)(B)} }
&{\Delta \cdot B} \ar[d]^{\rho^{\Delta, B}}
\\
\Gamma \ar[r]_{\varphi}
&\Delta
}\\
\quad \text{commutative }\In \cat{C}
`$

この相互関係の記述は、人により記法／言い回しが変わります。記法／言い回しの違いでゴチャゴチャ・バラバラな印象を受けます。それは印象だけです。

次にデカルト性〈Cartesianess〉の記述は次のとおり。

可換四角形 $`\mrm{CPBSq}(\Gamma, A)`$ はプルバック四角形である。

関手性〈functoriality〉は以下のようになります（下の図も参照）。

$`\quad \mrm{CPBSq}(\varphi; \psi, C)
= \mrm{CPBSq}(\varphi, \Delta\cdot(\msc{S}(\psi)(C) ) ) ;
\mrm{CPBSq}(\psi, C )\\
\quad \mrm{CPBSq}(\id_\Gamma, A) = \id_{\rho^{\Gamma, A}}
`$

以下の $`\text{c.p.b.}`$ は canonocal pullback の意味。

$`\quad \xymatrix{
\cdot \ar[r] \ar[d]
\ar@{}[dr]|{\text{c.p.b.}}
& \cdot \ar[r] \ar[d]
\ar@{}[dr]|{\text{c.p.b.}}
&{\Sigma\cdot C} \ar[d]
\\
\Gamma \ar[r]_\varphi
& \Delta \ar[r]_\psi
& \Sigma
}\\
\quad \In \cat{C}
`$

以上が、離散ファイブレーションの包括圏の定義です。型理論における定式化では、離散ファイブレーションの包括圏で十分なことが多いです。

包括クラン達の圏

「テレスコープと包括クラン」において、クランの上に拡張包括構造を載せたモノとして包括クラン〈comprehension clan〉を定義しました。

包括クラン $`\cat{C}`$ の台クランが小さい場合は、そのエス関手は通常の前層だとします。

$`\quad \msc{S}_\cat{C} : \cat{C}^\op \to \mbf{Set} \In \mbf{CAT}`$

台クランが大きい（必ずしも小さくない）場合、エス関手の値は大きい集合を許すとします。

$`\quad \msc{S}_\cat{C} : \cat{C}^\op \to \mbf{SET} \In \mathbb{CAT}`$

2つの包括クラン $`\cat{C},\cat{D}`$ のあいだの準同型射は、台クランのあいだの準同型射 $`F`$ と、次のような自然変換 $`\Phi`$ のペアです。以下のアスタリスク（'$`*`$'）は、関手の図式順結合記号です。また、$`F^\op : \cat{C}^\op \to \cat{D}^\op`$ です*1。

$`\quad \Phi :: \msc{S}_\cat{C} \twoto F^\op *\msc{S}_\cat{D} : \cat{C}^\op \to \mbf{Set} \In \mbf{CAT}`$

これは、小さい包括クランの場合であって、大きい包括クランのあいだの準同型射なら次のようです。

$`\quad \Phi :: \msc{S}_\cat{C} \twoto F^\op *\msc{S}_\cat{D} : \cat{C}^\op \to \mbf{SET} \In \mathbb{CAT}`$

包括クランのあいだの準同型射は、拡張包括構造の構成素をすべて厳密に保つことを要求します。この要求を具体的に書き下すと以下のようです。

コンテキスト拡張演算〈context extension operator〉の保存：

$`\text{For } \Gamma \in |\cat{C}|, A \in \msc{S}_\cat{C}(\Gamma)\\
\quad F(\Gamma \cdot A) = F(\Gamma)\cdot \Phi_\Gamma(A)
`$

標準射影〈canonical projection〉の保存：

$`\text{For } \Gamma \in |\cat{C}|, A \in \msc{S}_\cat{C}(\Gamma)\\
\quad F(\rho_\cat{C}^{\Gamma, A}) = \rho_\cat{D}^{F(\Gamma), \Phi_\Gamma(A)}
`$

標準プルバック四角形〈canonical pullback square〉の保存：

$`\text{For } \varphi : \Gamma \to \Delta \In \cat{C}, B \in \msc{S}_\cat{C}(\Delta)\\
\quad F_*(\mrm{CPBSq}_\cat{C}(\varphi, B) ) = \mrm{CPBSq}_\cat{D}( F(\varphi), \Phi_\Delta(B) )
`$

ここで、$`F_*`$ は、関手 $`F`$ をアロー圏（可換四角形の圏）に持ち上げた関手です。

拡張包括構造を構成する演算／写像をすべて厳密に保存するのは強い条件ですが、これを弱めると一貫性地獄〈coherece hell〉で悶え苦しみそうなので、強い条件を要求します。

小さい包括クラン達とそのあいだの準同型射達が形成する圏を $`\mbf{CClan}`$ 、大きい包括クラン達とそのあいだの準同型射達が形成する圏を $`\mbf{CCLAN}`$ とします。$`\mbf{CClan}`$ と $`\mbf{CCLAN}`$ は、型理論〈依存型理論〉／インスティチューション理論／論理の圏論的定式化において、かなり使いやすい圏（のドクトリン）です。

例1：集合達の包括クラン

最初の具体例は、依存性を持たない包括クランです。包括クランの各構成素を次のように決めます。

台圏： 空集合を除いた集合圏 $`\mbf{Set}_+`$
終対象：単元集合 $`\mbf{1} = \{\emptyset\}`$ （要素が空集合であるのは別にかまわない）
ファイブレーションクラス：すべての全射からなるクラス
エス関手：定数値関手 $`|\mbf{Set}_+| \ni \Gamma \mapsto |\mbf{Set}_+|`$ 、射〈関数 | 写像〉はすべて恒等関数 $`\id_{|\mbf{Set}_+|}`$ に移す。
コンテキスト拡張演算：集合の直積 $`(\Gamma, A) \mapsto \Gamma \times A`$
標準射影：直積の第一射影 $`\pi^{\Gamma, A}_1 : \Gamma \times A \to \Gamma \In \mbf{Set}_+`$
標準プルバック四角形：写像 $`\varphi:\Gamma \to \Delta`$ と集合 $`B`$ に対して以下のような可換四角形を対応させる。

$`\quad \xymatrix{
{\Gamma\times B} \ar[r]^{\varphi \times \id_B} \ar[d]_{\pi_1^{\Gamma, B}}
& {\Delta \times B}\ar[d]^{\pi_1^{\Delta, B}}
\\
\Gamma \ar[r]_\varphi
&\Delta
}\\
\quad \text{commutative }\In \mbf{Set_+}
`$

クランの条件、包括構造の条件を満たすことは律儀に調べれば分かります。こうして定義される大きな包括クランを $`\mbf{Set_+CC}`$ と名付けることにします。'$`\mbf{CC}`$' は "comprehension clan" の略です。

エス関手 $`\msc{S}_\mbf{Set_+CC}`$ は定数値関手ですが、その値は $`|\mbf{Set}_+|`$ です。$`|\mbf{Set}_+|`$ は大きい集合なので、エス関手は次のプロファイルを持ちます。

$`\quad \msc{S}_\mbf{Set_+CC} :\mbf{Set}_+ \to \mbf{SET} \In \mathbb{CAT}`$

$`\mbf{Set_+CC}\in |\mbf{CCLAN}|`$ です。

例2：圏達の包括クラン

次は、小さい圏を対象〈コンテキスト〉とする、依存性を持つ包括クランの例です。包括クランの各構成素を次のように決めます。

台圏：小さい圏達の1-圏（2-圏ではない） $`{_1\mbf{Cat}}`$
終対象：ただひとつの対象と恒等射からなる自明な圏 $`\mbf{I}`$
ファイブレーションクラス：すべての離散ファイブレーション（離散ファイバーのファイバー付き圏の射影関手）からなるクラス
エス関手：小さい圏 $`\Gamma`$ に、前層達の集合 $`|\mrm{PSh}(\Gamma)| = |[\Gamma^\op, \mbf{Set}]|`$ を対応させる関手
コンテキスト拡張演算：グロタンディーク構成 $`(\Gamma, A) \mapsto \int_{\Gamma} A`$
標準射影：グロタンディーク構成の標準射影 $`\pi^{\Gamma, A} : \int_{\Gamma} A \to \Gamma`$
標準プルバック四角形：関手 $`\varphi:\Gamma \to \Delta`$ と前層 $`B`$ に対して以下のような可換四角形を対応させる。

$`\quad \xymatrix{
{\int_\Gamma \varphi^*(B) } \ar[r] \ar[d]_{\pi^{\Gamma, B}}
& {\int_\Delta B} \ar[d]^{\pi^{\Delta, B}}
\\
\Gamma \ar[r]_\varphi
&\Delta
}\\
\quad \text{commutative }\In {_1\mbf{Cat}}
`$

$`\varphi^*(B)`$ は、前層 $`B`$ に対して、“関手 $`\varphi`$ をプレ結合して、$`\Gamma`$ 上の前層に引き戻したモノ”です。

$`\quad \varphi^* = \msc{S}(\varphi) : |\mrm{PSh}(\Delta)| \to |\mrm{PSh}(\Gamma)| \In \mbf{SET}`$

こうして定義される大きな包括クランを $`\mbf{CatCC}`$ と名付けることにします。パルムグレン〈Erik Palmgren〉の複前層（「パルムグレンによる、型理論の複前層モデル」参照）は、$`\mbf{CatCC}`$ のテレスコープ圏（「テレスコープと包括クラン」参照）として構成できます。

例3：ファミリー達の包括クラン

例1と例2の中間的な包括クランです。包括クランの各構成素を次のように決めます。

台圏：集合（小さい離散圏）達の圏 $`\mbf{Set}`$
終対象：単元集合 $`\mbf{1} = \{\emptyset\}`$
ファイブレーションクラス：任意の射〈関数 | 写像〉からなるクラス
エス関手：集合 $`\Gamma`$ に、ファミリー達の集合 $`\mrm{Map}(\Gamma, |\mbf{Set}|)`$ を対応させる関手
コンテキスト拡張演算：シグマ型構成 $`(\Gamma, A) \mapsto \sum(\Gamma \mid A)`$
標準射影：シグマ型構成の標準射影 $`\pi^{\Gamma, A} : \sum(\Gamma\mid A) \to \Gamma`$
標準プルバック四角形：関数 $`\varphi:\Gamma \to \Delta`$ とファミリー $`B`$ に対して以下のような可換四角形を対応させる。

$`\quad \xymatrix{
{\sum(\Gamma \mid \varphi^*(B)) } \ar[r] \ar[d]_{\pi^{\Gamma, B}}
& {\sum(\Delta \mid B)} \ar[d]^{\pi^{\Delta, B}}
\\
\Gamma \ar[r]_\varphi
&\Delta
}\\
\quad \text{commutative }\In \mbf{Set}
`$

こうして定義される大きな包括クランを $`\mbf{FamCC}`$ と名付けることにします。

3つの具体例の関係

例1、例2、例3は大きな包括クランですが、下部構造である大きなクランを $`\mbf{Set_+C}, \mbf{CatC}, \mbf{SetC}`$ とします。クランのレベルで、次のような埋め込み関手があります。

$`\quad \mbf{Set_+C} \to \mbf{SetC} \to \mbf{CatC} \In \mbf{CLAN}`$

二番目の埋め込みは、集合を小さい離散圏とみなす対応です。

下部構造のあいだの埋め込みを拡張する形で、大きな包括クランのあいだの準同型射を構成できます。

$`\quad \mbf{Set_+CC} \to \mbf{FamCC} \to \mbf{CatCC} \In \mbf{CCLAN}`$

上記の包括クランの準同型射を細部まで書き下すのはけっこう面倒ですが、直感的にも、これら3つの包括クランが相互に関係しているのは分かるでしょう。

*1:$`F`$ と $`F^\op`$ は区別されないことが多いです。「イイカゲンとインチキを悔い改めるためのコスト」参照