可換モナドとラックス・モノイド・モナド（動機も少し） - 檜山正幸のキマイラ飼育記 (はてなBlog)

$\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\u}[1]{\underline{#1}} \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\In}{\text{ in } } \newcommand{\id}{\mathrm{id} } \newcommand{\Id}{\mathrm{Id} } \newcommand{\twoto}{\Rightarrow } % 必要$ 「対称モノイド圏上の可換モナドはラックス・モノイド・モナドとみなせる」という事実があります。それを聞いても「あーそうですか、それで？」なんだけど、動機があって辿り着くと「ほー、そうかそうか、ウンウン」みたいな気分になります。

動機・経緯について手短に説明して、当該の事実も簡単にメモします。

内容：

構文モナド
可換モナド
厳密2-圏内のモナド対象
ラックス・モノイド・モナドと可換モナド

構文モナド

$\cat{S}$ をインスティチューション理論の意味での指標の圏だとします。対象 $\Sigma \in |\cat{S}|$ は指標です*1。なにかしら「指標から項を生成するメカニズム」があるとします。そのメカニズムは文法／構文生成規則と言っていいかも知れません。指標 $\Sigma$ から生成された項の集合を $T(\Sigma)$ とします。

$T(\Sigma)$ は単なる集合ではなくて何らかの構造を持つかもしれません。その構造込みで $T(\Sigma) \in |\cat{S}|$ だとしましょう。 $T(-)$ は圏 $\cat{S}$ の射（指標射）にも定義できて、 $T$ は圏 $\cat{S}$ 上の自己関手になるとします。つまり：

$\quad T:\cat{S}\to \cat{S} \In {\bf CAT}$

$\cat{S}$ が大きい圏である可能性も考えて ${\bf Cat}$ （小さい圏達の2-圏）ではなくて ${\bf CAT}$ （大きいかも知れない圏達の2-圏）にしておきました。

「入れ子の項を平坦化〈展開〉する」「基本記号を項とみなす」操作があるでしょうから、それらを $\mu, \eta$ とすると、 $(T, \mu, \eta)$ は $\cat{S}$ 上のモナドになります。このモナドを、記号の乱用により次のように書きます。

$\quad T = (T, \mu, \eta)/\cat{S}$

記号の乱用が嫌なときは、モナドの台関手〈underlying functor〉に下線〈underline〉*2を引いて：

$\quad T = (\u{T}, \mu, \eta)/\cat{S}$

このように、文法／構文生成規則を表現するモナドを構文モナド〈syntax monad〉と呼ぶことにします。

指標の圏 $\cat{S}$ 上の構文モナド $T$ を使ってナニヤカニヤやろうと思うと、 $\cat{S}, T$ に要請したい性質が幾つか出てきます。それらの要請をまとめると：

$\cat{S}$ は、余デカルト・モノイド圏であるべし。
$T$ は、可換モナドであるべし。

結局（って短絡し過ぎだが）、論理における項／論理式の言語やプログラミング言語などの形式的構文構造は、余デカルト・モノイド圏上の可換モナドで記述される、ということになります。

可換モナド

余デカルト圏は直和（2点図式の余極限）と始対象（空図式の余極限）を持つ圏です。その直和／始対象が、モノイド積／単位対象として与えられる場合が余デカルト・モノイド圏〈coCartesian monoidal category〉です。モノイド積としての直和は対称〈symmetric〉な積なので、余デカルト・モノイド圏は対称モノイド圏になります。

一般的な（余デカルトとは限らない）対称モノイド圏を、記号の乱用で次のように書きます。

$\quad \cat{C} = (\cat{C}, \otimes, I, \alpha, \lambda, \rho, \sigma)$

ポピュラーな記号を使っているので、記号の意味は説明しなくても分かるでしょう。記号の乱用が嫌なときは、モノイド圏の台圏〈underlying category〉に下線を引いて：

$\quad \cat{C} = (\u{\cat{C}}, \otimes, I, \alpha, \lambda, \rho, \sigma)$

モノイド圏 $\cat{C}$ 上の自己関手 $F$ の強度〈テンソル強度 | tensorial strength〉は、次の形の自然変換です。

$\quad \mrm{ls}_{A, B}:A\otimes F(B) \to F(A\otimes B) \In \cat{C} \text{ for }A, B \in |\cat{C}|$

強度の公理を満たす必要がありますが今日は割愛します。 $\mrm{ls}$ は左強度 "left strength" のつもりで、対応する右強度 $\mrm{rs}$ は次の図式が可換になるように定義します。

$\require{AMScd} \begin{CD} F(A) \otimes B @>{\sigma_{F(A), B}}>> B \otimes F(A)\\ @V{\mrm{rs}_{A, B}}VV @VV{\mrm{ls}_{B, A}}V\\ F(A \otimes B) @>{F(\sigma_{A, B})}>> F(B\otimes A) \end{CD}\\ \text{commutative in }\cat{C}$

右強度を余強度〈costrength〉と呼ぶこともありますが、ここでは（左強度に対する）右強度と呼びます。

台関手に（上記の意味で）対称な左強度／右強度が付いたモナド $(F, \mrm{ls}, \mrm{rs}, \mu, \eta)/\cat{C}$ を考えます。左右の強度とモナドの乗法／単位が強調している（詳細省略）場合、そのようなモナドを（対称モノイド圏上の）強モナド〈strong monad〉と呼びます。

$F(A)\otimes F(B) \to F(A\otimes B)$ という変換を、左強度／右強度／モナド乗法を使って次のように定義できます。

左強度を先に使用：

$\quad \begin{CD} F(A)\otimes F(B)\\ @V{\mrm{ls}_{F(A), B}}VV\\ F(F(A)\otimes B)\\ @V{F(\mrm{rs}_{A, B})}VV\\ F(F(A\otimes B))\\ @V{\mu_{A\otimes B}}VV\\ F(A\otimes B) \end{CD}$

右強度を先に使用：

$\quad \begin{CD} F(A)\otimes F(B)\\ @V{\mrm{rs}_{A, F(B)}}VV\\ F(A\otimes F(B) )\\ @V{F(\mrm{ls}_{A, B})}VV\\ F(F(A\otimes B))\\ @V{\mu_{A\otimes B}}VV\\ F(A\otimes B) \end{CD}$

これらの2つの $F(A)\otimes F(B) \to F(A\otimes B)$ が一致するとき、強モナド $(F, \mrm{ls}, \mrm{rs}, \mu, \eta)/\cat{C}$ を、対称モノイド圏 $\cat{C}$ 上の可換モナド〈commutative monad〉と呼びます。「可換である」という性質の記述にモナド乗法を使っているので、対称な左強度／右強度を持った自己関手に対して可換性は定義できません。可換性は（台関手ではなくて）モナドに対する性質です。

厳密2-圏内のモナド対象

$\cat{K}$ を厳密2-圏とします。 ${\bf Cat},{\bf CAT}$ は厳密2-圏の例ですが、ここでは一般的な厳密2-圏 $\cat{K}$ を考えます。

$\cat{K}$ 内のモナド対象〈monad object〉とは、4つ組 $(C, t, \mu, \eta)$ で：

$C\in |\cat{K}|$
$t:C \to C \In \cat{K}$
$\mu:: t*t \twoto t : C\to C \In \cat{K}$
$\eta:: \id_C \twoto t : C\to C \In \cat{K}$

結合律／左単位律／右単位律（詳細省略）を満たすものです。ここで、アスタリスク記号 ' $*$ ' は、厳密2-圏の横結合の図式順演算子記号です。縦結合の図式順演算子記号にはセミコロン ' $;$ ' を使います。

厳密2-圏 $\cat{K}$ 内のモナド対象 $(C, t, \mu, \eta)$ は、ホム・厳密モノイド圏 $\cat{K}(C, C)$ 内のモノイド対象です。ホム・厳密モノイド圏内の解釈では：

$t \in |\cat{K}(C, C)|$
$\mu : t*t \to t \In \cat{K}(C, C)$ （横結合をモノイド積とみなす）
$\eta : I \to t \In \cat{K}(C, C) \text{ where }I = \id_C$ （恒等射をモノイド単位とみなす）

「モナドはモノイドだ」と言うのは、上記の解釈があるからです。が、「そういう解釈も出来るよ」ってだけで、モナドとモノイドが同じものではない*3ので注意してください。

${}_2\mathbb{Str2CAT}^{\mrm{lax}}$ を、厳密2-圏を対象として、ラックス2-関手を射として、ラックス2-関手のあいだの乗法／単位を保つ自然変換を2-射とする2-圏とします。2-圏からなる圏は3-圏に構成できますが、ここでは2-射までしか考えてないので左下付き添字で 2 を入れています。黒板文字を使っているのは、次が成立するような超巨大な2-圏を想定しているからです。

$\quad {\bf CAT} \in |{}_2\mathbb{Str2CAT}^{\mrm{lax}}|$

${\bf I}$ を次のような自明な2-圏だとします。

対象はひとつだけ： $|{\bf I}| = \{\hat{0}\}$ （唯一の対象は何でもいい）
射は恒等射だけ： $\hat{1} := \id_{\hat{0}}: \hat{0} \to \hat{0} \In {\bf I}$
2射は恒等射の恒等2-射だけ： $\hat{2} := \Id_{\hat{1}} = \Id_{\id_{\hat{0}}}: \hat{1} \twoto \hat{1}: \hat{0} \to \hat{0} \In {\bf I}$

${\bf I}$ は厳密2-圏なので、次が成立します。

$\quad {\bf I}\in |{}_2\mathbb{Str2CAT}^{\mrm{lax}}|$

任意の厳密2-圏 $\cat{K}$ に対して、次の射 $F$ を考えることができます。

$\quad F:{\bf I} \to \cat{K} \In {}_2\mathbb{Str2CAT}^{\mrm{lax}}$

$F$ はラックス2-関手ですから、 $F = (\u{F}, \nu, \epsilon)$ と書けます*4。4つ組 $(C, t, \mu, \eta)$ を次のように作ります。

$C := \u{F}(\hat{0}) \in |\cat{K}|$
$t := \u{F}(\hat{1}): \u{F}(\hat{0}) \to \u{F}(\hat{0}) \In \cat{K}$
$\mu := \nu_{\hat{1}, \hat{1}}:: \u{F}(\hat{1})*\u{F}(\hat{1}) \twoto \u{F}(\hat{1} * \hat{1}) : \u{F}(\hat{0}) \to \u{F}(\hat{0}) \In \cat{K}$
$\eta := \epsilon_{\u{F}(\hat{0})} : \id_{\u{F}(\hat{0})} \twoto \u{F}(\hat{1}) : \u{F}(\hat{0}) \to \u{F}(\hat{0}) \In \cat{K}$

$\hat{1} * \hat{1} = \hat{1}$ を考慮して書き換えれば：

$C := \u{F}(\hat{0}) \in |\cat{K}|$
$t := \u{F}(\hat{1}): C \to C \In \cat{K}$
$\mu := \nu_{t, t}:: t * t \twoto t : C \to C \In \cat{K}$
$\eta := \epsilon_{t} : \id_{C} \twoto t : C \to C \In \cat{K}$

$F$ がラックス2-関手であることから、 $\mu, \eta$ の結合律／左単位律／右単位律は従います。つまり、4つ組 $(C, t, \mu, \eta)$ は厳密2-圏 $\cat{K}$ 内のモナド対象です。

逆に、厳密2-圏 $\cat{K}$ 内のモナド対象があると、それから以下のようなラックス2-関手 $F$ を構成できます（詳細省略）。

$\quad F = (\u{F}, \nu, \epsilon): {\bf I} \to \cat{K} \In {}_2\mathbb{Str2CAT}^{\mrm{lax}}$

以上から、次の2つの概念は同じことです。

厳密2-圏 $\cat{K}$ 内のモナド対象
自明な厳密2-圏 ${\bf I}$ から厳密2-圏 $\cat{K}$ へのラックス2-関手

特に $\cat{K} = {\bf CAT}\,\in |{}_2\mathbb{Str2CAT}^{\mrm{lax}}|$ のときのモナド対象を単にモナドと呼ぶので、次の2つの概念は同じことです。

モナド
自明な厳密2-圏 ${\bf I}$ から厳密2-圏 ${\bf CAT}$ へのラックス2-関手

さらに特殊化すると：

集合圏 ${\bf Set}\in |{\bf CAT}|$ 上のモナド
自明な厳密2-圏 ${\bf I}$ から厳密2-圏 ${\bf CAT}$ へのラックス2-関手 $F$ であって、 $\u{F}(\hat{0}) = {\bf Set}\in |{\bf CAT}|$ であるもの。

集合圏は大きな圏ですが、さらに大きな2-圏、もっともっと大きな3-圏（の切り捨て）を考えていることに注意してください。

${\bf Set} \in |{\bf CAT}|$
${\bf CAT} \in |\mathbb{Str2CAT}|$

ラックス・モノイド・モナドと可換モナド

${\bf MonCAT}^{\mrm{lax}}$ を、モノイド圏を対象として、ラックス・モノイド関手を射として、ラックス・モノイド関手のあいだの乗法／単位を保つ自然変換〈ラックス・モノイド自然変換〉を2-射とする2-圏とします。

${\bf MonCAT}^{\mrm{lax}}$ は2-圏であり、関手／自然変換の横結合は厳密な結合演算なので厳密2-圏となります。（この厳密性は ${\bf MonCAT}^{\mrm{lax}}$ に関するものであり、 ${\bf MonCAT}^{\mrm{lax}}$ の対象であるモノイド圏が厳密だとは言ってません。）次が成立します。

$\quad {\bf MonCAT}^{\mrm{lax}} \in |{}_2\mathbb{Str2CAT}|$

よって、前節の議論が適用できて、厳密2-圏 ${\bf MonCAT}^{\mrm{lax}}$ 内のモナド対象を定義できます。モナド対象は、結合律／左単位律／右単位律を満たす4つ組としても、自明な厳密2-圏からのラックス2-関手としても定義できます（どっちで定義しても同じ）。

厳密2-圏 ${\bf MonCAT}^{\mrm{lax}}$ 内のモナド対象をラックス・モノイド・モナド〈lax monoidal monad〉と呼びます。4つ組方式の定義でくだいて言えば：

$\quad M = (\cat{C}, T, \mu, \eta)\text{ satisfies monad laws}$

$\cat{C}$ はモノイド圏である。
$T = (\u{T}, \nu, \epsilon): \cat{C} \to \cat{C} \In {\bf MonCAT}^{\mrm{lax}}$ はラックス・モノイド関手である。
$\mu :: T*T \twoto T : \cat{C} \to\cat{C} \In {\bf MonCAT}^{\mrm{lax}}$ はラックス・モノイド自然変換である。
$\eta :: \Id_{\cat{C}} \twoto T : \cat{C} \to\cat{C} \In {\bf MonCAT}^{\mrm{lax}}$ はラックス・モノイド自然変換である。
モナドの法則である結合律／左単位律／右単位律を満たす。

さて、モノイド圏 $\cat{C}$ 上の可換モナドを、ラックス・モノイド・モナドとして扱ったほうが便利なときがあります。 $T' = (\u{T'}, \mrm{ls}, \mrm{rs}, \mu', \eta')/\cat{C}$ を対称モノイド圏 $\cat{C}$ 上の可換モナドとしましょう。（ダッシュ〈プライム〉を付けているのは、記号の混乱が起きないようにです。）可換モナド $T'$ からラックス・モノイド・モナド $M$ が作れればいいわけです。

おおよそ次のように定義します。

$\u{T} := \u{T'}$ とする。
$\mu_{A, B}: \u{T}(A)\otimes \u{T}(B) \to \u{T}(A\otimes B)$ は、 $T$ の左強度／右強度／モナド乗法を組み合わせて作る。
$\epsilon: I \to \u{T}(I)$ は、 ${\eta'}_I:I \to \u{T'}(I)$ とする。
$\mu := \mu'$ とする。
$\eta := \eta'$ とする。

対称モノイド圏 $\cat{C}$ 上の可換モナド $(\u{T'}, \mrm{ls}, \mrm{rs}, \mu', \eta')$ からこうして作った $(T, \mu, \eta)$ が実際にラックス・モノイド・モナドであることを確認するにはまだやることがありますが、頑張れば確認できます。