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

ご連絡は上記 X アカウントに DM にてお願いします。

［参照用 記事］

モナド-セオリー対応はラックス斜モノイド関手だろう

雑記／備忘

ヴォエヴォドスキーによると、ローヴェア・セオリーは相対モナドです。ローヴェア・セオリーに対応する（普通の）モナドは集合圏上の有限項モナド〈finitary monad〉です。「セオリー → モナド」対応は、相対モナドを（普通の）モナドに拡張しているのではないか？ と「リントンの定理と相対モナド」で述べました。

モナドの定義には、とあるモノイド圏内のモノイドとして定義する方式と、クライスリ拡張オペレーターを使って定義する方式があります。モノイド方式のほうが代数的には扱いやすいです。が、相対モナドにはモノイド方式が使えない（正確には使いにくい）ので、通常はクライスリ拡張方式で定義します。

実は、相対モナドにモノイド方式が絶対に使えないわけではなくて、外側の（環境となる）モノイド圏を斜モノイド圏〈skew monoidal category〉にゆるめると、相対モナドのモノイド方式の定義が出来るようです。そうなると、「相対モナド → モナド」の拡張は、ラックス斜モノイド関手により誘導された“モノイド達の圏のあいだの圏同値”なのではないだろうか、と思えます。

セオリーもモナドもどちらもモノイドであり、“拡張”と呼ばれる関手により対応しているなら話はスッキリします。しかも、“拡張”は実はカン拡張で与えられる、と。もしほんとなら、なんか大団円な感じがします。$`\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mbf}[1]{ \mathbf{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
%\newcommand{\mfk}[1]{\mathfrak{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\u}[1]{ \underline{#1} }
\newcommand{\id}{ \mathrm{id}}
\newcommand{\Id}{ \mathrm{Id}}
%\newcommand{\op}{ \mathrm{op}}
\newcommand{\In}{ \text{ in }}
\newcommand{\hyp}{\text{－} }
\newcommand{\EQV}{\mathrel{\overset{\sim}{\equiv}} }
%\newcommand{\Iff}{ \Leftrightarrow }
%\newcommand{\Imp}{ \Rightarrow }
%\newcommand{\twoto} {\Rightarrow }
%\newcommand{\o}[1]{ \overline{#1} }
%\newcommand{\T}[1]{ \text{#1} }
`$

内容：

基本概念と言葉づかいの約束

$`\cat{D}`$ を圏として、$`F`$ は $`\cat{D}`$ 上の自己関手とします。$`F`$ を台関手〈underlying functor〉とするモナドを、（一旦は）記号の乱用無しで次のように書くとします。

$`\quad \msc{F} = (F, \mu, \eta)/\cat{D}`$

このとき、次のような言い回しを使います。

  • $`\msc{F}`$ は、ルート圏〈root category〉 $`\cat{D}`$ 上のモナド〈monad over $`\cat{D}`$〉である。
  • $`\msc{F}`$ は、台関手 $`F`$ に載ったモナド〈monad on $`F`$〉である。

「ルート圏」は、相対モナドと用語を合わせるためです（以前は「基礎圏〈ground category〉」と呼んでました）。

相対モナド〈relative monad〉 $`\msc{A}`$ は次のように書きます。

$`\quad \msc{A} = (A, \eta, E)/J`$

ここで、$`J:\cat{C} \to \cat{D}`$ はルート関手〈root functor〉です。$`A`$ は相対モナドの台関手、$`\eta`$ は単位自然変換で、$`E`$ はクライスリ拡張オペレーター〈Kleisli extension operator〉です。以下に幾つかの注意事項：

  • $`A`$ の対象パートだけから、射パートと関手性を再現できるが、ここでは最初から関手としておく。
  • $`\eta`$ の自然性を後から証明できるが、ここでは最初から自然変換としておく。
  • 用語は適宜・適当に省略・短縮する。例えば、ルート関手 (略)→ ルート、クライスリ拡張オペレーター (略)→ クライスリ拡張 (略)→ 拡張 。

ドクトリン〈doctrine〉は、「補足と続き： ベックの分配法則に基づく“一般化圏の製造工場” // ドクトリン」で約束したように、圏または圏類似代数構造達の0-圏、1-圏、2-圏などの総称的な呼び名とします。「ドクトリン」という言葉のその他の意味合いについては以下の過去記事など（興味があれば）：

特に、極限ドクトリン〈limit doctrine〉／余極限ドクトリン〈colimit doctrine〉は、特定の種類の極限／余極限を定義するための小さい圏達の集合のことです。例えば、すべての（離散圏としての）有限集合の集合や、すべての小さいフィルター付き圏〈filtered category〉の集合などが極限ドクトリン／余極限ドクトリンに使われます。

リントン／ローヴェア・フレームワーク

リントンの定理は次を主張します（「リントンの定理」「リントンの定理： 概要、実例、注意事項」参照）。

  • セオリーとモナドのあいだの対応があり、セオリーの圏とモナドの圏は圏同値となる。（モナド-セオリー対応）
  • セオリーの表現とモナドのアイレンベルク／ムーア代数のあいだの対応があり、セオリーの表現の圏とモナドのアイレンベルク／ムーア代数の圏は圏同値となる。（代数-表現・対応）

習慣的に「モナド-セオリー対応〈monad-theory correspondence〉」といいますが、「セオリー → モナド」方向の対応を与える関手に注目します。この関手をリントン／ローヴェア関手〈Linton-Lawvere functor〉と呼びましょう。リントン／ローヴェア関手は $`\mbb{L}`$ と書きます*1。

$`\quad \mbb{L} : \text{セオリー達の圏} \to \text{モナド達の圏} \In \mbf{CAT}`$

セオリー $`T`$ に対する $`\mbb{L}(T)`$ が、$`T`$ のリントン／ローヴェア・モナド〈Linton-Lawvere monad〉です。リントンの定理の後半（代数-表現・対応）は次のように書けます。

$`\quad \mrm{Repr}(T) \EQV \mrm{EM}(\mbb{L}(T)) \In \mbf{CAT}`$

ここで '$`\EQV`$' は圏同値の記号です。

リントンの定理を成立させるために必要な基盤一式をリントン／ローヴェア・フレームワーク〈Linton-Lawvere framework〉と呼ぶことにします*2。リントン／ローヴェア・フレームワークの上にリントン／ローヴェア関手が構成できて、リントンの定理が成立する、という段取りです。

問題は、リントン／ローヴェア・フレームワークがどんなものであるべきか？ です。リントン／ローヴェア関手を実際に構成できて、リントンの定理が証明できるようなフレームワークじゃなきゃいけません。

余極限ドクトリンとリントン／ローヴェア・フレームワーク

リントン／ローヴェア・フレームワークは、余極限ドクトリンで統制されていると思われます。余極限ドクトリンを $`\msc{L}`$ とします。$`\msc{L}`$ 配下のリントン／ローヴェア・フレームワークは次の構成素からなります。

  1. 圏 $`\cat{D}`$
  2. 圏 $`\cat{C}`$
  3. 関手 $`J:\cat{C} \to \cat{D}`$

次の条件を要求します。

  1. $`\cat{D}`$ は、$`\msc{L}`$-余完備〈$`\msc{L}`$-cocomplete〉である。
  2. [追記]$`J`$ は、充満忠実である。（抜けていた）[/追記]
  3. $`J`$ は、$`\msc{L}`$-稠密〈$`\msc{L}`$-dense〉である。

$`\msc{L}`$-余完備は、$`S\in \msc{L}`$ を形状とする任意の図式 $`D: S\to \cat{D}`$ が余極限を持つことです。$`\msc{L}`$-稠密は、稠密関手〈dense functor〉の定義の「余極限」を「$`\msc{L}`$-余極限」に制限したものです。$`\msc{L}`$-余極限は、$`S\in \msc{L}`$ を形状とする図式の極限です。

リントン／ローヴェア・フレームワーク $`(\msc{L}, \cat{D}, \cat{C}, J)`$ があるとき、この上でリントン／ローヴェア関手を構成するときの基本手段は左カン拡張です。与えられた $`A:\cat{C}\to\cat{D}`$ の左カン拡張は、以下の図式の疑問符を埋める“テンプレート充填問題”の解（「カン拡張ラムダ計算化 方針」参照）のなかで最良〈普遍的〉なものです。

$`\quad \xymatrix{
\cat{C} \ar[d]_J \ar[r]^A
\ar@{}[dr]|{?}
&\cat{D} \ar[d]^{?}
\\
\cat{D} \ar@{=}[r]
&\cat{D}
}\\
\quad \In \mbf{CAT}
`$

$`J`$ に沿った $`A`$ の左カン拡張は $`\mrm{Lan}_J(A)`$ と書きます。この左カン拡張が任意の $`A`$ に対して存在するだけでなくて、$`\mrm{Lan}_J(\hyp)`$ は関手になるとします。つまり、次の関手があります。

$`\quad \mrm{Lan}_J : [\cat{C}, \cat{D}] \to [\cat{D}, \cat{D}] \In \mbf{CAT}
`$

関手 $`\mrm{Lan}_J`$ は頻繁に使うので、$`\mbb{J}`$ という短縮名を与えます。関手 $`\mbb{J}`$ がキチンと定義できることがリントン／ローヴェア・フレームワークの要点です。$`\mbb{J}`$ も含めてリントン／ローヴェア・フレームワーク $`(\msc{F}, \cat{D}, \cat{C}, J, \mbb{J})`$ としてもいいかも知れません。

リントン／ローヴェア関手

「リントンの定理と相対モナド 」で述べたように、セオリーは相対モナドと同一視可能なようです。となると、リントン／ローヴェア関手は次の形です。

$`\quad \mbb{L}: \mrm{RelMnd}(J) \to \mrm{Mnd}(\cat{D})`$

もし、「モナドはモノイドだ」というキャッチフレーズが相対モナドにも通用するなら、$`\mbb{L}`$ は次のように書けるでしょう。

$`\quad \mbb{L}: \mrm{Mon}([\cat{C}, \cat{D}]) \to \mrm{Mon}([\cat{D}, \cat{D}])`$

しかし、$`\mrm{Mon}([\cat{C}, \cat{D}])`$ は意味不明です。$`\mrm{Mon}(\hyp)`$ は、引数であるモノイド圏に対して、モノイド〈モノイド対象 | 内部モノイド〉達の圏を作る構成子です。$`[\cat{C}, \cat{D}]`$ はモノイド圏ではないので、モノイド達の圏を作りようがありません。

$`[\cat{C}, \cat{D}]`$ をモノイド圏には出来ないですが、モノイド圏に類似した斜モノイド圏〈skew monoidal category | lax monoidal category〉は作れます。斜モノイド圏は、モノイド圏から、モノイド積の結合律子〈associator〉と左右の単位律子〈left/right unitor〉の可逆性の条件を外した構造です。斜モノイド圏の公理系は、モノイド圏より複雑になります。

リントン／ローヴェア・フレームワークの $`J,\mbb{J}`$ を使うと、$`[\cat{C}, \cat{D}]`$ 上に斜モノイド構造が入ります。この斜モノイド圏を $`([\cat{C}, \cat{D}], \odot, J)`$ と書きます。ルート関手 $`J`$ がモノイド単位〈斜モノイド単位〉となります。

また、自己関手達の圏 $`[\cat{D}, \cat{D}]`$ にモノイド構造を載せたモノイド圏は $`([\cat{D}, \cat{D}], \otimes, I)`$ とします。'$`\otimes`$' は関手の結合 '$`*`$' と同じですが、モノイド積らしく書いただけです。$`I`$ は、恒等関手 $`\Id_\cat{D}`$ のことです。

以上に説明した記法で、リントン／ローヴェア関手は次のように書けます。

$`\quad \mbb{L}: \mrm{Mon}( ([\cat{C}, \cat{D}], \odot, J) ) \to \mrm{Mon}( ([\cat{D}, \cat{D}], \otimes, I) ) \In \mbf{CAT}`$

この形でリントン／ローヴェア関手は定義できるでしょうが、圏同値の保証はできません。圏 $`[\cat{D}, \cat{D}]`$ が豊富過ぎる（不要な対象を含む）可能性があります。$`\msc{L}`$-余連続〈$`\msc{L}`$-cocontinuous〉な自己関手だけに制限すれば次のようになります。 $`[\cat{D}, \cat{D}]^\msc{L}`$ は$`\msc{L}`$-余連続な自己関手達の圏です。

$`\quad \mbb{L}: \mrm{Mon}( ([\cat{C}, \cat{D}], \odot, J) ) \to \mrm{Mon}( ([\cat{D}, \cat{D}]^\msc{L} , \otimes, I) )\In \mbf{CAT}`$

集合圏上の有限項モナドの場合から類推して、おそらく、$`[\cat{D}, \cat{D}]^\msc{L}`$ に制限すれば圏同値となるでしょう。

斜モノイド的ガジェット達

斜モノイド圏 $`([\cat{C}, \cat{D}], \odot, J)`$ のモノイド積は、次のように定義されます。

$`\text{For }A, B\in |[\cat{C}, \cat{D}]|\\
\quad A\odot B := A * \mbb{J}(B)
`$

'$`*`$' は通常の関手結合の図式順演算子記号です。$`[\cat{C}, \cat{D}]`$ 上の斜モノイド構造は、$`\mbb{J}`$ を使って定義します。

また、リントン／ローヴェア関手 $`\mbb{L}`$ は、事実上 $`\mbb{J}`$ のことです。関手 $`\mbb{J}`$ は次のようなラックス斜モノイド関手〈lax skew monoidal functor〉を定義します。

$`\quad \mbb{J} : ([\cat{C}, \cat{D}], \odot, J) \to ([\cat{D}, \cat{D}], \otimes, I) \:\text{ lax } \In \mbf{SkewMonCAT}`$

$`([\cat{C}, \cat{D}], \odot, J)`$ 内のモノイド〈モノイド対象 | 内部モノイド〉は、自明な斜モノイド圏 $`\mbf{I}`$ からのラックス斜モノイド関手と同一視できます。ラックス斜モノイド関手とラックス斜モノイド関手の結合が再びラックス斜モノイド関手であることから、任意のラックス斜モノイド関手はモノイド対象を保存します。この事情により $`\mbb{J}`$ から誘導された関手が $`\mbb{L}`$ です。

以上に述べたあらすじを、キチンと定式化するには、モノイド的構造の結合律子／単位律子の条件をゆるめた斜モノイド的〈skew monoidal〉な代数的ガジェットを準備する必要があります。次のような構造達です。

  • 斜モノイド圏〈skew monoidal category〉
  • ラックス斜モノイド関手〈lax skew monoidal functor〉
  • 斜右アクテゴリー、斜左アクテゴリー〈skew {left | right} actegory〉
  • ラックス斜右アクテゴリー射、ラックス斜左アクテゴリー射〈skew lax {left | right} actegory morphism〉

これらの斜モノイド的ガジェット達と左カン拡張がうまく協調してくれれば、リントン／ローヴェア・フレームワーク上にリントン／ローヴェア関手を構成することが出来るでしょう。

と、シナリオはこんななんですが、ほんとかどうかを確認するのは大変。

追記： 参考文献

ローヴェアとリントンのオリジナルに近い形でのモナド-セオリー対応の解説は、「リントンの定理」で引用したハイランド／パワーの論文でしょう。

古典論を今風の視点から解説したものに、コービンのスライドがあります。

プロモナドや相対モナドを中間に挟んで古典的対応を構成しています。

「リントンの定理と相対モナド」で言及した、ローヴェア・セオリーが相対モナドだと言っているヴォエヴォドスキーの論文は：

このヴォエヴォドスキー論文、斜め読みしかしてないのですが、けっこう以前から気にしていたようです。2018年の記事「なにゆえにカン拡張なのか」で触れています。他に2024年の「型理論とインスティチューションの周辺」、「カートメル／ヴォエヴォドスキー／パルムグレンの型理」でも引用しています。

相対随伴〈relative adjunction〉という概念は、1968年にウルマー〈Friedrich Ulmer〉が提案しているようで、随分と古いのですが、相対モナドとしてリバイバルさせたのはアルテンキルヒ／チャップマン／ウウスタルです。

  • [ACU14-]
  • Title: Monads need not be endofunctors
  • Authors: Thosten Altenkirch, James Chapman, Tarmo Uustalu
  • Submitted: 22 Dec 2014 (v1), 4 Mar 2015 (v2)
  • Pages: 40p
  • URL: https://arxiv.org/abs/1412.7148

ArXivへの投稿は2014年ですが、2010年くらいには同名の論文が発表されています。2011年11月の記事「インデックス付き圏のフビニ／グロタンディーク同値」「大量のモナド類似物を取り扱う方法：参考文献」で言及されているので。

過去記事から参照したURLは今は無効ですが、21 May 2010 日付の21枚スライドがインターネットにありました。そして、15ページの論文が CiteSeerX に投稿されていました。

現在は40ページの長い論文になり、第3章が斜モノイド圏の話になっています。このブログ記事に書いたシナリオは、アルテンキルヒ／チャップマン／ウウスタルにより実行されているかも知れません。

相対モナドの形式論に関してはアーカー／マクダルメットが標準的解説です。「二重圏、縦横をもう一度 」、「二重圏の縦横 補遺」、「添加仮想二重圏」、「型理論とインスティチューションの周辺」などで引用しています。

  • [AM23-]
  • Title: The formal theory of relative monads
  • Authors: Nathanael Arkor, Dylan McDermott
  • Submitted: 27 Feb 2023 (v1), 1 Apr 2024 (v3)
  • Pages: 91p
  • URL: https://arxiv.org/abs/2302.14014

相対モナドの形式論を含むより包括的な内容は、アーカーの学位論文に書いてあるようです。

もうひとつ、モナド-セオリー対応のモダンな定式化として：

モナド-セオリーに関係があるかどうか分からないのですが、オペラッドの文脈でも斜モノイド圏が出てきます。

  • [Lac16]
  • Title: Operadic categories and their skew monoidal categories of collections
  • Author: Stephen Lack
  • Submitted: 20 Oct 2016
  • Pages: 37p
  • URL: https://arxiv.org/abs/1610.06282

*1:「リントンの定理： 概要、実例、注意事項」の $`\mbb{L}`$ は、指標にモナドを対応させる関手で、少し違います。

*2:なんらかの基盤一式を、「コンテキスト」、「セットアップ」、「状況〈situation〉」などと呼びます。