米田の補題をリストで
土曜日に層・圏・トポス勉強会 #3に参加してきたのだが、ちょうど米田の補題の証明が終わる直前でタイムアウトになった。帰宅してから証明の続きをやってみて、まあできたのだが、いつもどおりサッパリイメージが沸かない。
勉強会でのtMiyaさんの、何か例を考えた方がいいんじゃないかという言葉に従って、整数型とリスト化関手で考えてみた。以下、Haskell 風の適当記法で。
米田の補題は、圏 D と 圏 Sets に対して、関手 hom(C, -): D → Sets から 任意の関手 F: D → Sets への自然変換全体と、集合 F(C) が自然な 1 対 1 対応をするという主張。
対象 C は任意なので、Int型とする。関手 F も任意なので、リスト化関手でやってみる。記号は [] で囲むものにする。
関手 hom(Int, -) で Int、Float、String、Bool はそれぞれ
hom(Int, Int) = (Int → Int) 型 hom(Int, Float) = (Int → Float) 型 hom(Int, String) = (Int → String) 型 hom(Int, Bool) = (Int → Bool) 型
にうつる。一方、リスト化関手 [] ではそれぞれ
[Int] [Float] [String] [Bool]
にうつる。これらの間の自然変換 α、β を考える。つまり
α | β | (Int → Int) → [Int] | (Int → Int) → [Int] | | | α | β | (Int → Float) → [Float] | (Int → Float) → [Float] | | | ……… α | β | (Int → String) → [String] | (Int → String) → [String] | | | α | β | (Int → Bool) → [Bool] | (Int → Bool) → [Bool] | . . . . . .
のように、一群のαたち、βたち、… となる。圏論ではいちいちαInt、αFloatなどと書くが、Haskellだと
α :: (Int → a) → [a] β :: (Int → a) → [a] . . .
という、型変数をもつ多相型の関数のことになる。
米田の補題の主張は、このα、β、… のそれぞれ*1が [Int] 型の値と 1 対 1 に対応するというもの。つまり、[1, 2, 3] というリストが α に対応し、[5, 4] というリストが βに対応し…、となっていることを言っている。逆に、自然変換(を表す多相関数)が与えられたら、それに対応して [Int] の値が 1 つ決まるということも言っている。
[1, 2, 3] が決める多相関数を仮に α とする。どのようにして α を決めるのか。
α :: (Int → a) → [a] α(f) = [f(1), f(2), f(3)] = map f [1, 2, 3] -- Haskell の map で表現した = [f] [1, 2, 3] -- 関手 [] に f を適用した
とすればよい。つまり α は [1, 2, 3] というリストを内蔵していて、引数としてもらった関数をリストの要素それぞれに適用していく。内蔵しているリストによって、各自然変換は特徴づけられる。
逆はどうすればいいか。つまり、自然変換 α が与えられたとき、[Int] 型の値が決まるはず。それをどう見つけるか。
上の話から、α はリストを内蔵しているはずで、それをうまく出すようにすればよい。
α :: (Int → Int) → [Int] -- α の型変数を Int にしたもの。 id :: Int → Int -- 恒等関数 α(id) -- = [1, 2, 3]
と、Int 型の恒等関数をαに入れてやれば、上の α の定義から [1, 2, 3] が得られることがわかる。
米田の補題はより一般的に、型の圏でなくても、Int でなくても、リストでなくても、今見たような 1 対 1 対応があると言っている。上の構成法は米田の補題の証明をなぞっただけなので、一般的な場合でもそのまま行くはず。
まだ理解したとは思わないが、この例ではかなり具体的なイメージが持てた。
*1:任意の多相関数ではない。多相関数のうちで自然変換の性質を持っているものだけが [Int] と対応する。