hom集合自然同型による随伴系の構成
函手L\colon C→D,R\colon D→C
自然同型
\Phi \colon \hom_D(\_.L,\_) \Rightarrow \hom_C(\_,\_.R)
\colon C^\mathrm{op}× D \to \mathbf{Set}
転置オペレーター
\_^\cap \coloneqq (c,d).\Phi
\colon \hom_D(c.L,d) → \hom_C(c,d.R)
反転置オペレーター
\__{\cup} \coloneqq (c,d).\Phi^{-1} =(\_^{\cap})^{-1}
\colon \hom_C(c,d.R) → \hom_D(c.L,d)
このときL\dashv R
随伴系のhom自然同型の構成で行った証明の逆向き
証明
記号の定義
hom函手を用いて定義
\Phi \colon H ⇒ H'
H\coloneqq\hom_D(\_.L,\_)=(L^\mathrm{op}×D) \hom_D
H' \coloneqq \hom_C(\_,\_.R) = (C^\mathrm{op}×R)\hom_C
(C^\mathrm{op}×L)\Phi\colon (C^\mathrm{op}×L)H⇒(C^\mathrm{op}×L)H'
(c,c.L).\Phi\colon \hom_D(c.L,c.L) → \hom_C(c,c.LR)
写像の図式順適用;;を用いて
恒等射の転置、反転置として写像の組を定義
\eta[c]\colon c→c.LR
\eta[c]\coloneqq (c.L)^\cap=(c.L);;(c,c.L).\Phi
\epsilon[d] \colon d.RL→d
\epsilon[d]\coloneqq (d.R)_\cup = (d.R);;(d.R,d)\Phi^{-1}
[* \etaの自然性の証明]
任意のCの射s\colon c→c'について
(s.L)=(c'.L);;(s.L,c'.L)\hom_D
= (c.L);;(c.L,s.L)\hom_D
Hを用いれば
(s.L)=(c'.L);;(s,c'.L)H
= (c.L);;(c,s.L)H
(c,c'.L)\Phiを適用して転置
(s.L)^\cap=(s.L);;(c,c'.L)\Phi
=(c'.L);;(s,c'.L)H;(c,c'.L)\Phi
= (c.L);;(c,s.L)H;(c,c'.L)\Phi
\Phiの自然性:エレベーター性より
=(c'.L);;(c',c'.L)\Phi;(s,c'.L)H'
= (c.L);;(c,c.L)\Phi;(c,s.L)H'
\eta[c]とH'の定義より
=\eta[c'];;(s,c'.LR)\hom_C
= \eta[c];;(c,s.LR)\hom_C
最後にhom写像の定義より
= s;\eta[c']
=\eta[c];s.LR
以上より\eta[c]はエレベーター性を満たす
よって、改めて自然変換
\eta\colon C⇒LR
c.\eta\coloneqq \eta[c]= (c.L)^\cap
を定義できる
[* \epsilonの自然性の証明]
任意のDの射t\colon d→d'について
(t.R)=(d'.R);;(t.R,d'.R)\hom_C
=(d.R);;(d.R,t.R)\hom_C
H'の定義より
(t.R)=(d'.R);;(t.R,d')H'
=(d.R);;(d.R,t)H'
(d.R,d')\Phi^{-1}を適用して反転置
(t.R)_\cup = (t.R);;(d.R,d')\Phi^{-1}
=(d'.R);;(t.R,d')H';(d.R,d')\Phi^{-1}
=(d.R);;(d.R,t)H';(d.R,d')\Phi^{-1}
エレベーター性
=(d'.R);;(d'.R,d')\Phi^{-1};(t.R,d')H
=(d.R);;(d.R,d)\Phi^{-1};(d.R,t)H
\epsilonとHの定義より
=\epsilon[d'];;(t.RL,d')\hom_D
=\epsilon[d];;(d.RL,t)\hom_D
最後にhom写像の定義より
=t.RL;\epsilon[d']
=\epsilon[d];t
以上より改めて自然変換
\epsilon\colon RL⇒D
d.\epsilon\coloneqq \epsilon[d] = (d.R)_\cup
を定義できる
2020/4/15
L_♯;(C^\mathrm{op}×L)\Phi
\colon\hom_C ⇒ (C^\mathrm{op}×LR)\hom_C
\eta\coloneqq \left( L_♯;(C^\mathrm{op}×L)\Phi \right)_♭
\colon C⇒LR
\eta_♯= L_♯;(C^\mathrm{op}×L)\Phi
= (C^\mathrm{op}×\eta)\hom_C
= (LR)_♯;(\eta^\mathrm{op}×LR)\hom_C
#TODO 図の修正