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