１．米田の補題
圏論の重要な概念のひとつに米田の補題がある。これは次で表される。
\({\mathcal C}\)を圏とした時、任意の\({\mathcal C}\)の対象\(A\)と関手\(F: {\mathcal C} \rightarrow {\bf Sets}\)に対して
\({\rm Nat}({\rm Hom}(A,-),F) \cong F(A)\)
である。さらに、この同型\(\cong\)は、\(F\)と\(A\)に対して自然である。
２．米田の補題の証明
米田の補題で使われている専門用語の説明が終了したので、Haskellで利用できるようにする。米田の補題は煎じ詰めると次の可換図式になる。
この図は、前回の自然変換での説明に用いた図で、\(X\)を\(A\)に\(Y\)を\(X\)に変えたものである。さらに、\({\rm Hom}(A,A)\)を関数で表すと\(1_A\)となる。その他も関数を対応させると、図の内側に示した関数の可換図式が得られる。
Understanding Yonedaというブログには、豚の絵を使って視覚的に上記の可換図式が描かれている。それは次のようになっている。
ここで、豚は対象を示し、麻袋は射の集合を示す。
\(H_A(A)\)は\({\rm Hom}(A,A)\)に、\(H_A(X)\)は\({\rm Hom}(A,X)\)に、\(\phi_A\)は\(\vartheta_A\)に、\(\phi_X\)は\(\vartheta_X\)に読み替えると最初の可換図式と対応する。
そこで、米田の補題をこの可換図式を用いて読み砕くと次のようになる。
(自然であることを保証するために)任意の\(A\)と(自然であることを保証するために)任意の関手\(F\)に対して任意の\(p \in {\rm Hom}(A,A)\)を選ぶと、任意の\(X\)に対して\(\vartheta_X\)が一意に決まる。
ここでは、米田の補題の証明の概略だけを示す。
関数\(\phi : {\rm Nat} ( {\rm Hom}(A,-),F) \rightarrow F(A) \)を自然変換\(\vartheta \in {\rm Nat} ( {\rm Hom}(A,-),F) \)に対して
\(\phi(\vartheta)=\vartheta_A(1_A)\)
と定める(可換図式では\(\vartheta_X(f)\)となっているが、自然同型であるので、同型になっているものの一つを示せば、後は同様となるので、証明が簡単な\(\vartheta_A(1_A)\)を用いる）。
逆に、\(\psi : F(A) \rightarrow {\rm Nat} ( {\rm Hom}(A,-),F) \)を任意の\(u \in F(A) \)に対して
\(\psi(u)_X(f)=F(f)(u)\) ここで、\(f: X \rightarrow Y\)
と定める。
この時、証明は
1) \(\psi(u)\)が自然変換であること、
2) \(\psi = \phi^{-1}\)であること、
3) \(F, A\)に対する自然性
を示せばよい。詳しくは、Category Theoryを参照のこと。
２．米田の補題をHaskellに応用
そこで、上の証明の概要を用いてHaskellで表現する。\({\rm Nat} ( {\rm Hom}(A,-),F)\)に対して、
(forall x . (a -> x) -> f x)
が得られる。この式で、可換図式の記号は、Haskellの記号に変えてある。対応関係は、Haskellでのa,x,fは可換図式の\(A,X,F\)である。fが\(f\)でないことに注意してほしい。可換図式の\(f\)は(a -> x)である。
これが\(F(A)\)と自然同型になることから、次のプログラムが得られる。
(forall x . (a -> x) -> f x) ~ f a
Haskellには、演算子~がないので、証明の概略の\(\phi(\vartheta)=\vartheta_A(1_A)\)と\(\psi(u)_X(f)=F(f)(u)\)を用いると次のプログラムが得られる(なお、以下でfwは左から右、即ち、\(\phi\): (forall x . (a -> x) -> f x) -> f aであり、bwは右から左、即ち、\(\psi\): f a -> (forall x . (a -> x) -> f x) である）。
{-# LANGUAGE Rank2Types #-} fw :: (Functor f) => (forall x . (a -> x) -> f x) -> f a fw f = f id bw :: (Functor f) => f a -> (forall x . ((a -> x) -> f x) bw x f = fmap f x
二番目の関数bwはfmapの定義そのものである。
今、圏\({\mathcal C}\)から圏\({\mathcal D}\)へは、関手\(F\)によって写像できるものとする。圏\({\mathcal C}\)の対象\(A, B\)は関手\(F\)によって圏\({\mathcal D}\)の対象\(F(A), F(B)\)に移るものとする。このとき、対象\(F(B)\)の求め方には二通りある。一つは、\({\mathcal C}\)内で射\(f\)によって\(A\)から\(B\)に移した後、関手\(F\)を用いることである(関数fwは射\(f: A \rightarrow B\)の代わりに射\(1_A: A \rightarrow A\)を用いていると思えばよい）。
他の一つは、\(A\)から関手\(F\)によって\(F(A)\)に移した後、射\(F(f)\)を用いることである。射\(F(f)\)がfmapである。これが二番目の関数bwとなっている。
さらに、次のことが保証される必要がある。
fw bw :: id bw fw :: id
(forall x . (a -> x) -> f x)の部分をnewtypeで定義すると先のプログラムはさらに次のように書き換えることができる。
{-# LANGUAGE Rank2Types #-} newtype Yoneda f a = Yoneda (forall x. (a -> x) -> f x) fw :: (Functor f) => Yoneda f a -> f a fw (Yoneda f) = f id bw :: (Functor f) => f a -> Yoneda f a bw x = Yoneda (\f -> fmap f x)
