集合のバンドルは便利に使えます。集合のバンドルの圏化〈categorification〉はファイバー付き圏〈fibered category〉がふさわしいでしょうが、もっと素朴な“圏のバンドル”も定義しておいたほうが良さそうです。例えば、ジェイコブス〈Bart Jacobs〉の包括圏〈comprehension category〉を考える際に、ファイバー付き圏とは限らない“圏のバンドル”が登場します。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\cat}[1]{ \mathcal{#1} }
%\newcommand{\op}{ \mathrm{op} }
\newcommand{\In}{\text{ in }}
\newcommand{\base}[1]{ {{#1}\!\lrcorner} }
\newcommand{\Imp}{\Rightarrow}
%\newcommand{\u}[1]{\underline{#1}}
\newcommand{\o}[1]{\overline{#1}}
\newcommand{\twoto}{ \Rightarrow }
`$
内容：
集合のバンドルの圏
この節とほぼ同じ内容が「グロタンディーク構成・逆構成と同値対応 // 記法・概念の整理： バンドル」にありますが、過去記事を参照しなくて済むように再度書きます。
集合のバンドル〈bundle of sets | set bundle〉とは、単に写像のことです。
- $`f`$ はバンドル $`\iff`$ $`f`$ は写像
なんでわざわざ写像のことを「バンドル」と呼ぶかというと、
- 写像は集合圏の射のこと
- バンドルはバンドルの圏の対象のこと
つまり、写像を一種の構造だと考えて、その構造のあいだの射をさらに考えることになります。
バンドル $`f`$ 、つまり“構造としての写像”は、3つの構成素達〈constituents | components〉からなります。
- $`f`$ の域〈ドメイン〉である集合
- $`f`$ の余域〈コドメイン〉である集合
- $`f`$ そのもの
それぞれの構成素を次のように書く／呼ぶと約束します。
- $`\o{f}`$ ： バンドル $`f`$ のトータル集合〈total set〉
- $`\base{f}`$ ： バンドル $`f`$ のベース集合〈base set〉
- $`\pi^f`$ ： バンドル $`f`$ の射影{写像 | 関数}〈projection {map | function}〉、単に射影〈projection〉とも呼ぶ。射影とは呼んでも、全射であるとは仮定しない。何の仮定もしない単なる写像。
（集合の）バンドルは次の形に書くことにします。
$`\quad f = (\base{f}, \o{f}, \pi^f)\\
\text{Where}\\
\quad \base{f} \in |{\bf Set}|\\
\quad \o{f} \in |{\bf Set}|\\
\quad \pi^f : \o{f} \to \base{f} \In {\bf Set}
`$
2つのバンドル $`f`$ と $`g`$ のあいだの射（バンドル射〈bundle {map | morphism}〉）は、2つの写像のペア $`\varphi = (\base{\varphi}, \o{\varphi})`$ で次の図式を可換にするものです。
$`\quad \xymatrix{
\o{f} \ar[r]^{\o{\varphi}} \ar[d]_{\pi^f}
& \o{g} \ar[d]^{\pi^g}
\\
\base{f} \ar[r]_{\base{\varphi}}
&\base{g}
}\\
\quad \text{commutative }\In {\bf Set}
`$
バンドル射の結合〈composition〉と恒等バンドル射〈identity bundle map〉は説明しなくても明らかでしょう。
バンドルの射影による一点の逆像を次のように書きます。
$`\quad \o{f}_{@a} := (\pi^f)^{-1}(a) :=\{x\in \base{f} \mid \pi^f(x) = a \}`$
集合 $`\o{f}_{@a}`$ はトータル集合 $`\o{f}`$ の部分集合になります。この部分集合を、$`a \in \base{f}`$ における $`f`$ のファイバーと呼びます。バンドル射を制限して、ファイバーとファイバーのあいだの写像を定義できます。
$`\quad \varphi_{@a} : \o{f}_{@a} \to \o{g}_{@\base{\varphi}(a)} \In {\bf Set}\\
\text{Where}\\
\quad \o{f}_{@a} \subseteq \o{f}\\
\quad \o{g}_{@\base{\varphi}(a)} \subseteq \o{g}
`$
バンドル射 $`\varphi`$ に対して：
- $`\base{\varphi}: \base{f} \to \base{g}`$ を、$`\varphi`$ のベースパート〈base part〉と呼ぶ。
- $`\o{\varphi}: \o{f} \to \o{g}`$ を、$`\varphi`$ のトータルパート〈total part〉と呼ぶ。
- $`{\varphi}_{@a}: \o{f}_{@a} \to \o{g}_{\base{\varphi}(a)}`$ を、$`\varphi`$ の（$`a`$ における）ファイバーパート〈fiber part〉と呼ぶ。
バンドル射 $`\varphi`$ は、ファイバーパート達を寄せ集めたものと考えられるので、次のような書き方もします。
$`\quad \varphi = (\varphi_{@a})_{a\in \base{\varphi}}\\
\text{Where}\\
\text{For }a\in \base{\varphi}\\
\quad \varphi_{@a} : \o{f}_{@a} \to \o{g}_{@\base{\varphi}(a)} \In {\bf Set}
`$
集合のバンドルを対象として、バンドル射を射とする圏を次のように書きます。
$`\quad {\bf Bun} \; \in |{\bf CAT}|`$
次節で述べるバンドル圏構成〈アロー圏構成〉を使って書くと次のようです。
$`\quad {\bf Bun} := \mrm{Bun}({\bf Set}) = \mrm{Arr}({\bf Set})`$
バンドルの圏＝アロー圏
射を対象と思って新しい圏を作ることは、集合圏に限らず実行できます。$`\cat{C}`$ を圏として、$`\cat{C}`$ のバンドル（実体は射）を対象として、バンドル射を射とする圏を構成してみます。
圏 $`\cat{C}`$ に対して、新しい圏 $`\cat{B}`$ を次のように定義しましょう。
- 対象の集合は、 $`|\cat{B}| := \mrm{Mor}(\cat{C})`$
- 射 $`\varphi : f \to g`$ は、射のペア $`\varphi = (\varphi_0, \varphi_1)`$ で、以下の図式を可換にするもの。
$`\quad \xymatrix{
\cdot \ar[r]^{\varphi_1} \ar[d]_{f}
\ar@{}[rd]|{ }
& \cdot \ar[d]^{g}
\\
\cdot \ar[r]_{\varphi_0}
&\cdot
}\\
\quad \text{commutative }\In \cat{C}
`$
集合圏 $`{\bf Set}`$ から一般の圏 $`\cat{C}`$ に変わっただけで、圏の作り方は変わりません。このような構成法で作る圏は $`\cat{C}`$ のアロー圏〈arrow category〉とも呼びます。アロー圏については次の過去記事で述べています。ただし、過去記事では図式の縦横が違っているので注意してください。
$`\cat{C}`$ のバンドル達を対象とする圏と、$`\cat{C}`$ のアロー圏は同じものです。次のように書きます。
$`\quad \mrm{Bun}(\cat{C}) = \mrm{Arr}(\cat{C}) \; \in |{\bf CAT}|\\
\quad {\bf Bun} = \mrm{Bun}({\bf Set} ) = \mrm{Arr}({\bf Set} ) \; \in |{\bf CAT}|
`$
$`{\bf Bun}`$ の場合と同様な意味で、次の言葉を使います。
- バンドル〈bundle〉
- トータル対象〈total object）
- ベース対象〈base object〉
- 射影〈projection〉
- バンドル射〈bundle morphism〉
- バンドル射のベースパート〈base part〉
- バンドル射のトータルパート〈total part〉
ファイバーとバンドル射のファイバーパートは、一般的には定義できません。圏 $`\cat{C}`$ が、終対象 $`{
\bf 1}`$ とプルバック〈引き戻し〉（コスパンの極限）を持つ圏ならば、ファイバーに相当する対象 $`X`$ を次のように定義できます。
$`\quad \xymatrix {
X \ar[r]^{!} \ar[d]
\ar@{}[dr]|{\text{p.b.}}
& {\bf 1} \ar[d]^a
\\
\cdot \ar[r]_f
& \cdot
}\\
\quad \In \cat{C}
`$
ここでは特にファイバーにはこだわらないことにします。プルバックとファイバーに関しては以下の記事で書いています。
圏のバンドル達の圏
$`{\bf Cat}`$ を小さい圏達の2-圏とします。集合圏の場合と同様に、$`{\bf Cat}`$ の任意の射〈1-射〉をバンドル〈bundle〉と呼ぶことにします。$`{\bf Cat}`$ の射は関手ですから、関手がバンドルです。集合のバンドルと区別したいときは圏のバンドル〈bundle of categories | category bundle〉と呼びます。
次の言葉は集合のバンドルの場合と同様です。
- バンドル〈bundle〉
- トータル圏〈total category）
- ベース圏〈base category〉
- 射影{関手}?〈projection {functor}?〉
圏のバンドルは次の形に書けます。
$`\quad F = (\base{F}, \o{F}, \pi^F)`$
圏のバンドルのあいだのバンドル射は四種類考えます。まず、$`F, G`$ は圏のバンドル〈関手〉として、次のような図式を考えます。
$`\quad \xymatrix{
\cdot \ar[r]^{\Phi_1} \ar[d]_{F}
\ar@{}[rd]|{=}
& \cdot \ar[d]^{G}
\\
\cdot \ar[r]_{\Phi_0}
&\cdot
}\\
\quad \In {\bf Cat}
`$
ここで、四角形内のイコール記号は、この四角形が可換であることを示します。つまり、次の等式と同じことです。アスタリスクは、関手の図式順結合記号です。
$`\quad F*\Phi_0 = \Phi_1 * G \In {\bf Cat}`$
$`\Phi = (\Phi_0, \Phi_1)`$ が圏のバンドルのあいだのバンドル射となります。四角形が等式であるバンドル射は厳密バンドル射〈strict bundle morphism〉と呼びます。
次に、四角形が可換とは限らない図式を考えましょう。以下でのペースティング図の書き方は、「構造記述のための指標と名前 1/n 基本 // 図式による法則の記述」で述べたものです。
$`\quad \xymatrix{
\cdot \ar[r]^{\Phi_1} \ar[d]_{F}
\ar@{}[rd]|{\underset{\nearrow}{\cong}\, \alpha}
& \cdot \ar[d]^{G}
\\
\cdot \ar[r]_{\Phi_0}
&\cdot
}\\
\quad \In {\bf Cat}
`$
この図式は、次のような可逆な自然変換があることを示しています。
$`\quad \alpha :: F*\Phi_0 \overset{\cong}{\twoto} \Phi_1 * G \In {\bf Cat}`$
この場合は、$`\Phi = (\Phi_0, \Phi_1)`$ が圏のバンドルのあいだのスード・バンドル射〈pseudo bundle morphism〉です。スード・バンドル射は、関手のペア $`\Phi = (\Phi_0, \Phi_1)`$ だけではなくて、自然変換 $`\alpha`$ も構成素になります。
以下の図式では、四角形を埋める自然変換が可逆とも仮定していません。
$`\quad \xymatrix{
\cdot \ar[r]^{\Phi_1} \ar[d]_{F}
\ar@{}[rd]|{\underset{\nearrow}{\Rightarrow}\, \alpha}
& \cdot \ar[d]^{G}
\\
\cdot \ar[r]_{\Phi_0}
&\cdot
}\\
\quad \In {\bf Cat}
`$
$`\quad \xymatrix{
\cdot \ar[r]^{\Phi_1} \ar[d]_{F}
\ar@{}[rd]|{\overset{\swarrow}{\Rightarrow}\, \alpha}
& \cdot \ar[d]^{G}
\\
\cdot \ar[r]_{\Phi_0}
&\cdot
}\\
\quad \In {\bf Cat}
`$
どちらかをラックス、もう一方を反ラックスと呼ぶ習慣です。ここでは上の図式で定義されるバンドル射をラックス・バンドル射〈lax bundle morphism〉、下の図式で定義されるバンドル射を反ラックスバンドル射〈oplax bundle morphism〉と呼ぶことにします。
ラックス・バンドル射を構成する自然変換 $`\alpha`$ は：
$`\quad \alpha :: F*\Phi_0 \twoto \Phi_1 * G \In {\bf Cat}`$
一方、反ラックス・バンドル射を構成する自然変換 $`\alpha`$ は次のようです。
$`\quad \alpha :: \Phi_1 * G \twoto F*\Phi_0 \In {\bf Cat}`$
圏のバンドルを対象として、厳密バンドル射を射とする圏（2-圏ではない）を次のように書くことにします。
$`\quad {\bf CatBun}^\mrm{str} \in |{\bf CAT}|`$
右肩の $`\mrm{str}`$ は厳密〈strict〉を意味します。
スード・バンドル射、ラックス・バンドル射、反ラックス・バンドル射の場合、関手だけではなくて自然変換も考慮する必要があります。が、射の結合や恒等射は容易に定義できて、圏の公理を満たします。それぞれの種類のバンドル射を射とする“圏のバンドルの圏”を次のように書きます。
$`\quad {\bf CatBun}^\mrm{psd} \in |{\bf CAT}|\\
\quad {\bf CatBun}^\mrm{lax} \in |{\bf CAT}|\\
\quad {\bf CatBun}^\mrm{oplax} \in |{\bf CAT}|
`$
次の包含関係と等式があります。
$`\quad {\bf CatBun}^\mrm{str} \subseteq {\bf CatBun}^\mrm{psd}\\
\quad {\bf CatBun}^\mrm{psd}\subseteq {\bf CatBun}^\mrm{lax}\\
\quad {\bf CatBun}^\mrm{psd} \subseteq {\bf CatBun}^\mrm{oplax}\\
\quad {\bf CatBun}^\mrm{psd} = {\bf CatBun}^\mrm{lax}\cap{\bf CatBun}^\mrm{oplax}
`$
バンドル射の構成素は3つになります。
- バンドル射のベースパート〈base part〉
- バンドル射のトータルパート〈total part〉
- バンドル射の2-パート〈2-part〉
厳密バンドル射の場合の2-パートは恒等自然変換だとします。
バンドル射 $`\Phi`$ の2-パートを $`\Phi_2`$ と書くことにすると、バンドル射は次の図式に描けます。
$`\quad \xymatrix{
\o{F} \ar[r]^{\o{\Phi}} \ar[d]_{\pi^F}
\ar@{}[rd]|{ \Phi_2}
& \o{G} \ar[d]^{\pi^G}
\\
\base{F} \ar[r]_{\base{\Phi}}
&\base{G}
}\\
\quad \In {\bf Cat}
`$
厳密2-圏のバンドルの圏
$`\cat{K}`$ を厳密2-圏とします。$`{\bf Cat}`$ の場合と同様に、$`\cat{K}`$ のバンドル〈1-射〉を対象として、各種のバンドル射を射とする圏（2-圏ではない）を構成できます。この構成法によりできた圏を次のように書くことにします。
$`\quad \mrm{Bun}^\mrm{str}(\cat{K}) \; \in |{\bf CAT}|\\
\quad \mrm{Bun}^\mrm{psd}(\cat{K}) \; \in |{\bf CAT}|\\
\quad \mrm{Bun}^\mrm{lax}(\cat{K}) \; \in |{\bf CAT}|\\
\quad \mrm{Bun}^\mrm{oplax}(\cat{K}) \; \in |{\bf CAT}|
`$
厳密2-圏 $`\cat{K}`$ のサイズによっては、$`{\bf CAT}`$ の対象になるとは限りませんが、今は、$`{\bf CAT}`$ の対象になる場合を考えます。
$`\cat{C}`$ が1-圏のとき、特殊な（2-射が恒等だけの）厳密2-圏と考えることができます。すると、以前に定義した $`\mrm{Bun}`$ は $`\mrm{Bun}^\mrm{str}`$ と考えれば辻褄があいます。
“集合のバンドルの圏”と“圏のバンドルの圏”は、次のように定義できます。
$`\quad {\bf Bun} := \mrm{Bun}({\bf Set}) = \mrm{Bun}^\mrm{str}({\bf Set})\\
\quad {\bf CatBun}^\mrm{str} := \mrm{Bun}^\mrm{str}({\bf Cat}) \\
\quad {\bf CatBun}^\mrm{psd} := \mrm{Bun}^\mrm{psd}({\bf Cat}) \\
\quad {\bf CatBun}^\mrm{lax} := \mrm{Bun}^\mrm{lax}({\bf Cat}) \\
\quad {\bf CatBun}^\mrm{oplax} := \mrm{Bun}^\mrm{oplax}({\bf Cat})
`$
デカルト関手とファイバー付き圏
再び圏のバンドルの圏 $`{\bf CatBun}^\mrm{str}`$ を考えます。圏のバンドル $`F\in |{\bf CatBun}^\mrm{str}|`$ は単なる関手なので、ファイバー圏になるとは限りません。が、関手に対してもデカルト射〈Cartesian morphism〉は定義できます。関手のデカルト射については、例えばnLab項目 https://ncatlab.org/nlab/show/Grothendieck+fibration の Definition 2.1. に記述があります。
圏のバンドル（実体は関手） $`F`$ のデカルト射の全体を $`\mrm{Cart}(F)`$ とします。
$`\quad \mrm{Cart}(F) \subseteq \mrm{Mor}(\o{F})`$
圏のバンドル $`F`$ から $`G`$ への厳密バンドル射 $`\Phi`$ がデカルト・バンドル射〈Cartesian bundle morphism〉であるとは、次が成立することです。
$`\quad f\in \mrm{Cart}(F) \Imp \o{\Phi}(f) \in \mrm{Cart}(G)`$
$`\mrm{Cart}(F) \subseteq \mrm{Mor}(\o{F})`$ を、不正確な記法ですが $`\mrm{Cart}(F) \hookrightarrow \o{F}`$ と書くことにして、図式で示せば：
$`\quad \xymatrix{
\mrm{Cart}(F) \ar@{^{(}->}[d] \ar[r]^{\o{\Phi|}_{\mrm{Cart}(F)}}
& \mrm{Cart}(G)\ar@{^{(}->}[d]
\\
\o{F} \ar[r]^{\o{\Phi}} \ar[d]_{\pi^F}
& \o{G} \ar[d]^{\pi^G}
\\
\base{F}\ar[r]_{\base{\Phi}}
&\base{G}
}\\
\quad \text{commutative }\In {\bf CAT}
`$
バンドル（特別な場合としてファイバー付き圏）のデカルト射をデカルト射に移す関手はデカルト関手〈Cartesian functor〉とも呼ばれます。この定義には、バンドル射の2-パートが関与してないので、バンドル射 $`\Phi`$ が厳密でなくても有効な定義です。しかし、実際に使うのは厳密バンドル射の場合が多いでしょう。
圏のバンドルを対象として、（厳密な）デカルト・バンドル射を射とする圏を次のように書くことにします。
$`\quad {\bf CatBunCart}^\mrm{str} \;\in |{\bf CAT}|`$
ファイバー付き圏〈fibered category〉は、圏のバンドルの特殊なものです。対象をファイバー付き圏として、（厳密な）デカルト・バンドル射を射とする圏は、ファイバー付き圏の圏 $`{\bf FibCat}`$ です。
$`\quad {\bf FibCat} \;\in |{\bf CAT}|`$
次の包含関係があります。
$`\quad {\bf FibCat} \subseteq {\bf CatBunCart}^\mrm{str}\subseteq {\bf CatBun}^\mrm{str}
`$
例： 包括圏
バート・ジェイコブス〈Bart Jacobs〉は、型システムの圏論的モデルとして包括圏〈comprehension category〉を定義しました。包括圏は、型システムの特徴を、高レベルな構造にパックしてエンコードしたものです。
包括圏は、次の構成素からなります。
- 圏のバンドル $`\mathscr{E} = (\cat{C}, \cat{E}, P) `$
- 圏のバンドル $`\mathscr{C} = (\cat{C}, \mrm{Bun}(\cat{C}), \mrm{Base})`$
- （厳密な）デカルト・バンドル射 $`(\mrm{Ext}, \mrm{Id}_\cat{C})`$
図式に描けば次のようです。$`(\mrm{Ext}, \mrm{Id}_\cat{C})`$ がデカルト・バンドル射であることは、先ほどの“不正確な記法”で描いています。
$`\quad \xymatrix{
\mrm{Cart}(\mathscr{E}) \ar@{^{(}->}[d] \ar[r]^{\mrm{Ext}|_{\mrm{Cart}(\mathscr{E})}}
& \mrm{Cart}(\mathscr{C})\ar@{^{(}->}[d]
\\
\cat{E} \ar[r]^{\mrm{Ext} } \ar[d]_{P}
& \mrm{Bun}(\cat{C}) \ar[d]^{\mrm{Base} }
\\
\cat{C} \ar@{=}[r]_{\mrm{Id}_\cat{C} }
&\cat{C}
}\\
\quad \text{commutative }\In {\bf CAT}
`$
$`\mrm{Ext}`$ はコンテキスト拡張関手〈context extension functor〉と呼ばれます。$`\mrm{Bun}(\cat{C})`$ は、圏 $`\cat{C}`$ のバンドルの圏〈アロー圏〉です。$`\mrm{Base}`$ は、バンドルにそのベース対象（射の余域）を、バンドル射にそのベースパートを対応させる関手です。
上記の構造が包括圏となる条件〈公理〉は：
- $`P:\cat{E} \to \cat{C}`$ が（単なる圏バンドルではなくて）ファイバー付き圏となる。
これは、$`\cat{C}`$ の射を、$`\cat{E}`$ のデカルト射（$`\mrm{Cart}(\mathscr{E})`$ の要素）に持ち上げ可能であることを意味します。
包括圏の定義において、$`P`$ がファイバー付き圏（の射影）になることは要求していますが、$`\mrm{Base}`$ がファイバー付き圏になることは要求していません。$`\mrm{Base}`$ がファイバー付き圏（の射影）になるときは、$`\cat{C}`$ がプルバック（コスパンの極限）を持つときです。
包括圏が型システムのモデルとなると言われても、初見ではピンとこないでしょうが、型理論／型システムで使われる概念が、上記の構造のなかに巧みにエンコードされています。
