米田の補題の証明 ①~②
前提条件などは↑を参照
各A,Xに対し、[\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X)とX(A)の間に全単射があることを示す
つまり、A,Xを固定して見ている
流れ
そのために
①写像[\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X)\xrightarrow{(\hat{})} X(A)を定義する
②写像[\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X)\xleftarrow{(\tilde{})} X(A)を定義する
①②の証明の前の前提のおさらいと目的
[\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X)というのは集合である
元は「関手H_Aから関手Xへ向かう自然変換」である
X(A)も集合である
①や②では、この集合間の写像を定義したいわけである
つまり①の場合
[\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X)から一つ元(自然変換)\alphaを取ってきたときに、
写像の行き先\hat{\alpha}を(\alphaを使って)どう定義するか
が議論の対象になる
②の場合も同様で
x\in X(A)を取ってきたときに、
写像の行き先である\tilde{x}という自然変換を(xを使って)どう定義するか
が議論の対象になる
目的
証明
自然変換\alpha:H_A\to Xに対し、
\hat\alpha\in Xを、\hat\alpha=\alpha_A(1_A)と定義する
補足
図にするとこんなイメージ
①この自然変換から出発して、
②この中の元に対応させたい
③Aの恒等射と、
④\alphaのA成分に注目すれば、
⑤対応が取れる
簡素すぎてわかりづらいが、他の対応を考えようとしてみても難しいことに気づく
例えば、「じゃあ恒等写像1_A以外のもので対応させてみようや」と思ってやってみるとこうなる
①恒等射じゃなくて、他の対象Bへの射を見てみる
②さっきと同じように対象を取ってくると、、おっとこれはX(B)なので、そもそも前提に反する
③気を取り直して、X(A)との対応を見ようとするも、この射ってなに??
目的
流れ
xに対応する「自然変換\tilde{x}:H_A\to Xを定義したい」
コレが目的

「...」は自然変換なので、何かしらの射の族である
その射の1つは、\tilde{x}_B: \mathscr{A}(B,A)\to X(B)になっているはずである
自然変換の定義から自然に導かれる

じゃあ、その\tilde{x}_Bを良い感じに定義して、
ここで初めて定義される

このときに、ドメインのxを使って良い感じに対応させたい
ここのみが肝であって、これの前後の話はほぼ自明に流れる

その族\tilde{x}が自然性を満たしていれば、
族の話から自然変換の話に戻ってきている

自然性を満たさないと自然変換ではないのでそれを確認する
最初の目的が達成される
証明
x\in X(A)についての自然変換\tilde{x}:H_A\to Xを定義する
つまり、各B\in\mathscr{A}について、
関数\tilde{x}_B:H_A(B)=\mathscr{A}(B,A)\to X(B)を定義し、
その族\tilde{x}=(\tilde{x}_B)_{B\in\mathscr{A}}が自然性を満たすことを示す
ここで、
B\in\mathscr{A}とf\in\mathscr{A}(B,A)について、
\tilde{x}_B(f)=(Xf)(x)\in X(B)と定義する
これは以下のような対応になる
同じ
fから出発して、右回り、左回りで右下に至っている

問題はこの経路で来た2つが等しいのかどうか

関手Xの射の対応より、X(f\circ g)=Xg\circ Xfなので、これは等しい
よって上図は可換
補足
どこから\tilde{x}_B=(Xf)(x)\in X(B)の定義が来たのか
図にするとこんな感じ
①ここのxから出発して、
②ここに入る対応が欲しい
③そこで元の圏のBとの対応であるfに着目して
④その対応を見ると、自然に導かれる
この定義を提示されれば「せやな〜」となるけど、思いつけと言われると慣れてないと難しそう

書いてる通りだが、自然性を示すために、可換になることを示そうとしている
同じものから出発して、異なる経路で辿ってぶつかった物が等しいことを言えれば
可換である、と言える
これは
5項補題の証明でめちゃくちゃ使っているので、良い練習になる
