米田の補題 メモ

  • 米田の補題というのがある(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への射があって、そのうち自然変換(Nat(hom(A,-),F)と書く)を取ると、(それは集合であって)、その集合とF(A)という集合が1対1対応だ、と言っている
    • ここでAの取り方は自由だし、Fの取り方も自由(らしい)
  • このような1対1対応があることで、簡単な方の集合について検討することで、もう片方の集合について調べたことにできる、というのがメリット(らしい)
  • 共変hom関手hom(A,-),hom(B,-)の間にもいい感じの対応付けがあって、それも使える
  • Haskell
    • Haskellでは「すべて」が関数として表される
    • Haskellでは、「すべて」を関数として表すにあたり、階層構造にしている
    • この階層構造が「圏は対象と射からで来ている」「圏を対象とすれば、圏の圏ができる」「射の集合を対象としてとらえる」「関手を対象としてしまう」「関手(home(A,-))の、"-"のように、『ここに何かを入れた状態を○○とする』、というときの"-"は、引数を受け取りたい準備状態」「あちこちで同じ枠組みで書けるコードは使いまわす(クラス)」のようにHaskellが対応できるものになっている
    • 結局、(関数型)プログラミングでは、何かを受け取って何かを返すわけであるが、その受け渡し状態をHaskellでは型と言ったり関数と言ったりするが、圏論では、射と呼び、圏論では射を状況(どういう圏の射か、という状況)によって呼び名をつけて区別している
    • また、関数というのは、色々な値・姿をするものを代数変数とすることで、色々に使いまわす道具であって、Haskellでも圏論でも、その使いまわせるものを、階層構造の色々な場所で、いろいろな階層で使いまわすことで簡略化しようとしている。まだ見つかっていない使いまわし可能なものがみつかったら、それを登録しよう、というはなし