６．５ 随伴とモナド
ストリング・ダイアグラムを用いて、随伴からモナドが導き出されることを示そう。
前述したように随伴は、二つの圏\(\mathcal{C,D}\)と関手\(L:\mathcal{D} \rightarrow \mathcal{C}, R:\mathcal{C} \rightarrow \mathcal{D}\)で構成され、自然変換\(ε:LR \rightarrow I_\mathcal{C},η:I_\mathcal{D} \rightarrow RL\)を有し、counit-unit恒等式を\(I_L=εL \circ Lη, I_R=Rε \circ ηR\)を満たすというものであった。これらは図26のようになる。
同様にモナドは、圏\(\mathcal{D}\)と自己関手\(T:\mathcal{D} \rightarrow \mathcal{D}\)で構成され、自然変換\(μ:T^2 \rightarrow T,η:I_\mathcal{D} \rightarrow T\)を有し、\(μ\circ Tη=μ\circ ηT=I_T, μ\circ Tμ=μ\circμT \)を満たすであった(前の節では圏を\(\mathcal{M}\)としたが、ここでは証明の都合を考えて\(\mathcal{D}\)とする)。これらは図27のようになる。
それでは証明に移ろう。
随伴とモナドには、同じ名前の自然変換\(η\)がある。ドメインは同じだが、コドメインは、前者の方は\(RL\)であるのに対し、後者の方は\(T\)である。そこで、両者は一緒と見なすことにしよう。すなわち\(RL=T\)とする。
この関係を用いて、随伴であると仮定したときに、モナドの各条件が満たされることを示せばよい。すなわち、\(T\)を\(RL\)で置き換えることで示せばよい。
最初に、モナドの自然変換\(μ,η\)を置き換えると図28のようになる。
それではモナドの条件が満たされることを示そう。
最初に\(μ\circ Tη=I_T \)が成り立つことを示す。これは図29に示すように、随伴でのcounit-unit恒等式のストリング・ダイアグラムを用いることで、証明できる。\(μ\circ ηT=I_T \)も同様である。
最後に、\(μ\circ Tμ=μ\circμT \)が成り立つことを示す。これは図30に示すように、図の中ほどの下に、緑の山が二つほど描かれている。山の高さは計算の順序を示すが、圏の結合律から、どちらを先に計算してもよい。このため高さを入れ替えても構わないので、この性質を用いて図に示すように証明できる。
ストリング・ダイアグラムを用いることで、「随伴からモナドが導き出される」という命題をすっきりと証明することができた。
