日々の流転

λ. “Co-limits in topoi” by Robert Paré

Given a cartesian closed category E with subobject classifier t:l→Ω, it is shown that the functor Ω^{( )} : E^op→E is tripleable. Standard results from the theory of triples are then used to show that E has I-colimits if and only if it has I^op-limits. This gives a new proof of Mikkelsen's theorem which states that E has all finite colimits.

『圏論による論理学—高階論理とトポス』 清水 義夫 - ヒビルテ (2008-04-01) で、colimitの存在をtoposの定義から取り除けることについて「どうやるか分からなかった」と書いたけど、証明がこれに書いてあるらしいということをbonotakeさんに教えてもらった。

べき対象関手 Ω^{( )} : E^op→E は、自然同型 E(A, Ω^B) ≅ E(A×B, Ω) ≅ E(B×A, Ω) ≅ E(B, Ω^A) ≅ E^op(Ω^A, B) によって、自分自身を左随伴として持つ。 さらに、Ω^{( )} は tripleable (もしくはmonadic) 、すなわちE^opはこの随伴から定まるモナドの Eilenberg-Moore 代数の圏に等しい。 tripleableな関手に関するよく知られた結果(tripleable functor create limits)により、E における I^op-limit を E^op における I^op-limit に持ち上げられて、これは当然 E における I-colimit になってると。

流れは分かったが、tripleableであることの証明に使っている定理(Barr-Beck “crude tripleableness theorem” もしくは Beck's monadicity theorem)と、「tripleable functor create limits」をまだ理解できていないので、これを読んだだけではあまり分かった気になれず。 その辺りの話は Toposes, Triples and Theories の「3.3. Tripleability」「3.4. Properties of Tripleable Functors」あたりに超詳しく載っているみたいだけど。

λ. nobsunが生徒になってくれる人を募集している

• 生徒になってくれる人募集 - HaHaHa! - haskell

nobsunが生徒になってくれる人を募集している。 nobsunに対面で直接教えてもらえるなんて、多分すごくラッキーなことだと思うので、Haskellプログラミングに興味のある入門者の方は応募してみてはいかがでしょうか。