リントンの定理に関して、また妄想が湧いてしまった。いやー、妄想が捗りますわ。
「セオリー」という言葉は使いにくいですが、代替が無いので使います（「「セオリー」は使わざるをえないな」参照） 。通常、「セオリーのモデル」といいますが、ここでは「セオリーの表現〈representation〉」と呼びます。その理由は：
- 「指標のモデル」と「セオリーの表現」と使い分けたい。
- 「表現」は、「群の線形表現」とか「環の表現」とかの表現と同じ使い方。
リントンの定理（「リントンの定理」、「リントンの定理： 概要、実例、注意事項」参照）は、次の2つの主張からなります。
- モナド-セオリー対応： モナドの圏とセオリーの圏は圏同値になる。
- 代数-表現対応： モナド-セオリー対応で互いに対応するモナドとセオリーがあるとき、モナドのアイレンベルク／ムーア代数達の圏とセオリーの表現達の圏は圏同値になる。
僕の妄想をかきたてたのは、ヴォエヴォドスキーの論文 "Lawvere theories and Jf-relative monads" です。実際のところ、アブストラクトを読んだくらいなんですが(苦笑)。$`
\newcommand{\EQV}{\mathrel{\overset{\sim}{\equiv}} }
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mbf}[1]{ \mathbf{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\u}[1]{ \underline{#1} }
\newcommand{\In}{ \text{ in }}
\newcommand{\hyp}{\text{－} }
`$
ヴォエヴォドスキーによると、次の圏同値があります。
$`\quad \mbf{LawTh} \EQV \mrm{RelMnd}(J : \mbf{F} \to \mbf{Set})`$
ヴォエヴォドスキー論文と記法は少し変えていますが、ここで：
- $`\mbf{LawTh}`$ は、ローヴェア・セオリー達の圏
- $`\EQV`$ は、圏同値
- $`\mrm{RelMnd}(\hyp)`$ は、相対モナド〈relative monad〉達の圏、括弧内には相対モナドのルート関手〈root functor〉（すぐ下参照）が入る。
- $`\mbf{F}`$ は、有限集合達の圏 $`\mbf{FinSet}`$ の標準骨格〈canonical skeleton〉
- $`J`$ は、部分圏 $`\mbf{F}`$ を $`\mbf{Set}`$ にそのまま埋め込む包含関手
アーカー／マクダルメット〈Nathanael Arkor, Dylan McDermott〉達は、相対モナドの基礎となる関手をルート関手〈root functor〉、あるいは単にルート〈root〉と呼んでます（例えば、"The formal theory of relative monads" 参照）。これは非常に便利な用語で、相対随伴、カン拡張の文脈でも「ルート」を使うことにします。
ヴォエヴォドスキーの主張に基づき、ローヴェア・セオリー達の圏を相対モナド達の圏だと思いましょう。すると、リントンの定理の前半部分は次のように書けます。
$`\quad \mrm{RelMnd}(J: \mbf{F} \to \mbf{Set}) \EQV \mrm{FMnd}(\mbf{Set})`$
ここで、$`\mrm{FMnd}(\hyp)`$ は有限項モナド〈finitary monad〉達の圏です。括弧に入るのは今のところ集合圏ですが、アリティ付き圏〈category with arities〉なら意味を持つでしょう。
この形にすると、リントンの定理の前半は、相対モナド達の圏と有限項モナド達の圏の圏同値を主張していることになります。このような主張をするには、ルート関手 $`J`$ が重要で、$`J`$ がなんでもいいわけではありません。
関手がアリティ関手〈arity functor〉だとは次のことだと定義します。
- その関手は充満忠実関手〈fully faithful functor〉である。
- その関手は稠密関手〈dense functor〉である。
アリティ関手の域圏が小さい圏のとき小さいアリティ関手〈small arity functor〉と呼ぶことにします。上記の $`J`$ は小さいアリティ関手です。
$`J`$ がアリティ関手であることから、$`\mrm{RelMnd}(J) \EQV \mrm{FMnd}(\mbf{Set})`$ という圏同値が引き起こされるはずですが、この圏同値の根源は次の随伴関手ペアでしょう（おそらく）。
$`\quad \xymatrix{
{[\mbf{F}, \mbf{Set}]} \ar@/^1pc/[r]^{\mrm{Lan}_J}
\ar@{}[r]|{\bot}
&{[\mbf{Set}, \mbf{Set}]} \ar@/^1pc/[l]^{J^*}
}
\quad \In \mbf{CAT}
`$
ここで、$`J^*`$ は $`J`$ のプレ結合引き戻し、$`\mrm{Lan}_J`$ は $`J`$ をルート（先の記述参照）とする左カン拡張です。
相対モナド $`R`$ の台関手 $`\u{R} : \mbf{F} \to \mbf{Set}`$ と（通常の）モナド $`M`$ の台関手 $`\u{M}: \mbf{Set} \to \mbf{Set}`$ が対応し、それに伴って相対モナドとモナドの対応も引き起こされるのだと思います。
この見方をすると、モナド-セオリー対応はモナド-相対モナド対応です。通常のモナドは相対モナドの特別なものなので、
- モナド-セオリー対応は、相対モナド-相対モナド対応
と言えます。
次に、リントンの定理の後半部分ですが、これは、圏 $`\mrm{RelMnd}(J)`$ 上のインデックス付き圏 $`\mrm{Repr}[\hyp]`$ と、圏 $`\mrm{FMnd}(\mbf{Set})`$ 上のインデックス付き圏 $`\mrm{EM}[\hyp]`$ のあいだのある種の同値性の主張です。
説明を端折って一言でいってしまうのですが； 表現達の圏 $`\mrm{Repr}[R]`$ もアイレンベルク／ムーア代数達の圏 $`\mrm{EM}[M]`$ も、右加群〈right module〉達の圏だと思えます。左右は約束で決まるので、「右」に絶対的な意味はありませんが、ともかく片側加群です。相対モナドに対して右加群の圏（同じことだがアイレンベルク／ムーア圏）が定義できて、相対モナドの“右加群の圏”の特殊ケースとしてモナドの“右加群の圏”が定義できます。
この見方をすると、代数-表現対応は（相対モナドの）右加群-右加群対応です。
- 代数-表現対応は、右加群-右加群対応
と言えます。
相対モナド（通常のモナド含む）を“環のようなもの”と考えて、相対モナドのアイレンベルク／ムーア圏を“右加群の圏のようなもの”と考えると、相対モナドの話は（可換とは限らない）環上の線形代数とのアナロジーがあります。そして、リントンの定理は相対モナドの話だと解釈できます、たぶん。
