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

前提条件などは↑を参照

①~④により、

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

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

この全単射が各A,Xに対して自然であることを示す

そのためには以下の2つを示さなねばならない

⑤-1: ①が自然である

⑤-2: ②が自然である

しかし、自然変換の各成分が同型射のとき、その自然変換は同型を使うことで片方を示せば十分である

つまり、\spades\cong\heartsを示すために、

\spades,\hearts間の自然変換を定義する方法を選択するわけではなく、

各成分が同型射である

という方を選択しようとしているわけで、そうなると、\tilde{}と\hat{}で全く同じ議論を2回することになるので。

今回は⑤-1を示すことにする

つまり、関手\hat{}が組(A,X)について自然であることを示す

そのために、定義域が直積圏な関手の自然変換と、個別の自然変換は同値を使って、

2変数関手の自然性を、

A,Xをそれぞれ固定した2つの関手の自然性を示す

ことで示す

要するに示したいことは、以下の2つである

⑤-1-1: \hat{}が、固定したXごとにAについて自然

⑤-1-2: \hat{}が、固定したAごとにXについて自然

\hat{}が、固定したXごとにAについて自然であることを示す

各X\in[\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X)と、

\mathscr{A}のf:B\to Aについて

下図の可換性を言えればいい

つまり上図の赤の部分の等式を示せばいい

\alphaから出発している

\alphaはH_A\to Xな自然変換

(\alpha\circ H_f)_B(1_B)=\alpha_B((H_f)_B(1_B))

∵[\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X)における射の合成の定義

雑に言えば(g\circ f)(x)=g(f(x))と同じ話

=\alpha_B(f\circ 1_B)=\alpha_B(f)

∵ H_fの定義

ref 米田埋め込みを誘導する#5efc30bd1982700000a2d1f3

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

∵ 米田の補題の証明 ③~④#611145841982700000e220dbの等式

より、言える

\hat{}が、固定したAごとにXについて自然であることを示す

各A\in\mathscr{A}と、

[\mathscr{A}^\mathrm{op},\mathrm{Set}]の射\theta:X\to X'について

この\thetaね

下図の可換性を言えればいい

\alphaから出発している

\alphaはH_A\to Xな自然変換

[\mathscr{A}^\mathrm{op},\mathrm{Set}]内の合成の定義より、(\theta\circ\alpha)_A=\theta_A\circ\alpha_A

より、言える