随伴の単位-余単位と関手の合成の等式を用いた定義

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

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

定義

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

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

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

このとき、

$ Fは$ Gの左随伴であり、

$ Gは$ Fの右随伴である

補足

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

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

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

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

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

https://gyazo.com/13fd6ebbc204e37c831866d270a5b314

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

https://gyazo.com/84ae7bf0fe53b967f6d8c626de0dbf54

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

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

https://gyazo.com/04fd5d90548e32ca1a5682546c4b0a1e

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

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

https://gyazo.com/9743a6296c8d9402141d6919bb5a665e

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

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

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

https://gyazo.com/888b78aad716404d25a31c43110a5ceb

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

https://gyazo.com/808b25b3ab96ce1840b82efba117d4a1

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

参考

参考

Fの向きが逆なので注意mrsekut.icon