最近のモナド論の概観と注意事項 2/2

「最近のモナド論の概観と注意事項 1/2」の続きです。前回記事で導入した言葉や記号は、この記事でも使います。

内容：

ところで、なんでモナド？

昨年（2018年）の9月に「モナドはモノイドだが、モノイドじゃない」という記事を書きました。そのなかで：

2,3日前からn（不明）回目のマイ・モナドブームです。今回のブームのテーマは、「2-圏論からモナドを考える」です。キャッチフレーズは「モナドはモノイドじゃない」かな。

このブームは、諸般の事情で盛り上がることはありませんでした。が、くすぶり続けてはいて、昨年の年末になって「気になっていたことを調べよう」となったわけです。

僕がモナドに興味を持つ主たる理由は、プログラム構文論・意味論を記述する手段としてです。プログラム構文論・意味論では、さまざまな場面で、さまざまな形で、モナドまたはモナド類似物〈monad-like entity〉がたびたび登場します。

そのテの事例を僕はある程度は知っているのですが、事例に出会うたびに泥縄式にゴニョゴニョ調べているわけで、どうも系統的に理解している気がしない。なので、高次圏を使ったフォーミュレーションから、包括的に把握したいな、と思うのですよ。

現状では、高次圏ベースのモナド論のサワリを理解しただけです。それでも、チラリと見えた景観と、自分が戸惑ったところを（主に自分のために）記録しておきます。

モナド論の主題：モナドと随伴系

モナド論の主題は、モナド〈monad〉と随伴系〈adjunction | adjoint system〉だと言っていいでしょう。モナドの全体をMnd、随伴系の全体をAdjと書きます。今言った「…の全体」は曖昧で雰囲気的ですが、とりあえずはモンヤリとした話をします。

随伴系からモナドが作られることはよく知られています。随伴系からモナドを作る構成を mnd:Adj→Mnd とします。逆に「モナドを随伴系に分解〈factorize〉できるか？」という問題があります。この問題の解（分解）の存在は、一般的には保証されませんが、古典的非形式論（つまり、CatやCATでの議論）では解が存在します。しかし、一意的ではありません。典型的な解（分解）としては、アイレンベルク／ムーア構成〈Eilenberg-Moore construction〉とクライスリ構成〈Kleisli construction〉があります。これらを（存在すると仮定して）、emadj:Mnd→Adj, kladj:Mnd→Adj とします。

今、非常に曖昧に述べた Mnd, Adj, mnd, emadj, kladj を細部までキッチリと定義して、その相互関係を調べることが“モナドの基本理論”でやるべきことです。

形式モナド論では、モナドと随伴系が棲む場所として、抽象的な厳密2-圏Kを想定します。Mnd, Adj は、厳密2-圏Kをパラメータにして、

• Mnd(K) ： K内のモナドの全体
• Adj(K) ： K内の随伴系の全体

となります。パラメータKは、mnd, emadj, kladj にも付くので：

• mnd_K:Adj(K)→Mnd(K)
• emadj_K:Mnd(K)→Adj(K)
• kladj_K:Mnd(K)→Adj(K)

mnd_Kは任意の厳密2-圏Kに対して定義可能ですが、emadj_K, kladj_K が存在する（定義できる）ことは保証されません。厳密2-圏Kが、emadj_Kを持つとき、アイレンベルク／ムーア構成を許容する〈admitting Eilenberg-Moore construction〉と言います。同様に、kladj_Kを持つならクライスリ構成を許容する〈admitting Kleisli construction〉と言います。

アイレンベルク／ムーア構成とクライスリ構成は、厳密2-圏論のなかで形式的に定義できるので、「アイレンベルク／クライスリ構成を許す／クライスリ構成を許す」は厳密2-圏が持つ性質とみなせます。つまり、次のような単項述語 admitsEilenberg-MooreConstruction, admitsKleisliConstruction が定義できます。

• For K in s2-Cat_#r, admitsEilenberg-MooreConstruction(K) := ナニヤラカニヤラ
• For K in s2-Cat_#r, admitsKleisliConstruction(K) := ナニヤラカニヤラ

s2-Cat_#rは3-圏ですが、admitsEilenberg-MooreConstruction(K) である対象Kの全体 ｛K∈Obj(s2-Cat_#r) | admitsEilenberg-MooreConstruction(K)｝を対象集合にして、充満部分3-圏を作れるので、それを s2-Cat_EM#r と書きます。同様に、クライスリ構成を許容する厳密2-圏からなる3-圏は s2-Cat_Kl#r と書きます。

K in s2-Cat_EM#r ならば、emadj_K:Mnd(K)→Adj(K) を使ってよく、K in s2-Cat_Kl#r ならば、kladj_K:Mnd(K)→Adj(K) を使っていいわけです。K in s2-Cat_EM-Kl#r = s2-Cat_EM#r∩s2-Cat_Kl#r ならば、K内で古典的非形式論のかなり部分を再現できます。

色々な厳密2-圏内のモナドと随伴系

モナドの全体と随伴系の全体は、厳密2-圏Kをパラメータにして、Mnd(K), Adj(K) と書くのでした。圏の圏Catは、自然変換まで考えれば厳密2-圏（Cat in s2-CAT）なので、K = Cat として、Mnd(Cat), Adj(Cat) を考えることができます。これは、非形式大域モナド論となります。

集合圏Setは、モナドの台圏〈基礎圏〉としてよく使われます。Set in Cat ではなく、Set in CAT（CAT = Cat_#1）なので、(Set = 0-Cat_#0) in (CAT = 1-Cat_#1) in s2-Cat_#2 という系列のなかで考えることになります。Mnd(CAT), Adj(CAT) を扱う非形式大域モナド論のなかで、Set in CAT を台圏として固定した局所モナド論が、Set上のモナド論になります。もちろん、Set特有の性質を使って、一般論だけでは無理な細かい議論が出来ます。

厳密2圏は、CatやCAT以外にも色々あります。「モナド論をヒントに圏論をする（弱2-圏の割と詳しい説明付き） // 2-圏の例 10選」で10個の例を挙げてあります（非厳密2-圏も含まれます）。いくつかの厳密2-圏に関して、Mnd(K)とAdj(K)を考えてみます。Mnd(K)もAdj(K)も、高次の圏的構造〈higher categorical structure〉を持ちます（持たせることが出来ます）が、その対象部分（₀Mnd(K), ₀Adj(K) と書く）だけを述べます。

順序集合の圏 Ord

厳密2-圏としてのOrdに関しては、「モナド論をヒントに圏論をする（弱2-圏の割と詳しい説明付き） // 2-圏の例 10選」を見てください。

Aが順序集合、f:A→A が自己単調写像で、f;f≦f, id_A≦f を満たすとき（順序に関する）閉包作用素〈closure operator〉と呼びます（位相に関する閉包作用素とは違います）。(A, f, f;f≦f, id_A≦f) はOrd内のモナドになるので：

• ₀Mnd(Ord) = (閉包作用素の全体)

Ord内の随伴系がガロア接続〈Galois connection〉であることはよく知られています。

• ₀Adj(Ord) = (ガロア接続の全体)

Ord内のモナド／随伴系に関することは次の記事にも書いてあります。

• 順序集合の上でモナドなど
• 3Dでニョロニョロしたい： 随伴・双対・ガロア接続
• 順序随伴性： ガロア接続の圏論
• 記法バイアスと記法独立な把握： 順序随伴を例として

関係の圏 Rel

厳密2-圏としてのRelに関しては、「モナド論をヒントに圏論をする（弱2-圏の割と詳しい説明付き） // 2-圏の例 10選」を見てください。

Aが集合、R:A→A がA上の（二項）関係で、R;R⊆R, Δ_A⊆R （Δ_A := {(x, y)∈A×A| x = y}）を満たすとき、RはA上のプレ順序関係（推移的・反射的関係）です。(A, R, R;R⊆R, Δ_A⊆R) はRel内のモナドになるので：

• ₀Mnd(Rel) = (プレ順序関係の全体)

Rel内の随伴系は、次のような関係のペア (R, S) です。

• R:A→B, S:B→A in Rel
• Δ_A⊆R;S
• S;R⊆Δ_B

興味深いのは、S = R^t（R^tは、関係Rの転置、(x, y)∈R ⇔ (y, x)∈R^t）としたとき、

• Δ_A⊆R;R^t は、Rが全域〈total〉であることを表す。
• R^t;R⊆Δ_B は、Rが単葉〈univalent | 一価〉であることを表す。

(R, R^t)という形の随伴系とは、全域かつ単葉であるRのことなので、Rは写像と同一視できて、

• ((R, R^t)という形の随伴系の全体) = (写像の全体)

となります。

スパンの圏 Span(C)

ファイバー積〈引き戻し〉が存在する圏Cに対して、そのスパンの圏はSPAN(C)と書きます。SPAN(C)は厳密2-圏にはなりません。ホムセットに同値関係を入れて商集合をとると厳密2-圏になります。これをSpan(C)と書きます。次の記事を参照してください。

• スパンの圏と行列の圏

商集合をとった後のホムセットが（考えている宇宙のなかで）小さくなるかはアヤシイです。

• スパンの圏の構成に疑問

ホムセットのサイズは気にしないことにすれば、Span(C)は厳密2-圏となります。Span(C)内のモナドは、圏Cの内部圏〈internal category〉（の同値類）になります。内部圏については、nLab項目を参照してください。

• ₀Adj(Span(C)) = (Cの内部圏の全体)

通常の圏〈ordinary category〉は、Setの内部圏なので、₀Adj(Span(Set))は、通常の圏の全体になります。

₀Adj(Span(C))も機械的に定義できますが、₀Adj(Span(C))の要素が既存の構造なのかどうか？ 僕は知りません。

いずれにしても、Span(C)におけるモナド論は、C-内部圏論のひとつの形を提示すると思われます。厳密2-圏ではなくて、弱2-圏ベースで考えてみたのが「モナド論をヒントに圏論をする（弱2-圏の割と詳しい説明付き）」の内容です。

モナドの2-随伴状況

厳密2-圏Kに対するMnd(K)とAdj(K)には、さまざまな圏的構造を入れることができます。そのなかでも一番便利そうなのは、Mnd(K)にもAdj(K)にも厳密2-圏の構造を入れる場合でしょう。

厳密2-圏の構造が入ったMnd(K)とAdj(K)を、_s2Mnd(K), _s2Adj(K) と書くことにします。Kも厳密2-圏だったので、

• K, _s2Mnd(K), _s2Adj(K) in s2-Cat_#r

宇宙の階数rは目的により適当に決めますが、話を簡単にするため、以下 r = 0 として階数は省略します。

_s2Mnd(K), _s2Adj(K) 以外に、_s2Idをs2-Cat上の恒等関手として、

• _s2Id(K) = K

とします。

_s2Id(K), _s2Mnd(K), _s2Adj(K) はいずれもs2-Catのなかに居ますが、これらは2-随伴状況〈{2-bi}{adjoint | adjunction} {situation | context}〉を形成しています。2-随伴状況とは、「背後には2-随伴系があるぞ」という程度の割と漠然とした意味です。2-随伴系の定義は安定していません（次節）。

2-随伴状況をより正確に言うには、MndとAdjにさらに修飾が付くのですが、修飾の説明はせずにとりあえず結果だけを言うと：

• K in s2-Cat_EM に対する _s2RAdj_L(K) と _s2Mnd_EM(K) のあいだに、アイレンベルク／ムーア・2-随伴ペア〈Eilenberg-Moore 2-adjoint pair〉が存在する。
  • 左2-関手 mnd_K: _s2RAdj_L(K) → _s2Mnd_EM(K)
  • 右2-関手 emadj_K: _s2Mnd_EM(K) → _s2RAdj_L(K)
• K in s2-Cat_Kl に対する _s2Mnd_Kl(K) と _s2LAdj_L(K) のあいだに、クライスリ・2-随伴ペア〈Kleisli 2-adjoint pair〉が存在する。
  • 左2-関手 kladj_K: _s2Mnd_Kl(K) → _s2LAdj_L(K)
  • 右2-関手 mnd_K: _s2LAdj_L(K) → _s2Mnd_Kl(K)

前回紹介した"バスケス-マルケス 2015"（https://arxiv.org/abs/1510.04724）は、これらの2-随伴状況を解説しています。ただし、使っている記号が違うので、対応を示します。

檜山	バスケス-マルケス
s2RAdjL(K)	AdjR(K)
s2MndEM(K)	Mnd(K)
mndK （EMの）	ΦE
emadjK	ΨE
s2MndKl(K)	Mnd●(K)
s2LAdjL(K)	AdjL(K)
kladjK	ΨK
mndK （Klの）	ΦK

Mnd_EM, Mnd_Kl という書き方は"クリメン／ソリヴェレス 2010"（https://www.uv.es/~solivere/Articles/Kleisli%20and%20Eilenberg-Moore%20constructions%20as%20parts%20of%20biadjoint%20situations.pdf）に倣いました。RAdj_Lといった書き方は次の論文から採りました*1。

• Title: Multivariable adjunctions and mates (2012)
• Authors: Eugenia Cheng, Nick Gurski, Emily Riehl
• Pages: 52p
• URL: https://arxiv.org/abs/1208.4520

MndとIdのあいだにも2-随伴状況があります。こちらは、2-随伴ペアではなくて、2-随伴トリオになります。Mnd-Idの2-随伴トリオについては、"ザワドウスキ 2010"（https://arxiv.org/abs/1012.0547）に簡単な記述があります。バスケス-マルケスのMnd^●を、ザワドウスキはMnd_opと書いており、これは"ブーム 2018"（https://arxiv.org/abs/1810.11300）が使っている水平方向の反対圏の記法と同じです。記法は人により全くバラバラなので、注意が必要です。

2-随伴について

Id(K) = K, Mnd(K), Adj(K) などは、厳密2-圏とみなすことができて、それらのあいだに2-随伴状況／2-随伴系があります。しかし、2-随伴〈2-adjunction | 2-adjoint system〉の定義は安定していません。

nLab項目"2-adjunction"によると：

A 2-adjunction is a common name for various kinds of adjunctions in 2-category theory; not only adjunctions between 2-categories themselves, but more generally adjunctions within an arbitrary 3-category.

---

2-随伴とは、2-圏論におけるさまざまな種類の随伴に対する総称的な呼び名である。2-圏のあいだの具体的随伴だけでなく、任意の3-圏内のより一般的随伴概念もある。

単に「2-随伴」といっただけでは、さまざまな種類の随伴概念のどれかを示す、というだけでハッキリはしません。「2-圏のあいだの具体的随伴」とは、今話題にしているような、K, L in s2-Cat の2-随伴のことです。これを形式化すると、3-圏の対象 K, L in T, T in ?3-Cat に対する2-随伴が定義できる、ということです。

nLabによると、現在提案されている2-随伴は：

1. 厳密2-随伴〈strict 2-adjuncation〉
2. 双随伴〈biadjunction〉
3. 疑随伴〈pseudoadjunction〉
4. ラックス2-随伴〈lax 2-adjunction〉

厳密2-圏のあいだのアイレンベルク／ムーア・2-随伴とクライスリ・2-随伴に関しては、厳密2-随伴で足りるような気がします（ちょっと自信がないが）。しかし、アイレンベルク／ムーア構成とクライスリ構成の背後には、もっと高次で大規模な随伴構造が存在しているような気もします。

MndとIdのあいだには随伴トリオが存在しますが、随伴トリオをチャンと扱うには多項随伴系〈multivariable adjunctions〉が必要かも知れません。多項随伴系の2次元版、つまり、多項・2-随伴系も存在しているはずです。

モナドと随伴を調べるのに、高次（2次元以上）のモナドと随伴が必要になる -- ここでもマイクロコスモ原理が働いているようです。

• マイクロコスモ原理と構造の無限タワー

その他の問題点や注意点

前節で、随伴の圏Adjは厳密2-圏 _s2Adj(K) とみなせると言いました。しかし、Adjを厳密二重圏〈strict double category〉とみなすほうが都合がいいこともあります。厳密二重圏とみなした随伴の圏を _sdAdj(K) としましょう。

厳密2-圏 _s2Adj(K) と 厳密二重圏 _sdAdj(K) は、とりあえずは別物で、関連性は明らかではありません。これらを統合するには、3-圏 _sc3Adj(K) を導入するとよさそうです。前置プレフィックスの"sc3"は厳密柱状3-圏〈strict cylindrical 3-category〉のつもりです。

今、厳密柱状3-圏 _sc3Adj(K) についてこれ以上述べませんが、厳密2-圏 _s2Adj(K) も厳密二重圏 _sdAdj(K) も、厳密柱状3-圏 _sc3Adj(K) から取り出すことができます。

随伴とモナドを取り扱うとき、留意すべき概念に、

• メイト
• 反対圏

があります。

メイトは、随伴系におけるホムセット同型 D(F(A), Y) C(A, G(Y)) を拡張した概念で、自然変換の集合のあいだのメイト対応（同型）を通じて「互いにメイト」という関係が定義できます。_s2Adj(K), _dAdj(K) の構成のときには、メイトが必須です。

AdjもMndも厳密2-圏Kをもとに作られ、それ自身が厳密2-圏になります。しばしば2-圏の反対圏を考えます。とはいえ、2次元以上の圏では、方向がニ方向以上あるので、“どの方向に対して反対か”に注意する必要があります。「高次圏の反対圏をどう書くか」でブーム〈Gabriella Böhm〉の書き方を紹介しましたが、他に色々な書き方があります。よく確認しないと混乱します。

---

アイレンベルク／ムーア構成とクライスリ構成に関わる2-随伴状況や、厳密二重圏／厳密柱状3-圏としてのAdjなど、その詳細は述べられませんでしたし、述べるにはけっこうな準備も必要です。マイ・モナドブームがゆるやかに続くなら、さらに続きがあるかも知れません。

*1:元の論文では、下付きのLはデフォルトなので省略して書かないのですが、デフォルトと省略は諸悪の根源なので書くことにします。