Saturday 24 August 2013

ハッカーズチャンプルー

行ってきました。今回は、スポンサーちゃんといるので、なんと、

* ビーチパーティがただ

ぱちぱちぱちぱち。

長丁場でしたが、僕は、ゆっくり行ったので問題なしです。気持ちの良いビーチパーティでした。

 * * *

Agdaでは、Hom(F(-),-)=Hom(-,U(-)) から随伴関手を導くってのに行き詰っていたんですが(逆はすぐにできた)…

あまりにわからないので、
<a href="http://en.wikipedia.org/wiki/Adjoint_functors">英語のWikipedia</a> を見たんですが

* Naaturality of Φ imply that

はぁ? そんなの聞いてませんが。で、ハッカーズチャンプルーを抜けだして、The Book (黄色のMacLaneのやつ)を
取ってきてみると、ご丁寧に可換図まで書いてある。つまり、この二日悩んでいた証明は…

* 問題の仮定だった

らしいです(笑)。確かに、射の対応だけで、あんな複雑な式が出るわけない。その naturality は f = U(f*)○η で、 普遍問題の解そのものだったりするので、ちょっとあきれ気味です。随伴関手ってのは実は自然変換そのものだったのか。

No comments: