a proof of RAPL
すっきり証明する方法を考えました。
概要。
- right adjoint preserves terminals*1
- limit is a terminal of a cone category
- adjoint between categories induces an adjoint between cone categories
証明を厳密に全部書き下したら結局すっきりしてないんですが、それはまた別の話。
right adjoint preserves terminals
とすると
より。
adjoint between cone categories
で D を diagram (in the source category of G) とすると
で となるものが作れる。
は cone をそのまま写すだけ、
は cone を写すと
に入るので、その足に
の counit を post-compose すると
の cone が作れる。
これらが adjoint になっていることは を使うといえます。cone category の射はデータとしては diagram の存在するところの圏*2の射であることから、実質的にこの同型の制限という形で
が得られます。
たぶん。
right adjoint preserves limits
そうすると、right adjoint が terminal を保つことは分かっているので
は terminal を保つ、つまり D の limit を飛ばした先の GD-cone も limit になることがわかります。
