随伴系の同型を除いた一意性

$ L\dashv R かつ$ L'\dashv R' のとき

$ L\cong L' $ \iff $ R\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

https://gyazo.com/b69093c7ed75e0e23a62f84179d29449

https://gyazo.com/b70efb751a234aaa9da923ccd0a2f327