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

作成日: 2023-07-02

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

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

圏

\mathbf C

は対象

\rm Obj(\mathbf C)

を複数持ちます。

対象 $\rm X, Y$ の間には射 $\rm Hom(X,Y)$ が複数あり、射をつなげる演算で閉じています。

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

(f\triangleright g) \triangleright h = f\triangleright (g \triangleright h )

始まりと終わりが同じ射 $\rm Hom(X,X)$ には特別な恒等射

\rm id_X

が存在し、射につなげると溶けて消えます。

f\triangleright {\rm id_Y} = f\\ {\rm id_X}\triangleright f=f

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

なお、普通は射をつなげる演算は

g \circ f

で書きます。射をつなげる順序と関数適用の向きが逆でややこしいので、この記事では

f \triangleright g

で書きます。あくまでローカルルールです。

例: 集合の関数の圏

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

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

例: モノイドの圏

全てのモノイド

(M, \circ)

は圏として扱えます。対象をただひとつの

\ast

として、射

{\rm Hom}(\ast,\ast)

をモノイド

M\ni x

とします。射をつなげると演算をして

x\triangleright y=x \circ y

の圏になります。

例: 順序の圏

全ての順序集合

(S,\ge)

は圏として扱えます。対象

x,y

を集合の要素、射を順序

x\ge y

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

関手は圏をまるごと移す

圏

\mathbf C

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

{\bm F}\colon{\bf C} \Rightarrow {\bf D} \\ {\bm F}\colon {\rm X} \mapsto {\bm F} {\rm X} \\ {\bm F}\colon f\mapsto {\bm F} f

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

恒等射の保存 ${\bm F}{\rm id_X} = {\rm id}_{{\bm F}{\rm X}}$

射をつなげる演算の保存 ${\bm F}(f \triangleright g) = {\bm F}f \triangleright {\bf F} g$

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

${\bf C}$ : 有限集合を対象 $\rm X,Y$ として、全射の関数 $f: \rm X \to Y$ を射とする圏

$\bf D$ : 自然数を対象 $\rm x,y$ として、 $x \ge y$ なら射が1つだけある圏

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

{\bm F}\colon \bf C \Rightarrow D

が作れる。

${\bm F}({\rm X})=|\rm X|$

${\bm F}(f\colon {\rm X}\to {\rm Y})=|X|\ge|Y|$ を表す唯一の射

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

例: List<T>型

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

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

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

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

{\bm H}^{\rm A}\colon {\bf C} \Rightarrow {\rm Set}

です。

{\bm H}^{\rm A}({\rm X})= {\rm Hom}(\rm A,X)

例えば集合の圏の場合、Hom関手

{\bf H}^{\rm Int}

は集合

{\rm X}

を「Intを引数に取る(

\rm Int \to X

)全ての関数の集合」に移します。

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

Hom関手

{\bm H}^{\rm A}

は射

f

を「関数から関数に移す関数」に移します。

{\bm H}^{\rm A}(f\colon {\rm X \to Y}) = \sigma \mapsto \sigma \triangleright f \\ {\bm H}^{\rm A}\colon({\rm X\to Y})\to ({\rm Hom(A,X) \to Hom(A,Y)})

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

Hom関手

{\bf H}^{\rm Int}

の場合、関数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関手もあります。

{\bm H}_{\rm A}({\rm X})= {\rm Hom}(\rm X,A)

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

{\bm H}_{\rm A}(f\colon {\rm X \to Y}) = \sigma \mapsto f \triangleright \sigma \\ {\bm H}_{\rm A}\colon({\rm X\to Y})\to ({\rm Hom(Y, A) \to Hom(X,A)})

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

{\bm F}\colon {\bf C \Rightarrow D}

であれば

f\colon {\rm X \to Y}

を

{\bm F}{\rm X}\to {\bm F}{\rm Y}

に移しますが、

{\bm H}_{\rm A}

は

{\bm F}{\rm Y}\to{\bm F}{\rm X}

に移します。

このような、射を逆向きにして移す関手を反変関手

{\bm F}: {\bf C}^{\rm op}\Rightarrow{\bf D}

として扱います。

{\bm H}_{\rm A}:{\bf C}^{\rm op}\Rightarrow {\bf Set}

です

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

べき集合関手

\bm P\colon\bf Set^{\rm op} \Rightarrow Set

を次のように定義します。

{\bm P}({\rm X}) = \{X' | X' \subset X\} \\ {\bf P}(f)=f^{-1}={\rm Y}\mapsto \{x | f(x) \in {\rm Y}, x \in {\rm X}\}

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

\bm P

は反変関手になります。

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

関手

{\bm F},{\bm G}\colon {\bf C \Rightarrow D}

の間の関係が自然変換 $\theta\colon {\bm F}\leadsto {\bm G}$ です。自然変換の中身は関手の元の圏

\bf C

の対象から

\bf D

の射を返す写像です。対象に対する射を自然変換の成分

\theta_{\rm X} = f\colon {\bf F }{\rm X}\to{\bf G}{\rm X}

と書きます。

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

{\bm F}f\triangleright\theta_{\rm Y}=\theta_{\rm X}\triangleright{\bm G}f

※

\leadsto

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

例: 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つの間に全単射

y

が存在することです。

圏

\bf C

の対象

\rm A

と反変関手

{\bm F}\colon{\bf C}^{\rm op}{\bf \Rightarrow Set}

について、

$\theta: {\bm H}_{\rm A}\leadsto{\bm F}$ 　(Aに行くHom関手から関手Fへの自然変換)

${\bm F}{\rm A}$ 　(関手で移した先の対象)

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

※ 異なる対象A,B、射

f\colon\rm A\to B

について全単射が

y_{\rm A}

y_{\rm B}

が自然になる

\bm Ff\triangleright y_{\rm A}^{-1}=y_{\rm B}^{-1}\triangleright \bm Gf

ことも補題の一部です。

\bm G

は対象を自然変換に移す関手で、

f\colon\rm A \to B

を

{\bm G}f\colon(\phi:{\bm H_{\rm B}}\leadsto \bm F)→(\theta:{\bm H_{\rm A}}\leadsto {\bm F})

に移します。

※ 同様に、異なる関手

{\bm F,\bm G}

、自然変換

\psi:\bm F\leadsto\bm G

についても自然

\psi_{\rm A}\triangleright y^{-1}_{\bm G}=y^{-1}_{\bm F}\triangleright \Psi_{\rm A}

です。

\Psi_A: (\theta\colon \bm H_ {\rm A}\leadsto F) \to (\phi\colon\bm H_{\rm A}\leadsto G)

です。

例: べき集合関手

${\bf C} = {\bf Set}$

${\rm A} = \{0, 1\}$

${\bm F}\colon {\bf Set}^{\rm op}\Rightarrow {\bf Set}$ べき集合関手

とすると、

$\theta\colon{\bm H}_{\rm \{0,1\}} \leadsto {\bm P}$ ({0,1}に行くHom関手からべき集合関手への自然変換)

${\bm F}{\rm A} = {\bm P}\{0,1\} = \{\varnothing, \{0\}, \{1\}, \{0,1\}\}$

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

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

\theta

って具体的に何でしょうか。自然変換の定義を思い出すと、Setの対象XからSetの射

\theta_{\rm X}

が得られるものでした。Setの射は関数です。つまり、Xから{0,1}を返す関数

\sigma

を得て、Xのべき集合を返す多相関数が自然変換です。

\theta_{\rm X} : (X \to \{0,1\})\to{\bm P}{\rm X}

米田の補題の自然変換で対象からSetの射

\theta_{\rm X}\colon {\bf Set \to Set}

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

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

全単射

y=\theta \mapsto a \colon ({\bm H}_{\rm A}\leadsto {\bm F}) \to {\bm F}{\rm A}

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

対象

\rm X

について自然変換の成分

\theta_{\rm X}\colon{\bm H}_{\rm A}{\rm X}\to{\bm F}{\rm X}

とします。成分は先ほどの通り関数です。

自然変換の成分のうち

{\rm X} = {\rm A}

としてみます。関数

\theta_A \colon {\bm H}_{\rm A}{\rm A} \to {\bm F}{\rm A}

が得られます。

{\bm H}_{\rm A}{\rm A} = {\rm Hom(A,A)}

のことでした。圏には恒等射

{\rm id_A}:{\rm A \to A}

が存在します。Setの恒等射は恒等関数です。

自然変換の成分に恒等関数を適用して

\theta_{\rm A}({\rm id_A})

ができます。得られた結果は

{\bm F}{\rm A}

の対象になっています。やりました！

y(\theta)=\theta_{\rm A}(\rm id_A)

が全単射を与えてくれるようです。

べき集合関手の例の続き

べき集合関手では

y(\theta)=\theta_{\rm A}(\rm id_A)

はどうなるでしょうか。

\theta_X

はXから{0,1}を返す関数

\sigma

を得て、Xのべき集合を返す多相関数でした。Xから{0,1}を返す関数

\sigma

をみて、1を返す要素を集めて返す関数が自然変換になりそうです。

\theta_{\rm X}(\sigma\colon {\rm X}\to\{0,1\})=\{x\in X|\sigma(x)=1\}

\theta_{\rm A}(\rm id_A)

を考えてみると、

\theta_{\{0,1\}}(\sigma:\{0,1\}\to\{0,1\}) = \{x \in \{0,1\} | \sigma(x)=1\}\\\theta_{\{0,1\}}({\rm id_A})=\{1\}

1を返す要素を集めて返す多相関数

\theta

は、

\{1\}\in{\bf P}\{0,1\}

と対応しているようです。

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

ところで、米田の補題は全単射を与えてくれます。つまり、

{\bm P}\{0,1\} = \{\varnothing, \{0\}, \{1\}, \{0,1\}\}

に対応して、多相関数

\theta

が得られるようです。

y^{-1}=a \mapsto \theta \colon {\bm F}{\rm A} \to ({\bm H}_{\rm A}\leadsto {\bm F})

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

全ての対象Xについて、自然変換の成分

\theta_{\rm X}\colon {\bm H}_{\rm A}{\rm X}\to{\bm F}{\rm X}

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

AからXへの射

\sigma \in {\bm H}_{\rm A}{\rm X}={\rm Hom(X,A)}

を

\theta_{\rm X}

の引数に得たとき、反変関手

\bm F\colon {\bf C}^{\rm op}\Rightarrow {\bf Set}

で

\sigma

を移すと関数

{\bm F}\sigma

が得られます。

\sigma: X\to A\\{\bm F}\sigma = {\bm F}{\rm A}\to{\bm F}{\rm X}

{\bm F}\sigma(a)

を計算すれば、無事に

{\bm F}X

が得られました。

y^{-1}(a)_{\rm X}=\sigma \mapsto {\bm F}\sigma(a)

で良さそうです。

べき集合関手の例で

\{0\}\in{\bm P}\{0,1\}

としたときの自然変換

\theta

は次のようになります。

y^{-1}(\{0\})_{\rm X}=\sigma \mapsto {\bm P}\sigma(\{0\})=\{x\in X | \sigma (x) =0\}

\sigma:{\rm X}\to\{0,1\}

について、0を返す要素の集合を返す多相関数が

\theta_{\rm X}

のようです。1を返す要素を集めて返す関数とよく似ていますね。

{\bm P}\{0,1\} = \{\varnothing, \{0\}, \{1\}, \{0,1\}\}

に対応して、関数

\sigma

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

米田の補題の嬉しさ

米田の補題は、

{\bm F}={\bm H}_{B}\colon{\bm C}^{\rm op}\Rightarrow{\bf Set}

とした形がよく利用されます。

y\colon ({\bm H}_{\rm A}\leadsto{\bm H}_{\rm B})\to {\bm H}_{\rm B}A\ (={\rm Hom(A,B)})

自然変換

\theta

とAからBへ行く射

f\in {\rm Hom(A,B)}

が1対1に対応するようです。ポイントは、射

f

は関数とは限らない謎の矢印であるのに、自然変換の成分 $\theta_X\colon{\bm H}_{\rm A}{X}\to{\bm H}_{\rm B} X$ は関数であるということです。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)

{\bm F}={\bm H}_{B}\colon{\bm C}^{\rm op}\Rightarrow{\bf Set}

版だと、

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