読者です 読者をやめる 読者になる 読者になる

北海道苫小牧市出身の壮年PGが書くブログ

永遠のプログラマを夢見る、苫小牧市出身のおじさんのちらしの裏

今日は 圏論勉強会 第12回 の日です

レポート math

木曜日なので圏論勉強会ではない方の圏論勉強会 第12回に来ています。資料ustreamは公開されています。

第12回: 自然性・米田の補題 / 講師 @9_ties さん

  • 圏論は自然性の記述のために生まれた
  • 自然変換は射の集合
    • 射をcomponentという
  • 圏論は「構成」に興味がある。個別の対象や射ではない
    • 「構成」は関手で扱う。自然変換は構成の間の関係
  • 例: F X = X × B と G X = Xについてπ_1Xを集めると、自然変換π_1:F→Gが作れる
  • 自然同型: すべてのcomponentが同型射
    • 例: A×(B×C) =~ (A×B)×CはA,B,Cについて自然
    • つまり、関手-×(B×C)と関手(-×B)×C、関手A×(-×C)と関手(A×-)×C、関手A×(B×-)と関手(A×B)×-が自然同型
  • 自然変換同型*1は、関手圏の同型
    • 関手圏は、対象が関手、射が自然変換 (第3回の復習)
  • 関手圏はCatにおける指数対象。1はCatにおける終対象。積圏はCatにおける積。
  • 関手圏のHom集合は自然変換の集合
    • プログラミングにおいて、関手は多相型(単純型だと定数関手)
    • 自然変換は多相関数
    • 例えば、[a]、Intは関手で、[a] -> Int は自然変換
    • sort は自然変換ではない。[a] -> [a]ではなく、Ord a =>が必要 (ad-hoc多相なので)
  • 米田の補題 : 圏論の至るところで使う重要な補題
  • F:C→Sets → 集合値関手
    • 関手圏D^CにはDの構造が入る
    • Setsはなんでもできる、いい性質を持っている
    • Sets^CにはSetsの構造が入るので、それを利用してCを調べられる
    • 物体を調べるときには、長さや重さを調べる
    • 物体から数字へのマッピングを使っていることになる
    • CをSetsにマッピングして調べるとよい
  • 米田の補題
    • F:C^OP → Setsに対して、Nat(C(-, X), F) =~ F Xで、FとXについて自然
    • 左辺は自然変換の集まり。F Xは集合。
    • よくわからない左辺が、具体的な集合で与えられる
  • 「自然」と言われたら図式をぱぱっと書けるようになること。意味はわからなくても。
  • 例: X=A×B、F X = Hom(X, A)×Hom(X, B)
    • Nat(Hom(-, A×B), Hom(-, A)×Hom(-, B)) =~ Hom(A×B, A)×Hom(A×B,B)
    • 左辺の自然同型であるものに着目
    • <f,g>:X→A×Bと(f, g):(X→A)×(X→B)。右辺はπ_1とπ_2
    • <f,g>と(f,g)の1-1対応は、π_1とπ_2で決まる、ということを含んでいる
  • 例2: X=B^A、F X=Hom(X×A, B)
    • Nat(Hom(-,B^A), Hom(-×A,B)) =~ Hom(B^A×A, B)
    • 自然同型にたいしてeval mapが対応する
  • 証明
    • NatからFXへのマッピングは、θ_X(1)
    • FXからNatへのマッピングは、F(f)(x)
    • ψ=φ^-1であることを確かめてみる → ごりごり計算
  • 米田の補題の双対
    • F:C→Sets、Nat(C(X,-),F) =~ F X
    • HaskellでCoYonedaを
    • newtype CoYoneda f x = CoYoneda (forall a. (x -> a) -> f a)
    • liftCoYoneda :: f x -> CoYoneda f x, \x f -> fmap f x
    • lowerCoYoneda :: CoYoneda f x -> f x, \(CoYoneda y) -> y id
    • (liftCoYoneda . lowerCoYoneda) [1,2,3] == [1,2,3]
  • 任意のデータ型から関数が作れ、関数が作れればFunctorにできる
  • 米田の補題より、Nat(Hom(-, A), Hom(-, B)) =~ Hom(A, B)
    • AとBの間の射から、X→AをX→Bへのマッピングが一つ作れる
  • 米田の原理
    • Hom(-, A) =~ Hom(-,B) であれば、A =~ B
    • Hom(X, (A^B)^C) =~ ... =~ Hom(X,A^(B×C))の証明は簡単
    • これから(A^B)^C =~ A^(B×C)が言えた。(前回の証明は数ページ)
  • 米田の埋め込み
    • y(A) = Hom(-, A): C→Sets^(C^OP)
    • Hom(-,A)は良い性質を持つ(Setsの要素なので)。そこへ埋め込む。米田の原理で元に戻ってこれる
    • Sets^(C^op)はデカルト閉圏、極限を保つ、トポス
    • 前層とも呼ばれる
随伴の予習
  • MacLaneによる標語 "Adjunction arises everywhere"
    • ほとんどを随伴で説明できる
    • 随伴(F,G,φ)。関手F, G。φ:D(F X,Y) =~ C(X, G Y)となる
    • F |- G
    • id_FXに対応するηを単位元、id_GYに対応するεを余単位元
  • 対角関手Δ X=(X, X) について、Δ |- ×。つまり、fとgの組みと<f, g>が1対1
    • 積はΔの右随伴。(π1, π2)は余単位元
    • +|- Δ |- ×。実は任意のlimit、colimitをとれる
  • カリー化は、随伴 (-)×A |- (-)^A
  • 自由対象、lim,com、指数対象、すべて随伴

*1:Thanks to @1to100penさん