随伴系のhom自然同型の構成

随伴系$ \Sigma = \left(L\dashv R \colon C→D, \eta, \epsilon \right)

hom自然同型を構成する

$ \Phi \colon \hom_D(\_.L,\_) \Rightarrow \hom_C(\_,\_.R)

$ \colon C^\mathrm{op}× D \to \mathbf{Set}

まず、転置、反転置に相当する写像を定義:

$ \Phi[c,d] \colon \hom_D(c.L,d) → \hom_C(c,d.R)

$ g\colon c.L→d について

$ \Phi[c,d](g)\coloneqq c.\eta;g.R

$ \Psi [c,d] \colon \hom_C(c,d.R) → \hom_D(c.L,d)

$ f\colon c→d.R について

$ \Psi[c,d](f) \coloneqq f.L;d.\epsilon

まだ自然かわからないので角かっこにしておく

https://gyazo.com/e2f7ec430df3ac05b53a9e15ebe7fdf2

このとき

$ \Phi[c,d](\Psi [c,d](f))= c.\eta;(f.L;d.\epsilon).R

$ =c.\eta;f.LR;d.\epsilon R

↓エレベーター性

$ =f.C;d.R\eta;d.\epsilon R

$ =f;d.(R\eta;\epsilon R)

↓ニョロニョロ性

$ =f;d.R =f

https://gyazo.com/438b104e2977a0d3c4d3dfd3e115d6e0

$ \Psi[c,d](\Phi [c,d](g))= (c.\eta;g.R).L;d.\epsilon

$ =c.\eta L;g.RL;d.\epsilon

$ =c.\eta L;c.L\epsilon ;g.D

$ =c.(\eta L;L\epsilon) ;g

$ =c.L;g = g

https://gyazo.com/f1a2dc18c7abfb9bbc3e9accccd80084

より同型射である

$ \Psi[c,d] = \Phi[c,d]^{-1}

射から自然変換の構成を行う

$ H\coloneqq\hom_D(\_.L,\_) ,$ H' \coloneqq \hom_C(\_,\_.R)

$ \Phi [c,d] \colon (c,d).H \to (c,d).H'

圏$ C^\mathrm{op}× D の射

$ (s,t)\colon (c,d) \to (c',d')

$ s\colon c' \to c ,$ t\colon d \to d'

$ (s.t).H =\hom_D(s.L,t)

$ \colon (c,d).H \to (c',d').H

$ \colon g \mapsto s.L;g;t

$ (s,t).H' = \hom_C(s,t.R)

$ \colon (c,d).H' \to (c',d').H'

$ \colon f \mapsto s;f;t.R

https://gyazo.com/3a376900ed970c1232581dded61fe2db

任意の射$ (s,t)\colon (c,d) \to (c',d') についてエレベーター性

$ \Phi [c,d];(s,t).H' = (s,t).H;\Phi [c',d']

を示せばよい

これは$ \mathbf{Set} の射、つまり写像

任意の$ g \in (c,d).H = \hom_D(c.L,d) について

$ \Phi [c,d];(s,t).H'

$ \colon g \mapsto s;c.\eta;g.R;t.R

$ (s,t).H;\Phi [c',d']

$ :g\mapsto c'.\eta;(s.L;g;t).R

$ =c'.\eta;s.LR;g.R;t.R

$ \eta のエレベーター性

$ =s;c.\eta;g.R;t.R

よって写像として等しい

以上より、改めて自然変換

$ \Phi \colon H → H'

を

$ (c,d).\Phi = \Phi[c,d]

によって定義できる

全てが同型射なのでこれは自然同型