北海道苫小牧市出身の初老PGが書くブログ

永遠のプログラマを夢見る、苫小牧市出身のおじさんのちらしの裏

米田のレンマのイメージ図

米田のレンマ(層・圏・トポス―現代的集合像を求めてのP.71)がどうも不思議な定理に感じたので、イメージ図を書いてみました。

元の圏ではなく、Setsの圏内の図として書いてます。真ん中のC(を関手Fで移した集合)がhom関手をとる時に起点となる対象です。hom関手によって各対象は、射を束ねた集合に移ります。hom(C,A)等がそれです。

hom(C, -)とFの間の自然変換は、緑の矢印と青の矢印です。もちろん表記は省略してますが、二つだけじゃなくたくさんあります。

例えば、緑の自然変換の対象Aコンポーネント(hom(C,A)からFAへの矢印)を考えると、これはC→Aなる射に対してFA上の値を与える関数となります。そのためには、射の出元であるFC*1の元を固定するとよさげです。図では緑のXとして書きました。この、緑のXと緑の矢印が対応すると言うのが、米田のレンマの主張となります。

レンマを文面で見ただけだと摩訶不思議でしたが、図を見るとFCの元が自然変換を定める理由がなんとなく理解できます。

あ、書き忘れ。赤で書いたのは、恒等射のつもりです。こいつで自然変換から元となるFCの元を引き出せます。詳細は書籍内の証明を見て下さい。

おまけ

id:oto-oto-otoさんが、米田の補題をリストでと言うHaskellライクな例を作ってくれてますので、そのイメージ図も載せておきます。

一応補足すると、fは中央から外側に伸びる黒と赤の矢印です(自然変換はこれらの射を引数にとる関数ですので)。

*1:正確には、「射を関手Fで移したSets上の関数の定義域であるFC」となる。