ようやく理解した米田の補題とHom関手

作成日: 2023-07-02

この前、知り合いに米田の補題を教えてもらって、ようやく腹落ちしました。

圏は群の拡張っぽい(違います)

圏は対象を複数持ちます。

対象の間には射が複数あり、射をつなげる演算で閉じています。

射をつなげる演算は結合法則が成立します。

始まりと終わりが同じ射には特別な恒等射が存在し、射につなげると溶けて消えます。

射の逆元は保証されないので、圏は群の拡張ではなくモノイドの拡張です。そういえば、競プロのセグメント木に載る構造はモノイドではなく正確には圏が載るという話がありましたね。

なお、普通は射をつなげる演算はで書きます。射をつなげる順序と関数適用の向きが逆でややこしいので、この記事ではで書きます。あくまでローカルルールです。

例: 集合の関数の圏

集合を対象として、集合と集合の間の射を関数とすると圏をなします。

neg: Int -> Int
to_str: Int -> String
neg |> to_str : Int -> String

例: モノイドの圏

全てのモノイドは圏として扱えます。対象をただひとつのとして、射をモノイドとします。射をつなげると演算をしての圏になります。

例: 順序の圏

全ての順序集合は圏として扱えます。対象を集合の要素、射を順序が成り立つときだけある1つの射とすると、順序集合は圏になります。どんな2つの対象の間も射は0本か1本です。

関手は圏をまるごと移す

圏の対象と射を圏の法則を保ったまま変化させる写像を関手といいます。

圏の規則を保ったまま移すために、射の写像に課される条件は次の2つです。

恒等射の保存

射をつなげる演算の保存

例: 有限集合の全射を自然数の順序に移す関手

: 有限集合を対象として、全射の関数を射とする圏

: 自然数を対象として、なら射が1つだけある圏

について要素数を対応させるの関手が作れる。

を表す唯一の射

全く別の2つの圏の関係を調べられるのが関手の嬉しさですね。

例: List<T>型

List: 型Tを型List<T>にする。
map: 関数(a -> b)を -> 関数(List<a> -> List<b>)にする。

Hom関手は射を対象にする関手

Hom関手が出でてきたあたりから、ややこしくて苦手でした。

対象Xを対象Aから始まりXで終わる射でつくられた集合に移す関手がHom関手です。

例えば集合の圏の場合、Hom関手は集合を「Intを引数に取る()全ての関数の集合」に移します。

注意: 圏の射が集合をなすとは限らないのですが、ここではそう扱います。

Hom関手は射を「関数から関数に移す関数」に移します。

射を写像の型は複雑ですが、定義はシンプルです。「Aを引数に取る関数σ」の終わりに「与えられた射f」をぶっ刺す関数です。

Hom関手の場合、関数f: Bool→Stringを移すと(Int→Bool)→(Int→String)になります。

HInt: (X -> Y) -> (Int -> X) -> (Int -> Y)
HInt(f) = fun σ -> σ |> f

to_str: Bool -> String
g(b) = if b { "T" } else { "F" }

is_large: Int -> Bool
h x = x > 100

HInt to_str :: (Int -> Bool) -> (Int -> String)

HInt to_str is_large x
== (fun σ -> σ |> to_str) is_large x
== (is_large |> to_str) x
== to_str (x > 100)
== if x > 100 {"T"} else { "F" }

半変関手のHom関手

Intを引数に取るHom関手があるなら、Intを返すHom関手もあります。

射を移すときは頭にぶっ刺します。

ところが、ここで1つ問題があります。射を移す写像の返す射の向きが逆向きになっています。本来の関手であればをに移しますが、はに移します。

このような、射を逆向きにして移す関手を反変関手として扱います。です

例: べき集合と逆像の反変関手

べき集合関手を次のように定義します。

集合をべき集合に移し、関数は逆像に移します。このとき、べき集合関手は反変関手になります。

自然変換は2つの関手で移した先を移す

関手の間の関係が自然変換です。自然変換の中身は関手の元の圏の対象からの射を返す写像です。対象に対する射を自然変換の成分と書きます。

関手で移した射と自然変換の成分について、射の交換が成立する必要があります。これを自然性と言います。

※ の矢印もメジャーな記法ではないです。

例: List<T>とOption<T>の間の多相関数

例えば、List<T>→Option<T>の多相head関数はList→Optionの自然変換List~>Optionになります。

head<T> : List<T>  -> Option<T>
head(l) = if l.size() > 0 { Some(l[0]) } else { None }

fmap<F> : (X -> Y) -> (F X -> F Y) 

to_str : Int -> String

fmap<List> to_str |> head<String> :: List<Int> -> Option<String>

(fmap<List> to_str |> head<String>) [1, 2]
== head<Int> (["1", "2"])
== Some("1")

head<Int> | fmap<Option> to_str :: List<Int> -> Option<String>

(head<Int> | fmap<Option> to_str) [1, 2]
== (fmap<Option> to_str)(Some(1))
== Some("1")

米田の補題

関手、Hom関手、自然変換が出てくる有名な補題が米田の補題です。

米田の補題は次の2つの間に全単射が存在することです。

圏の対象と反変関手について、

　(Aに行くHom関手から関手Fへの自然変換)

　(関手で移した先の対象)

……なんか突然いっぱい文字が出てきて困りました。集合の圏の例でなぞってみましょう。

※ 異なる対象A,B、射について全単射がが自然になることも補題の一部です。は対象を自然変換に移す関手で、をに移します。

※ 同様に、異なる関手、自然変換についても自然です。です。

例: べき集合関手

べき集合関手

とすると、

({0,1}に行くHom関手からべき集合関手への自然変換)

が1対1に対応すると言っているらしいです。

{0,1}に行くHom関手からべき集合関手への自然変換って具体的に何でしょうか。自然変換の定義を思い出すと、Setの対象XからSetの射が得られるものでした。Setの射は関数です。つまり、Xから{0,1}を返す関数を得て、Xのべき集合を返す多相関数が自然変換です。

米田の補題の自然変換で対象からSetの射が得られるのは、べき集合関手に限らず一般にそうです。Setの射は関数なので要素を関数適用できる。ここが僕の理解できていなかったポイントでした。

全単射yを実際に構成する

全単射を実際に作ってみましょう。

対象について自然変換の成分とします。成分は先ほどの通り関数です。

自然変換の成分のうちとしてみます。関数が得られます。のことでした。圏には恒等射が存在します。Setの恒等射は恒等関数です。

自然変換の成分に恒等関数を適用してができます。得られた結果はの対象になっています。やりました！が全単射を与えてくれるようです。

べき集合関手の例の続き

べき集合関手でははどうなるでしょうか。

はXから{0,1}を返す関数を得て、Xのべき集合を返す多相関数でした。Xから{0,1}を返す関数をみて、1を返す要素を集めて返す関数が自然変換になりそうです。

を考えてみると、

1を返す要素を集めて返す多相関数は、と対応しているようです。

逆向きの全単射とべき集合関手

ところで、米田の補題は全単射を与えてくれます。つまり、に対応して、多相関数が得られるようです。

を具体的に与えみましょう。

全ての対象Xについて、自然変換の成分を与えれば自然変換を定義したことになるのでした。そして、成分は関数です。

AからXへの射をの引数に得たとき、反変関手でを移すと関数が得られます。

を計算すれば、無事にが得られました。で良さそうです。

べき集合関手の例でとしたときの自然変換は次のようになります。

について、0を返す要素の集合を返す多相関数がのようです。1を返す要素を集めて返す関数とよく似ていますね。

に対応して、関数がその要素を返す要素を集めると、それぞれ自然変換が手に入るようです。

米田の補題の嬉しさ

米田の補題は、とした形がよく利用されます。

自然変換とAからBへ行く射が1対1に対応するようです。ポイントは、射は関数とは限らない謎の矢印であるのに、自然変換の成分は関数であるということです。Xから始まる射の集合とその間の関数を調べるだけで、謎の射の矢印のことがわかるのがうれしいですね。

米田の補題は型の圏だと

contramap : (X -> Y) -> (F Y -> F X)

A = Int とする。
F を反変関手とし、contramapがある。

y : (forall X. (X -> Int) -> F X) -> F Int
y(σ) = σ<Int>(id<Int>)
y_: F Int -> (forall X. (X -> Int) -> F X)
y(a) = fun σ -> contramap<F>(σ)(a)

版だと、

F = * -> Stringとすると
y : (forall X. (X -> Int) -> (X -> String) -> Int -> String
y(σ) = σ<Int>(id<Int>)
y_: (Int -> String) -> (forall X. (X -> Int) -> (X -> String)
y_(f) = fun σ -> contramap<* -> String>(σ)(f)

contramap<* -> Sring>: (X -> Y) -> (Y -> String) -> (X -> String)
contramap(σ)(f) = σ |> f
y_(f) = fun σ -> σ |> f

具体的にto_str: Int→Stringを与えると、(X → Int) → (X → String)に変換できる。

to_str: Int -> String
y_(to_str) : (X -> Int) -> (X -> String)
y_(to_str) == fun σ -> σ |> to_str

map_to_str: (X -> Int) -> (X -> String)
map_to_str(σ) = fun x -> to_str(σ(x)) == σ |> to_str
y(map_to_str): Int -> String
y(map_to_str) == map_to_str(fun x -> x) == fun x -> to_str(x)

ところで、残念ながらHaskellの反変関手Data.Functor.Contravariantにはほとんど例がない。

数少ない中でEquivalenceがそうらしい。引数が型変数だと反変になりがち。

newtype Equiv a = Equiv { getEquiv :: a -> a -> Bool }
contramap<Equiv>: (X -> Y) -> (Equiv Y) -> (Equiv X)
contramap(σ) = fun e -> Equiv (fun x y -> getEquiv e (σ x) (σ y))

リストの先頭だけで等価判定
head_eq = Equiv (List Int)
head_eq = Equiv (fun x y -> head x == head y)

タプルの1つ目をリストにする関数で
fst_to_init :: (Int, a) -> List Int
fst_to_init (x, _) = [x]

タプルの1つ目で判定する。やはり、頭にぶっ刺して、先に処理する。
fst_eq :: Equiv (Int, a)
fst_eq = contramap fst_to_init