米田の補題の証明

定理再掲

\mathscr{A}を局所的に小さな圏とすると、

[\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X)\cong X(A) -- (*)

がA\in\mathscr{A}とX\in[\mathscr{A}^\mathrm{op},\mathrm{Set}]について自然に成り立つ

証明の概略

(*) の両辺が2つの変数A,Xに対して関手的であることを示せばいい

つまり、 (*) を\spades\cong\heartsと書くと、

(A,X)\mapsto \spadesという関手と、

\:(A,X)\mapsto\heartsという関手

この2つの関手が自然同型であることを示せばいい

そのために、まず各A,Xに対し、\spades,\hearts間の全単射を定義する

そのために、

①写像\spades\to \heartsを定義し、

②写像\spades\leftarrow\heartsを定義し、

③\spades\circ\hearts= \mathrm{Id}であり

④\hearts\circ \spades=\mathrm{Id}である

ことを示す必要がある

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

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

⑤-1: ①が自然

⑤-2: ②が自然

自然変換の各成分が同型射のとき、その自然変換は同型を使うことで片方で済むの で 前者 を示す

そのためにはまず準備として

⓪-1(A,X)\to \spadesが本当に関手になっているのかという確認

⓪-2(A,X)\to\heartsが本当に関手になっているのかという確認

もしておきたい

証明

ベシ圏の証明をなぞっており、初見でわかりづらかった箇所の補足を大量にしたメモなので、形式的な証明自体は本を読んだほうがいい

参考

ベシ圏 pp.115-119

圏論入門のよりこちらの方が流れがわかりやすかった

『圏論入門』 pp.249-253

前層版、余前層版の両方が載っている