米田の補題をリストで

土曜日に層・圏・トポス勉強会 #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] と対応する。