p.109あたりの話

Hom関手から米田埋め込みを誘導する

大まかな順序

共変関手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}

対象の対応をラムダ記法で書くと、

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'}は自然変換になる

複数の①を同じ図の中に描いてみる

Aを固定したH^Aと、A'を固定したH^{A'}を描いている

この2つのHom関手H^A, H^{A'}の間に自然変換H^fがある

この図からYを消したものを見ておくと、②の話にスムーズに行ける

②について

①をさらにメタに見る

反変関手H^\bullet:\mathscr{A}^\mathrm{op}\to[\mathscr{A}, \mathrm{Set}]

①の話だった関手H^A:\mathscr{A}\to\mathrm{Set}の集まりがコドメイン

右側の[\mathscr{A},\mathrm{Set}]は関手圏

対応する射の向きが逆転しているのでこれは反変関手である

対象の対応

対象Aに対して、H^-(A)=H^Aとなる

ラムダ記法で書くと

H^-:\lambda A.\lambda X.\mathscr{A}(A,X)

これは部分適用すれば①になるのでメタになっているのがわかりやすい

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

米田埋め込みを誘導する#6102c25a19827000003f1d15の図と記号を合わせているので見るとわかりやすい

ラムダ記法で書くと

H^f:\lambda X.\lambda h\in\mathscr{A}(A',X).h\circ f

これって呼び方ないの #??

強いて言えば、「米田埋め込みの双対」になるのか？

③について

①の双対

対象の対応をラムダ記法で書くと、

H_A: \lambda X.\mathscr{A}(X,A)のようになる

射の対応をラムダ記法で書くと、

H_A(f)=\lambda g\in\mathscr{A}(X,A).g\circ fのようになる

③と④の間

④について

②の双対

これが米田埋め込みになる

H_-は、\mathscr{A}を[\mathscr{A}^\mathrm{op}, \mathrm{Set}]に埋め込む

関手H_-:\mathscr{A}\to[\mathscr{A}^\mathrm{op}, \mathrm{Set}]

対象の対応

対象Aに対して、H_-(A)=H_Aとなる

ラムダ記法で書くと

H_-:\lambda A.\lambda X.\mathscr{A}(X,A)

これは部分適用すれば③になるのでメタになっているのがわかりやすい

射の対応

\forall X\in\mathscr{A}に対して、

{H_-(f)}_X=(H_f)_X:H_A(X)\to H_{A'}(X), h\mapsto f\circ h

米田埋め込みを誘導する#5efc440a1982700000a2d211の図と記号を合わせているので見るとわかりやすい

ラムダ記法で書くと

H_f:\lambda X.\lambda h\in\mathscr{A}(X,A).f\circ h

⑤

①②と③④を統合する

の定義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

これ恒等Profunctorなのか