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

木曜日なので圏論勉強会ではない方の圏論勉強会第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における積。
- 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、指数対象、すべて随伴
- 次回はモナド。モナドと随伴は密接な関係