必ずしも関手や自然変換にならないような写像や部分写像も積極的に使うべきだ、ということは何度か言っています。そのことに関するブログ内検索は:
ひとつだけ記事を挙げるなら:
これらの過去記事で、「圏論的コンビネータ」という言葉を使っているのですが、幾つかの事例を出しているだけで、明確な定義を与えていませんでした。この記事で圏論的コンビネータの定義をハッキリさせます。
圏の射と圏の上の圏論的コンビネータが混同される傾向があるので、デカルト圏/デカルト閉圏を事例として、射と圏論的コンビネータが別物であることを説明します。$`\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\hyp}{\text{-} }
\newcommand{\In}{\text{ in } }
\newcommand{\id}{\mathrm{id} }
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\For}{\Keyword{For }}
`$
内容:
ファミリーの圏
インデックス付けられた集合の族〈indexed family of sets〉を単にファミリー〈family〉と呼びます。$`I`$ をインデックス集合〈indexing set〉として、ファミリー $`F`$ のプロファイル(域と余域の仕様)は次のように書けます。
$`\quad F:I \to |{\bf Set}| \In {\bf SET}`$
ここで、$`{\bf SET}`$ は大きな集合 $`|{\bf Set}|`$ も対象として含むような(1レベル上の)集合圏です。
通常、集合族というと、全体集合 $`X`$ の部分集合族を考えることが多いでしょう。
$`\quad F:I \to \mrm{Pow}(X) \In {\bf Set}`$
ここで、$`\mrm{Pow}(X)`$ は $`X`$ のベキ集合です。$`\mrm{Pow}(X) \subset |{\bf Set}|`$ なので、包含写像を後結合すれば、$`F:I \to |{\bf Set}| \In {\bf SET}`$ とみなせます。
一方、$`F:I \to |{\bf Set}|`$ があったとき、
$`\quad X := \bigcup_{i\in I}F(i)`$
と定義すれば、$`F: I \to \mrm{Pow}(X) \In {\bf Set}`$ とみなせます。
全体集合 $`X`$ を考えるかどうかは、目的により適宜調整します。この節では、ファミリーを $`I \to |{\bf Set}|`$ という形の写像だとします。
ファミリー $`F:I \to |{\bf Set}|`$ に対して、そのシグマ型〈sigma type〉は次のように定義します。
$`\quad \sum_{i \in I} F(i) := \bigcup_{i\in I}(\{i\} \times F(i))`$
シグマ型の要素は、$`i\in I`$ と $`x\in F(i)`$ のペア $`(i, x)`$ (依存ペア、タグ付き値)です。$`(i, x) \mapsto i`$ を標準射影〈{canonical | standard} projection〉と呼び、次のように書きます*1。
$`\quad \pi : \sum_{i \in I} F(i) \to I \In {\bf Set}`$
ファミリーのパイ型〈pi type〉は、シグマ型を使って次のように定義します。
$`\quad \prod_{i \in I} F(i) := \{s \in \mrm{Map}(I, \sum_{i \in I} F(i)) \mid s;\pi = \id_I \}`$
パイ型の要素はインデックス集合 $`I`$ からの写像になります。パイ型の要素を、セクション〈section〉、タプル〈tuple〉、選択関数〈choice function〉などと呼びます*2。
$`F:I \to |{\bf Set}|,\, G:J \to |{\bf Set}|`$ が2つのファミリーのとき、ファミリーのあいだの射〈morphism between families〉を、次のように定義します。
- $`F`$ から $`G`$ への射は、ペア $`(f, \alpha)`$
- $`f:I \to J \In {\bf Set}`$
- $`\alpha`$ は、 $`I`$ でインデックスされた写像の族 $`I\ni i\mapsto \alpha_i`$ で、 $`\alpha_i : F(i) \to G(f(i)) \In {\bf Set}`$
$`(f, \alpha) : F \to G`$ と $`(g, \beta): G \to H`$ がファミリーのあいだの射のとき、その結合〈composition〉は次のように定義します。
- $`(f, \alpha); (g; β)`$ を $`(h, \gamma)`$ と置くと:
- $`h:= f;g = g\circ f`$
- $`\gamma_x := \alpha_x ; \beta_{f(x)} = \beta_{f(x)} \circ \alpha_x`$ (チェーンルール*3)
ファミリーの恒等射 $`\id_F`$ は自明に定義できます。結合と恒等は圏の法則〈公理〉を満たすので、ファミリーの全体とそのあいだの射達は圏を形成します。この圏を $`{\bf Fam}`$ とします。
圏 $`{\bf Fam}`$ のホムセットはパイ型とシグマ型を使って表現できます。なお、ファミリー $`F`$ のインデックス集合も明示したいときは $`F = (I, F)`$ と書きます。
$`\quad {\bf Fam}( (I, F), (J, G) ) \cong \sum_{f\in \mrm{Map}(I, J)} \prod_{i\in I}\mrm{Map}(F(i), G(f(i)))`$
射ファミリー
この節では、ファミリーを $`F:I \to \mrm{Pow}(X)`$ の形で考えます。この形だと、$`F`$ は余域が $`X`$ の非決定性写像だとみなすことも出来ますが、非決定性写像としての結合は考えません。それでも、集合 $`X`$ をファミリーのターゲット域〈target domain〉と呼ぶことにします。
$`\cat{C}_1, \cat{C}_2, \cdots, \cat{C}_n`$ を圏の並びだとします。同じ圏が複数回並んでいてもかまいません。サイズの問題を避けるために、出現する圏はすべて小さい圏だと仮定します。ファミリー $`F`$ のターゲット域が、これらの圏の射集合〈set of all morphisms〉の直積であるとき、$`F`$ をn-組・射ファミリー〈n-tuply morphism family〉と呼ぶことにします。n-組・射ファミリーは次のような写像です。
$`\quad F:I \to \mrm{Pow}(\mrm{Mor}(\cat{C}_1) \times \mrm{Mor}(\cat{C}_2) \times \cdots \times \mrm{Mor}(\cat{C}_n) ) \In {\bf Set}`$
インデックス集合も、k個の集合の直積のときは、k-項n-組・射ファミリー〈k-ary n-tuply morphism family〉と呼びます。
$`\quad F:I_1\times \cdots \times I_k \to \mrm{Pow}(\mrm{Mor}(\cat{C}_1) \times \mrm{Mor}(\cat{C}_2) \times \cdots \times \mrm{Mor}(\cat{C}_n) ) \In {\bf Set}`$
k-項n-組・射ファミリーのプロファイルを簡略にして、かつ、k, n を明示的に書くために、次の記法を採用します。
$`\quad F: (I_1, \cdots, I_k) \leadsto (\cat{C}_1, \cat{C}_2, \cdots, \cat{C}_n)`$
プロファイルの書き方は変えましたが、実体はファミリーなので、
$`\For i_1\in I_1, \cdots, i_k \in I_k\\
\quad F(i_1, \cdots, i_k) \in \mrm{Pow}(\mrm{Mor}(\cat{C}_1) \times \mrm{Mor}(\cat{C}_2) \times \cdots \times \mrm{Mor}(\cat{C}_n) )`$
圏のホムセットは、2項1-組・射ファミリーになります。
$`\mrm{Hom}_\cat{C} : (|\cat{C}|, |\cat{C}|) \leadsto (\cat{C})\\
\For A\in |\cat{C}|, B\in |\cat{C}|\\
\quad \mrm{Hom}_\cat{C}(A, B) := \cat{C}(A, B) \;\in \mrm{Pow}(\mrm{Mor}(\cat{C}))`$
圏のエンドセット〈end-set | endo set〉は、1項1-組・射ファミリーになります。
$`\mrm{End}_\cat{C} : (|\cat{C}|) \leadsto (\cat{C})\\
\For A\in |\cat{C}|\\
\quad \mrm{End}_\cat{C}(A) := \cat{C}(A, A) \;\in \mrm{Pow}(\mrm{Mor}(\cat{C}))`$
圏論的コンビネータ
射ファミリーもファミリーなので、射ファミリーのあいだの射は、通常のファミリーのあいだの射として定義します。
$`\quad F: (I_1, \cdots, I_k ) \leadsto (\cat{C}_1, \cdots, \cat{C}_n)\\
\quad G: (J_1, \cdots, J_l )\leadsto (\cat{D}_1, \cdots, \cat{D}_m)
`$
を2つの射ファミリーとして、このあいだの射は、次の2つの構成素で定義されます。
- $`f: I_1 \times \cdots\times I_k \to J_1 \times \cdots\times J_l \In {\bf Set}`$
- $`( \alpha_{i_1, \cdots, i_k}:F(i_1, \cdots, i_k) \to G(g(i_1, \cdots, i_k))\In {\bf Set} )_{(i_1, \cdots, i_k)\in I_1 \times \cdots\times I_k }`$
射ファミリーのあいだの射を特に圏論的コンビネータ〈categorical combinator〉と呼びます。「圏論的」も「コンビネータ」も一般的で多義的な言葉なので、「圏論的コンビネータ」の他の用法とコンフリクトしますが、ここでの圏論的コンビネータはこの意味です。圏論の文脈なら「圏論的」を外して単に「コンビネータ」でもかまいません。
射ファミリー達と圏論的コンビネータ達は全体として圏を形成するので、その圏を $`{\bf Comb}`$ と書いて、{圏論的}?コンビネータの圏〈category of {categorical}? combinators〉と呼びます。
圏 $`{\bf Comb}`$ は圏 $`{\bf Fam}`$ に埋め込めます。$`{\bf Fam}`$ は対象の呼称で圏を命名していて、$`{\bf Comb}`$ は射の呼称で圏を命名しているので注意してください。どちらも、対象はファミリーで、射はファミリーのあいだの射です。
圏論的コンビネータの簡単な例: 圏の結合
圏の結合〈composition〉は圏論的コンビネータとみなせます。まず、コンビネータの両端(域と余域の射ファミリー)を決めます。
$`\mrm{Hom2} : (|\cat{C}|, |\cat{C}|, |\cat{C}| ) \leadsto (\cat{C}, \cat{C})\\
\For A, B, C\in |\cat{C}|\\
\quad \mrm{Hom2}(A, B, C) := \cat{C}(A, B)\times \cat{C}(B, C) \;\in \mrm{Pow}(\mrm{Mor}(\cat{C})\times \mrm{Mor}(\cat{C}))\\
\:\\
\mrm{Hom} : (|\cat{C}|, |\cat{C}| ) \leadsto (\cat{C} )\\
\For A, B \in |\cat{C}|\\
\quad \mrm{Hom}(A, B) := \cat{C}(A, B) \;\in \mrm{Pow}(\mrm{Mor}(\cat{C}) )
`$
コンビネータとしての結合は、以下の構成素で定義されます。$`\mrm{comp} = (\mrm{firstThird}, \mrm{comp})`$ のように記号の乱用をします。
$`\mrm{firstThird} : |\cat{C}|^3 \to |\cat{C}|^2 \In {\bf Set}\\
\For A, B, C\in |\cat{C}|\\
\quad \mrm{firstThird}(A, B, C) := (A, C) \;\in |\cat{C}|^2\\
\:\\
\mrm{comp} : |\cat{C}|^3 \to \mrm{Mor}({\bf Set}) \In {\bf SET}\\
\For A, B, C \in |\cat{C}|\\
\quad \mrm{comp}_{A, B, C} : \mrm{Hom2}(A, B, C) \to \mrm{Hom}(\mrm{firstThird}(A, B, C))
\In {\bf Set}`$
そして、$`\mrm{comp}_{A, B, C}`$ は、圏 $`\cat{C}`$ に備わっている結合演算です。
$`\quad \mrm{comp}_{A, B, C} : \cat{C}(A, B)\times \cat{C}(B, C) \to \cat{C}(A, C)
\In {\bf Set}`$
デカルト圏の圏論的コンビネータ
ここから先は、単なる圏ではなくてデカルト圏またはデカルト閉圏に関係するコンビネータを見ていきます。関係する話が次の記事にあります。
まず、圏 $`\cat{C}`$ はデカルト圏(直積と終対象を持つ)として、デカルト・ペアリングと射影をコンビネータとして定義します。射とコンビネータを区別するために、射は小文字から始める名前かギリシャ文字小文字、コンビネータは大文字から始める名前にします。射とコンビネータは違います。コンビネータは射に働くオペレータです。
デカルト・ペアリング(というコンビネータ)の両端(域と余域の射ファミリー)は次のようになります。
$`\mrm{SpanHom} : (|\cat{C}|, |\cat{C}|, |\cat{C}| ) \leadsto (\cat{C}, \cat{C})\\
\For X, A, B\in |\cat{C}|\\
\quad \mrm{SpanHom}(X, A, B) := \cat{C}(X, A)\times \cat{C}(X, B) \;\in \mrm{Pow}(\mrm{Mor}(\cat{C})\times \mrm{Mor}(\cat{C}))\\
\:\\
\mrm{HomProd} : (|\cat{C}|, |\cat{C}|, |\cat{C}| ) \leadsto (\cat{C})\\
\For X, A, B \in |\cat{C}|\\
\quad \mrm{HomProd}(X, A, B) := \cat{C}(A, A\times B) \;\in \mrm{Pow}(\mrm{Mor}(\cat{C}) )
`$
デカルト・ペアリング自体は次のように定義します。
$`\mrm{Pair} : \mrm{SpanHom} \to \mrm{HomProd} \In {\bf Comb}\\
\mrm{Pair} = (\id, \mrm{Pair})\\
\:\\
\id : |\cat{C}|^3 \to |\cat{C}|^3 \In {\bf Set}\\
\For X, A, B \in |\cat{C}|\\
\quad \id(X, A, B) := (X, A, B) \:\in |\cat{C}|^3\\
\:\\
\mrm{Pair} : |\cat{C}|^3 \to \mrm{Mor}({\bf Set}) \In {\bf SET}\\
\For X, A, B \in |\cat{C}|\\
\quad \mrm{Pair}_{X, A, B} : \mrm{SpanHom}(X, A, B) \to \mrm{HomProd}(\id(X, A, B) )
\In {\bf Set}\\
\quad \For f\in \cat{C}(X, A), g\in \cat{C}(X, B)\\
\qquad \mrm{Pair}_{X, A, B}(f, g):= \langle f, g\rangle \;\in \cat{C}(X, A\times B)
`$
最後の行の $`\mrm{Pair}_{X, A, B}(f, g):= \langle f, g\rangle`$ は、$`\langle \hyp, \hyp\rangle`$ が公理的に与えられているときは同語反復(別名を付けただけ)ですが、集合圏などではより具体的な定義に還元できます。
集合圏における $`\langle \hyp, \hyp\rangle`$ の具体的な定義は:
$`\For X, A, B \in |{\bf Set}|\\
\For f:X \to A,\, g:X \to B \In {\bf Set}\\
\quad \langle f, g\rangle := \lambda\, x\in X.(\, (f(x), g(x)) \;\in A\times B\,)`$
[/補足]
デカルト圏には、射影射〈projection morphism〉
$`\quad \pi^{A, B}_1 : A\times B \to A \In \cat{C}\\
\quad \pi^{A, B}_2 : A\times B \to B \In \cat{C}`$ があります。射影射を使って、コンビネータとしての射影を定義できます。詳細に定義する代わりに、$`\hyp`$ を使って簡潔に(その代償にやや曖昧に)書きます。
$`\mrm{Proj1} : \cat{C}(\hyp, \hyp \times \hyp) \to \cat{C}(\hyp, \hyp) \In {\bf Comb}\\
\mrm{Proj1} = (\id, \mrm{Proj1})\\
\:\\
\id := \id_{|\cat{C}|^3}
\:\\
\mrm{Proj1} : |\cat{C}|^3 \to \mrm{Mor}({\bf Set}) \In {\bf SET}\\
\For X, A, B \in |\cat{C}|\\
\quad \mrm{Proj1}_{X, A, B} : \cat{C}(X, A \times B) \to \cat{C}(X, A) \In {\bf Set}\\
\quad \For h\in \cat{C}(X, A\times B)\\
\qquad \mrm{Proj1}_{X, A, B}(h) := h;\pi^{A, B}_1 \;\in \cat{C}(X, A)
`$
この例で、射影射 $`\pi^{A, B}_1`$ と射影コンビネータ $`\mrm{Proj1}`$ は別物です。混同しないように。
コンビネータ $`\mrm{Proj2}`$ も同様に定義できます。デカルト・ペアリングのコンビネータと射影のコンビネータのあいだには次の関係があります。
$`\For X, A, B \in |\cat{C}|\\
\For f\in \cat{C}(X, A), g\in \cat{C}(X, B)\\
\quad \mrm{Proj1}_{X, A, B}(\mrm{Pair}_{X, A, B}(f, g) ) = f\\
\quad \mrm{Proj2}_{X, A, B}(\mrm{Pair}_{X, A, B}(f, g) ) = g
`$
デカルト閉圏の圏論的コンビネータ
$`\cat{C}`$ をデカルト閉圏とします。デカルト閉圏には、指数がありますが、左指数と右指数を区別して書くことにします。カリー同型は次のようになります。
$`\quad \cat{C}(A\times B, C) \cong \cat{C}(A, C^B) \In {\bf Set}\\
\quad \cat{C}(A\times B, C) \cong \cat{C}(B, {^A C}) \In {\bf Set}
`$
左右の評価射〈left/right evaluation morphism〉も区別します。
$`\quad \mrm{rev}_{A, B} : B^A \times A \to B \In \cat{C}\\
\quad \mrm{lev}_{A, B} : A \times {^A B} \to B \In \cat{C}
`$
射 $`\mrm{rev}_{A, B},\, \mrm{lev}_{A, B}`$ に対応するコンビネータ $`\mrm{REv}_{X, A, B},\, \mrm{LEv_{X, A, B}}`$ を定義しましょう。
$`\mrm{REv} : \cat{C}(\hyp , \hyp^\hyp )\times \cat{C}(\hyp, \hyp) \to \cat{C}(\hyp, \hyp) \In {\bf Comb}\\
\mrm{REv} = (\mrm{FirstThird}, \mrm{REv})\\
\:\\
\mrm{firstThird} : |\cat{C}|^3 \to |\cat{C}|^2 \In {\bf Set}\\
\For X, A, B\in |\cat{C}|\\
\quad \mrm{firstThird}(X, A, B) := (X, B) \;\in |\cat{C}|^2\\
\:\\
\mrm{REv} : |\cat{C}|^3 \to \mrm{Mor}({\bf Set}) \In {\bf SET}\\
\For X, A, B \in |\cat{C}|\\
\quad \mrm{REv}_{X, A, B} : \cat{C}(X, B^A)\times \cat{C}(X, A) \to \cat{C}(X, B)
\In {\bf Set}\\
\quad \For f\in \cat{C}(X, B^A), a\in \cat{C}(X, A)\\
\qquad \mrm{REv}_{X, A, B}(f, a) := \langle f, a\rangle; \mrm{rev}_{A, B} \;\in \cat{C}(X, B)
`$
この例で、右評価射 $`\mrm{rev}_{A, B}`$ と右評価コンビネータ $`\mrm{REv}`$ は別物です。左評価コンビネータ $`\mrm{LEv}`$ も同様に定義できます。
圏に関する計算では、対象・射の計算だけではなくて圏論的ファミリーや圏論的コンビネータの計算をしていることも多くあります。対象、射、ファミリー、コンビネータをゴッチャにしないで区別しながら計算しましょう。