横結合のhom屈曲
F,G\colon C→D,F',G'\colon D→E
\alpha\colon F⇒G,\alpha'\colon F'⇒G'について
横結合のhom屈曲は以下のように分解できる
(FF')_♯=F_♯;(F^\mathrm{op}×F)F'_♯
(\alpha F')_♯=\alpha_♯;(F^\mathrm{op}×G)F'_♯
(F\alpha')_♯=F_♯;(F^\mathrm{op}×F)\alpha'_♯
(\alpha \alpha')_♯=\alpha_♯;(F^\mathrm{op}×G)\alpha'_♯
証明
hom屈曲の定義の一貫性より、ハット格上げについて
F_♯=(F^\circ)_♯
F^\circ\alpha'=F\alpha'
などが成り立つ
よって、自然変換と自然変換の横結合についてのみ示せば十分
定義よりコンポーネントは写像
(a,b).(\alpha\alpha')_♯\colon\hom_C(a,b)→\hom_D(a.FF',b.GG')
h;;(a,b).(\alpha\alpha')_♯=h.\alpha\alpha'
=(a.\alpha;h.G).\alpha'
=a.F\alpha';(a.\alpha;h.G).G'
=h;;(a,b).\alpha_♯;(a.F,b.G).\alpha'_♯
図の対角線
任意のhについて等しいので写像として等しい
(a,b).(\alpha\alpha')_♯=(a,b).\alpha_♯;(a.F,b.G).\alpha'_♯
=(a,b).\left[ \alpha_♯;(F^\mathrm{op}×G)\alpha'_♯ \right]
コンポーネントが等しいので自然変換として等しい
(\alpha \alpha')_♯=\alpha_♯;(F^\mathrm{op}×G)\alpha'_♯