米田埋め込みを誘導する
ベシ圏.icon p.109あたりの話
大まかな順序
共変関手$ H^A:\mathscr{A}\to\mathrm{Set}について、
①$ A\in\mathscr{A}を固定したHom関手$ H^A:\mathscr{A}\to\mathrm{Set}をみる ②その後、固定を外して更にメタに見た反変関手$ H^-:\mathscr{A}^\mathrm{op}\to[\mathscr{A}, \mathrm{Set}] を見る
反変関手$ H_A:\mathscr{A}^\mathrm{op}\to\mathrm{Set}について
③$ A\in\mathscr{A}を固定した反変Hom関手$ H_A:\mathscr{A}^\mathrm{op}\to\mathrm{Set}を見る ④その後、固定を外して更にメタに見た反変関手$ H^-:\mathscr{A}\to[\mathscr{A}^\mathrm{op},\mathrm{Set}] を見る
⑤
①②と③④の統合
補足
$ [\mathscr{A},\mathscr{B}] という表記は関手圏Funを表す ①について
普通のHom関手$ H^A:\mathscr{A}\to\mathrm{Set} https://gyazo.com/9c9088394050856205f84c09249566b7
対象の対応をラムダ記法で書くと、
$ H^A: \lambda X.\mathscr{A}(A,X)のようになる
射の対応をラムダ記法で書くと、
$ H^A(f)=\lambda g\in\mathscr{A}(A,X).f\circ gのようになる
①と②の間について
①では$ A\in\mathscr{A}を一つに固定していたが、それの集まり、つまり族を見る
$ (H^A)_{A\in\mathscr{A}}
$ H^Aと$ H^{A'}の間の射$ H^fを扱えるようになる
$ H^f:H^A\Rightarrow H^{A'}は自然変換になる
複数の①を同じ図の中に描いてみる
https://gyazo.com/203893205f6b778e4c006ad2a5d3a083
$ Aを固定した$ H^Aと、$ A'を固定した$ H^{A'}を描いている
この2つのHom関手$ H^A, H^{A'}の間に自然変換$ H^fがある
この図から$ Yを消したものを見ておくと、②の話にスムーズに行ける
https://gyazo.com/00239accdede817c9e9aa99c47111548
②について
①をさらにメタに見る
反変関手$ H^\bullet:\mathscr{A}^\mathrm{op}\to[\mathscr{A}, \mathrm{Set}]
①の話だった関手$ H^A:\mathscr{A}\to\mathrm{Set}の集まりがコドメイン
https://gyazo.com/5189ab2d15eb4d255102b2f579803c43
右側の$ [\mathscr{A},\mathrm{Set}] は関手圏
対応する射の向きが逆転しているのでこれは反変関手である
対象の対応
対象$ Aに対して、$ H^-(A)=H^Aとなる
ラムダ記法で書くと
$ H^-:\lambda A.\lambda X.\mathscr{A}(A,X)
これは部分適用すれば①になるのでメタになっているのがわかりやすいmrsekut.icon
$ H^A:\lambda X.\mathscr{A}(A,X)=\mathscr{A}(A,-)
射の対応
$ \forall X\in\mathscr{A}に対して、
$ {H^-(f)}_X=H^f_X: H^{A'}(X)\to H^A(X), h\mapsto h\circ f
ラムダ記法で書くと
$ H^f:\lambda X.\lambda h\in\mathscr{A}(A',X).h\circ f
③について
https://gyazo.com/39df25c28d9550416a5cc2b03459d471
対象の対応をラムダ記法で書くと、
$ H_A: \lambda X.\mathscr{A}(X,A)のようになる
射の対応をラムダ記法で書くと、
$ H_A(f)=\lambda g\in\mathscr{A}(X,A).g\circ fのようになる
③と④の間
https://gyazo.com/e8f38f60177b075c3cb18c84bae48de4
④について
$ H_- は、$ \mathscr{A} を$ [\mathscr{A}^\mathrm{op}, \mathrm{Set}] に埋め込む
関手$ H_-:\mathscr{A}\to[\mathscr{A}^\mathrm{op}, \mathrm{Set}]
https://gyazo.com/8681aec45ffa6a43ca55820d90a5c6fc
対象の対応
対象$ Aに対して、$ H_-(A)=H_Aとなる
ラムダ記法で書くと
$ H_-:\lambda A.\lambda X.\mathscr{A}(X,A)
これは部分適用すれば③になるのでメタになっているのがわかりやすいmrsekut.icon
射の対応
$ \forall X\in\mathscr{A}に対して、
$ {H_-(f)}_X=(H_f)_X:H_A(X)\to H_{A'}(X), h\mapsto f\circ h
ラムダ記法で書くと
$ H_f:\lambda X.\lambda h\in\mathscr{A}(X,A).f\circ h
⑤
①②と③④を統合する
ベシ圏.iconの定義4.1.22
関手$ \mathrm{Hom}_\mathscr{A}:\mathscr{A}^\mathrm{op}\times\mathscr{A}\to\mathrm{Set}
定義
$ \mathrm{Hom}_\mathscr{A}(A,B)=\mathscr{A}(A,B)
$ (\mathrm{Hom}_\mathscr{A}(f,g))(p)=g\circ p\circ f
https://gyazo.com/3b4dd3f9ba899e733d7e290ea03bc210