米田の補題を証明するだけの記事
はじめに
メリークリスマス！(激遅)今回は米田の補題の証明を書きました。米田の補題といえば圏論初学者が挫折することで有名ですね。今日はそんな方向けに書きましたのでぜひ「米田の補題の証明を理解したい...!」という方は一読していただける幸いです。
目に疲れが生じた場合は速やかにブラウザを閉じることを推奨します。
ほんへ
おやくそく
・写像$f:X\to Y$と$x\in X$に対して、対応する行き先を$f(x)\in Y$と記述する
・関手$\mathcal F:\mathcal C\to\mathcal D$と$X\in\mathcal C,f\in\mathrm{Mor}\ \mathcal C$に対して、対応する行き先を$\mathcal F[X]\in\mathcal D,\mathcal F[f]\in\mathrm{Mor}\ \mathcal D$と記述する
$(\mathrm i)$
$\mathcal F,\mathcal G:\mathcal C\to\mathcal D$を関手とする。自然変換$\tau:\mathcal F\Rightarrow\mathcal G$とは、$\mathcal C$の対象を添え字とする$\mathcal D$の射の族$(\tau_X:\mathcal F[X]\to\mathcal G[X])_{X\in\mathcal C}$であり かつ$\mathcal C$の任意の射$f:X\to Y$に対して$\mathcal G[f]\circ\tau_X=\tau_Y\circ\mathcal F[f]$を満たす物のことである
$$\xymatrix{ \mathcal F[X]\ar@{}[rd]|{\circlearrowright}\ar[d]_{\tau_X}\ar[r]^{\mathcal F[f]}&\mathcal F[Y]\ar[d]^{\tau_Y} \\ \mathcal G[X]\ar[r]_{\mathcal G[f]}&\mathcal G[Y]}$$
$(\mathrm {ii})$$\mathcal C$を局所小圏とし,$X\in\mathcal C$とする。$X$に付随する$\mathrm{Hom}$関手$\mathrm{Hom}(X,＿):\mathcal C\to\boldsymbol {\mathrm{Set}}$とは、
$Y\in\mathcal C$に対して、$$\mathrm{Hom}(X,＿)[Y]:=\mathrm{Hom}(X,Y)$$
射$g:Y\to Z$に対して、$$\xymatrix@C=0.1pt@R=3.5pt{
\mathrm{Hom}(X,＿)[g]&:& \mathrm{Hom}(X,Y) \ar[rrrrrrrr] &&&&&&&& \mathrm{Hom}(X,Y)
\\& &f \ar@{(-}[u] & \ar@{|->}[rrrrrr]&&&&&&& g\ \circ\ f \ar@{(-}[u]
}$$
という対応の関手である。特に$\mathrm{Hom}(X,＿)[g](f)=g\circ f$である
$\mathcal C$を局所小圏、$\obc{A}\n{\in\mathcal C}$に付随する$\mathrm{Hom}$関手を$\fun{h}^{\obc A}\ \n\simeq\ \mathrm{Hom(}\obc A\ \n,\ \obc{＿}\n ):\mathcal C\to\boldsymbol {\mathrm{Set}}$、$\fun{\mathcal F}\n,\ \fun{\mathcal G}\n\ :\mathcal C\to\boldsymbol {\mathrm{Set}}$の間の自然変換全体を$\nat{\mathrm{Nat(}}\fun{\mathcal F}\n,\ \fun{\mathcal G}\nat)$と表す。このとき米田写像という全単射
$$ y:\nat{\mathrm{Nat(}}\fun{h}^{\obc A}\n,\ \fun{\mathcal F}\nat)\n\ \to\ \fun{\mathcal F[}\obc A\fun ]$$
が存在する。
$y:\nat{\mathrm{Nat(}}\fun{h}^{\obc A}\n,\ \fun{\mathcal F}\nat)\ \n\to\ \fun{\mathcal F[}\obc A\fun ]\ \n;\ \sz\tau\ \n\mapsto\ \sz\tau_{\obc A}\fun(\sy{\mathrm{id}}_{\obc A}\fun)$とする。
$$\xymatrix@C=0.1pt@R=3.5pt{
y&:& \nat{\mathrm{Nat(}}\fun{h}^{\obc A}\n,\ \fun{\mathcal F}\nat)\ar[rrrrrr] &&&&&& \ \fun{\mathcal F[}\obc A\fun ]
\\& &\sz\tau \ar@{(-}[u] & \ar@{|->}[rrrr]&&&&& \sz\tau_{\obc A}\fun(\sy{\mathrm{id}}_{\obc A}\fun) \ar@{(-}[u]
}$$
これが米田写像である。この全単射性を今から示す。
・単射性
$\obs a\ \n\in\ \fun{\mathcal F[}\obc A\fun ]$とし$\obs a\n\ =y(\sz\tau\n)=y(\sz\tau'\n)\ (\sz\tau\ \n,\ \sz\tau'\ \n\in\ \nat{\mathrm{Nat(}}\fun{h}^{\obc A}\n,\ \fun{\mathcal F}\nat)\n)$とする。このとき$\sz\tau\ \n=\ \sz\tau'$、つまり任意の$\obc B\ \n\in\ \mathcal C$に対して、$\sz\tau_{\obc B}\ \n=\ \sz\tau'_{\obc B}$であることを示せばOK
$\sz\tau$は自然変換なので$\sy f\ \n:\ \obc A\ \sy\to\ \obc B$に対して、$\fun{\mathcal F[}\sy f\fun]\n\circ\ \sz\tau_{\obc A}\ \n=\ \sz\tau_{\obc B}\n\circ\ \fun h^{\obc A}\fun[\sy f\fun]$である。
$$\xymatrix{
\fun h^{\obc A}\fun[\obc A\fun]\ar@{}[rd]|{\circlearrowright}\ar[d]_{\sz\tau_{\obc A}}\ar[r]^{\fun h^{\obc A}\fun[\sy f\fun]}&\fun h^{\obc A}\fun[\obc B\fun]\ar[d]^{\sz\tau_{\obc B}}
\\ \fun{\mathcal F[}\obc A\fun]\ar[r]_{\fun{\mathcal F[}\sy f\fun]}& \fun{\mathcal F[}\obc B\fun]}$$
よって$\fun{h}^{\obc A}\fun[\sy f\fun]\fun(\sy{\mathrm{id}}_{\obc A}\fun)\ \n=\mathrm{Hom}(\obc A\ \n,\ \obc＿\n)[\sy f\n](\sy{\mathrm{id}}_{\obc A}\n)=\sy f\ \n\circ\ \sy{\mathrm{id}}_{\obc A}\ \n=\ \sy f$に気を付けて計算すると
$\sz{\tau}_{\obc B}(\sy f\sz)$
$=\sz\tau_{\obc B}(\fun{h}^{\obc A}\fun[\sy f\fun]\fun(\sy{\mathrm{id}}_{\obc A}\fun)\sz)$ （$\mathrm{Hom}$関手より）
$=(\sz\tau_{\obc B}\n\circ\fun h^{\obc A}\fun[\sy f\fun]\n)\sz(\sy{}\mathrm{id}_{\obc A}\sz)$
$=(\fun{\mathcal F[}\sy f\fun]\n\circ\sz\tau_{\obc A}\n)\sz(\sy{}\mathrm{id}_{\obc A}\sz)$ （自然変換より）
$=\fun{\mathcal F[}\sy f\fun]\fun(\sz\tau_{\obc A}\sz(\sy{}\mathrm{id}_{\obc A}\sz)\fun)$
$=\fun{\mathcal F[}\sy f\fun](\n y(\sz\tau\n)\fun)$ （$y$の定義より）
$=\fun{\mathcal F[}\sy f\fun](\obs a\fun)$ （$a$の定義より）
同様に$\sz{\tau'}_{\obc B}(\sy f\sz)\ \n=\ \fun{\mathcal F[}\sy f\fun](\obs a\fun)$。$\sz{\tau}_{\obc B}$と$\sz{\tau'}_{\obc B}$は全ての$\sy f\ \n\in\ \mathrm{Hom}(\obc A\n,\obc B\n)$で値が一致するので$\sz{\tau}_{\obc B}\ \n=\ \sz{\tau'}_{\obc B}$
・全射性
$\obs a\ \n\in\fun{\mathcal\ F[}\obc A\fun]$に対して、$\sz\tau_{\obc B}\ \n:\ \mathrm{Hom}(\obc A\n,\obc B\n)\ \sz\to\ \fun{\mathcal F[}\obc B\fun]\ \n;\ \sy f\ \n\mapsto\ \fun{\mathcal F[}\sy f\fun](\obs a\fun)$とする。
$$\xymatrix@C=0.1pt@R=3.5pt{
\fun{\mathcal F[}\obc A\fun ] \ar[rrrrrr]^{ \fun{\mathcal F[}\sy f\fun]} &&&&&& \ \fun{\mathcal F[}\obc B\fun ]
\\\obs a \ar@{(-}[u] & \ar@{|->}[rrrr]&&&&& \fun{\mathcal F[}\sy f\fun](\obs a\fun) \ar@{(-}[u]
} \xymatrix@C=0.1pt@R=3.5pt{
\sz\tau_{\obc B}&:& \mathrm{Hom}(\obc A\n,\obc B\n)\ar[rrrrrr] &&&&&& \ \fun{\mathcal F[}\obc B\fun ]
\\& &\sy f \ar@{(-}[u] & \ar@{|->}[rrrr]&&&&& \fun{\mathcal F[}\sy f\fun](\obs a\fun) \ar@{(-}[u]
}$$
このとき、$\sy\tau\ \n:=(\sy\tau_{\obc B}\n)_{\obc B\n\in\mathcal C}$は自然変換$\sy\tau\ \n: \ \fun h^{\obc A}\ \sy\Rightarrow\ \fun{\mathcal F}$となり かつ$y(\sy\tau\n)=\obs a$となることを示せばOK。
$\sy g\ \n:\ \obc B\ \sy\to\ \obc C$と$\sy f\ \n\in\ \mathrm{Hom}(\obc A\n,\obc B\n)$に対して、
$(\fun{\mathcal F}[\sy g\fun]\n\circ\sz\tau_{\obc B}\n)\sz(\sy f\sz)$
$=\fun{\mathcal F[}\sy g\fun](\sz\tau_{\obc B}(\sy f\sz)\fun)$
$=\fun{}\mathcal F[\sy g\fun](\mathcal F[\sy f\fun](\obs a\fun))$ （$\sz\tau_{\obc B}$の定義より）
$=(\fun{}\mathcal F[\sy g\fun]\n\circ\fun{}\mathcal F[\sy f\fun]\n)\fun(\obs a\fun)$
$=\fun{\mathcal F[}\sy g\n\circ\sy f\fun](\obs a\fun)$
$=\sz\tau_{\obc C}\sz(\sy g\n\circ\sy f\sz)$ （$\sz\tau_{\obc C}$の定義より）
$=\sz\tau_{\obc C}(\fun h^{\obc A}[\sy g\fun](\sy f\fun)\sz)$ （$\mathrm{Hom}$関手より）
$=(\sz\tau_{\obc C}\n\circ\fun h^{\obc A}[\sy g\fun]\n)\sz(\sy f\sz)$
よって$\fun{}\mathcal F[\sy g\fun]\n\circ\sz\tau_{\obc B}$と$\sz\tau_{\obc C}\n\circ\fun h^{\obc A}[\sy g\fun]$は全ての$\sy f\ \n\in\ \mathrm{Hom}(\obc A\n,\obc B\n)$で値が一致するので$\fun{}\mathcal F[\sy g\fun]\n\circ\sz\tau_{\obc B}\ \n=\ \sz\tau_{\obc C}\n\circ\fun h^{\obc A}[\sy g\fun]$となり$\sz\tau$は自然変換。
$$\xymatrix{
\fun h^{\obc A}\fun[\obc B\fun]\ar@{}[rd]|{\circlearrowright}\ar[d]_{\sz\tau_{\obc B}}\ar[r]^{\fun h^{\obc A}\fun[\sy g\fun]}&\fun h^{\obc A}\fun[\obc C\fun]\ar[d]^{\sz\tau_{\obc C}}
\\ \fun{\mathcal F[}\obc B\fun]\ar[r]_{\fun{\mathcal F[}\sy g\fun]}& \fun{\mathcal F[}\obc C\fun]}$$
また
$y(\sz\tau\n)$
$=\sz\tau_{\obc A}(\sy{}\mathrm{id}_{\obc A}\sz)$ （$y$の定義より）
$=\fun{}\mathcal F[\sy{}\mathrm{id}_{\obc A}\fun](\obs a\fun)$ （$\tau$の定義より）
$=\sz{}\mathrm{id}_{\fun{}\mathcal F[\obc A\fun]}\sz(\obs a\sz)$
$=\obs a$
追記
文字に色を付けるにあたって、マクロの開発をあずびわさん（@AZBY__azby）にして頂きました。このおかげで記述量が減ったことは勿論のこと文字も大変見やすくなりとても助かりました。この場を借りて御礼申し上げます。ありがとうございました！ ($12/26$)
参考文献
この記事を高評価した人
この記事に送られたバッジ
投稿者
