この記事内では、「型」と「集合」は同義語です。つまり、sets-as-types の立場をとります*1。
集合〈型〉のファミリー〈族〉があったとき、それからシグマ型とパイ型を構成できます。この構成は、次のような写像を与えます。
$`\quad \sum, \prod: |{\bf Fam}| \to |{\bf Set}|`$
これは、ファミリーの圏の対象に集合圏の対象を対応させます。$`\sum, \prod`$ は、対象類（「類」は小さくないかも知れない集合）のあいだの写像ですが、関手にはなってません。関手に仕立てることはできるでしょうか？ -- この問〈とい〉について考えてみます。
この記事では、定義や説明に出てくる言葉や記号について、注意や補足をできるだけ付けるようにします。冒頭の文「『型』と『集合』は同義語です」はそのような注意の例です。いわずもながでしょうが、「写像」と「関数」も同義語です。同義語なので使い分けの基準はなく、どちらを使うかは気分だけの問題です。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\In}{\text{ in } }
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\hyp}{\text{－} }
\newcommand{\op}{\mathrm{op} }
\newcommand{\id}{\mathrm{id} }
\newcommand{\inv}{\leftarrow }
%\newcommand{\pto}{ \supseteq\!\to }
%\newcommand{\u}[1]{\underline{#1}}
\require{color} % 緑色
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
\newcommand{\Define}{\Keyword{Define } }%
%\newcommand{\Subject}{\Keyword{Subject } }%
\newcommand{\Where}{\Keyword{Where } }
\newcommand{\And}{\Keyword{And } }
\newcommand{\Let}{\Keyword{Let } }
`$
内容：
ファミリーの圏
ここでのファミリー〈family〉は、集合のインデックス付きファミリー〈indexed family of sets〉です。ファミリー $`F`$ は次のような写像です。
$`\quad F: I \to |{\bf Set}| \In {\bf SET}\\
\Where I \in |{\bf Set}|
`$
$`{\bf SET}`$ （すべて大文字）は、$`|{\bf Set}| \in |{\bf SET}|`$ が成立するような、“より大きな集合圏”です。
ファミリー $`F`$ を次のようにも書きます。
$`\quad F = (I, F)`$
これは、よくある記号の乱用〈abuse of notation〉（例えば、「モノイド $`M = (M, *, e)`$」）ではありません。右辺が冗長な書き方になっているだけです。冗長に書いたほうが便利なことがあるからです。
圏に仕立てることを想定して、すべてのファミリーの集合（小さくない集合）を $`|{\bf Fam}|`$ と書きます。$`|{\bf Fam}|`$ は、今までの定義・記述によりハッキリと定まった固有特定の集合（小さくないけど）です。
$`F = (I, F)`$ と $`G = (J, G)`$ が2つの（異なる2つではなくて同一かも知れない）ファミリーだとして、そのあいだの準同型射〈homomorphism〉（あるいは単に射〈morphism〉）は、次のように定義・記述します。
$`\For (I, F), (J, G) \in |{\bf Fam}|\\
\Define (f, \varphi) : (I, F) \to (J, G) :\Iff\\
\quad f: I \to J \In {\bf Set}\\
\quad \And\\
\quad \varphi = (\varphi_i)_{i\in I} \:\Where \varphi_i : F(i) \to G(f(i)) \In {\bf Set}
`$
またまた、圏を作る下心まるだしで、上記の最初の2行と同じことを次のように書きます。
$`\For (I, F), (J, G) \in |{\bf Fam}|\\
\Define (f, \varphi) \in {\bf Fam}( (I, F), (J, G) ) :\Iff
`$
3行目以降が、ホムセットにどんな要素が所属するかの具体的な条件の記述です。
この時点で、対象類 $`|{\bf Fam}|`$ と、対象のペアごとのホムセット $`{\bf Fam}(\hyp, \hyp)`$ の定義が終えたことになります。2つの射（ホムセットの要素）の結合〈composition〉は次のように定義します。
$`\For (I, F), (J, G), (K, H) \in |{\bf Fam}|\\
\For (f, \varphi) \in {\bf Fam}( (I, F) , (J, G) )\\
\For (g, \psi) \in {\bf Fam}( (J, G), (K, H) )\\
\Define (f, \varphi) ; (g, \psi) := (f; g, \xi)\\
\Where\\
\quad \For i \in I\\
\quad \Define \xi_i := \lambda\,x \in F(i).(\, \psi_{f(i)}( \varphi_i(x) ) \;\in H(g(f(i))) \,)
`$
恒等射〈identity morphism〉 $`\id_F = \id_{(I, F)}`$ の定義は自明でしょう。
今まで提示した素材たちは：
- 対象の類 $`|{\bf Fam}|`$
- 対象のペアごとのホムセット $`{\bf Fam}(F, G)`$
- 射〈ホムセットの要素〉の結合演算 $`;`$〈セミコロン〉
- 対象ごとの恒等射 $`\id_F`$
これらが全体として圏になるために満たすべき法則は：
- 結合法則〈associative law〉
- 左右の単位法則〈unit law〉
法則を確認すれば（今は確認を省略しますが）、$`{\bf Fam}`$ が圏であることが分かります。これがファミリーの圏〈the category of families〉です。
$`{\bf Fam}`$ （というボールド体の名前で指されるモノ）は、固有特定の圏です。そして：
- 圏 $`{\bf Fam}`$ の対象の類は、$`|{\bf Fam}|`$ と書く。
- 圏 $`{\bf Fam}`$ のホムセットは、$`\mrm{Hom}_{\bf Fam}(\hyp, \hyp) = {\bf Fam}(\hyp, \hyp)`$ と書く。
- 圏 $`{\bf Fam}`$ の結合〈composition〉は、図式順演算子記号 $`;`$ で書く。が、固有特定の圏 $`{\bf Fam}`$ に備わった固有特定の演算であることを明示したいなら $`;^{\bf Fam}`$ とでも書くべき。ほとんどの場合、右上付き $`{\bf Fam}`$ は省略されるが。
- 圏 $`{\bf Fam}`$ の恒等射は、$`\id`$ で書く。が、固有特定の圏 $`{\bf Fam}`$ に備わった固有特定の射（の族）であることを明示したいなら $`\id^{\bf Fam}`$ とでも書くべき。ほとんどの場合、右上付き $`{\bf Fam}`$ は省略されるが。
述語
この節の内容は、次々節のための準備です。
述語〈predicate〉とは、ブール値〈真偽値〉を値とする関数です。述語 $`p`$ は次のように書けます。
$`\quad p : X \to {\bf B} \In {\bf Set}`$
ファミリーの場合と同じく、$`p = (X, p)`$ と冗長な表現を許します。
述語の域〈domain〉が小さくなくてもよい場合は：
$`\quad p : X \to {\bf B} \In {\bf SET}`$
小さくない域を持つ述語として、次の形の述語を考えましょう。
$`\quad p : \mrm{Mor}({\bf Set}) \to {\bf B} \In {\bf SET}`$
この形の述語の域は、集合圏の射の集合（小さくない集合）です。つまり、この形の述語は、関数〈写像〉を引数に受け取って真偽値を返します。
幾つかの固有特定の述語を考えます。
| 述語の名前 | 意味 |
|---|---|
| $`\msf{inj}`$ | 関数は単射〈injection〉である |
| $`\msf{surj}`$ | 関数は全射〈surjection〉である |
| $`\msf{bij}`$ | 関数は双射〈bijection | 全単射〉である |
| $`\msf{id}`$ | 関数は恒等写像〈identity map〉である |
| $`\msf{incl}`$ | 関数は包含写像〈inclusion map〉である |
| $`\msf{any}`$ | なんでもよい |
ローカルなネーミングコンベンションとして、述語の固有名（固有特定の述語を指す名前）にはサンセリフ体（ヒゲなしの文字フォント）を使うことにします。これらの名前は固有名ですが、僕が勝手にネーミングしたものですから、気に入らなかったら別な名前を付けるのは自由です。
紛らわしいですが、ローマン体の $`\id`$ は圏の恒等射のことで、サンセリフ体の $`\msf{id}`$ は関数が恒等であるかどうかを判定する述語です。$`f\in \mrm{Mor}({\bf Set})`$ に対して $`\msf{inj}(f)`$ という表現は真偽が決まるという意味で命題〈proposition〉です。もっと言えば、固有特定な具体的な関数を $`\msf{inj}`$ に渡したときに、真か偽のどちらかになる、ということです。$`\msf{inj}(f)`$ を論理式で書き下すなら次です。
$`\quad \msf{inj}(f) :\Iff \forall x, y\in \mrm{dom}(f).\,
x \ne y \Imp f(x) \ne f(y)`$
ファミリーの圏の変種： 逆向き
ファミリーの圏 $`{\bf Fam}`$ を少し変形した圏として $`{\bf Fam}_\inv`$ を定義します。対象類は $`{\bf Fam}`$ と同じです。
$`\quad |{\bf Fam}_\inv| := |{\bf Fam}|`$
射 $`(f, \psi)`$ の定義が違います。
$`\For (I, F), (J, G) \in |{\bf Fam}_\inv|\\
\Define (f, \psi) : (I, F) \to (J, G) :\Iff\\
\quad f: I \to J \In {\bf Set}\\
\quad \And\\
\quad \psi = (\psi_i)_{i\in I} \:\Where \psi_i : G(f(i)) \to F(i) \In {\bf Set}
`$
違っている部分は、$`G(f(i)) \to F(i)`$ です。 $`F`$ から $`G`$ への射といいながら、各 $`i\in I`$ ごとの写像が逆向きになっています。この定義に基づいても圏は作れるので、そうしてできた圏が $`{\bf Fam}_\inv`$ です。
$`{\bf Fam}_\inv`$ との対比を強調したい場合は、$`{\bf Fam}`$ に右向きの矢印を付けます。
$`\quad {\bf Fam}_\to := {\bf Fam}`$
「$`{\bf Fam}_\to`$ または $`{\bf Fam}_\inv`$」の意味で $`{\bf Fam}_\alpha`$ という書き方も使います。ここで、ギリシャ文字 $`\alpha`$ は集合 $`\{\to, \inv\}`$ （2つの矢印記号からなる集合）を変域とする変数です。変数 $`\alpha`$ が取り得る値は二値です。$`\alpha = \,\to`$ のとき $`{\bf Fam}_\alpha`$ は$`{\bf Fam}_\to`$ を意味し、$`\alpha = \,\inv`$ のとき $`{\bf Fam}_\alpha`$ は$`{\bf Fam}_\inv`$ を意味します。
ファミリーの圏の変種： 写像に条件を付ける
この節の内容はこの記事内では利用しません。飛ばしてもかまいません。いずれ他の記事で利用することがあると思います。
$`p, q`$ は、（小さくない）集合 $`\mrm{Mor}({\bf Set})`$ を域とする述語とします。述語 $`p, q`$ に対して、圏 $`{\bf Fam}^{p,q}`$ を次のように定義します。対象類は $`{\bf Fam}`$ と同じです。
$`\quad |{\bf Fam}^{p, q}| := |{\bf Fam}|`$
射 $`(f, \varphi)`$ の定義が違います。
$`\For (I, F), (J, G) \in |{\bf Fam}^{p, q}|\\
\Define (f, \varphi) : (I, F) \to (J, G) :\Iff\\
\quad f: I \to J \In {\bf Set} \:\And p(f)\\
\quad \And\\
\quad \varphi = (\varphi_i)_{i\in I} \\
\quad \Where \varphi_i : F(i) \to G(f(i)) \In {\bf Set} \:\And q(\varphi_i)
`$
つまり、射 $`(f, \varphi)`$ に条件が付きます。$`f`$ は述語 $`p`$ を満たす必要があり、$`\varphi_i`$ は述語 $`q`$ を満たす必要があります。この定義に基づいても圏は作れるので、そうしてできた圏が $`{\bf Fam}^{p,q}`$ です。
上記の定義の一部を $`G(f(i)) \to F(i)`$ に書き換えると $`{\bf Fam}_\inv^{p, q}`$ が定義できます。矢印の向き（二値）と2つの述語でインデックス〈パラメトライズ〉された圏の族〈{indexed | parameterized} family of categories〉は次のように書けます。
$`\quad {\bf Fam}^{p,q}_\alpha\\
\Where \\
\quad \alpha \in \{\to, \inv\}\\
\quad p, q \in {\bf SET}( \mrm{Mor}({\bf Set}) , {\bf B})
`$
パラメータ $`\alpha`$ のデフォルト値は '$`\to`$' です。勝手な $`p, q`$ に対して圏を定義できるわけではありません。述語の外延が、集合圏 $`{\bf Set}`$ の部分圏を形成するような $`p, q`$ に限ります*2。
例えば、被覆族の細分〈refinement of covering families〉を考えるときは $`{\bf Fam}^{\msf{any},\msf{incl}}`$ 内で考えると便利です。最近僕は、$`{\bf Fam}^{\msf{bij},\msf{bij}}`$ や $`{\bf Fam}^{\msf{bij},\msf{id}}`$ に興味を持っています。
シグマ共変関手
シグマ型構成 $`\sum`$ を関手に仕立てましょう。関手となったシグマを $`\sum_*`$ という名前で呼びます。この時点ではまだ定義してませんが、ここの文脈における「$`\sum_*`$」は、（下付きアスタリスクも含めて）固有特定の関手を指す個有名です。下付きアスタリスクは、名前の一部で、共変関手であることを強調する目印です。
$`\quad \sum : |{\bf Fam}|\to |{\bf Set}| \In {\bf SET}\\
\quad \sum_* : {\bf Fam}\to {\bf Set} \In {\bf CAT}
`$
$`\sum_*`$ は関手なので、次のようなパートを持ちます。
- 対象パート： $`(\sum_*)_\mrm{obj} : |{\bf Fam}| \to |{\bf Set}| \In {\bf SET}`$
- 射パート： $`(\sum_*)_\mrm{mor} : \mrm{Mor}({\bf Fam}) \to \mrm{Mor}({\bf Set}) \In {\bf SET}`$
- ホムパート： $`F, G \in |{\bf Fam}|`$ ごとに
$`(\sum_*)_{ \mrm{hom}(F, G) } :{\bf Fam}(F, G) \to {\bf Set}( (\sum_*)_\mrm{obj}(F), (\sum_*)_\mrm{obj}(G)) \In {\bf Set}`$
射パートとホムパートは、どちらか一方を定義すれば、残りは自動的に出てきます。ここでは、ホムパートのほうを定義することにします。
シグマ共変関手 $`\sum_*`$ の対象パートは、もちろんシグマ型を構成する写像です。
$`\quad (\sum_*)_\mrm{obj} := \sum \;: |{\bf Fam}| \to |{\bf Set}| \In {\bf SET}`$
煩雑さを避けるために、$`(\sum_*)_\mrm{obj}`$ は単に $`\sum`$ と書き、射パートとホムパートは $`\sum_*`$ と書くことにします。
以下の「$`\cdots`$」部分が明確になれば、シグマ関手を定義したことになります。
$`\For (f, \varphi) : (I, F) \to (j, G) \In {\bf Fam}\\
\quad\sum_* ( f, \varphi ) =\sum_* ( (f, \varphi) ) := \cdots
`$
定義すべき目的の関数を $`\Phi`$ と置いて、書き下すこととにしましょう。
$`\Let \Phi :=\sum_* ( f, \varphi ) \;: \sum(I, F) \to \sum(J, G) \In {\bf Set}`$
集合 $`\sum(I, F)`$ の要素は、次の依存ペアの形に書けます。
$`\quad (i, x)\\
\Where i \in I, x\in F(i)
`$
したがって、依存ペアに対する値を書き下せばいいわけです。
$`\For (i, x) \in \sum(I, F)\\
\Define \Phi (i, x) = \Phi ( (i, x)) := \\
\quad (f(i), \varphi_i (x)) \; \in \left(\{f(i)\} \times G(f(i))\right) \subseteq \sum(J, G)
`$
これは素直で直感的な定義で、ファミリーを集合論的バンドルとみなせば、ファイバーからファイバーへの写像を束ねた写像になります。また、次の図式は可換図式になります。
$`\require{AMScd}
\quad \begin{CD}
\sum(I, F) @>{\Phi = \sum_* (f, \varphi)}>> \sum(J, G)\\
@V{\pi^F}VV @VV{\pi^G}V\\
I @>{f}>> J
\end{CD}\\
\quad \text{commutative in }{\bf Set}
`$
$`\pi^F, \pi^G`$ は、ファミリー $`F, G`$ に付随するシグマ型の標準射影です。
$`\sum_*`$ が関手であるためには、関手性、すなわち結合と恒等を保存することが必要となりますが、律儀に定義を追いかければ出ます。
シグマ関手 $`\sum_*`$ は、「ファミリーを集合論的バンドルとみなす」という行為（の全空間を作るところ）を、関手として明示的に表現したものです。シグマ関手により、ファミリー〈集合族〉の圏と集合論的バンドルの圏は圏同値（ほとんど区別する必要がない2つの圏）になります。
パイ反変関手
シグマ型構成を関手にすることは、特に問題もなく想定内の結果になりました。が、パイ型構成を関手にするのは、なんだかうまくいきません。共変関手を作るのは無理そうなので諦めます。反変関手にします。反変関手の場合でも、$`{\bf Fam}`$ ではうまくいきません。次の形の関手にします。
$`\quad \prod^* : ({\bf Fam}_\inv)^\op \to {\bf Set} \In {\bf CAT}`$
$`{^\op}`$ を付けているのは、$`\prod^*`$ が反変関手であることを示します。しかし、$`{^\op}`$ を付けた反対圏〈opposite category〉を使うのは分かりにくい点があるので、次の書き方も使います。
$`\quad \prod^* : {\bf Fam}_\inv \overset{\mrm{contra}}{\longrightarrow} {\bf Set} \In {\bf CAT}`$
$`\mrm{contra}`$ が、関手が反変〈contravariant〉であることを示しています。反変関手については、（詳しく知りたいなら）次の過去記事を参照してください。
$`\prod^*`$ の対象パートはパイ型構成 $`\prod`$ なので、対象 $`F, G`$ に対するホムセット $`{\bf Fam}_\inv(F, G)`$ 上での $`\prod^*`$ のホムパートを定義しましょう。
以下の「$`\cdots`$」部分が明確になれば、パイ関手を定義したことになります。
$`\For (f, \psi) : (I, F) \to (J, G) \In {\bf Fam}_\inv\\
\quad\prod^* ( f, \psi ) =\prod^* ( (f, \psi) ) := \cdots
`$
定義すべき目的の関数を $`\Psi`$ と置いて、書き下すことにしましょう。
$`\Let \Psi :=\prod^* ( f, \psi ) \;: \prod(J, G) \to \prod(I, F) \In {\bf Set}`$
写像 $`\Psi`$ の向きはこれであってます。なぜなら、$`\prod^*`$ は反変関手だからです。
集合 $`\prod(J, G)`$ の要素は、次のタプル〈セクション〉です。
$`\quad y : J \to \sum(J, G) = \sum_{j\in J} G(j)\\
\Where \forall j\in J.\, \pi^G(y(j)) = j`$
定義によれば、$`y(j) \in (\{j\}\times G(j))`$ ですが、暗黙の同一視 $`(\{j\}\times G(j)) \cong G(j)`$ により $`y(j) \in G(j)`$ であるかのようにも扱います。要するに、$`(\{j\}\times G(j)) \leftrightarrow G(j)`$ という切り替えを断りなしにちょくちょく行います。
タプル〈セクション〉 $`y`$ に対する値 $`\Psi(y)`$ を書き下します。
$`\For y \in \prod(J, G)\\
\Define \Psi ( y ) := \\
\quad \lambda\, i\in I.(\, \psi_i ( y(f(i)) ) \;\in F(i)\,)`$
得られた $`\Psi ( y )`$ が $`\pi^F:\sum(I, F) \to I`$ のセクションになっていることはすぐ分かるので、$`\Psi = \prod^* ( f, \psi )`$ が次のプロファイル（域と余域）の関数なのは大丈夫です。
$`\quad \Psi :=\prod^* ( f, \psi ) \;: \prod(J, G) \to \prod(I, F) \In {\bf Set}`$
$`\prod^*`$ が反変関手であるためには、反変の関手性、結合を逆向きに保存すること／恒等を保存することが必要です。これも、律儀に定義を追いかければ出ます。
これで、パイ型構成を関手に拡張できましたが、次の点には注意が必要です。
- $`\prod^*`$ は、$`{\bf Fam}`$ からの関手ではなくて、$`{\bf Fam}_\inv`$ からの関手である。
- $`\prod^*`$ は、共変関手ではなくて反変関手である。
まとめ
シグマ関手の様子を、ひとつの図にまとめてみれば次のようです。
$`\begin{matrix}
\xymatrix{
(I, F) \ar[d]_{(f, \varphi)}^{\text{ in }{\bf Fam}}
\\
(J, G)
}
&
\xymatrix{
{} \ar@{}[d]^{\overset{\sum_*}{ |\!\longrightarrow}}
\\
{}
}
&
\xymatrix{
\sum(I, F) \ar[d]_{\sum_* (f, \varphi) }^{\text{ in }{\bf Set}}
\\
\sum(J, G)
}
\end{matrix}
`$
パイ関手なら次のようです。パイ関手は反変関手なので、射の矢印は逆転します。
$`\begin{matrix}
\xymatrix{
(I, F) \ar[d]_{(f, \psi)}^{\text{ in }{\bf Fam}_\leftarrow}
\\
(J, G)
}
&
\xymatrix{
{} \ar@{}[d]^{\overset{\prod^*}{ |\!\longrightarrow}}
\\
{}
}
&
\xymatrix{
\prod(I, F)
\\
\prod(J, G) \ar[u]^{\prod^* (f, \psi) }_{\text{ in }{\bf Set}}
}
\end{matrix}
`$
関手 $`\prod^*`$ は、ある意味で“逆向き”に作った圏 $`{\bf Fam}_\inv`$ 上で定義され、射の向きが“逆転する”という性質を持つ反変関手です。ニ種類の“逆”が含まれるのでややこしいです。ご注意ください。
