米田の補題 メモ
- 米田の補題というのがある(Wiki)
- Wikiの冒頭文をそのまま書くと:
- 『米田の補題とは、小さなhom集合をもつ圏 C について、共変hom関手 hom(A, -) : C → Set から集合値関手 F : C → Set への自然変換と、集合である対象 F(A) の要素との間に一対一対応が存在するという定理である。』
- これが解るには何が解ればよいのかーーー
- 圏C
- 圏っていうのは、なんでもよいから、対象があって射があるもの
- 共変hom関手 hom(A,-) : C -> Set
- そもそも関手というのは、ある圏からある圏への矢印。言い換えると、圏を対象として持つ圏における射
- ここで、圏Cから圏Setへの関手、と書いてある。これは、圏Cの方のCは圏ならなんでもよいが、圏Setは、「集合の圏」と呼ばれる、特定の圏であると限定している。したがって、共変hom関手は、関手(圏から圏への射)であるが、行く先の圏が「集合の圏」に限定
- さらに条件がある。hom(*,#)というのが、「集合の圏」への関手と言う意味だが、圏Cからどういう集合を対応付けるのか、というと、圏Cの対象をあるルールで対応付け、圏Cの射をあるルールで対応付ける、というようにすることになっhている。その際、*に圏Cのある対象Aをとることにするとき、それをhom(A,#)と書き、とくに、対象Aから出るすべての射と、その射の行先の対象を問題にするとき、#を「アノニマス」にして、hom(A,-)と書く
- hom(A,-)の意味は分かったが、hom(-,A)というものもできそうである。これは、対象Aに入るすべての射と、その射の出発元対象すべてについての「集合の圏」への対応付け関手を表している
- 最後に残った、「共変」であるが、hom(A,-)が共変、home(-,A)が反変
- 集合値関手 F : C -> Set
- 集合値関手というのは、hom(A,-)で考えたのと同じように、集合の圏への関手。ただし、hom(*,#)である必要はなく、圏Cの対象と射とを集合オブジェクトに対応付ける関手であればよい
- F(A) というのは、この集合値関手によって、圏Cの対象Aを集合にした、集合である対象のこと
- 自然変換
- 自然変換というのは、関手を対象そした圏を考えたときの射の特別なもの。関手と関手があって、それに何かしらの対応付けができれば、それは圏。そこの射が気になるのは圏論なら当たり前のこと。ただし、そのような関手と関手との関係杖kには、いい素性のものがあり、それが自然変換
- 1対1対応が存在する
- 今、圏Cがあって、そのCに属する対象Aを取り出したとき、hom(A,-)という共変hom関手があるし、集合値関手Fがあれば、Aが対応する集合F(A)がある
- また、Fがあれば、hom(A,-)からFへの射があって、そのうち自然変換(と書く)を取ると、(それは集合であって)、その集合とF(A)という集合が1対1対応だ、と言っている
- ここでAの取り方は自由だし、Fの取り方も自由(らしい)
- このような1対1対応があることで、簡単な方の集合について検討することで、もう片方の集合について調べたことにできる、というのがメリット(らしい)
- 共変hom関手hom(A,-),hom(B,-)の間にもいい感じの対応付けがあって、それも使える
- Haskell
- Haskellでは「すべて」が関数として表される
- Haskellでは、「すべて」を関数として表すにあたり、階層構造にしている
- この階層構造が「圏は対象と射からで来ている」「圏を対象とすれば、圏の圏ができる」「射の集合を対象としてとらえる」「関手を対象としてしまう」「関手(home(A,-))の、"-"のように、『ここに何かを入れた状態を○○とする』、というときの"-"は、引数を受け取りたい準備状態」「あちこちで同じ枠組みで書けるコードは使いまわす(クラス)」のようにHaskellが対応できるものになっている
- 結局、(関数型)プログラミングでは、何かを受け取って何かを返すわけであるが、その受け渡し状態をHaskellでは型と言ったり関数と言ったりするが、圏論では、射と呼び、圏論では射を状況(どういう圏の射か、という状況)によって呼び名をつけて区別している
- また、関数というのは、色々な値・姿をするものを代数変数とすることで、色々に使いまわす道具であって、Haskellでも圏論でも、その使いまわせるものを、階層構造の色々な場所で、いろいろな階層で使いまわすことで簡略化しようとしている。まだ見つかっていない使いまわし可能なものがみつかったら、それを登録しよう、というはなし