随伴系〈adjunction | adjoint system〉があるとモナドを作れます。逆に、モナドを随伴系に分解〈resolution〉して調べたいことがあります。となると、ある特定のモナドに対して、随伴系への分解はどのくらいあるのだろう? と知りたくなるのが人情です。
モナドの随伴系への分解の全体は圏をなすので、その圏の構造を知りたい、ってことですね。これに関しては、ベック〈Jon Beck〉達による結果がありますが、名前がないみたいなので*1、とりあえず「モナドの分解の比較定理」と呼んでおきます。
モナドの分解の比較定理を大雑把に述べます。僕は、この比較定理が重要であることは知ってますが、よくわかってないです。最近(昨日だけど)使いたい気がしたので、わかる部分だけ書きます。
内容:
モナドの随伴系への分解
T = (T, μ, η)/C (記号の乱用)をC上のモナドだとします。T = T/C という略記〈乱用〉も使うことにします。
随伴系の書き方は毎度悩むのですが(「随伴系の書き方」「随伴に関する注意事項」参照)、以下の図の状況を (F -| G, η, ε)/(C, D) と書くことにします。
ドット&アロー図+随伴記号:
ストリング図(のつもり):
典型的事例は、F:C → D in CAT が自由生成関手、G:D → C in CAT が忘却関手のときです。
モナド T/C が、随伴系 (F -| G, η, ε)/(C, D) から得られるとき、逆に考えて、モナド T/C は随伴系 (F -| G, η, ε)/(C, D) に分解される、あるいは随伴系への分解〈adjunction resolution〉であると呼びます。
モナド T/C を固定したとき、Tの随伴系への分解の全体を Resol(T) = Resol(T/C) とします。Resol(T/C) がどんな圏かと言うと:
- Resol(T/C) の対象は、Tの分解である随伴系 (F -| G, η, ε)/(C, D) 。
- (F -| G, η, ε)/(C, D) と (F' -| G', η', ε')/(C, D') が2つの“Tの分解”だとして、そのあいだの射は、関手 H:D → D' in CAT であって、以下の図式を部分的に可換にする(下側の等式が成立する)もの。
要求される等式を、関手のプレ結合引き戻しとポスト結合前送りで書けば次のようです。
圏 Resol(T/C) が空ではないことは、Tのクライスリ圏 Kl(T) と IdKl(T):Kl(T) → Kl(T) in CAT があることから分かります。が、もう少し詳しい情報が知りたいわけです。
クライスリ圏とアイレンベルク/ムーア圏
モナドTの随伴系への分解として、クライスリ圏とアイレンベルク/ムーア圏があります。
クライスリ圏による分解:
アイレンベルク/ムーア圏による分解:
分解を構成している随伴系の関手対は次のものです。
- クライスリ圏による分解の左関手 JT: モナドの基礎圏Cを、対象上では恒等〈identity-on-objects〉でクライスリ圏に埋め込む関手
- クライスリ圏による分解の右関手 KExT: クライスリ射をC内でクライスリ拡張する関手
- アイレンベルク/ムーア圏による分解の左関手 FreeT: モナドの自由アイレンベルク/ムーア代数を作る自由生成関手
- アイレンベルク/ムーア圏による分解の右関手 UT: モナドのアイレンベルク/ムーア代数の台対象を対応させる忘却関手
クライスリ圏による分解(以下、クライスリ分解〈Kleisli resolution〉とアイレンベルク/ムーア圏による分解(以下、アイレンベルク/ムーア分解〈Eilenberg-Moore resolution〉)は、何か特殊な地位を占めている印象がありますが、モナドTの分解の圏 Resol(T) のなかで、ぞれぞれ始対象、終対象になっています。実を言うと、僕は詳細を詰めてないので実感が湧かないですが、まー、ほんとの事でしょう。
雰囲気的に言えば、クライスリ分解が一番小さな分解で、アイレンベルク/ムーア分解が一番大きな分解ということになります。
比較関手ペア
クライスリ分解が最小の分解、アイレンベルク/ムーア分解が最大の分解だとすれば、どんな分解でもクライスリ分解とアイレンベルク/ムーア分解のあいだに入るわけです。このことをもっとハッキリと言うと、次のような関手 L, K があることです。関手の随伴対を両矢印で略記します。
上の図に現れる、分解のあいだの射(圏 Resol(T) の射) L, K を比較関手〈comparison functor〉と呼びます。単なる関手ではなくて、Resol(T) の射ですけどね。Resol(T) の射を“比較関手”と呼ぶのだ思えばいいでしょう。
比較関手 L は、当該の分解がクライスリ分解よりどのくらい“大きいか”を表し、比較関手 K は、当該の分解がアイレンベルク/ムーア分解よりどのくらい“小さいか”を表しています。なので、L を下側比較関手〈lower comparison functor〉、K を上側比較関手〈upper comparison funcor〉*2、ペア (L, K) を比較関手ペア〈comparison functor pair〉と呼ぶことにします。
モナド T/C の分解(である随伴系)(F -| G, η, ε)/(C, D) が与えられたとき、下側比較関手 L 、上側比較関手 K が具体的にどう定義されるかを次節で述べます。
比較関手の構成
モナド T = T/C の分解 (F -| G, η, ε)/(C, D) に対する下側比較関手 L は、分解の圏 Resol(T) の始射(始対象からの唯一の射)ということになります。L:Kl(T) → D in CAT を具体的に与えましょう。
- For X∈|Kl(T)|, L(X) := F(X) in D
- For f:X → T(Y) in C
L(f) := F(f);εF(X) in D
ここで、T = F*G = G・F ('*', '・' は図式順と反図式順の結合記号)を使っています。二番目の、射に対する定義は、完全に図式順で書いたほうが分かりやすいでしょう('.' は図式順の適用記号)。ストリング図が一番分かりやすいので描いてみてください。
- f.L := f.F ; (Y.F).ε : X.F → Y.F in D
L はホムセットごとに全単射〈双射〉になります。g:F(X) → F(Y) に対して、次の射(を対応させる写像)がホムセットごとの逆写像を与えます。
- ηF(X);T(g)
(f F(f);εF(X)) と (g ηF(X);T(g)) が互いに逆であることは、随伴系のニョロニョロ等式〈snake {equation | relation}〉から分かります。
次に、上側比較関手 K:D → EM(T) を構成しましょう。上側比較関手は、圏 Resol(T) における終射(終対象への唯一の射)と言ってもいい(はず)です。
EM(T) の対象はアイレンベルク/ムーア代数なので、それを A = (A, αA) in EM(T) と書くことにします。代数構造とその台対象(Cの対象)は区別します。ここで区別しない(記号の乱用をする)とワケワカランことになります。
K:D → EM(T) in CAT の具体的な定義は:
- For X∈|D|, K(X) := (G(X), G(εX)) in EM(T)
- For f:X → Y in D
K(f) := G(f) : G(X) → G(Y) in C
このままだと、Kの射パートが in EM(T) とはなってません。G(f) in EM(T) と言えるためには、G(f):G(X) → G(Y) in C がアイレンベルク/ムーア代数 K(X) から K(Y) への代数射(アイレンベルク/ムーア圏の射)であることを示す必要があります。その示すべき条件は次の可換図式です。
関手 K の定義から、アイレンベルク/ムーア代数の代数演算は随伴の余単位 ε を使って書けるのでした。
この状況を使えば、G(f) : (G(X), αG(X) → (G(Y), αG(Y) in EM(T) が言えるので、K は確かに D → EM(T) in CAT だと分かります(ストリング図で計算しましょう)。
モナドの分解の比較定理
前節で状況設定〈セットアップ〉ができました。モナドの分解の比較定理が何を主張しているかと言うと、次のようなことです。
- 任意のTの分解に対して、下側比較関手 L は一意的に決まる。
- 任意のTの分解に対して、上側比較関手 K は一意的に決まる。
- 下側比較関手 L は充満忠実関手である。
- 圏Dが、反射的ペア〈反映的ペア | reflexive pair〉の余等値核〈coequaliser〉を持つなら、上側比較関手 K は左随伴関手(随伴系の左関手)を持つ。
「よくわかってない」「実感が湧かない」と言ったのは、上記の主張をちゃんと確認してないからです。
比較定理の延長線に、ベックのモナド性定理〈Beck's monadicity theorem〉があります。これは、上側比較関手 K:D → EM(T) がどんなときに圏同値になるかを述べたものです。別な言い方をすると、分解に現れた圏 D の対象をアイレンベルク/ムーア代数だと思ってよい条件を与えていることになります。
比較定理もモナド性定理も、モナドを扱う上での基本定理なんですが、昨日まで必要性をしみじみと感じることもなかったので「よくわかってない」「実感が湧かない」のです -- しばらく、モナドの随伴系への分解をいじってみることにします。