随伴系の同型を除いた一意性
L\dashv RかつL'\dashv R'のとき
L\cong L'\iffR\cong R'
とくに
L\dashv RかつL\dashv R'ならばR\cong R'
L\dashv RかつL'\dashv RならばL\cong L'
証明
随伴系
\left(L\dashv R \colon C→D, \eta, \epsilon \right)
\left(L'\dashv R' \colon C→D, \eta', \epsilon' \right)
⇒
自然同型を\varphi\colon L\Rightarrow L'とする
\psi\colon R⇒R'と\psi\colon R'⇒Rを
\psi \coloneqq R\eta';R\varphi^{-1} R';\epsilon R'
= R\eta';(R\varphi^{-1} ;\epsilon) R'
\psi' \coloneqq R'\eta ;R'\varphi R;\epsilon' R
=R'(\eta ;\varphi R);\epsilon' R
このとき
\psi ;\psi'= R\eta';(R\varphi^{-1} ;\epsilon) R';D\psi'
↓エレベーター性
= R\eta';RL'\psi';(R\varphi^{-1} ;\epsilon) R
= R\eta';RL'(R'(\eta ;\varphi R);\epsilon' R);(R\varphi^{-1} ;\epsilon) R
↓整理
=R(\eta'C;L'R'(\eta ;\varphi R));RL'\epsilon' R;(R\varphi^{-1} ;\epsilon) R
↓カッコの中でエレベーター
=R(C(\eta ;\varphi R);\eta' L'R);RL'\epsilon' R;(R\varphi^{-1} ;\epsilon) R
=R(\eta ;\varphi R);R\eta' L'R;RL'\epsilon' R;(R\varphi^{-1} ;\epsilon) R
=R(\eta ;\varphi R);R(\eta' L';L'\epsilon') R;(R\varphi^{-1} ;\epsilon) R
↓ニョロニョロ
=R(\eta ;\varphi R);RL' R;(R\varphi^{-1} ;\epsilon) R
=R\eta ;R\varphi R;R\varphi^{-1} R;\epsilon R
=R\eta ;R(\varphi ;\varphi^{-1} )R;\epsilon R
=R\eta ;\epsilon R
=R
同様に、
' の有無を逆にして\psi';\psi=R'
よってR\cong R'
⇐
上の双対を考えれば明らか
2020/4/9
