モナドや随伴系〈adjunction | adjoint system〉が見つかると良いことあります*1。なので、モナドや随伴系を頑張って探すわけです。相対モナド／相対随伴系は、より一般性がある構造です。もちろん、見つかると良いことあります。しかし、相対モナド／相対随伴系は通常のモナド／随伴系より見つけるのが大変です。相対モナド／相対随伴系の構成素の一部しか見えてないことが多いのです。それらしい臭いを嗅ぎつけたら、残りの構成素があるんじゃないか？ と詮索してみましょう。
この記事では、一部しか見えてない状態の相対モナド／相対随伴系を幾つか紹介します。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\parto}{ \supset\!\to }
\newcommand{\In}{\text{ in }}
%\newcommand{\op}{\mathrm{op}}
%\newcommand{\id}{\mathrm{id}}
\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{ \text{－} }
\newcommand{\H}{ \text{-} }
\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\AS}{ \circledast }
%\newcommand{\SEArrow}{\style{display: inline-block; transform: rotate(45deg)} {\Rightarrow} }
\newcommand{\NEArrow}{\style{display: inline-block; transform: rotate(-45deg)} {\Rightarrow} }
%\newcommand{\Models}{ \mathrel{|\!\!\models} }
`$
内容：
相対随伴系と相対モナド
相対随伴系／相対モナドそのものを主題的に扱った過去記事はないのですが、以下の記事達で相対随伴系／相対モナドを使っています。参考にはなるでしょう。
関手 $`J`$ が相対随伴系のルート関手、関手 $`L, R`$ が相対随伴系の左関手、右関手であることを次の図で表します。
$`\quad \xymatrix{
{}
&{\cat{C}} \ar[dr]^R
\ar@{}[d]|{\dashv}
&{}
\\
{\cat{A}} \ar[ur]^L \ar[rr]_J
&{}
&{\cat{E}}
}\\
\quad \In \mbf{CAT}
`$
テキストで略式に書くときは次のようです。
$`\quad L \dashv R`$
相対モナドは、記号の乱用で次のように書きます。
$`\quad T = T/J = (T, \eta, \mrm{Ext})/J`$
台〈underlying thing | carrier〉である $`T`$ は、定義の上では関手である必要はありませんが、すぐに関手に出来るので関手として扱ってかまいません。$`J`$ は相対モナドのルート関手です。この状況を以下のように図示することにします。スラッシュを over または along と読みます。
$`\quad \xymatrix{
\cat{A} \ar[r]_J \ar@{}@/^/[r]|{/} \ar@/^1pc/[r]^T
&\cat{E}
}\\
\quad \In \mbf{CAT}
`$
相対随伴系と相対モナドを一緒に描くと次のようです。
$`\quad \xymatrix@R+1.2pc{
{}
&{\cat{C}} \ar[dr]^R
\ar@{}[d]|{\dashv}
&{}
\\
{\cat{A}} \ar[ur]^L \ar[rr]_J
\ar@{}@/^/[rr]|{/}\ar@/^1pc/[rr]^T
&{}
&{\cat{E}}
}\\
\quad \In \mbf{CAT}
`$
三角形の上側は、$`L \dashv R`$ だけでなく、$`L*R = T`$ も表します（アスタリスクは関手の図式順結合記号）。
相対随伴系から相対モナドは一意的に構成できますが、相対モナドから色々な相対随伴系を作れます（相対随伴系への分解〈resolution〉という）。最も簡単で最もよく使う分解はクライスリ分解です。
ローヴェア・セオリー
ヴォエヴォドスキーの以下の論文によると、ローヴェア・セオリーは相対モナドです。
- [Voe16-B]
- Title: Lawvere theories and Jf-relative monads
- Author: Vladimir Voevodsky
- Submitted: 9 Jan 2016
- Pages: 21p
- URL: https://arxiv.org/abs/1601.02158
ローヴェア・セオリーは、定義の上では次の形をしています（詳細は「ローヴェア・セオリーとその周辺」参照）。
$`\quad \mbf{F} \overset{L}{\to} \cat{C} \In \mbf{Cat}`$
ここで、$`\mbf{F}`$ は有限集合達の圏の標準骨格です。$`\cat{C}`$ は小さな厳密デカルト圏で、関手 $`L`$ は対象集合上で恒等〈identity-on-objects〉な離散極限を保つ関手です。ヴォエヴォドスキーがそうしているように、$`\mbf{F}`$ も $`\cat{C}`$ も（デカルト圏ではなくて）余デカルト圏として、$`L`$ は離散余極限を保つ関手としたほうが都合がいいかも知れません。
$`\mbf{F}`$ から $`\mbf{Set}`$ への標準的な埋め込みを $`J`$ として、以下の図式を考えます。
$`\quad \xymatrix{
{}
&{\cat{C}} \ar@{.>}[dr]^{?R}
\ar@{}[d]|{\dashv}
&{}
\\
{\mbf{F}} \ar[ur]^L \ar[rr]_J
&{}
&{\mbf{Set} }
}\\
\quad \In \mbf{CAT}
`$
これは、与えられた〈given〉$`L, J`$ に対して、未知の〈unknown〉関手 $`?R`$ が相対随伴系を形成していることを表します。つまり、一種の方程式問題です。首尾よく未知の $`?R`$ が求まれば、問題が解けたことになります。
$`\mbf{F}, \cat{C}`$ のデカルト構造、$`L`$ が対象集合上で恒等で連続なことを使うと、目的である相対随伴系の右関手 $`R`$ が構成できます（ヴォエヴォドスキーが非常に丁寧にやっています）。
相対随伴系からは相対モナドが自動的に構成できます。$`T := L*R`$ として、当該相対モナドを（記号の乱用で） $`T/J`$ とします。相対モナド $`T/J`$ のクライスリ分解を作ると、相対随伴系 $`L\dashv R`$ が再現します。左関手だけ取り出すと、それはローヴェア・セオリーです。
以上により、次の三者は互いに変換可能な同値な構造だと言えます。
- ローヴェア・セオリー $`\mbf{F} \overset{L}{\to} \cat{C}`$
- ルート関手が $`J`$ で、左関手が $`\mbf{F}`$ からの“対象集合上で恒等な離散連続関手”である相対随伴系
- ルート関手が $`J`$ である相対モナド
上記の内容、ただし相対モナドではない普通のモナドに関することは、「モナドとクライスリ包含」で触れています。
Diag構成と自由関手
「Diag構成のメタレベル」において、Diag構成のセットアップ（という構造）として次の図（コスパン）を挙げました。
$`\quad \xymatrix{
\mbf{Shape} \ar[dr]_{\mrm{J}}
&{}
&\mbf{Targ} \ar[dl]^{\mrm{K}}
\\
{}
& \mbf{Amb}
&{}
}`$
上記過去記事に説明がありますが、ここでの太字が固有名ではないのですよね。誤解されそうなので、太字をカリグラフィー体に変えて、相対随伴系らしいレイアウトにします。
$`\quad \xymatrix{
{}
&{\cat{T}} \ar[dr]^{\mrm{K}}
\ar@{}[d]|{\dashv}
&{}
\\
{\cat{S}} \ar[rr]_J \ar@{.>}[ur]^{?F}
&{}
&{\mbf{CAT}}
}\\
\quad \In 2\mathbb{CAT}
`$
これは、「Diag構成のメタレベル」におけるメタレベル 1 のセットアップです。
- $`\cat{S}`$ は形状達のドクトリン〈doctrine of shapes〉、2-圏である必要はない。
- $`\cat{T}`$ はターゲット達のドクトリン〈doctrine of targets〉、2-圏であるのが望ましい。
- アンビエント・ドクトリン〈ambient doctrine〉は圏達の2-圏 $`\mbf{CAT}`$ とする。
- $`J`$ は形状編入関手〈shape incorporation functor〉
- $`K`$ はターゲット編入関手〈target incorporation functor〉、2-関手かも知れない。
Diag構成は次のように定義されます。
$`\text{For }A\in |\cat{S}|\\
\text{For }X\in |\cat{T}|\\
\quad \mrm{Diag}[A](X) := \mbf{CAT}(J(A), K(X))
`$
Diag構成のセットアップ（コスパン）が相対随伴系でなくても十分役に立ちますが、上記図式の $`?F`$ がうまく見つかって相対随伴系（相対スード随伴系）が作れるとさらに面白くなります。ホム圏のあいだに次の圏同値（$`\overset{\sim}{\equiv}`$ と書く）があります。
$`\text{For }A\in |\cat{S}|\\
\text{For }X\in |\cat{T}|\\
\quad \cat{T}(F(A), X) \overset{\sim}{\equiv} \mbf{CAT}(J(A), K(X))
`$
これは、関手意味論（より一般には変換手意味論、「変換手意味論とブラケット記法」、「続・変換手意味論とブラケット記法」参照）が二種類の方法で与えられることを意味します。
相対モナドの全域化
通常の随伴系やモナドを示すために、アーカー〈Nathanael Arkor〉達は形容詞「非相対〈non-relative〉」を使っています。absolute は使いたくなかったのでしょう。が、「相対」と「非相対」では排他的印象があるので、ここでは「非相対」の代わりに「全域〈total〉」を使います。
全域モナド（普通のモナド） $`F`$ は、ルート関手が恒等関手である相対モナドです。相対モナドの描き方で次の図になります。
$`\quad \xymatrix{
\cat{E} \ar[r]_{\mrm{Id}_\cat{E}} \ar@{}@/^/[r]|{/} \ar@/^1pc/[r]^F
&\cat{E}
}\\
\quad \In \mbf{CAT}
`$
全域モナド $`F`$ を、関手 $`J:\cat{A} \to \cat{E}`$ で引き戻すと相対モナド $`T = J*F`$ が得られます。$`J*F`$ と $`F`$ の関係は、通常、“制限”と“拡張”と呼ばれますが、“拡張”がクライスリ拡張と混同されるのが嫌なので、“打ち切り〈truncation〉”と“延長〈prolongation〉”と呼ぶことにします。$`J`$ によるプレ結合が打ち切りです。
相対モナド（全域モナド含む）の台関手に関して、打ち切りと延長が随伴系を形成する（下図）と嬉しいです。
$`\quad \xymatrix{
{[\cat{E}, \cat{E}]} \ar@/^/[r]^{\mrm{Trunc}_J}
\ar@{}[r]|{\top}
&{[\cat{A}, \cat{E}]}\ar@/^/[l]^{\mrm{Prol}_J}
}\\
\quad \In \mbf{CAT}
`$
ここで、$`\mrm{Trunc}_J(F) = J*F`$ で以下の“自然なホムセット同型”が成立します。
$`\text{For }T: \cat{A}\to \cat{E} \In \mbf{CAT}\\
\text{For }F: \cat{E}\to \cat{E} \In \mbf{CAT}\\
\quad [\cat{E}, \cat{E}](\mrm{Prol}_J(T), F)\cong [\cat{A}, \cat{E}](T, \mrm{Trunc}_J(F))
`$
こういう随伴系がいつでも存在するわけではなくて、関手 $`J`$ が良い性質（稠密性）を持たないとうまくいきません。関手 $`J`$ が良い関手の場合は、$`T:\cat{A}\to \cat{E}`$ に対して次の左カン拡張が存在します。
$`\quad \mrm{Lan}_J F : \cat{E}\to\cat{E} \In \mbf{CAT}`$
この $`\mrm{Lan}_J`$ が $`\mrm{Prol}_J`$ を与えます。
以上は、単なる関手の延長ですが、相対モナドの他の構成素達も適切に定義すると、相対モナドから全域モナドへの延長が出来ます。相対モナドの延長も同じく $`\mrm{Prol}_J`$ と書くと：
$`\quad \mrm{Prol}_J : \mrm{RelMnd}(J) \to x\mrm{Mnd}(\cat{E}) \In \mbf{CAT}`$
ここで、$`\mrm{RelMnd}(\hyp)`$ は相対モナド達の圏で、$`x\mrm{Mnd}(\hyp)`$ は全域モナド達の圏ですが、$`x`$ で象徴される何らかの条件が付きます。相対モナドの全域モナドへの延長は全域化〈totalization〉と言えます。すべての相対モナドが全域化できるわけではないですが、もし全域化できれば、通常のモナドの議論に持ち込めるので話が単純になります。
相対モナドの全域化はリントンの定理に関わります（「リントンの定理と相対モナド」参照）。
そしてそれから
相対モナドや相対随伴系は、存在していてもなかなか見つからない、一部が見えていても残りがよく分からないという事態がよくあります。
「形式言語理論にも使える導出系 // 圏類似代数系-導出系の相対随伴」で述べた圏類似代数系-導出系の相対随伴とか、「自由拡張原理： 最も簡単な場合」で述べたアタッチメント-コンテイメント随伴系のより一般的な場合とか、ボンヤリとは見えているのですが、まだ現実のものというより、僕の白昼夢のなかに居ます。
*1:随伴系が見つかったらすぐに注目すべきことは「随伴系の十項目（ショートチートシート）」にあります。
