from 様々な随伴の定義

三角等式を用いた随伴の定義

随伴の単位-余単位と関手の合成の等式を用いた定義の書き換えのようなもの

定義

圏\mathscr{A},\mathscr{B}間の関手F:\mathscr{B}\to\mathscr{A}、G:\mathscr{A}\to\mathscr{B}について、

自然変換\varepsilon:FG\to\mathrm{Id}_\mathscr{A} 、\eta: \mathrm{Id}_\mathscr{B}\to GF が存在して、

これらが三角等式を満たすとき、

つまり、下図を可換にするとき、四つ組(F,G,\epsilon,\eta)のことを随伴関係という

図の導出のイメージ

ここから

ここまで動かして、上下を結んで三角形にしている感じ

]

これで左の三角形はできた

三角等式の可換性の証明

左側の三角形の可換性を示す

↑の図はポイントフリーになっているの微妙に分かりづらい

対象を設定してあげる

個人的にはB_1と書いて代表感を出したほうがパッと理解できる

示したいのは以下の対応

FB\xrightarrow{(F\eta)_B}FGFB\xrightarrow{(\varepsilon F)_B}FB

=

FB\xrightarrow{\mathrm{id}_{FB}}FB

以下の転置関係を用いる

一つの図にすると

赤線同士は等しいので、青=緑になる

参考

『圏論入門』 pp.152-155

『圏論の道案内』 p. 225