bitterharvest’s diary

A Bitter Harvestは小説の題名。作者は豪州のPeter Yeldham。苦闘の末に勝ちえた偏見からの解放は命との引換になったという悲しい物語

随伴関手 - 随伴関手をHaskellで表現する

7.8 随伴関手をHaskellで表現する

随分と時間がかかったが、随伴関手をHaskellで表現するための準備がほぼ出そろった。ほぼといったのは、もう一つだけ、頭の体操をしておかなければならないことがある。それは、右随伴関手が表現可能関手でもあるということだ。

1)右随伴関手は表現可能関手である

表現可能関手を復習しておこう。局所的に小さな圏\(\mathcal{C}\)と集合の圏\(\mathcal{Set}\)において、\({\rm Hom}\)関手\(\mathcal{C}(A,-)\)と関手\(F\)の自然変換が、自然同型である時、即ち、
\begin{eqnarray}
\mathcal{C}(A,-) \simeq F
\end{eqnarray}
ならば、\(F\)を表現可能関手という。

それでは、右随伴関手が表現可能関手であることを示そう。随伴の定義は次のようになっていた。

\(\fbox {随伴の定義2:}\)
二つの局所的に小さな圏\(\mathcal{C},\mathcal{D}\)において、関手の対\(R: \mathcal{C} \rightarrow \mathcal{D}, L: \mathcal{D} \rightarrow \mathcal{C}\)が次の条件を満たす時、随伴であるという。
\begin{eqnarray}
\mathcal{C} (L(Y),X) \simeq \mathcal{D} (Y,R(X)) \\
\end{eqnarray}

これを図で示すと以下のようになることも示した。
f:id:bitterharvest:20180526090958p:plain

そこで、\(\mathcal{D}\)は集合の圏でもあるので、これを\(\mathcal{Set}\)で、\(Y\)を単集合(singleton setに置き換えると下図を得る。
f:id:bitterharvest:20180526102225p:plain

従って、
\begin{eqnarray}
\mathcal{C} (L( ),X) \simeq \mathcal{D} ( ( ),R(X))
\end{eqnarray}
を得る。右側の\(\mathcal{D} ( ( ),R(X))\)は、単集合を\(R(X)\)に写すものである。関数の数は、その集合の要素の数と同じになる。従って、各\(x \in X\)に対して、一つの関数を与えるので、\(R\)は表現可能関手となる。即ち、
\begin{eqnarray}
\mathcal{C} (L( ),-) \simeq R
\end{eqnarray}
である。

2)Haskellで表現する

それではすべての材料がそろったので、Haskellで表すことにしよう。ここでは、最初に定義したものを実装することとしよう。定義は次のようになっていた。
\(\fbox {随伴の定義1:}\)
二つの局所的に小さな圏\(\mathcal{C},\mathcal{D}\)において、関手の対\(R: \mathcal{C} \rightarrow \mathcal{D}, L: \mathcal{D} \rightarrow \mathcal{C}\)が次の条件を満たす時、随伴であるという。

\begin{eqnarray}
\xi : L \circ R \rightarrow I_\mathcal{C} \\
\mu : I_\mathcal{D} \rightarrow R \circ L
\end{eqnarray}

そこで、\(L,R\)を\(f,u\)とし、\(\xi,\mu\)を\(counit,unit\)とすると、次のようになる。

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

class (Functor f, Representable u) => Adjunction f u where
  unit :: a -> u (f a)
  counit :: f (u a) -> a

class Representable f where
  type Rep f :: *
  tabulate :: (Rep f -> x) -> f x
  index :: f x -> Rep f -> x