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

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

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

参照用 記事

モナド: 随伴系の圏の上のインデックス付き圏として


\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{\ID}{\mathrm{ID} }
\newcommand{\op}{\mathrm{op} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\Imp}{\Rightarrow }
\require{color} % 緑色
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For }  }%
\newcommand{\Define}{\Keyword{Define }  }%
\newcommand{\Let}{\Keyword{Let }  }%
\newcommand{\Declare}{\Keyword{Declare }  }
\newcommand{\Holds}{\Keyword{Holds }  }
2022年あけましておめでとうございます。

というわけで、圏に対してその上のモナドの圏を対応させる関手=インデックス付き圏の話をします。これは、10年近く前2012年4月の記事「またインデックス付き圏が出てきたけど、これはどうなっている?」のコメント欄でksさんに教えていただいたことをまとめたレポートです。とても遅れたレポートです。ksさん、その節はありがとうございました。

内容:

概要

10年前の過去記事で、独りごとのようにモソモソと言っていたことは; 次の2つの対応がどちらもインデックス付き圏〈indexed category〉になるだろう、ということです。

  1. \cat{C} にその上のモナドの圏を対応させる \cat{C} \mapsto \mrm{Monad}(\cat{C})
  2. \cat{C} 上のモナド M にそのクライスリ圏を対応させる (\cat{C}, M) \mapsto \mrm{Kl}(\cat{C}, M) *1

これらが二段階のインデックス付き圏、あるいは入れ子のインデックス圏を形成しそうです。まずは第一段階のインデックス付き圏を構成したいのですが、途中で往生していたのでした。

そのときksさんに教えていただいたキーとなる事実は次のことです。

  • ラックス・モノイド関手により、モノイドは保存される。

なるほど! これで \cat{C} \mapsto \mrm{Monad}(\cat{C}) がインデックス付き圏になることは容易に示せます。

以上の構成を、(10年前よりは)詳しく話します。難しいところはないのですが、面倒です。細部まで詰めると長くなるので、ある程度は端折りますが、ストーリーは追えるように記します。

セットアップ

小さい圏の2-圏 {\bf Cat} を基本に据えて話をします。“大きいか知れない厳密2-圏”達の3-圏を {\bf Str2CAT} とすると、

\quad {\bf Cat}\in |{\bf Str2CAT}|

です。以下の議論は、{\bf Cat} の代わりに、任意の厳密2-圏 \cat{K} \in |{\bf Str2CAT}| を基本に据えても同様にできます。が、典型的厳密2-圏として {\bf Cat} で話を進めます。

{\bf Cat} の図式順の演算子記号は次を使います(「等式的推論と高次圏論 // 結合の演算子記号」でも述べました)。反図式順の記号は使いません

  • 横結合(関手と関手):  F*G
  • 横結合(関手と自然変換):  \alpha*G,\: F*\beta
  • 横結合(自然変換と自然変換): \alpha*\beta
  • 縦結合(自然変換): \alpha;\beta

恒等射は次のように書きます。

  • 恒等関手(1-射): \Id_\cat{C} : \cat{C}\to\cat{C} \In {\bf Cat}
  • 恒等自然変換(2-射): \mrm{ID}_F::F \twoto F :\cat{C}\to\cat{D}\In {\bf Cat}

以下のギリシャ小文字は、この記事内での使用法を固定します。

  • \eta〈エータ | イータ〉 : 随伴系とモナドの単位
  • \varepsilonイプシロン〉 : 随伴系の余単位
  • \nu〈ニュー〉 : ラックス・モノイド関手の乗法*2
  • \iota〈イオタ〉 : ラックス・モノイド関手の単位
  • \mu〈ミュー〉 : モナドの乗法

この記事内では、横着してペースティング図もストリング図も描いてませんが、各自描いてみることをおススメします。

随伴系の圏

最初に、随伴系の圏 \mrm{Adj}({\bf Cat}) を定義します。これは、任意の厳密2-圏 \cat{K} \in |{\bf Str2CAT}| に対して定義できる \mrm{Adj}(\cat{K}) の、\cat{K} = {\bf Cat} と置いた具体例です。以下、\cat{K} = {\bf Cat} である場合は、

\quad {\bf Adj} := \mrm{Adj}({\bf Cat})

と略記します。{\bf Adj} は大きい圏となるので、{\bf Adj} \in |{\bf CAT}| です。ここで、{\bf CAT} は大きいかも知れない圏〈1-圏〉達の2-圏です。

{\bf Adj} の対象の集合は次のようになります。

\quad |{\bf Adj}| := |{\bf Cat}|

つまり、(小さい)圏が {\bf Adj} の対象です。その意味で、{\bf Adj} は“圏の圏”と言えますが、射は関手ではありません。

{\bf Adj} の射は随伴系〈adjunction | adjoint system〉です。\cat{C}, \cat{D}\in |{\bf Adj}| に対して、\cat{C} から \cat{D} への随伴系は、4つ組 (L, R, \eta, \varepsilon) で:

  • L:\cat{C} \to \cat{D} \In {\bf Cat} 随伴系の左関手〈left functor〉
  • R:\cat{D} \to \cat{C} \In {\bf Cat} 随伴系の右関手〈right functor〉
  • \eta: \Id_{\cat{C}} \twoto L*R \In {\bf Cat} 随伴系の単位〈unit〉
  • \varepsilon: R*L \twoto \Id_{\cat{D}} \In {\bf Cat} 随伴系の余単位〈counit〉

随伴系が満たすべき法則は、次の2つのニョロニョロ関係式〈snake {relation | equation | identity}〉です*3


\quad (\eta * L) ; (L * \varepsilon) = \ID_L \;::L \twoto L : \cat{C}\to \cat{D} \In {\bf Cat}\\
\quad (R*\eta ); ( \varepsilon * R) = \ID_R \;::R \twoto R : \cat{D}\to \cat{C}\In {\bf Cat}

随伴系の域と余域である圏も含めれば、随伴系は6つ組 (\cat{C}, \cat{D}, L, R, \eta, \varepsilon) です。

随伴系を表すために、次のような記号の乱用をします。


\quad F 
= (F, F', \eta^F, \varepsilon^F)
= (\cat{C}, \cat{D}, F, F', \eta^F, \varepsilon^F)

つまり:

  1. 随伴系とその左関手を同じ記号で表す(オーバーロード)。
  2. 随伴系の右関手は随伴系の名前にダッシュ〈プライム〉を付けた記号で表す。
  3. 随伴系の単位は \eta の右肩に随伴系の名前を乗せた記号で表す。
  4. 随伴系の余単位は \varepsilon の右肩に随伴系の名前を乗せた記号で表す。
  5. 必要に応じて、4つ組で書いたり6つ組で書いたりする。

随伴系は圏 {\bf Adj} の射〈1-射〉なので、次のように書けます。

  •  F= (F, F', \eta^F, \varepsilon^F):\cat{C} \to \cat{D} \In {\bf Adj}
  •  F = (F, F', \eta^F, \varepsilon^F)\in {\bf Adj}(\cat{C}, \cat{D}) \in |{\bf Set}|

随伴系の向きは、その左関手の向きと同じに取ります*4

{\bf Adj} における結合と恒等射の記号は次のように決めます。

記号の乱用により、恒等関手と恒等随伴系のどちらも記号 \Id_\cat{C} で表すので注意してください(適宜、自分で読み分けてください*5)。

{\bf Adj} の結合と恒等射の定義は次のとおりです。

\For F = (F, F', \eta^F, \varepsilon^F): \cat{C} \to \cat{D} \In {\bf Adj}\\
\For G = (G, G', \eta^G, \varepsilon^G): \cat{D} \to \cat{E} \In {\bf Adj}\\
\Declare F;G : \cat{C} \to \cat{E} \In {\bf Adj}\\
\Define F;G :=
(F*G, G'*F', \eta^F;(F*\eta^G* F'), (G'*\varepsilon^F*G);\varepsilon^G )\\
\:\\
\For \cat{C} \in |{\bf Adj}|\\
\Declare \Id_\cat{C} : \cat{C} \to \cat{C}\\
\Define \Id_\cat{C} := (\Id_\cat{C}, \Id_\cat{C}, \ID_{\Id_\cat{C}}, \ID_{\Id_\cat{C}})

以上の記述において、宣言した〈declareした〉プロファイルと実際に定義した〈defineした〉プロファイルが整合的〈正当 | justified | well-defined〉であるためには次の条件が必要です。

  • F;G \in {\bf Adj}(\cat{C}, \cat{E}) \text{ i.e. }F;G : \cat{C} \to \cat{E} \In {\bf Adj}
  • \Id_\cat{C} \in {\bf Adj}(\cat{C}, \cat{C}) \text{ i.e. } \Id_\cat{C} : \cat{C}\to \cat{C} \In {\bf Adj}

また、{\bf Adj} が実際に圏であるためには、次の条件(圏の{公理 | 法則})を満たす必要があります。

\For F = (F, F', \eta^F, \varepsilon^F): \cat{C} \to \cat{D} \In {\bf Adj}\\
\For G = (G, G', \eta^G, \varepsilon^G): \cat{D} \to \cat{E} \In {\bf Adj}\\
\For H = (H, H', \eta^H, \varepsilon^H): \cat{E} \to \cat{F} \In {\bf Adj}\\
\Holds (F;G); H = F;(G;H) \:: \cat{C} \to \cat{F} \In {\bf Adj}\\
\Holds \Id_\cat{C}; F = F \:: \cat{C} \to \cat{D} \In {\bf Adj}\\
\Holds F;\Id_\cat{D} = F \:: \cat{C} \to \cat{D} \In {\bf Adj}

これらの条件を確認することにより、{\bf Adj} = ({\bf Adj}, (;), \Id) が圏〈1-圏〉であることが分かります。つまり、

\quad {\bf Adj} \in |{\bf CAT}|

{\bf Adj} は、後述する“モナドのインデックス付き圏”の域(インデキシング圏)として使います。

ここでは、{\bf Adj} は、|{\bf Adj}| = |{\bf Cat}| であるような1-圏として定義しました。随伴系を二重圏に仕立てることもできます。次の記事を参照してください。

随伴系の圏上のEnd関手

{\bf Cat} は2-圏なので、そのホムシング〈hom-thing〉{\bf Cat}(\cat{C}, \cat{D}) は圏 -- つまりホム圏〈hom-category〉になります。ホム圏〈関手圏〉は {\bf Cat}(\cat{C}, \cat{D}) \in |{\bf Cat}| であり、内部ホムとみなすことができます。ホム圏は次のように幾つかの書き方があります。

\quad {\bf Cat}(\cat{C}, \cat{D})
 = \mrm{hom}_{\bf Cat}(\cat{C}, \cat{D}) = [\cat{C}, \cat{D}]_{\bf Cat} 
  = [\cat{C}, \cat{D}] \;\in |{\bf Cat}|

特に、自己ホム圏 {\bf Cat}(\cat{C}, \cat{C}) は関手・自然変換の横結合 * をモノイド積とみなして(非対称な)厳密モノイド圏になります。モノイド圏としてのホム圏を次のように書きます。

\quad \mrm{End}_{\bf Cat}(\cat{C})
 = \mrm{End}(\cat{C})

厳密モノイド圏に対する記号の乱用を使えば次のように書けます。

\quad \mrm{End}(\cat{C}) = (\mrm{End}(\cat{C}), *, \Id_\cat{C})

厳密モノイド圏なので、結合律子〈associator〉、左単位律子〈left unitor〉、右単位律子〈right unitor〉はすべて恒等射で、意識する必要はありません。

厳密モノイド圏とラックス・モノイド関手とラックス・モノイド自然変換の2-圏を {\bf StrMonCat}^\mrm{lax} とします。ラックス・モノイド関手/ラックス・モノイド自然変換については次の記事を参照してください。

上で定義した \mrm{End} は、

\quad \mrm{End}:|{\bf Adj}| \to |{\bf StrMonCat}^\mrm{lax}|

という写像です(まだ関手にはなってない)。なお、\mrm{End} = \mrm{End}_{\bf Cat} という省略であって、\mrm{End}_{\bf Adj}(F) = {\bf Adj}(F, F) とは違うので気を付けてください*6

この \mrm{End} を、次のような反変関手に拡張します。反変関手にも同じ記号を使います(オーバーロード)。

\quad \mrm{End}:{\bf Adj}^\op \to {\bf StrMonCat}^\mrm{lax}|_{\le 1} \In {\bf CAT}

ここで、記号 -|_{\le 1} は2-圏の切り捨てで、「圏の離散化、切り捨て、次元調整」で説明しました。今の場合は、2-圏 {\bf StrMonCat}^\mrm{lax} の2-射である自然変換をすべて捨ててしまった1-圏を考えることになります*7

さて、\cat{C} \in |{\bf Adj}| に対する \mrm{End}(\cat{C}) は既に定義済みなので、{\bf Adj} の射である随伴系 F に対する \mrm{End}(F) を定義します。

一時的に \Phi := \mrm{End}(F) と置くと、\Phi{\bf StrMonCat}^\mrm{lax}|_{\le 1} の射のはずなので、ラックス・モノイド関手です。このラックス・モノイド関手 \Phi は次のように書けます。

\quad \Phi = (\Phi, \nu, \iota) : \mrm{End}(\cat{D}) \to \mrm{End}(\cat{C}) \In {\bf StrMonCat}^\mrm{lax}|_{\le 1}

ここで、\Phi = (\Phi, \nu, \iota) はまたしても記号の乱用ですが:

  • イコールの左辺の \Phi はラックス・モノイド関手
  • イコールの右辺の \Phi はラックス・モノイド関手の台関手
  • \nu はラックス・モノイド関手の乗法
  • \iota はラックス・モノイド関手の単位

記号の乱用では混乱が起きそうなときは、厳密モノイド圏の台圏、ラックス・モノイド関手の台関手には下線を引くことにします。必要があれば、右肩への添字で識別(オーバーロード解決)もします。つまり、次の書き方も使います。

  • \mrm{End}(\cat{C}) = (\u{\mrm{End}(\cat{C})}, *, \Id_\cat{C}) 厳密モノイド圏
  • \Phi = (\u{\Phi}, \nu, \iota) = (\u{\Phi}, \nu^\Phi, \iota^\Phi) ラックス・モノイド関手

このような記法のもとで、\Phi = \mrm{End}(F) を定義しましょう。まず、先に前提を宣言しておきます。


\For F = (F, F', \eta^F, \varepsilon^F):\cat{C} \to \cat{D} \In {\bf Adj}\\
\Let \Phi = (\u{\Phi}, \nu, \iota) := \mrm{End}(F)\\
\Declare \Phi : \mrm{End}(\cat{D})\to \mrm{End}(\cat{C}) \In {\bf StrMonCat}^\mrm{lax}\\
\Declare \u{\Phi}: \u{\mrm{End}(\cat{D})} \to \u{\mrm{End}(\cat{C})} \In {\bf Cat}\\
\For M, N\in |\u{\mrm{End}(\cat{D})}|\\
\Declare \nu_{M, N} : \u{\Phi}(M) * \u{\Phi}(N) \to \u{\Phi}(M * N)\In \u{\mrm{End}(\cat{C})}  \text{ natural } \\
\Declare \iota: \Id_\cat{D} \to \u{\Phi}(\Id_\cat{C})\In \u{\mrm{End}(\cat{C})}

\text{natural} は自然変換の成分であることを示しています。その自然変換は:

\quad
\nu :: (\u{\Phi}\times \u{\Phi})* (*) \twoto (*) * \u{\Phi}
: \u{\mrm{End}(\cat{D})}\times \u{\mrm{End}(\cat{D})} \to \u{\mrm{End}(\cat{C})}
 \In {\bf Cat}

丸括弧で囲んであるアスタリスクは、\mrm{End}(-) のモノイド積〈二項関手〉です。裸のアスタリスクは2-圏 {\bf Cat} の1-射〈関手〉の結合です。アスタリスク記号をオーバーロードしてますが、結合の次元の違い(「等式的推論と高次圏論 // 高次圏における結合」参照)と役割の違いに注意してください。念の為、2-射 \nu = \nu^\Phi の1次元境界仕様(プロファイルの詳細化)を図式で書いておきます。

\require{AMScd}
\begin{CD}
\u{\mrm{End}(\cat{D})}\times \u{\mrm{End}(\cat{D})} 
    @>{ \u{\Phi}\times\u{\Phi} }>>
    \u{\mrm{End}(\cat{C})}\times \u{\mrm{End}(\cat{C})}\\
@V{(*)}VV         @VV{(*)}V\\
\u{\mrm{End}(\cat{D})}
    @>{ \u{\Phi} }>>
    \u{\mrm{End}(\cat{C})}
\end{CD}\\
\In {\bf Cat}

続いて定義の本体です。


\For M \in |\u{\mrm{End}(\cat{D})}| \\
\Define \u{\Phi}(M) := F*M*F'\\
\For M, N \in |\u{\mrm{End}(\cat{D})}| \\
\Define \nu_{M,N} := (F*M)*\varepsilon^F*(N* F')\\
\Define \iota := \eta

この定義とすぐ上の宣言が整合的であるための条件は次です。


\quad F*M*F' \in |\u{\mrm{End}(\cat{C})}|\\
\quad (F*M)*\varepsilon^F*(N* F') : \u{\Phi}(M)*\u{\Phi}(N) \to
    \u{\Phi}(M*N) \In \u{\mrm{End}(\cat{C})}\\
\quad \iota :\Id_{\cat{C}} \to \u{\Phi}(\Id_\cat{D}) \In \u{\mrm{End}(\cat{C})}

さらに、\Phi = (\u{\Phi}, \nu, \iota) がラックス・モノイド関手であるための条件があります。このことは、前提と定義から証明できますが今は割愛します。

\Phi がラックス・モノイド関手であることが分れば、次が言えます。

\For F : \cat{C} \to \cat{D} \In {\bf Adj}\\
\Holds\\
\quad 
\Phi = \mrm{End}(F) : \mrm{End}(\cat{D}) \to \mrm{End}(\cat{C}) \In 
 {\bf StrMonCat}^\mrm{lax}|_{\le 1}

これだけではまだ \mrm{End} が関手であることにはなりません。次の関手性を示す必要があります。

\For \cat{C}, \cat{D}, \cat{E} \in |{\bf Adj}|\\
\For F:\cat{C}\to \cat{D}, G: \cat{D}\to \cat{E} \In {\bf Adj}\\
\Holds \mrm{End}(F;G) = \mrm{End}(G) * \mrm{End}(F)\\
\Holds \mrm{End}(\Id_\cat{C}) = \Id_{\mrm{End}(\cat{C})}

このように、ルーチンワークが長く続くことが「難しいところはないのですが、面倒です」と言った理由です。面倒な作業を淡々と遂行すれば、次が言えます。

\quad
\mrm{End}: {\bf Adj}^\op \to {\bf StrMonCat}^\mrm{lax}|_{\le 1} \In {\bf CAT}

もう一度繰り返しまとめておくと:

  • \mrm{End} は随伴系の圏の上で定義され、厳密モノイド圏とラックス・モノイド関手の圏に値をとる反変関手である。圏に(非対称な)モノイド圏を対応させ、随伴系にラックス・モノイド関手を対応させる。

厳密モノイド圏の内部モノイドとMon関手

\cat{M} = (\u{\cat{M}}, \otimes^\cat{M}, I^\cat{M}) を(小さい)厳密モノイド圏とします。モノイド積の対称性は仮定しません。記号の乱用で書けば \cat{M} = (\cat{M}, \otimes, I) 。単一の対象  0 *8と恒等射 \id_0 のみからなる自明圏に、自明なモノイド積を入れた厳密モノイド圏を {\bf 1} で表します({\bf 1} は色々な意味でオーバーロードされます)。

M を自明厳密モノイド圏 {\bf 1} から厳密モノイド圏 \cat{M} へのラックス・モノイド関手とします。

\quad
M = (\u{M}, \nu^M, \iota^M): {\bf 1} \to \cat{M} \In {\bf StrMonCat}^\mrm{lax}

次の事実があります。

  • 自明厳密モノイド圏から厳密モノイド圏へのラックス・モノイド関手 M は、当該の厳密モノイド圏内の内部モノイド〈モノイド対象〉になる。
  • その内部モノイドの台対象〈underlying object〉は \u{M}(0) である。
  • その内部モノイドの乗法〈multiplication〉は \nu^M である。
  • その内部モノイドの単位〈unit〉は \iota^M である。

さらに、内部モノイドのあいだの準同型射はラックス・モノイド自然変換で与えられます。まとめると、厳密モノイド圏 \cat{M} 内の内部モノイド〈モノイド対象〉とそのあいだの準同型射からなる圏 \mrm{Mon}(\cat{M}) は次のように定義できます。


\quad \mrm{Mon}(\cat{M}) := {\bf StrMonCat}^\mrm{lax}({\bf 1}, \cat{M})

この定義の右辺は2-圏のホム圏です -- 対象はラックス・モノイド関手で、射はラックス・モノイド自然変換、モノイド積はありません。

2つの厳密モノイド圏のあいだのラックス・モノイド関手 \Psi を考えます。


\quad \Psi = (\u{\Psi}, \nu^\Psi, \iota^\Psi) : \cat{M} \to\cat{N} \In {\bf StrMonCat}^\mrm{lax}

\Psi によるポスト結合〈post-composition〉で前送り〈push forward〉すれば、次の関手ができます。


\quad \Psi_*  : {\bf StrMonCat}^\mrm{lax}({\bf 1}, \cat{M})
\to {\bf StrMonCat}^\mrm{lax}({\bf 1}, \cat{N})
 \In {\bf Cat}

\mrm{Mon}(\Psi) := \Psi_* とすると、\mrm{Mon} は次のような関手になります。

\quad
\mrm{Mon} = {\bf StrMonCat}^\mrm{lax}({\bf 1}, -): {\bf StrMonCat}^\mrm{lax}|_{\le 1} \to {\bf Cat} \In {\bf CAT}

モノイド/モナドの保存

サラッと書きましたが、関手 \mrm{Mon} が定義可能であるためには、次の事実が肝心です。

  • \Psi:\cat{M}\to\cat{N} がラックス・モノイド関手で、M\in |\mrm{Mon}(\cat{M})| ならば、\Psi_*(M) \in |\mrm{Mon}(\cat{N})|

これが、最初の節で述べた

  • ラックス・モノイド関手により、モノイドは保存される。

です。

厳密2-圏に対して同じことを言えば次のようになります。

  • \Psi:\cat{K}\to\cat{L} が厳密2-圏のあいだのラックス2-関手で、F = (F, \nu, \eta)\cat{K} 内のモナドならば、\Psi_*(F)\cat{L} 内のモナドになる。

ラックス・モノイド関手/ラックス2-関手で、モノイド/モナドは保存されるのです。定式化によってはまったく自明に見えてしまいますが*9、重要な事実です。これが、10年前にksさんに教えていただいたことです。

モナドのインデックス付き圏の構成

前々節と前節において、次の2つの関手を定義しました。


\quad \mrm{End}: {\bf Adj}^\op \to {\bf StrMonCat}^\mrm{lax}|_{\le 1} \In {\bf CAT} \\
\quad \mrm{Mon} : {\bf StrMonCat}^\mrm{lax}|_{\le 1} \to {\bf Cat} \In {\bf CAT}

この2つの関手を結合した関手を \mrm{Mnd} とします*10


\Let \mrm{Mnd} := \mrm{End}*\mrm{Mon}: {\bf Adj}^\op \to {\bf Cat} \In {\bf CAT}

\cat{C} に対する \mrm{Mnd}(\cat{C}) は:

\quad \mrm{Mnd}(\cat{C}) = \mrm{Mon}(\mrm{End}(\cat{C}))

これは、次のよく知られた事実の表現です。

  • モナドは、自己関手〈エンド関手〉のモノイド圏におけるモノイド〈内部モノイド | モノイド対象〉である。

したがって、\mrm{Mnd}(\cat{C}) は圏 \cat{C} 上のモナドの圏です。射は、モノイド(としてのモナド)の準同型射(モノイド構造を保つ自然変換)です。

なんらかの圏から {\bf Cat} への反変関手をインデックス付き圏〈indexed category〉と呼ぶので、\mrm{Mnd} は圏 {\bf Adj} 上で定義されたインデックス付き圏です。

こうして、10年前の記事でボンヤリと語っていた

  • \cat{C} にその上のモナドの圏を対応させる対応はインデックス付き圏になるだろう。

という期待は現実だと分かったのです。

*1:記法は10年前の記事に合わせています。\mrm{Kl}(\cat{C}, M) の代わりに \mrm{Kl}(M, \cat{C}) \mrm{Kl}(M/\cat{C})\mrm{Kl}(M) と書くこともあります。

*2:laxatorと呼ぶこともあるようです。

*3:ニョロニョロ関係式は2-射のあいだの等式です。 「等式的推論と高次圏論 // 2-圏の3-射、4-射」で述べたように、2-射のあいだの等式は {\bf Cat} の3-射になります。例えば、1つめのニョロニョロ関係式は次のように書けます。
\quad \text{snake-1} ::: (\eta * L) ; (L * \varepsilon) \;\overset{\id}{\equiv\!\gt}\; \ID_L \;::L \twoto L : \cat{C}\to \cat{D} \In {\bf Cat}

*4:右関手の向きを採用することもあります。

*5:オーバーロードを解決するのが苦手な人もいるでしょう。僕も苦手です。が、記号の乱用/オーバーロードはものすごく使われているので、オーバーロード解決能力は必要です。

*6:混乱しないように記法を工夫すべきかも知れません。End の代わりに、"endo-monoidal-category of -" で \mrm{EMC}(-) とかにすればよかったかも。

*7:2-射を捨てた1-圏にデカルト閉構造を入れたりもしますが、圏の種別が暗黙に変換されることがあります。このへんの“圏の種別の変換”についてはいつかキチンと説明したい。

*8:通常僕は、自明圏の対象を * で表していますが、今回はモノイド積/横結合と記号がコンフリクト〈衝突〉するので 0 にしました。

*9:今回は、この事実が自明に見えるように定式化したのです。

*10:圏の2-圏 {\bf Cat} を1-圏に切り捨てたほうが正確な記述になります。