7.随伴関手
7.1 米田の補題:復習
米田の補題は次のようになっていた。
局所的に小さな圏\(\mathcal{C}\)と集合の圏\(\mathbf{Set}\)、これらによって作られる関手圏\([\mathcal{C},\mathbf{Set}]\)を考えよう。今、任意の対象\(A \in \mathcal{C}\)と任意の関手\(F: \mathcal{C} \rightarrow \mathbf{Set}\)に対して、
\begin{eqnarray}
[\mathcal{C},\mathbf{Set}](\mathcal{C}(A,-),F) \cong F(A)
\end{eqnarray}
が成り立つ。ただし、\(\mathcal{C}(A,-) : \mathcal{C} \rightarrow \mathbf{Set}\)である。すなわち、これは関手である。このため、\([\mathcal{C},\mathbf{Set}](\mathcal{C}(A,-),F)\)は、関手\(\mathcal{C}(A,-)\)から\(F\)への自然変換である。
米田の補題をHaskellでは、どのようにあらわすことができるであろうか。自然変換は、多相関数(polymorphic function)で表すことができる。従って、型シグネチャで表すと
forall x. (a -> x) -> F x ~= F a
となる。Haskellでは、\(forall \ x\)を省略することができるが、ここでは、\(\mathcal{C}(A,-)\)の部分がどのように表されるかを正確に期するために、\(forall \ x\)をわざわざ付けた。
上の型シグネチャで、\( forall \ x. (a \rightarrow x) \rightarrow F \ x \)は高次の多相関数となっている。また、\(F \ a\)はデータ型である。
それでは少し、例を挙げてみよう。
例1)リスト
リストは関手なので、これを用いると、米田の補題は次のように書き換えられる。
\begin{eqnarray}
[\mathcal{C},\mathbf{Set}](\mathcal{C}(A,-),[- ]) \cong [A]
\end{eqnarray}
また、Haskellで表すと
forall x. (a -> x) -> [x] ~= [a]
となる。
そこで、左辺を自然変換\(\alpha\)とすると、
α :: forall x. (a -> x) -> [x]
となる。
これは、リストに対する関手と同じなので、
α f = fmap f
と考えることができる。これをクロージャと考えると、これに対する入力は\([a]\)と考えることができる。例えば、\([a1,a2,…,an]\)とすると、
fmap f [a1,a2,…,an] =[f(a1),f(a2),…,f(an)] =[x1,x2,…,xn]
となる。
例2)\({\rm Hom}\)集合の関手
関手を\(\mathcal{C}(B,-)\)にしてみよう。この時、\(F(A)\)は\(\mathcal{C}(B,A)\)になることに注意すると、米田の補題から、
\begin{eqnarray}
[\mathcal{C},\mathbf{Set}](\mathcal{C}(A,-), \mathcal{C}(B,-)) \cong \mathcal{C}(B,A)
\end{eqnarray}
となる。これをHaskellで表すと、
forall x. (a -> x) -> (b -> x) ~= (b -> a)
となる。\((b \rightarrow x)\)はリーダーであることに注意しよう。これは、
α :: (a -> x) -> (b -> x) g :: b -> a
とすると、
α f = f . g
となる。