レンズ／オプティックなどの議論では、エンド／コエンドをヘビーに使います。この記事では、自然変換の集合をエンドで表示することを目的にして、エンドの説明をします。当該の目的に不要なことはカットして、できるだけ短い説明にします。
この記事内では、小さい圏の対象をラテン小文字で表すので注意してください。$`
\newcommand{\End}{\overline{\prod} }
\newcommand{\qto}[1]{\mathrel{\text{-}_{\text{#1}}\!\!\!\to} }
\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\In}{\text{ in } }
\newcommand{\op}{\mathrm{op} }
\newcommand{\id}{\mathrm{id} }
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
\newcommand{\Define}{\Keyword{Define } }%
\newcommand{\Where}{\Keyword{Where } }%
\newcommand{\Declare}{\Keyword{Declare } }%
`$
内容：
プロ関手とエンド
$`\cat{C}, \cat{D}`$ は小さい圏とします。$`\cat{C}`$ から $`\cat{D}`$ へのプロ関手〈profunctor〉とは、$`\cat{C}^\op \times \cat{D} \to {\bf Set}`$ という関手のことです。「米田テンソル計算 2： 準備 // 修飾付き矢印」で述べたように、プロ関手のプロファイルは修飾付き矢印を使います。次はすべて同じ意味です。
- $`P`$ は、$`\cat{C}`$ から $`\cat{D}`$ へのプロ関手
- $`P: \cat{C} \qto{p} \cat{D}`$
- $`P: \cat{C}^\op \times \cat{D} \to {\bf Set}`$
修飾されてない矢印は関手を表します。
次もすべて同じ意味です。
- $`P`$ は、$`\cat{C}`$ の自己プロ関手〈endo-profunctor〉
- $`P: \cat{C} \qto{p} \cat{C}`$
- $`P: \cat{C}^\op \times \cat{C} \to {\bf Set}`$
自己プロ関手の最も重要な例は、プロ関手と解釈したホム関手です。
- $`\cat{C}(-, -)`$ は、$`\cat{C}`$ の自己プロ関手
- $`\cat{C}(-, -): \cat{C} \qto{p} \cat{C}`$
- $`\cat{C}(-, -): \cat{C}^\op \times \cat{C} \to {\bf Set}`$
エンド〈end〉は、自己プロ関手に対して集合（$`{\bf Set}`$ の対象）を割り当てる対応です。
$`
\quad (P:\cat{C} \qto{p} \cat{C}) \mapsto \mrm{end}(P) \in |{\bf Set}|
`$
自己プロ関手のあいだの自然変換に写像を割り当てる対応もありますが、今日は触れません。
これからこの記事で、自己プロ関手 $`P`$ のエンド $`\mrm{end}(P)`$ の具体的な構成について述べていきます。
関手のドットパートとアローパート
対象と射の図式をラベルを付けないで描けば：
$`\xymatrix{
{\cdot} \ar[dr] \ar[r] & {\cdot} \ar[d] \\
{} & {\cdot}
}
`$
対象はドットで射はアローです。ドットが対象の象徴、アローは射の象徴と考えて、関手の対象パートと射パートを次のように表します。
$`\For F:\cat{C} \to \cat{D} \In {\bf Cat}\\
\quad \dot{F} := F_{\mrm{obj}} : |\cat{C}| \to |\cat{D}| \In {\bf Set}\\
\quad \vec{F} := F_{\mrm{mor}} : \mrm{Mor}(\cat{C}) \to \mrm{Mor}(\cat{D}) \In {\bf Set}
`$
関手 $`F`$ のドットパート〈対象パート〉とアローパート〈射パート〉は通常オーバーロードされますが、区別したほうがいいときもあるので、この記法を導入しました。
関手の域・余域に大きな圏が含まれる場合も同様な記法を使います。特にプロ関手に関しては：
$`\For P:\cat{C}^\op \times \cat{C} \to {\bf Set} \In {\bf CAT}\\
\quad \dot{P} := P_{\mrm{obj}} : |\cat{C}^\op|\times |\cat{C}| \to |{\bf Set}| \In {\bf SET}\\
\quad \vec{P} := P_{\mrm{mor}} : \mrm{Mor}(\cat{C}^\op)\times\mrm{Mor}(\cat{C}) \to \mrm{Mor}({\bf Set}) \In {\bf SET}
`$
集合としては、$`|\cat{C}^\op| = |\cat{C}|`$ 、$`\mrm{Mor}(\cat{C}^\op)= \mrm{Mor}(\cat{C})`$ ですが、$`(-)^\op`$ は残しておきます。
ドット／アローはいつでも付けるわけではありません。関手やプロ関手の対象パート／射パートの違いを強調したいときに使う注釈的記法です。なくてもかまわないし、あっても無視できます。
自己プロ関手の対角総直積
エンドの記号として、「米田の「よ」とニンジャ米田の補題」で述べた次の記法を使います。
$`\quad
\mathrm{end}(P) = \End_{x \in|\cat{C}|} \dot{P}(x, x) \;\in |{\bf Set}|
`$
この記号を採用する理由は、エンドが総直積の部分集合として定義されるからです。
$`\quad
\End_{x \in|\cat{C}|} \dot{P}(x, x) \subseteq \prod_{x \in|\cat{C}|} \dot{P}(x, x)
`$
エンドの親集合である $`\prod_{x \in|\cat{C}|} \dot{P}(x, x) `$ は、集合族の総直積です。その集合族とは：
$`\quad
\lambda\, x\in |\cat{C}|.(\, \dot{P}(x, x)\; \in |{\bf Set}|\,)
: |\cat{C}| \to |{\bf Set}| \In {\bf SET }
`$
これは、自己プロ関手のドットパート $`\dot{P}:|\cat{C}^\op|\times |\cat{C}| \to |{\bf Set}|`$ の対角部分への制限です。この集合族の総直積とは、対角部分 $`\Delta_{|\cat{C}|} \subseteq |\cat{C}|\times |\cat{C}|`$ に渡って $`\dot{P}`$ の成分（集合）をすべて掛け合わせたものです。
総直積は、「リスト、タプル、タグ付きデータ、関数、依存関数」で述べた“型ファミリー〈集合族〉のパイ型”とまったく同じ概念です。
総直積＝パイ型 の定義から、次の2つは同じ意味です。
- $`\xi \in \prod_{x \in|\cat{C}|} \dot{P}(x, x) `$
- $` \xi:|\cat{C}| \to \bigcup_{x\in |\cat{C}|}\dot{P}(x, x)`$ かつ $`\forall x\in |\cat{C}|.\, \xi(x)\in \dot{P}(x, x)`$
対角総直積の典型的な例に、圏 $`\cat{C}`$ の自己ホムセット〈エンドセット〉をすべて掛けた $`\prod_{x\in |\cat{C}|} \cat{C}(x, x)`$ があります。この対角総直積の要素は、対象ごとに自己射を割り当てたタプル $`\xi`$ です。
$`\quad |\cat{C}| \ni x \mapsto \xi_x \in \cat{C}(x, x)`$
エンド条件
前節で述べたように、自己プロ関手のエンドは、対角総直積の部分集合になっているので次のように書けます。
$`\quad
\End_{x \in|\cat{C}|} \dot{P}(x, x) = \{\xi \in \prod_{x \in|\cat{C}|} \dot{P}(x, x) \mid \cdots \}
`$
今は明示されてない絞り込みの条件をエンド条件〈end condition〉と呼ぶことにします*1。エンド条件を以下で順次明らかにします。
対角総直積は無限個の成分の直積かも知れませんが、射影関数を持ちます。
$`\For w\in |\cat{C}|\\
\Declare \pi_w: \prod_{x \in|\cat{C}|} \dot{P}(x, x) \to \dot{P}(w, w) \In {\bf Set}\\
\For \xi \in \prod_{x \in|\cat{C}|} \dot{P}(x, x)\\
\Define \pi_w(\xi) := \xi(w) \;\in \dot{P}(w, w)
`$
射影関数を適用することは、タプルの成分を取ることですが、それは関数としてのタプルを評価することです。次は同値です。
- タプル $`\xi`$ に射影関数 $`\pi_w`$ を適用する。
- タプル $`\xi`$ の第$`w`$成分を取る。
- 関数 $`\xi`$ を点$`w`$において評価する。（タプルは関数。）
つまり：
$`\quad \pi_w(\xi) = \xi_w = \xi(w) `$
エンド条件は、射ごとに決まる等式（方程式）を、すべての射に渡って“連立”します。ひとつの射 $`f:a \to b \In \cat{C}`$ に対する条件〈等式 | 方程式〉は次の可換図式で表されます。
$`\xymatrix{
{}
& {\prod_{x \in|\cat{C}|} \dot{P}(x, x)} \ar[dl]_{\pi_a}\ar[dr]^{\pi_b}
& {}
\\
{\dot{P}(a, a)} \ar[dr]_{\vec{P}(a, f)}
& {}
& {\dot{P}(b, b)} \ar[dl]^{\vec{P}(f, b)}
\\
{}
& {\dot{P}(a, b)}
& {}
}\\
\text{commutative in }{\bf Set}
`$
混乱の心配がないので、$`\id_a`$ を $`a`$ と書いています。一時的に $`f_* := \vec{P}(a, f),\, f^* := \vec{P}(f, b)`$ と略記して、要素を追いかけると：
$`\xymatrix{
{}
& {\xi} \ar@{|->}[dl]_{\pi_a}\ar@{|->}[dr]^{\pi_b}
& {}
\\
{\xi_a} \ar@{|->}[dr]_{ f_*}
& {}
& {\xi_b} \ar@{|->}[dl]^{f^*}
\\
{}
& {f_*(\xi_a) = f^*(\xi_b) }
& {}
}
`$
これは単一の射に対する条件なので、すべての射に対して連立させると、次のような全称命題になります。
$`\quad
\forall f:a \to b \In \cat{C}.\,
\vec{P}(a, f)(\xi_a) = \vec{P}(f, b)(\xi_b )\\
\Where\\
\quad \xi_a := \pi_a(\xi)\\
\quad \xi_b := \pi_b(\xi)\\
`$
これがエンド条件です。この条件により、自己プロ関手のエンドは以下のように定義します。
$`
\Define \End_{x \in|\cat{C}|} \dot{P}(x, x) := \\
\quad \{\xi \in \prod_{x \in|\cat{C}|} \dot{P}(x, x) \mid \\
\qquad \forall f:a \to b \In \cat{C}.\, \vec{P}(a, f)(\xi_a) = \vec{P}(f, b)(\xi_b )\\
\quad \} \\
\Where\\
\quad \xi_a := \pi_a(\xi)\\
\quad \xi_b := \pi_b(\xi)\\
`$
対角総直積 $`\prod_{x\in |\cat{C}|} \cat{C}(x,x)`$ をエンド条件で絞り込んでエンドを作ると次のようになります（確認してみてください）。
$`\quad \End_{x\in |\cat{C}|}\cat{C}(x, x) = \{\id \} = \{(\id_x)_{x\in |\cat{C}|} \}`$
エンドを構成する手順をまとめると次のようです。
- 対象の集合 $`|\cat{C}|`$ に渡って、集合族 $`(\dot{P}(x, x))_{x\in \cat{C}}`$ の総直積を作る。
- 射の集合 $`\mrm{Mor}(\cat{C})`$ に渡って、射 $`f`$ のエンド条件をすべて連立させて（論理ANDを取って）絞り込みをする。
この構成法が、自然変換の定義と同じになっていることを次節で見ます。
自然変換の集合
この記事の目的である事実を説明します。$`F, G:\cat{C}\to\cat{D} \In {\bf Cat}`$ を2つの関手とします。$`F`$ から $`G`$ への自然変換全体の集合を $`\mrm{Nat}(F, G)`$ と書きます。この自然変換の集合はエンドを使って次のように書けます。
$`\quad
\mrm{Nat}(F, G) \cong \End_{x\in |\cat{C}|} \dot{\cat{D}}(F(x), G(x))
`$
このことをこの節と次節で示します。
まず、$`\alpha \in \mrm{Nat}(F, G)`$ とはどういうことかをおさらいすると：
- $`\alpha `$ は、対象でインデックスされた射の族である。つまり、
$`\quad \alpha = (\alpha_x : F(x) \to G(x)\;\In \cat{D})_{x\in |\cat{C}|} `$ - $`\alpha`$ は自然性の条件を満たす。
一番目から次が言えます。
$`\quad
\alpha \in \prod_{x\in|\cat{C}|} \dot{\cat{D}}(F(x), G(x))
`$
なぜなら、$`x \mapsto \alpha_x`$ は次の条件を満たすからです。
- $`\alpha : |\cat{C}| \to \bigcup_{x\in |\cat{C}|} \dot{\cat{D}}(F(x), G(x))`$
- $`\forall x\in |\cat{C}|.\, \alpha_x \in \dot{\cat{D}}(F(x), G(x))`$
あとは、エンド条件と自然性の条件が同じであることを示せばいいわけです。自然性の条件は次のようでした。
$`\require{AMScd}
\forall f:a \to b \In \cat{C}.\\
\begin{CD}
F(a) @>{\alpha_a}>> G(a)\\
@V{F(f)}VV @VV{G(f)}V\\
F(b) @>{\alpha_b}>> G(b)
\end{CD}\\
\text{commutative in }{\bf Set}
`$
等式で書けば：
$`\quad \forall f:a \to b \In \cat{C}.\\
\qquad \alpha_a ; G(f) = F(f) ; \alpha_b`$
これは次のようにも書けます。
$`\quad \forall f:a \to b \In \cat{C}.\\
\qquad G(f)_*(\alpha_a) = F(f)^*(\alpha_b) `$
ここで、下付きアスタリスク／上付きアスタリスクはそれぞれ、ポスト結合による前送りとプレ結合による引き戻しです。
上記の条件は、ほとんどエンド条件ですが、自然性とエンド条件が一致することを示すには次のことを確認する必要があります。
$`
\quad \vec{P}(a, f)(\alpha_a) = \alpha_a; G(f) \\
\quad \vec{P}(f, b)(\alpha_b) = F(f); \alpha_b \\
\Where\\
\quad \vec{P}(-, - ) := \vec{\cat{D}}(F(-), G(-))
`$
節をあらためて等式を確認しましょう。
自然性とエンド条件
圏 $`\cat{C}`$ のホム関手 $`\cat{C}(-, -)`$ は自己プロ関手なので、同じ記号 $`\cat{C}(-, -)`$ でプロ関手も表すとします。圏を表す記号がオーバーロードされるので注意してください。
ホム・プロ関手のアローパート $`\vec{\cat{C}}`$ は次の公式で与えられます。
$`\quad \vec{\cat{C}}(h, k)(u) = h;u;k `$
引数 $`u`$ に対して、$`h`$ によるプレ結合〈pre-composition〉と $`k`$ によるポスト結合〈post-composition〉をしているのでディ結合〈di-composition〉と呼びますが、ここではより分かりやすいサンドイッチ結合〈sandwich composition〉と呼び、上記の公式はサンドイッチ公式として参照します。
サンドイッチ結合を図に描くと次のようです。
$`
\begin{CD}
\cdot @>{\vec{\cat{C}}(h, k)(u) }>> \cdot\\
@V{h}VV @AA{k}A\\
\cdot @>>{u \in \dot{\cat{C}}(\cdot, \cdot)}> \cdot
\end{CD}
`$
ラベル〈名前〉を付けないままにプロファイルを書けば：
$`\quad \vec{\cat{C}}(h, k): \dot{\cat{C}}(\cdot, \cdot) \to \dot{\cat{C}}(\cdot, \cdot) \In {\bf Set}\\
\Where\\
\quad \vec{\cat{C}}(h, k)(-) := h;-;k = k\circ - \circ h
`$
次も成立します。
$`\quad \vec{\cat{C}}(h, k) = h^*;k_* = k_*;h^* `$
$`h^*`$ はプレ結合による引き戻し、$`k_*`$ はポスト結合による前送りです。引き戻しと前送りが可換なのは、結合の結合律〈associative law of composition〉からです。いずれにしてもサンドイッチ結合を定義します。
さて、前節最後の等式は次のような計算で出ます。
$`\quad \vec{P}(a, f)(\alpha_a) \\
= \vec{\cat{D}}(F(\id_a), G(f))(\alpha_a)\\
= F(\id_a) ; \alpha_a ; G(f)\\
= \id_{F(a)} ; \alpha_a ; G(f)\\
= \alpha_a ; G(f)\\
\:\\
\quad \vec{P}(f, b)(\alpha_b) \\
= \vec{\cat{D}}(F(f), G(\id_b))(\alpha_b)\\
= F(f); \alpha_b; G(\id_b)\\
= F(f); \alpha_b; \id_{G(b)}\\
= F(f); \alpha_b
`$
以上で、射の族の自然性がエンド条件と一致することが示せました。結論を再掲すれば：
$`\quad
\mrm{Nat}(F, G) \cong \End_{x\in |\cat{C}|} \dot{\cat{D}}(F(x), G(x))
`$
*1:エンドは総直積をエンド条件で絞り込んで部分集合を作り、コエンドは総直和をコエンド同値関係で割って商集合を作ります。
