米田さんの話
圏論やってると米田さんにお世話になる機会も多いと思うが,
イマイチ意味も使い方も分からんいう僕みたいな人向けの記事です.
記事を書くにあたって,主に
圏論番外:米田の補題の周辺から(via 檜山檜山正幸のキマイラ飼育記)
や,
MathAdventCalenderの12月24日の記事
等を参考にしました.
簡単なことしか書いてません,ごめんなさい.
まず米田さんとは
locally smallってのは
各オブジェクト
例えば集合と写像を射とする圏
また,各 に対して,
という関手が定まります.
ここで
で
です.
さっきのlocally smallはこの 関手の定義が意味をなすために必要なわけです.
米田の補題(※CWMではcontravariat versionと呼ばれているもの)
任意の関手
と
に対して,
自然な同型
が存在する.
因みに米田の補題は圏論における外延性のようなものと言われています.
どういうことでしょうか.
まず,圏論では基本的にオブジェクトの同一性概念なんてものはあまり考えず,重要視されるのは圏での同型概念です.
オブジェクトの の``外延''を見たい時にはその情報は
を参照すればよい,というのが米田さんが教えてくれることです.
では前の米田の補題の に
を入れてみましょう.
米田さんの系
任意の
に対して,自然な同型
が存在する.特に,前層の圏
における同型
と圏
における同型
は上の対応で移りあう.
つまり,オブジェクト
が同型であることの必要十分条件は,
と
が同型であることである.
で
が同じかどうかを検査したいときには元を取ればよかったのですが,一般の圏のオブジェクト
の同型を調べるにはまず任意の
と任意の射
をとって,
と
の間に一対一対応があり,しかもそれが
に関して自然であることを証明すればよいのです!
ところで,SGLとかだと射 は
の一般化元(generalized element)なんて呼ばれていたりします.
つまり,集合論では元をとるけど,圏論では一般化元をとって議論すれば同型判定ができる,ということです.
では応用してみましょう.
今考える圏 はカルテジアン閉圏です.
指数法則
.
証明
さて,米田さんの出番です.
目的の同型を示すためには,一般化元と
の間に自然な一対一対応があることを示せば良いのです.
まず,注意すべきはexponentialの定義となる随伴の性質です:
.
これは
に関して自然でなければなりません.
次に,productは図式のuniversalityから定義されますが,locally smallな圏では以下のに関する自然な同型でもって定義しても同じです:
.
いま
として,
が証明できます.
上の同型はに関して自然であるので米田さんにより
が証明出来ました.
やっぱ米田さんってすごい.