米田の補題の証明の中盤をやる

前提条件などは↑を参照

次に、

③ \hat{\tilde{}}が恒等写像であることを示す

④ \tilde{\hat{}}が恒等写像であることを示す

x\in X(A)について、

\hat{\tilde{x}}=\tilde{x}_A(1_A)

∵\hat{}の定義 ref 米田の補題の証明 ①~②#610f8e76198270000018ecee

=(X1_A)(x)

∵ \tilde{}の定義 ref 米田の補題の証明 ①~②#610f977c198270000018ed2b

=1_{X(A)}(x)

∵ Xの射X1_A:X(A)\to X(A)は、X(A)の恒等射1_{X(A)}に等しい

=x

∵恒等射の行き先は自分自身

目的

自然変換\alpha:H_A\to Xについて、\tilde{\hat\alpha}=\alphaを示す

つまり ある自然変換 = ある自然変換 を示そうとしている

自然変換というのは射の族だったので、その1つの射に注目して、等しさを示せばいい

つまり ある射 = ある射 を示すことにする

つまり\forall B\in\mathscr{A}成分に着目して、(\tilde{\hat\alpha})_B=\alpha_Bを示す

この射はどこからどこへの射かと言うと、

H_A(B)=\mathscr{A}(B,A)から、X(B)への射である

ちなみに\mathscr{A}(B,A)やX(B)の元もまた射なので、「「射の集合」から「射の集合」への射」の話をしようとしている

が、このメタさそこまで意識する必要はない

この元の1つをfとして示す

まとめるとこんな感じ

ある自然変換 = ある自然変換 を示したい

つまり、 ある射の族 = ある射の族 を示したい

そこで1つに注目し、 ある射 = ある射 を示す

そこで、任意の元fを取ってきて ある射(f) = ある射(f) であることを示せばいい

ややこいが別に難しい話ではない

証明

自然変換\alpha:H_A\to Xについて、\tilde{\hat\alpha}=\alphaを示す

自然変換同士の等しさを示すために、各B\in\mathscr{A}について(\tilde{\hat\alpha})_B=\alpha_Bを示す

この関数同士の等しさを示すということは、定義域の各元について同じ行き先へ行くということなので、

\forall B\in\mathscr{A}と、\mathscr{A}のf:B\to Aについて

(\tilde{\hat\alpha})_B(f)=\alpha_B(f)を示す

(\tilde{\hat\alpha})_B(f)=(Xf)(\hat\alpha)

∵ \tilde{}の定義 ref 米田の補題の証明 ①~②#610f977c198270000018ed2b

=(Xf)(\alpha_A(1_A))

∵\hat{}の定義 ref 米田の補題の証明 ①~②#610f8e76198270000018ecee

=\alpha_B(f)

これは以下より言える

自然変換\alphaの自然性より下図が可換になる

左上で1_Aから出発した2経路の終端は等しくなるので、(Xf)(\alpha_A(1_A))=\alpha_B(f)

以上より、任意のA\in\mathscr{A}とX\in[\mathscr{A}^\mathrm{op},\mathrm{Set}]について、

[\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X)とX(A)の間に全単射を定義できた