hom反屈曲
定義
任意の自然変換$ \beta\colon \hom_C⇒(F^\mathrm{op}×G)\hom_D
に対し
hom屈曲$ (\beta_♭)_♯=\beta を満たす自然変換$ \beta_♭ が一意に存在する $ \beta_♭\colon F⇒G\colon C→D
$ c.\beta_♭=c^\circ;;(c,c).\beta
これを$ \beta のhom反屈曲と呼ぶことにする
証明
自然性
写像の組$ \beta_♭[c]\colon c.F→c.G を
$ \beta_♭[c]\coloneqq c^\circ;;(c,c).\beta
$ (\beta_♭[c])_♯=c_♯;(c,c).\beta
によって定義する
これがエレベーター性を満たすことを確認する
任意の$ C の射$ f\colon c→c' について
$ f = c';;(f,c').\hom_C
$ = c;;(c,f).\hom_C
$ (c,c').\beta を適用
$ f;;(c,c).\beta
$ = c';;(f,c').\hom_C;(c,c').\beta
$ = c;;(c,f).\hom_C;(c,c').\beta
$ \beta のエレベーター性より
$ = c';;(c',c').\beta;(f.F,c'.G.).\hom_D
$ = c;;(c,c).\beta;(c.F,f.G).\hom_D
$ \beta_♭ の定義から
$ = \beta_♭[c'];;(f.F,c').\hom_D
$ = \beta_♭[c];;(c.F,f.G).\hom_D
hom写像の定義より
$ =f.F;\beta_♭[c']
$ =\beta_♭[c];f.G
以上より、改めて自然変換$ \beta_♭ を得る
$ \beta_♭\colon F⇒G
$ c.\beta_♭=\beta_♭[c]=c^\circ;;(c,c).\beta
逆変換性
任意の$ \beta について
hom屈曲の定義より
$ (\beta_♭)_♯\colon \hom_C⇒(F^\mathrm{op}×G)\hom_D
$ (a,b).(\beta_♭)_♯\colon $ \hom_C(a,b)→\hom_D(a.F,b.G)
$ h;;(a,b).(\beta_♭)_♯=h.\beta_♭
$ =a.\beta_♭;h.G
hom反屈曲の定義より
$ =(a^\circ;;(a,a)\beta);h.G
$ =a^\circ;;(a,a)\beta;(a.F,h.G)\hom_D
エレベーター性より
$ =a^\circ;;(a,h)\hom_C;(a,b)\beta
$ =h;;(a,b)\beta
よって写像として$ (a,b).(\beta_♭)_♯=(a,b). \beta
コンポーネントが等しいので$ (\beta_♭)_♯=\beta
任意の$ \alpha について
hom反屈曲の定義より
$ (\alpha_♯)_♭\colon F⇒G \colon C→D
$ c.(\alpha_♯)_♭=c^\circ;;(c,c).\alpha_♯
hom屈曲の定義より
$ =c^\circ.\alpha
$ =c.\alpha
コンポーネントが等しいので$ (\alpha_♯)_♭=\alpha