米田の補題の証明

定理再掲

$ \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が本当に関手になっているのかという確認

もしておきたい

証明

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

参考

ベシ圏 pp.115-119

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

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