from 様々な随伴の定義

随伴関手であることが分かっている関手に関係する証明を書くのに便利である

直接操作できる公式を持つから

定義

以下の2式を満たすとき随伴F\dashv Gと記述する

\varepsilon F\circ F\eta = \mathrm{id}_F

G\varepsilon\circ\eta G=\mathrm{id}_G

このとき、

FはGの左随伴であり、

GはFの右随伴である

補足

この式に出てくるまとまりは全部自然変換だよ

\varepsilon F, \eta G, \mathrm{id}_Fなどは全部自然変換

自然変換\etaを単位と言う

自然変換\varepsilonを余単位と言う

状況として下図の様になっている

青の部分と緑の部分を縦に並べて描く

それぞれ、自然変換の水平合成をする

水平合成によって関手FGFが得られ、縦に並べて描くことによって、そのまま垂直合成をイメージできる

垂直合成によって自然変換\varepsilon F\circ F\etaを得る

これと恒等自然変換\mathrm{id}_Fが等しい、というのが随伴の定義の1つ目の式だ

同様の定義をストリング図を用いて示す

描く量が少ないので両方示す

単位、余単位と関手の合成の等式を用いるものを図にしたもの

最後の図の自然変換\varepsilon F\circ F\eta:F\to Fと、恒等自然変換\mathrm{id}_Fが等しくなる

これも同様にG\varepsilon\circ\eta G=\mathrm{id}_Gとなる

参考

参考

Fの向きが逆なので注意

『圏論入門』 pp.150-152