前提とされる知識

etc.

定理

\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}]について自然に成り立つ

補足

H_Aは反変Hom関手

米田埋め込みを誘導するの③

Xは表現可能関手

[\mathscr{A}^\mathrm{op},\mathrm{Set}]は関手圏Fun

[\mathscr{A}^\mathrm{op},\mathrm{Set}](H_A, X)は↑の関手圏の射の集合

つまり、自然変換H_A\to Xの集合

定理 その2

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

[\mathscr{A},\mathrm{Set}](H^A,X)\cong X(A)

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

上と同じことを言っている

反変Hom関手に対して言ってるか、余前層に対して言っているかの違いしかない

雑に言えば、米田埋め込みを誘導するの③を使っているのが上の定理で、これは①を使っているもの

証明

何を言っているのか

「H_AからXへの自然変換の集合」と「X(A)(集合)」が本質的に同値だと言っている

つまり、自然変換H_A\to Xは、X(A)の元である

何が嬉しいのか

ref ベシ圏 p.115

関連

p.78 演習問題3

\mathrm{Nat}(K,D(a,-))\cong\mathrm{Nat}(a,Q)

プログラミングとの関連

HaskellにYonedaというライブラリがある ref

継続と関係がある #??

というよりは継続渡しだったか

参考

ベシ圏 p.113~

『圏論入門』 p.242~

scala

米田の補題の3つの帰結

ref ベシ圏 p.119~

この3つのことで合ってる？