このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

ベックの分配法則、ベック分配系、複合モナド

ベックの分配法則の事例と計算法」で、ベックの分配法則〈Beck's distributive law〉の話をしたのですが、分配法則はひとつの代数的構造とみなすのがいいと思うんですよ。「法則」という呼び名が、構造とみなすことへの違和感となるので、呼び名と記号法を少し変えて論じてみます。

この記事の内容は、次の論文の第4節"Modules"に書いてあることです。

内容:

ベック分配系

Cを圏として、MとAがC上のモナドのとき、ベックの分配法則δを考えることができます。が、何を指して分配法則と呼ぶのでしょうか? 自然変換 δ::A*M⇒M*A:CC そのものでしょうか? それとも、MとAとδをまとめたものでしょうか? 用例を見てもあまりハッキリしません。

ここでは、自然変換δを分配法則と呼び、MとAとδが作る構造のほうはベック分配系と呼ぶことにします。モナドがモノイド類似物とするなら、ベック分配系は半環類似物です。

ベック分配系をハッキリ定義しましょう。M = (M, η, μ) on C, A = (A, ζ, α) on C を2つのモナドとします。自然変換 δ::A*M⇒M*A:CC ('*'は関手の図式順結合記号)はベックの分配法則の公理を満たすとします。このとき、(M, A, δ) がベック分配系Beck's distributive system〉です。

MとAは、半環の掛け算部分と足し算部分に相当するので、Mをベック分配系の乗法的モナド〈multicative monad〉、Aをベック分配系の加法的モナド〈additive monad〉と呼ぶことにします。それに伴い、ベック分配系の構成素を次のように呼びます:

  • ηはベック分配系の単位〈unit〉
  • μはベック分配系の乗法〈multiplication〉
  • ζはベック分配系の〈zero〉
  • αはベック分配系の加法〈addition〉
  • δはベック分配系の分配法則〈distributive law〉(=ベックの分配法則)

零は加法的モナドモナド単位で、加法は加法的モナドモナド乗法です。

C上のベック分配系 (M, A, δ) on C に対して、そのアイレンベルク/ムーア代数を定義しましょう。Cの対象Vと、射 m:M(V)→V, a:A(V)→V の組 (V, m, a) in C が次の条件を満たすとき、ベック分配系 (M, A, δ) のアイレンベルク/ムーア代数〈Eilenberg-Moore algebra〉と呼びます。

  1. (V, m) は、モナドMのアイレンベルク/ムーア代数である。
  2. (V, a) は、モナドAのアイレンベルク/ムーア代数である。
  3. M(a);m = δV;A(m);a : M(A(V))→V が成立する。

ここで、セミコロン';'はCの射の図式順結合記号です。3番目の等式を、完全に図式順記法で書けば: a.M;m = V.δ;m.A;a : V.A*M→V です。ドット'.'は関手/自然変換の対象への適用、アスタリスク'*'は関手の結合です。これを絵で描けば:

ここで、絵(ストリング図)の見方を注意しておきます; 描画の方向は、↓方向が射の結合/自然変換の縦結合の方向、→方向が関手の結合/自然変換の横結合の方向です。何も書いてない背景領域は圏Cを表します。ただし、VはCの対象なので、Vの左側は自明な圏☆(ひとつの対象と恒等射のみ)だと解釈します(下図)。

これは対象・射の格上げですが、格上げについては次の記事を参照してください。

さて、2つの代数 (V, m, a) と (W, m', a') のあいだの準同型射とは、台対象のあいだの射 f:V→W in C であって、次の条件を満たすものです。

  1. fは、モナドMのアイレンベルク/ムーア代数射(EM(C, M) の射)である。
  2. fは、モナドAのアイレンベルク/ムーア代数射(EM(C, A) の射)である。

ベック分配系 (M, A, δ) のアイレンベルク/ムーア代数とそのあいだの準同型射は圏をなすので、この圏を (M, A, δ) のアイレンベルク/ムーア圏〈Eilenberg-Moore category〉と呼びます。ベック分配系 (M, A, δ) のアイレンベルク/ムーア圏を EM(C, (M, A, δ)) または C(M, A, δ) と書きます。

ベック分配系は半環と似てますが、そのアイレンベルク/ムーア代数がいつも半環になるとは言ってません。例えば、「ベックの分配法則の事例と計算法」で述べた (List, Maybe, δMaybe,List) はベック分配系ですが、そのアイレンベルク/ムーア代数は零〈吸収元〉付きのモノイドです。

ベック分配系と複合モナド

分配法則 δ::A*M⇒M*A:CC があれば、MとAの複合モナドが作れます。複合モナドの台関手は M*A であり、δにより複合されているので、(M*A)δ または M*δA と書くことにします(反図式順結合記号を使って A\circδM がよく使われるようです)。

複合モナド (M*A)δ の単位と乗法を ε, ν〈ニュー〉 とすると:

  • ε := η*ζ :: IdC⇒M*A:CC
  • ν := (M*δ*A);(μ*α) :: (M*A)*(M*A)⇒M*A:CC

アスタリスク'*'は関手の結合以外に、自然変換の横結合、関手と自然変換のヒゲ結合の意味でも使います。ε, ν〈ニュー〉 の定義を絵で描けば:

複合モナド (M*A)δアイレンベルク/ムーア圏 C(M*A)δ と、ベック分配系 (M, A, δ) のアイレンベルク/ムーア圏 C(M, A, δ) は同型(同値より強い)になります。複合モナドとベック分配系は、そのアイレンベルク/ムーア圏で見ると区別が付かないので、ある観点からは同じものなのです。ここから先で、そのことを示します。互いに逆になる関手対 Φ:C(M*A)δC(M, A, δ) in CAT と Ψ:C(M, A, δ)C(M*A)δ in CAT を構成します。

C(M*A)δ の対象も、C(M, A, δ) の対象も、どちらもアイレンベルク/ムーア代数です。この呼び名だと区別が付かないで混乱するので、モナドアイレンベルク/ムーア代数は1演算代数〈1-operator algebra〉、ベック分配系のアイレンベルク/ムーア代数は2演算分配代数〈2-operator distributive algebra〉と呼び分けることにします。

  • モナドアイレンベルク/ムーア代数は、演算をひとつ持つ。よって、1演算代数
  • ベック分配系のアイレンベルク/ムーア代数は、演算をふたつ持ち、それらは分配法則で関連している。よって、2演算分配代数

複合モナドの1演算代数の圏 C(M*A)δ と、ベック分配系の2演算分配代数の圏 C(M, A, δ) が同型であることを示すためにやるべき作業を並べてみます(証明のプランニングです)。

  1. 複合モナド (M*A)δ の1演算代数 (V, v) in C(M*A)δ に対して、Φ(V, v) = Φ((V, v)) を定義する。
  2. Φ(V, v) が、ベック分配系 (M, A, δ) の2演算分配代数(C(M, A, δ) の対象)であることを示す。
  3. 2つの1演算代数のあいだの準同型射 ψ:(V, v)→(W, w) in C(M*A)δ に対して、Φ(ψ) を定義する。
  4. Φ(ψ) が、2つの2演算分配代数 Φ(V, v) と Φ(W, w) のあいだの準同型射であることを示す。
  5. Φが関手であること(結合と恒等の保存)を示す。
  6. ベック分配系 (M, A, δ) の2演算分配代数 (V, m, a) in C(M, A, δ) に対して、Ψ(V, m, a) = Ψ((V, m, a)) を定義する。
  7. Ψ(V, m, a) が、複合モナド (M*A)δ の1演算代数(C(M*A)δ の対象)であることを示す。
  8. 2つの2演算分配代数のあいだの準同型射 φ:(V, m, a)→(W, m', a') in C(M, A, δ) に対して、Ψ(φ) を定義する。
  9. Ψ(φ) が、2つの1演算代数 Ψ(V, m, a) と Ψ(W, m', a') のあいだの準同型射であることを示す。
  10. Ψが関手であること(結合と恒等の保存)を示す。
  11. 1演算代数 (V, v) in C(M*A)δ に対して、Ψ(Φ(V, v)) = (V, v) であることを示す。
  12. 1演算代数のあいだの準同型射 ψ:(V, v)→(W, w) in C(M*A)δ に対して、Ψ(Φ(ψ)) = ψ であることを示す。
  13. 2演算分配代数 (V, m, a) in C(M, A, δ) に対して、Φ(Ψ(V, m, a)) = (V, m, a) であることを示す。
  14. 2演算分配代数のあいだの準同型射 φ:(V, m, a)→(W, m', a') in C(M, A, δ) に対して、Φ(Ψ(φ)) = φ であることを示す。

ほとんど自明なこともあるので、目ぼしい項目だけをピックアップしてやってみます。具体的には:

  • 1と2を合わせて、1演算代数から2演算分配代数の構成。
  • 6と7を合わせて、2演算分配代数から1演算代数の構成。
  • 11の、1演算代数→2演算分配代数→1演算代数 とラウンドトリップして戻ること。
  • 13の、2演算分配代数→1演算代数→2演算分配代数 とラウンドトリップして戻ること。

アイレンベルク/ムーア圏の同型性証明の目ぼしいところ

基本的に、絵(ストリング図)で計算します。テキストで書くときは、次の結合記号を使います。主に図式順記法を使います。

図式順横結合/ヒゲ結合 * (アスタリスク
図式順縦結合 ; (セミコロン)
図式順適用 . (ドット)
反図式順横結合/ヒゲ結合 ・ (ナカグロ)
反図式順縦結合 \circ (サークル)
反図式順適用 () (丸括弧)
恒等 (-)^ (右肩にハット)
1演算代数から2演算分配代数の構成

(M*A)δ の1演算代数 (V, v) に対して、(V, m, a) = Φ(V, v) と置きます。このとき:

  • m := V.M.ζ;v
  • a := V.η.A;v

と定義します。絵で描けば:

ここで、三角形(赤と青)はモナド単位を表します。また、モナド乗法(ベック分配系の“加法”も)赤/青の丸印で示すことにします。

示すべき等式は:

  1. [mの結合律] V.μ;m = m.M;m
  2. [mの単位律] V.η;m = V^
  3. [aの結合律] V.α;a = a.M;a
  4. [aの単位律] V.ζ;m = V^
  5. [mのaに対する分配律] m.A;a = V.δ:a

右肩の'^'は恒等射を示します(V^ = idV)。これらの等式を絵で描けば:


上の4つは簡単なので、5番目の[mのaに対する分配律]だけを示します。

最初に次の事実[ア]に注意しておきます。

等式で書けば:

  • [ア] ζ+η;μ*α = (M*A)^ :::M*A⇒M*A::CC

次の補題[イ]を準備します。

  • [イ] m.A;a = v

この補題の証明は、次の絵の変形(絵等式)です。

変形の各ステップを簡略に説明します。

  1. mとaの定義
  2. モナド単位の位置をずらす(交替律による)
  3. vの結合律とν〈ニュー〉の定義
  4. 事実[ア]
  5. ラベルをM*Aに付け替えただけ(あまり意味はない)。

補題[イ]を使うと、次のような絵の変形ができます。


  1. aとmの定義
  2. モナド単位の位置をずらす(交替律による)
  3. vの結合律とν〈ニュー〉の定義
  4. 補題[イ]
  5. モナド単位を消す(単位律による)
2演算分配代数から1演算代数の構成

(M, A, δ) の2演算分配代数 (V, m, a) に対して、(V, v) = Ψ(V, m, a) と置きます。このとき:

  • [ウ] v := m.A;a

すぐ前の補題[イ]にこの等式が出てきましたが、今度は定義です。絵で描けば:

複合モナドの単位と乗法は ε, ν として、示すべき等式は:

  1. [vの結合律] V.ν;v = v.(M*A);v
  2. [vの単位律] V.ε;ν = V^

絵で描けば:

単位律は簡単なので、結合律だけ示します。


  1. vの定義
  2. aの結合律
  3. mの結合律
  4. mのaに対する分配律
  5. vの定義
1演算代数→2演算分配代数→1演算代数

先に述べた 1演算代数→2演算分配代数 の構成と 2演算分配代数→1演算代数 の構成をこの順で実行すると元に戻ることを示します。詳細は述べませんが、次の絵をヒントにすれば難しくはありません。


2演算分配代数→1演算代数→2演算分配代数

今度は、2演算分配代数→1演算代数 の後に 1演算代数→2演算分配代数 という順で構成すると元に戻ることを示します。容易です。

おわりに

目ぼしいところだけの記述でしたが、複合モナドの1演算代数の圏 C(M*A)δ と、ベック分配系の2演算分配代数の圏 C(M, A, δ) が同型であることが分かりました。

モナド、複合モナド、ベック分配系などは、圏上の代数系とみなせます。アイレンベルク/ムーア圏は、これらの代数系の“不変量”になります。不変量であるアイレンベルク/ムーア圏(あるいはクライスリ圏)を通じてモナド類似物の性質を調べる際に、 C(M*A)δ \stackrel{\sim}{=} C(M, A, δ) は基本的な事実です。