モナドにおける「拡張」とは何なのか？ 色々と計算してみる

「再びモナドへ」にて：

過去にモナドについて僕が書いたものを読み直すと、説明不十分だったり、混乱や誤解を招きそうな記述が見つかったりもします。しかし、それらを修正する気はないです。不足な部分は新たに書き足すことにします。

計算方法を説明したので、気になるところの補足を書きます。

随分と昔、2006年に書いた「モナドの定義とか」で、「拡張（extension）」という言葉を使い、fの拡張を f^{^} という記号で表しています。Haskellなら「>>=」または「=<<」で拡張を示します。ここで言う拡張は、特定のモナドに対して定義されるので、モナドをFとして f^{^F} のように書くのがより正確でしょう。

これとはまったく別な意味の「拡張」として、「クライスリ拡張」という言葉を使ったこともあります。クライスリ拡張はクライスリ圏と同じことですが、もとの圏Cに対して、モナドFのクライスリ圏 K = Kl(C, F) が拡張圏となっていることを強調した言い方です。J:C→K を埋め込み関手として、Jにより C⊆K と見なせるのです。

さて、F = (F, η, μ) が圏C上のモナドだとして、クライスリ圏をKとして、さきほど f^{^F} と書いた「fの拡張」をExt_F(f) とも書くことにします。Ext_Fは、Ext_F:K→C という関手になります（後述）。また、埋め込み関手を J_F:C→K とします。このとき、J_F、Ext_F のこの順での結合（合成）J_F;Ext_F:C→C は、もとのモナド（の台関手）Fを再現します。

もともとクライスリ圏は、与えられたモナドFを、随伴関手対で再構成することを目的（のひとつ）としていたので、J_F -| Ext_F :C←→K は随伴になるように作られているのです。よって、Ext_FとモナドFとの関係は、随伴の右側関手と対応するモナドとの関係となります。

これらの事情を理解するには、具体的な定義と計算をワシャワシャとやってみるのが一番だと思います。考察は後回しにして、今日は計算だけしてみます。

モナドの定義

(F, η, μ) がC上のモナドだとは、

1. F:C→C
2. η::I⇒F:C→C （I = Id_C）
3. μ::FF⇒F:C→C
4. ηF;μ = F、 Fη;μ = F （単位律）
5. μF;μ = Fμ;μ （結合律）

モナドは、非対称モノイド圏End(C)内のモノイドだ、って立場ですね。

モナドの単位律（2つ）と結合律を、「僕は嫌いなのだが、バイダイレクショナルな自然変換計算はこうする」で説明した記法を使って具体化しておきます。Cの対象Aに対する成分表示を書き下してみましょう。

等式 ηF;μ = F 
---------------- 
  左辺のA成分
= (ηF;μ)[A]
= (ηF)[A];μ[A]
= η[F(A)];μ[A]
  右辺のA成分
= F[A]
= id[F(A)]
  よって、
η[F(A)];μ[A] = id[F(A)]


等式 Fη;μ = F
---------------- 
  左辺のA成分
= (Fη;μ)[A] 
= (Fη)[A];μ[A] 
= F(η[A]);μ[A] 
  右辺のA成分
  F[A]
= id[F(A)]
  よって、
F(η[A]);μ[A] = id[F(A)] 


等式 μF;μ = Fμ;μ
--------------------
  左辺のA成分
= (μF;μ)[A]
= (μF)[A];μ[A]
= μ[F(A)];μ[A]
  右辺のA成分
= (Fμ;μ)[A]
= (Fμ)[A];μ[A]
= F(μ[A]);μ[A]
  よって、
μ[F(A)];μ[A] = F(μ[A]);μ[A] 

次の等式が得られました。

1. η[F(A)];μ[A] = id[F(A)]
2. F(η[A]);μ[A] = id[F(A)]
3. μ[F(A)];μ[A] = F(μ[A]);μ[A]

クライスリ圏

モナド F = (F, η, μ) に対して、そのクライスリ圏 K = Kl(C, F) は次のように定義します。

1. 対象類 |K| = |C|
2. ホムセット K(A, B) = C(A, F(B))
3. 恒等射 kid_A = η_A
4. 射の結合 f∈K(A, B)、g∈K(B, C) に対して、f#g := f;F(g);μ_C

クライスリ圏Kは、もとの圏Cの部分圏ではありません。しかし、Obj(K) = Obj(C) だし、Mor(K)⊆Mor(C) なので、Kの素材は全部Cのなかに入っています。これが混乱の原因になります。次の点に注意しましょう。

1. Kの対象は、Cの対象と同じである。
2. Kの射は、Cの射である。
3. しかし、Kの恒等射はCの恒等射ではなく、射の結合も異なる。
4. したがって、Mor(K)⊆Mor(C) という包含が関手となるわけではない。
5. 素材を共有していても、KとCは別な圏と考えなくてはならない。

別な圏であることを強調するために、Kの恒等射は kid_A、Kの結合は f#g と別な記号を割り当ててあります。

Kが実際に圏であるためには、f:A→F(B)、g:B→F(C)、h:C→F(D) に対して、

1. kid_A#f = f : A→F(B)
2. f#kid_B = f : A→F(B)
3. (f#g)#h = f#(g#h) : A→F(D)

が成立する必要があります。計算で確認しましょう。最初に、ηとμが自然変換である事実を書き並べておきます、これ、忘れがちなので。

クライスリ射 f:A→F(B) in C に対して、

• η[A];F(f) = f;η[F(B)]
• FF(f);μ[F(B)] = μ[A];F(f)

では、実際の計算です。「//」はコメントで、次の行に移る根拠を示しています。

  kid[A]#f // kid[A]の定義
= η[A]#f  // # の定義
= η[A];F(f);μ[B] // f:A→F(B)に対するηの自然性
= f;η[F(B)];μ[B] // モナドの単位律
= f;id[F(B)] // idの性質
= f
  よって、
kid[A]#f = f

  f#kid[B]   // kid[B] の定義
= f#η[B]    // #の定義
= f;F(η[B]);μ[B] // モナドの単位律
= f:id[F(B)] // idの性質
= f
  よって、
f#kid[A] = f

  (f#g)#h  // #の定義
= (f;F(g);μ[C])#h  // #の定義
= (f;F(g);μ[C]);F(h);μ[D] // 括弧を外す（結合律）
= f;F(g);μ[C];F(h);μ[D]

  f#(g#h) // #の定義
= f#(g;F(h);μ[D]) // #の定義
= f;F((g;F(h);μ[D]));μ[D]   // Fは関手
= f;F(g);FF(h);F(μ[D]);μ[D] // モナドの結合律
= f;F(g);FF(h);μ[F(D)];μ[D] // h:C→F(D)に対するμの自然性
= 
  よって、
(f#g)#h = f#(g#h)

埋め込み関手

埋め込み関手 J:C→K を、J(f) = f;η_B で定義します。f:A→B in C に対して、J(f):A→F(B) in C ですが、K で考えれば、J(f):A→B in K となります。Jが関手であるためには、

1. J(id_A) = kid_J(A)
2. J(f;g) = J(f)#J(g)

が必要です。また計算します。

  J(id[A])    // Jの定義
= id[A];η[A] // idの性質
= η[A]       // kidの定義
= kid[A]      // J(A) = A
= kid[J(A)]
  よって、
J(id[A]) = kid[J(A)]

  J(f;g)       // Jの定義
= (f;g);η[C]  // 括弧を外す（結合律）
= f;g;η[C]

  J(f)#J(g)           // J の定義
= (f;η[B])#(g;η[C]) // # の定義
= f;η[B];F(g;η[C]);μ[C]    // Fは関手
= f;η[B];F(g);F(η[C]);μ[C] // モナドの単位律
= f;η[B];F(g);id[F(C)]       // idの性質
= f;η[B];F(g)        // g:B→F(C)に対するηの自然性
= f;(g;η[C])         // 括弧を外す（結合律）
= f;g;η[C]
  よって、
J(f;g) = J(f)#J(g)

拡張関手

拡張関手 Ext:K→C を、f:A→B in K を f:A→F(B) in C と見た上で、Ext(f) = F(f);μ[B] と定義します。対象Aに対して、Ext(A) = F(A) であることに注意してください。
Extが関手であるためには、

1. Ext(kid_A) = id_Ext(A)
2. Ext(f#g) = Ext(f);Ext(g)

が必要です。もちろん計算します。

  Ext(kid[A])  // kidの定義
= Ext(η[A])   // Extの定義
= F(η[A]);μ[A] // モナドの単位律
= id[F(A)]     // F(A) = Ext(A)
= id[Ext(A)]
  よって、
Ext(kid[A]) = id[Ext(A)]

  Ext(f#g)          // #の定義
= Ext(f;F(g);μ[C]) // Extの定義
= F(f;F(g);μ[C]));μ[C]    // Fは関手
= F(f);FF(g);μ[F(C)];μ[C] // g:B→F(C)に対するμの自然性
= F(f);μ[B];F(g);μ[C]

  Ext(f);Ext(g) // Extの定義
= (F(f);μ[B]);(F(g);μ[C]) // 括弧を外す（結合律）
= F(f);μ[B];F(g);μ[C]
  よって、
Ext(f#g) = Ext(f);Ext(g)

JとExtからFを再現

J -| Ext と随伴なんですが、とりあえず、ExtJ = J;Ext= F となることだけ確認しておきます。

  Ext(J(A)) // J(A) = A
= Ext(A)    // Ext(A) = F(A)
= F(A)
  よって、
Ext(J(A)) = F(A)

  Ext(J(f)) // Extの定義
= F(J(f));μ[B]    // Jの定義
= F(f;η[B]);μ[B] // Fは関手
= F(f);F(η[B]);μ[B] // モナドの単位律
= F(f);id[F(B)]    // idの性質
= F(f)
  よって、
Ext(J(f)) = F(f)

疲れた

計算は疲れますね。慣れないと時間もかかります。でも、やることは等式的変形だけですから、律儀に頑張れば必ずできます。「律儀に頑張る」は、僕の価値観に著しく反するのですが、まー、しょうがない。