トポスは有限余極限を持つ

層・圏・トポス読書会も読了をもって先日めでたく終了したわけですが、その最後を飾る定理「トポスは finite colimit を持つ」*1の純圏論的証明に興味を持ったので調べてみました。その証明は「層・圏・トポス」にもあるように*2、初等的とは言いがたいですが、方針はAn informal introduction to topos theory (Tom Leinster, PDF)に簡潔に出ています:

For every topos E, we have the contravariant power set functor P = Ω(-): Eop → E. It can be shown that P is monadic. But monadic functors create limits, and E has finite limits. Hence Eop has finite limits; that is, E has finite colimits.

証明は難しいので、ここに出てくる言葉をちょっと説明して、お茶を濁すことにします。

contravariant power set functor P

集合圏でいうと、集合にそのベキ集合を対応させ、写像 f に f-1 を対応させる反変関手です。

P is monadic.

関手Pがモナディックとは、P とその随伴対 Q が作るモナドに Eilenberg-Moore 構成を行うと、元の P と同値になるということです。もっとくだけていうと、最初から EM 構成になってるような関手です。

monadic functors create limits

これは Beck の定理です。関手が極限を創出するというのは、関手で行った先で極限をとれば、その関手で極限もろとも元に戻せて、さらに極限になっているということです。詳しくはマックレーン本にあるので、頑張ってください。マックレーン本では、coequalizer を創出するとなっていますが、この定理は色々なバージョンがあるようなのでその一つなのでしょう。

証明の詳細は、

  1. Topos Theory (P.T. Johnstone.)
  2. TOPOSES, TRIPLES AND THEORIES (Barr, Wells. PDF)
  3. Sheaves in Geometry and Logic: A First Introduction to Topos Theory (MacLane, Moerdijk.)

にあるそうです*3。
私は 3 を、なか見検索とGoogle Books で眺めました。Sheaves in ... には、難しい証明の後に、余極限の手作りの構成を実演してみせています。これは表向きには、証明に出てきた小難しいモロモロが出てこないので、眺めると楽しいかもしれません。


この定理が面白いのは、乗法的なもの(1、×、pullback 等、極限)だけから、加法的なもの(0、+ 等、余極限)をつくることができるというところです。かなりアクロバティックでテクニカルですが、できてしまうというのが興味深いです。

*1:「層・圏・トポス」では実は証明されてない！

*2:p.122.

*3:CLTT p. 350.