「自然変換の集合のエンド表示」で、自然変換の集合がエンドで表現できることを示しました。投稿の時間順序は前後してますが、必要な基本事項を「ホム関手とサンドイッチ結合」で解説しています。また、「米田テンソル計算 3： 米田の「よ」、米田の星、ディラックのブラケット 再論」では、米田の「よ」記法について説明し、ニンジャ米田の補題にも触れました。
この記事では、ニンジャ米田の補題を主題的に扱い、その証明もします。上記の過去記事の内容は仮定しますが、必要に応じて拾い読みすればいいでしょう。$`
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\id}{\mathrm{id} }
\newcommand{\op}{\mathrm{op} }
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\In}{\text{ in } }
\newcommand{\Imp}{\Rightarrow }
\newcommand{\Iff}{\Leftrightarrow }
%
\newcommand{\End}{\overline{\prod} }
\newcommand{\vin}{ \style{display: inline-block; transform: rotate(-90deg)}{\in} }
%
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
\newcommand{\Define}{\Keyword{Define } }%
\newcommand{\Declare}{\Keyword{Declare } }%
\newcommand{\Holds}{\Keyword{Holds } }%
\newcommand{\Where}{\Keyword{Where } }%
\newcommand{\Using}{\qquad \Keyword{Using } }%
%`$
内容：
ニンジャ米田の補題
ニンジャ米田の補題〈ninja Yoneda lemma〉は、集合圏値関手のエンドに関する次の命題です。
$`\For \cat{C} \in |{\bf Cat}|\\
\For F:\cat{C} \to {\bf Set} \In {\bf CAT}\\
\For a\in |\cat{C}|\\
\Holds \End_{x\in |\cat{C}|} F(x)^{よ_a(x)} \cong F(a) \;\In {\bf Set}
`$
ここで：
- $`{\bf Cat}`$ は、小さい圏の2-圏
- $`{\bf CAT}`$ は、小さいとは限らない圏の2-圏
- $`\End`$ は、エンドを表す記号
- $`よ_a(x) = {^\cat{C}よ}_a(x) = \cat{C}(a, x)`$
米田の「よ」とクロネッカーのデルタは類似している（「米田の「よ」とニンジャ米田の補題」参照）ので、上記のニンジャ米田の補題は次の公式に相当します。
$`\For I \in |{\bf FinSet}|\\
\For f:I \to {\bf R} \In {\bf Set}\\
\For n \in I\\
\Holds \prod_{i\in I} f(i)^{\delta_n(i)} = f(n) \;\text{ on } {\bf R}
`$
集合圏における指数 $`B^A`$ は、他に次のような書き方もあります*1。
- $`[A, B]`$
- $`A \text{ -> } B`$ （プログラミング言語）
- $`{\bf Set}(A, B)`$ （指数とホムセットは一致する）
- $`\mrm{Map}(A, B)`$
ブラケットが見やすいので、ブラケットを使うことにします。ブラケットを使ってニンジャ米田の同型を書けば：
$`
\quad \End_{x\in |\cat{C}|} [{よ_a(x)}, F(x)] \cong F(a) \;\In {\bf Set}
`$
本家・米田の補題からニンジャ米田の補題
本家・米田の補題〈classical Yoneda lemma〉は次の命題です。
$`\For \cat{C} \in |{\bf Cat}|\\
\For F:\cat{C} \to {\bf Set} \In {\bf CAT}\\
\For a\in |\cat{C}|\\
\Holds \mrm{Nat}(よ_a, F) \cong F(a) \In {\bf Set}
`$
ここで、$`\mrm{Nat}(-, -)`$ は2つの関手のあいだの自然変換の集合です。“すべての自然変換の集まり”という得体の知れない集まりが、関手の値（である集合）で記述されてしまう、という主張です。自然変換である条件（自然性）が非常に強い条件なので、結局のところ自然変換は少ないのです。
一方、「自然変換の集合のエンド表示」で示した“自然変換の集合のエンド表示”を集合圏に適用すると次の命題になります。
$`\For \cat{C} \in |{\bf Cat}|\\
\For F, G:\cat{C} \to {\bf Set} \In {\bf CAT}\\
\Holds \mrm{Nat}(F, G) \cong \End_{x\in |\cat{C}|} [F(x), G(x)] \In {\bf Set}
`$
これらを使えば、ニンジャ米田の補題は次のごく短い計算で出ます。
$`\quad \End_{x\in |\cat{C}|} [{よ_a(x)}, F(x)] \\
\Using \text{ 自然変換の集合のエンド表示 }\\
\cong \mrm{Nat}(よ_a, F)\\
\Using \text{ 本家・米田の補題}\\
\cong F(a)
`$
本家・米田の補題
本家・米田の補題を示しておきます。何の工夫もなしに、愚直な直接計算を使うことにします。
示すべきことは $`\mrm{Nat}(よ_a, F) \cong F(a)`$ なので、2つの集合のあいだの同型（可逆写像）を具体的に構成します。前節のセッティングは引き継ぎます。念の為繰り返し書くと：
$`
\quad \cat{C} \in |{\bf Cat}|\\
\quad F:\cat{C} \to {\bf Set} \In {\bf CAT}\\
\quad a\in |\cat{C}|
`$
まず、$`\mrm{Nat}(よ_a, F) \to F(a)`$ の方向の写像を定義します。
$`\Declare \Phi : \mrm{Nat}(よ_a, F) \to F(a) \In {\bf Set} \\
\For \xi \in \mrm{Nat}(よ_a, F)\\
\Define \Phi(\xi) := \xi_a(\id_a) \in F(a)
`$
補足説明します； $`\xi`$ は自然変換なので成分を持ちます。特に$`a`$成分を取ると：
$`\quad \xi_a : よ_a(a) \to F(a) \in {\bf Set}`$
$`よ_a(a) = \cat{C}(a, a)`$ なので $`\id_a \in よ_a(a)`$ 、この特定の射（ホムセットの要素）を写像 $`\xi_a`$ に渡した値が $`\Phi(\xi)`$ です。
次に、$`F(a) \to \mrm{Nat}(よ_a, F)`$ の方向の写像を定義します。
$`\Declare \Psi: F(a) \to \mrm{Nat}(よ_a, F) \In {\bf Set} \\
\For t \in F(a) \\
\Define \Psi(t) := \lambda\, x\in |\cat{C}|.\,
\lambda\, u\in \cat{C}(a, x).(\, F(u)(t) \;\in F(x) \,)
`$
入れ子になったラムダ式が分かりにくいかも知れません。入れ子を分解して書いてみます。
$`
\Define \Psi(t) := (\tau_x)_{x\in |\cat{C}|} :: よ_a \Rightarrow F : \cat{C} \to {\bf Set} \In {\bf CAT}\\
\Where\\
\quad \For x\in |\cat{C}|\\
\quad \Declare \tau_x : よ_a(x) = \cat{C}(a, x) \to F(x) \In {\bf Set}\\
\quad \Define \tau_x := \lambda\, u\in \cat{C}(a, x).(\, F(u)(t) \;\in F(x) \,)
`$
次の図も参考になるでしょう。
$`
\begin{array}{cccc}
a & \overset{u}{\longrightarrow} & x & \In \cat{C}\\
& \downarrow F & &\\
F(a)&\overset{F(u)}{\longrightarrow}& F(x)& \In {\bf Set}\\
\vin & & \vin & \\
t & \mapsto & F(u)(t) \\
\end{array}
`$
以上で、写像の族 $`(\tau_x)_{x\in |\cat{C}|}`$ は定義できましたが、これが自然変換であるには自然性が必要です。自然性は次の図式の可換性です。
$`\require{AMScd}
\forall f:x \to y \In \cat{C}.\\
\begin{CD}
よ_a(x) @>{\tau_x}>> F(x) \\
@V{よ_a(f)}VV @VV{F(f)}V\\
よ_a(y) @>{\tau_y}>> F(y)
\end{CD}\\
\text{commutative in }{\bf Set}
`$
可換四角形を等式で書けば：
$`\For u\in よ_a(x) = \cat{C}(a, x)\\
\Holds F(f)(\tau_x(u)) = \tau_y(よ_a(f)(u))
`$
計算してみると：
$`
\quad F(f)(\tau_x(u)) \\
\Using \tau_x = \Psi(t)_x \text{ の定義}\\
= F(f)(F(u)(t)) \\
\Using { 写像の結合の定義}\\
= (F(f)\circ F(u)) (t)\\
\Using F {の関手性}\\
= F(f\circ u)(t) \\
\:\\
\quad \tau_y(よ_a(f)(u))\\
\Using よ_a(f) \text{ の定義}\\
= \tau_y ( \cat{C}(\id_a, f)(u) )\\
\Using \text{サンドイッチ結合}\\
= \tau_y ( f\circ u \circ \id_a )\\
\Using \text{恒等射だから}\\
= \tau_y ( f\circ u )\\
\Using \tau_y = \Psi(t)_y \text{ の定義}\\
= F(f\circ u)(t)
`$
これで、$`\Psi(t) = \tau \in \mrm{Nat}(よ_a, F)`$ が示せました。
本家・米田の補題 続き
$`\Phi`$ と $`\Psi`$ が互いに逆写像になること、つまり次の2つの命題を示す必要があります。
$`
\quad \forall \xi \in \mrm{Nat}(よ_a, F).\, \Psi(\Phi(\xi)) = \xi\\
\quad \forall t \in F(a).\, \Phi(\Psi(t)) = t
`$
これらも計算で示します。
まず、$` \Psi(\Phi(\xi)) = \xi`$ を示します。計算の途中で、自然変換 $`\xi :: よ_a \Rightarrow F`$ の自然性を使うので、先に注意しておきます。特定の射 $`u:a \to x \In \cat{C}`$ に対する自然性可換図式は次のようです。
$`
\For u:a \to x \In \cat{C}\\
\begin{CD}
よ_a(a) @>{\xi_a}>> F(a)\\
@V{よ_a(u)}VV @VV{F(u)}V\\
よ_a(x) @>{\xi_x}>> F(x)
\end{CD}\\
\text{commutative in }{\bf Set}
`$
これを等式に翻訳すれば：
$`\quad
F(u)\circ \xi_a = \xi_x \circ よ_a(u)
`$
$`よ`$ をホム関手（「ホム関手とサンドイッチ結合」参照）として書けば：
$`\quad
F(u)\circ \xi_a = \xi_x \circ \cat{C}(a, u) = \xi_x \circ \cat{C}(\id_a, u)
`$
この等式は、後で「自然性等式」として参照します。
では計算しましょう。最初に、
$`\quad
s := \Phi(\xi) = \xi_a(\id_a) \in F(a) `$
と置きます。$`\Psi(s)`$ は自然変換になるので、その$`x`$成分を計算します。
$`
\quad \Psi(s)_x\\
\Using \Psi(s)_x \text{ の定義}\\
= \lambda\, u\in \cat{C}(a, x).\, F(u)(s)\\
\Using s \text{ の定義}\\
= \lambda\, u\in \cat{C}(a, x).\, F(u)( \xi_a(\id_a) )\\
\Using { 写像の結合の定義}\\
= \lambda\, u\in \cat{C}(a, x).\, (F(u) \circ \xi_a)(\id_a) \\
\Using { 自然性等式}\\
= \lambda\, u\in \cat{C}(a, x).\, (\xi_x \circ \cat{C}(\id_a, u) )(\id_a) \\
\Using { 写像の結合の定義}\\
= \lambda\, u\in \cat{C}(a, x).\, \xi_x( \cat{C}(\id_a, u) (\id_a) )\\
\Using { サンドイッチ結合}\\
= \lambda\, u\in \cat{C}(a, x).\, \xi_x( u \circ \id_a \circ \id_a )\\
\Using { 恒等射だから}\\
= \lambda\, u\in \cat{C}(a, x).\, \xi_x(u)\\
\Using { ラムダ記号の消去}\\
= \xi_x
`$
これで、$` \Psi(\Phi(\xi)) = \xi`$ は示せました。
次は $` \Phi(\Psi(t)) = t`$ を示します。
$`\quad
\tau := \Psi(t) \in \mrm{Nat}(よ_a, F)`$
と置きます。$`\Phi(\Psi(t)) = \Phi(\tau) `$ を計算します。
$`
\quad \Phi(\tau)\\
\Using \Phi(\tau) { の定義}\\
= \tau_a(\id_a) \\
\Using \tau_a { の定義}\\
= (\lambda\, u\in \cat{C}(a, a).\, F(u)(t))(\id_a)\\
\Using {ラムダ式の代入}\\
= F(\id_a)(t)\\
\Using F{ の関手性}\\
= \id_{F(a)}(t)\\
\Using { 恒等写像だから}\\
= t
`$
これで $` \Phi(\Psi(t)) = t`$ は示せました。
おわりに
2008年4月に書いた記事「自己関手の圏とモナド // 余談：圏論は、ほぼ計算だけ」で次のように書いています：
圏論は、抽象的な印象を受けます（事実、まー抽象論と言っていいでしょう）が、定義を理解したら（いや、理解できなくても）、あとは計算するだけです。僕はモノグサなので、計算の手間を嫌って他の手段で理解しようと試みたりしますが、結局我慢して計算するハメになります。教訓としては、四の五の言ってないで計算するほうがいいと思います。
圏論の最重要定理である米田の補題も、ご覧の通りの愚直な計算です。
ただ計算を追うだけでは味気ないでしょうから、米田の補題の意義や周辺事情は例えば次の記事を参照してください。
米田の補題の直接的産物である米田埋め込みのプログラミング的な意味、米田埋め込みによる確率変数の解釈、米田埋め込みを単位とするモナドの話が次の記事にあります。
- CPS（継続渡し方式）変換をJavaScriptで説明してみるべ、ナーニ、たいしたことねーべよ
- CPS（継続渡し方式）変換で裏返る理由
- 「確率変数」の正体は米田埋め込み
- 米田埋め込み、米田拡張、そして米田モナド
その他：
「米田の補題に向けてのオシャベリ」は、ほぼ15年前の2007年1月の記事です。が、米田写像（Yoneda map、この記事の $`\Phi, \Psi`$ のこと）の具体的な計算を書き下したのは今日（2021年12月）が初めてです。だいぶ長期間に渡り保留（あるいは放置）だった*2ことが実行できました。
