ナタリエル・アーカー〈Nathanael Arkor〉のトーク動画の322秒あたり（下のURL）からの話が面白かったので紹介します。アーカーは相対モナドについて語っていますが、この記事では普通のモナドの場合に限定します。$`\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mbf}[1]{ \mathbf{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\id}{ \mathrm{id}}
\newcommand{\In}{ \text{ in }}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\T}[1]{ \text{#1} }
\require{color}
\newcommand{\red}[1]{ \textcolor{red}{#1}}
\newcommand{\blue}[1]{ \textcolor{blue}{#1}}
`$
- https://www.youtube.com/watch?v=RguqGBhSEOc&t=322s ("Arkor - The formal theory of theories" Category Theory CT20->21)
内容：
クライスリ包含
$`M`$ を、圏 $`\cat{C}`$ 上のモナド〈monad over $`\cat{C}`$ 〉だとします。このことを記号の乱用（と略記）で次のように書きます。
$`\quad M = M/\cat{C} = (M, \mu, \eta)/\cat{C}`$
モナド $`M`$ のクライスリ圏は次のように書きます。
$`\quad \mrm{Kl}(M) = \mrm{Kl}(M/\cat{C})`$
とある圏 $`\cat{K}`$ が、モナド $`M`$ のクライスリ圏と圏同値になるか？ という問題を考えます。$`\cat{K}`$ だけを見ていてもさすがに分からないので、次のような関手を一緒に考えます。
$`\quad J:\cat{C} \to \cat{K} \In \mbf{CAT}`$
関手 $`J`$ に条件を付けて、$`K`$ が $`\mrm{Kl}(M/\cat{C})`$ と圏同値になると結論したいわけです。結果的に、圏同値より強く圏同型が言えます。
関手 $`J`$ に条件を付けた関手をクライスリ包含〈Kleisli inclusion〉と呼ぶのですが、混乱を避けるために二種類のクライスリ包含を区別します。
- 具象クライスリ包含〈concrete Kleisli inclusion〉： 圏 $`\cat{C}`$ から、実際のクライスリ圏 $`\mrm{Kl}(M/\cat{C})`$ への標準的関手 $`\cat{C} \to \mrm{Kl}(M/\cat{C})`$
- 抽象クライスリ包含〈abstract Kleisli inclusion〉： 圏 $`\cat{C}`$ からとある圏 $`\cat{K}`$ への関手、条件は付く。
具象クライスリ包含は、対象上で恒等〈identity-on-objects | i.o.o.〉で、射に関しては、
$`\quad (f:A\to B) \mapsto (f;\eta_B : A \to M(B))`$
で与えられます。
具象クライスリ包含も抽象クライスリ包含も、「包含」と呼んでいるだけで、包含関手／埋め込み関手であることを要求していません。例えば、クラッシュモナドの具象クライスリ包含は、まったく包含になっていません。呼び名から、要求してない余計な条件を類推しないでください！
クラッシュモナド $`\mrm{Crush}`$ については：
$`J:\cat{C} \to \cat{K} \In \mbf{CAT}`$ が抽象クライスリ包含である条件〈公理 | 法則〉は以下です。
- 対象上で恒等〈i.o.o.〉な関手である。つまり、$`|\cat{C}|=|\cat{K}|`$ で、$`J_\mrm{obj} = \id_{|\cat{C}|}`$
- $`J`$ は左随伴関手である。
ここで、「左随伴関手である」は、とても分かりにくい圏論特有の“良くない言い回し”だと思うので次節で説明します。
左随伴関手である とは
$`J:\cat{C} \to \cat{K}\In \mbf{CAT}`$ が左随伴関手である〈is a left adjoint functor〉とは、$`J`$ が左随伴関手になり得る〈can be a left adjoint functor〉ことです。さらに言い回しをブレークダウンすると：
- $`J`$ は左随伴関手になり得る。
- $`J`$ を左随伴関手とする随伴系〈adjunction | adjoint system〉が存在する。
- とある随伴系が存在して、$`J`$ はその随伴系の左関手の役割りを担う。
「$`J`$ は右随伴関手を持つ（ことが可能）」とも言います。言い回しが違っても同じことです。
随伴系は、構成素〈constituent〉達から構成される構造です。構造を指標で記述すると以下のようになります。この指標は過去記事「 構造を持つ概念的事物の記述と参照： コンパニオンを例に」からの再掲で、説明は過去記事にあります。
$`\T{signature }\T{AdjointSystem }\:\{\\
\quad \red{\cat{D}} \In \mbf{Cat}\\
\quad \blue{\cat{C}} \In \mbf{Cat}\\
\quad \red{R} : \red{\cat{D}}\to \blue{\cat{C}} \In \mbf{Cat} \\
\quad \blue{L} : \blue{\cat{C}}\to \red{\cat{D}} \In \mbf{Cat} \\
\quad \red{\eta} :: \mrm{Id}_{ \blue{\cat{C}}} \twoto \blue{L} * \red{R} : \blue{\cat{C}}\to\blue{\cat{C}} \In \mbf{Cat} \\
\quad \blue{\varepsilon} : \red{R}*\blue{L} \twoto \mrm{Id}_{\red{\cat{D}}} : \red{\cat{D} } \to\red{\cat{D}} \In \mbf{Cat} \\
\quad \red{\text{snake-1}} ::: (\mrm{ID}_{\red{R}} * \red{\eta});(\blue{\varepsilon}*\mrm{ID}_{\red{R}}) \Rrightarrow \mrm{ID}_{\red{R} }\\
\quad \blue{\text{snake-2}}::: (\red{\eta} * \mrm{ID}_{\blue{L}});(\mrm{ID}_{\blue{L} }* \blue{\varepsilon} ) \Rrightarrow \mrm{ID}_{\blue{L}}\\
\}
`$
今の場合は、“とある随伴系”〈some adjunction〉の役割り $`L`$（左関手）に相当するのが $`J`$ ということです。左関手 $`J`$ に対応する右関手を $`G`$ とすると、次のように書けます。
$`\quad \xymatrix@C+1.5pc{
\cat{C} \ar@/^1pc/[r]^{J}
\ar@{}[r]|{\bot}
&\cat{K} \ar@/^1pc/[l]^{G}
}`$
随伴系の単位／余単位やニョロニョロ関係式は暗黙に想定されます。
随伴系はホムセット同型を伴うので、次のような同型（の族）があります。
$`\text{For }A\in |\cat{C}|, Y\in |\cat{K}|\\
\quad \cat{K}(J(A), Y) \cong \cat{C}(A, G(Y)) \In \mbf{Set}
`$
$`J`$ が対象上で恒等〈i.o.o.〉だったので、$`J(A) = A`$ です。なので、ホムセット同型は次のように書けます。
$`\quad \cat{K}(A, Y) \cong \cat{C}(A, G(Y)) \In \mbf{Set}`$
言い換えると、次のような一対一対応があります。
$`\quad (A \to Y \In \cat{K}) \longleftrightarrow (A \to G(Y)\In \cat{C})`$
ここまで来ると、$`\cat{K}`$ の射がクライスリ射である“感じ”が強くします。“感じ”を事実とするには、随伴関手ペア $`J \dashv G`$ からモナドを構成して、そのクライスリ圏と圏 $`\cat{K}`$ を比較すればいいのです。ホムセットごとの同型を寄せ集めて圏同型関手を構成できます。
これにより、抽象クライスリ包含は具象クライスリ包含であることが分かります。「抽象／具象」を取り去って、単にクライスリ包含と呼ぶことが正当化〈justify〉されます。
