随伴系の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
まだ自然かわからないので角かっこにしておく
このとき
\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
\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
より同型射である
\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
任意の射(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]
によって定義できる
全てが同型射なのでこれは自然同型