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}

https://gyazo.com/bab3c2d72b4e84fa8be4989acf8251f3

転置オペレーター

$ \_^\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}

https://gyazo.com/fea659b56a89acc13d7d1e83b1c4b223

$ \eta の自然性の証明

任意の$ C の射$ s\colon c→c' について

hom函手のスライディング性から

$ (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' について

hom函手のスライディング性から

$ (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

この手順をhom屈曲、hom反屈曲としてまとめた

$ 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

自然変換のhom屈曲のスライディング性

$ = (C^\mathrm{op}×\eta)\hom_C

$ = (LR)_♯;(\eta^\mathrm{op}×LR)\hom_C

https://gyazo.com/d0fa8028c59d1bedd165ab9f40412100

#TODO 図の修正

ref.iconscrap:圏論の随伴をちゃんと抑えよう