多項式コモナドの準同型 ≃ Retrofunctor

\gdef\id{\mathop{\mathrm{id}}} \gdef\comp{\circ} \gdef\placeholder{{-}} \gdef\setsum{\operatorname{\raisebox{-0.2em}{$\Large\Sigma$}}} \gdef\setprod{\operatorname{\raisebox{-0.2em}{$\Large\Pi$}}} \gdef\Set{\mathrm{\mathbf{Set}}} \gdef\Cat{\mathrm{\mathbf{Cat}}} \gdef\Functors#1{\mathrm{\mathbf{Fun}}\left({#1}\right)} \gdef\Monads#1{\mathrm{\mathbf{Monads}}\left({#1}\right)} \gdef\Comonads#1{\mathrm{\mathbf{Comonads}}\left({#1}\right)} \gdef\CatC{\Cat^\sharp} \gdef\Ob{\mathop{\mathrm{Ob}}} \gdef\Mor{\mathop{\mathrm{Mor}}} \gdef\dom{\mathop{\mathrm{dom}}} \gdef\cod{\mathop{\mathrm{cod}}} \gdef\map{\mathop{\mathrm{map}}} \gdef\binprod{\mathbin{\Pi}} \gdef\bincoprod{\mathbin{\amalg}} \gdef\Id{\mathrm{Id}} \gdef\homset#1#2#3{{#1}\! \left\lbrack {#2}, {#3} \right\rbrack} \gdef\homsetl#1#2{{#1}\! \left\lbrack {#2} \right\rbrack} \gdef\asfunctor#1{\left. \llbracket {#1} \rrbracket^{c} \right.} \gdef\Cont{\mathrm{\mathbf{Cont}}} \gdef\Poly{\mathrm{\mathbf{Poly}}} \gdef\PolyFunctor#1{\mathrm{\mathbf{PFun}}\left({#1}\right)} \gdef\contcomp{\lhd} \gdef\inl{\operatorname{\mathtt{inl}}} \gdef\inr{\operatorname{\mathtt{inr}}} \gdef\divleft#1#2{\frac{{#1}, \_}{{#1}, {#2}}} \gdef\divright#1#2{\frac{\_, {#2}}{{#1}, {#2}}} \gdef\rootpos{o} \gdef\nextshape{\darr} \gdef\posplus{\oplus} \gdef\retroarr{\nrightarrow}

この記事は、以前から投稿している「多項式コモナドと小さい圏の対応」関連のシリーズです。

• 射の分割をもつ圏
• 解説: Directed Containers as Categoires

多項式コモナドの圏 ＝ ??? (≠ 小さい圏の圏)

前回の記事では、文献(“Directed Containers as Categories”)の 解説として「多項式コモナドと小さい圏には(同型を除いて)1対1の対応が付く」ことを解説しました。 しかし、「1対1の対応が付く」だけでは不満が残る点があります。

（あらゆる数学的構造がそうであるように、）コモナドは個々のコモナドを別々に考えるのではなく、それらの間の関係を調べることが大事であり、 通常はコモナド準同型というコモナドの間の自然変換を考え、それらを射とするコモナドの圏\Comonads{\Set}を考察対象とします。同じように、小さい圏は関手を射とする小さい圏の圏\Catを考えることが普通です。ここで「1対1の対応が付く」というのは、それらの圏の対象の間の対応がとれているという意味でしかなく、射については何一つ言及できていません。

実際、前回の記事でも少し述べましたが、多項式コモナドの圏（\Comonads{\Set}の部分圏）と小さい圏の圏\Catの射は対応しません。そこで、射として関手ではなくコモナド準同型と正確に対応する何かを考えた新しい圏\CatCを考えることにします。 この何かはcofunctorあるいはretrofunctorと呼ばれています。

この記事では以下の参考文献に基づきcofunctor, retrofunctorを解説していきます。 この参考文献においては(おそらくcofunctorの定義が先行する文献内で微妙にブレているため?)retrofunctorという名称を(新たに?)用いており、本記事ではそれに倣い、以降はretrofunctorに呼称を統一します。

• Nelson Niu and David I. Spivak, “Polynomial Functors: A Mathematical Theory of Interaction,” https://github.com/ToposInstitute/poly/blob/pdf/poly-book.pdf

  • Retrofunctorの定義は§7.3 (2025年1月現在)

この記事の内容は特筆しない限り上記の文献に基づきます。また、上記文献は現在も執筆が進んでいる途中のようであることに注意してください。私はここで解説する内容に大きな修正はないだろうと予想していますが、 章番号の変化などはあるでしょう。

「多項式コモナドの準同型」からretrofunctorへ

多項式コモナドの準同型と対応する「小さい圏の間の射」を考えることで、retrofunctorの定義を導出します。

前回の記事で述べたことをまとめると、多項式関手W = \asfunctor{S,P}を台とするコモナドは、directedコンテナ(S,P,\rootpos, \nextshape, \posplus)として以下のように記述でき、

\begin{align} \begin{aligned} W(\placeholder) &= \setsum (s \in S). \left( Ps \to \placeholder \right) \\ &= \set{ (s,v) | s \in S, v \in Ps \to \placeholder } \\ \operatorname{extract}_{W} (s,v) &= v(\rootpos_s) \\ \operatorname{duplicate}_{W} (s,v) &= \left( s, \lambda p. \left( s \nextshape p, \lambda p'. v(p \posplus_{s} p') \right) \right) \end{aligned} \end{align}

directedコンテナは小さい圏Cと以下の式によって1対1に対応します。

\begin{align} S &= \Ob(C) \\ Ps &= \homsetl{C}{s} \notag\\ &= \set{ p | p \in \Mor(C), \dom p = s } \\ \rootpos_s &= \id_s \\ s \nextshape p &= \cod p \\ p \posplus_{s} p' &= p;p' \end{align}

ここからdirectedコンテナの定義を消去すると、以下の通り多項式コモナドWと小さい圏Cを直接関係付ける式が得られます。¹

\begin{align} W(\placeholder) &= \setsum (c \in \Ob(C)). (\homsetl{C}{c} \to \placeholder) \\ &= \set{ (c,v) | c \in \Ob(C), v \in \homsetl{C}{c} \to \placeholder } \notag \\ \operatorname{extract}_{W}(c,v) &= v(\id_{c}) \\ \operatorname{duplicate}_{W}(c,v) &= (c, \lambda p. (\cod p, \lambda p'. v(p;p')) ) \end{align}

この対応関係を用いて、多項式コモナドWとW'の間のコモナド準同型、 すなわちコモナド演算を保つような自然変換\tau_a : Wa \to W'aが、 小さい圏については何を表すのかを求めていきます。

\begin{align} \operatorname{extract}_{W'} \comp \tau &= \operatorname{extract}_{W} \\ \operatorname{duplicate}_{W'} \comp \tau &= \map_{W'} \tau \comp \tau \comp \operatorname{duplicate}_{W} \end{align}

多項式コモナドW,W'は小さい圏C,Dをそれぞれ用いて上記のように表現されているとします。 多項式関手の間の自然変換はどれも、一定の方法でコンテナの射(t,q)として表すことができます。自然変換\tau_a : Wa \to W' aをコンテナの射(t,q)として表すと以下のようになります。

\begin{align} \tau_a(c,v) &= (tc, v \comp qc) \end{align}

ここで(t,q)はそれぞれ以下のような型をもった関数です。

\begin{align} t &: \Ob(C) \to \Ob(D) \\ q &: \setprod (c : \Ob(C)). \homsetl{D}{tc} \to \homsetl{C}{c} \end{align}

このコンテナの射は、CからDへの関手に似て非なるものになっています。 関手のごとくtはCの対象cをDの対象tcへ送る写像ですが、 コンテナの射のもう一部qはDの射p : \homsetl{D}{tc}をCの射qcp' : \homsetl{C}{c}に送ります。通常の関手と違い、対象と射で逆の方向に送る写像で定義されているのです！

また、関手は恒等射と射の合成を保つという性質も持つ必要がありました。コモナド準同型\tauも、それがコモナド演算を保つ必要があるため、それに対応して(t,q)にも満たすべき性質があります。

コモナド演算のうち\operatorname{extract}を保つという性質を考えると、

\begin{align} \operatorname{extract}_{W'} (\tau(c,v)) &= \operatorname{extract}_{W}(c,v) \notag \\ (v \comp qc)(\id_{tc}) &= v(\id_c) \notag \\ v(qc(\id_{tc})) &= v(\id_c) \notag \end{align}

であり、vは任意の関数であったので

\begin{align} qc(\id_{tc}) &= \id_c \end{align}

を得ます。また、\operatorname{duplicate}を保つという性質から

\begin{align*} \operatorname{duplicate}_{W'} (\tau(c,v)) &= (\map_{W'} \tau \comp \tau \comp \operatorname{duplicate}_{W})(c,v) \\ \text{左辺} &= \operatorname{duplicate}_{W'} (\tau(c,v)) \\ &= \operatorname{duplicate}_{W'} (tc, v \comp qc) \\ &= (tc, \lambda p. (\cod p, \lambda p'. (v\comp qc) (p;p') ))\\ \text{右辺} %= (\map_{W'} \tau \comp \tau \comp \operatorname{duplicate}_{W})(c,v) \\ &= (\map_{W'} \tau \comp \tau)(c, \lambda p. (\cod p, \lambda p'. v(p;p'))) \\ &= \map_{W'} \tau (tc, \lambda p. (\cod (qcp), \lambda p'. v(qcp; p'))) \\ &= (tc, \lambda p. (t (\cod (qcp)), \lambda p. v(qcp; q(\cod(qcp))p'))) \end{align*}

です。両辺の比較から、まず任意のc : \Ob(c)とp : \homsetl{D}{tc}について

\begin{align} \cod p &= t(\cod (qcp)) \end{align}

であり、加えて任意のp' : \homsetl{D}{\cod p}について

\begin{gather} qc(p;p') = qcp; qc'p' \\ \quad \quad \text{where} \quad c' = \cod(qcp) : \Ob(C) \end{gather}

を得ます。

Retrofunctorは、単にここから(t,q)の記号を変更したものです。

(定義) Retrofunctor

C,Dを小さい圏とする。Retrofunctor F : C \retroarr Dとは、

• 対象について順方向の関数 F : \Ob(C) \to \Ob(D)²
• 射について逆方向の関数 F_{c}^{\sharp} : \homsetl{D}{Fc} \to \homsetl{C}{c}

からなり、以下の性質をすべて満たすもののことである。

1. 恒等射を保つ。 任意のc \in \Ob(C)について次式が成り立つ。

   F_{c}^{\sharp} \id_{Fc} = \id_{c}

2. 余域(\cod)を保つ。 任意のc \in \Ob(C)とg \in \homsetl{D}{Fc}について次式が成り立つ。

   F(\cod F_{c}^{\sharp} g) = \cod g

3. 合成を保つ。 任意のc \in \Ob(C)と g \in \homsetl{D}{Fc}, h \in \homsetl{D}{\cod g}について次式が成り立つ。

   F_{c}^{\sharp} (g; h) = F_{c}^{\sharp} g; F_{c'}^{\sharp} h

   ただしc' = \cod F_{c}^{\sharp} g \in \Ob(C)とおいた。³

Retrofunctorは、もともと圏を成している多項式コモナドの射に対応しているので、それ自体も「retrofunctorを射とする圏」を作ることができます。小さい圏を対象、retrofunctorを射とする圏を\CatCと表記することにします。 構成の仕方から、\CatCは多項式コモナドの圏と圏同値です。

Retrofunctorの気持ち

ここで定義したretrofunctorF : C \retroarr Dは、あまり直感的に理解できない概念かと思います。 Retrofunctorの気持ちの一つとして、「retrofunctorはユーザーインターフェースのようなものである」という たとえ話ができます。

• 小さい圏Cを、ある機械(“本体”)だとみなします。対象c \in \Ob(C)はこの機械の状態であり、 射f \in \homset{C}{c}{c'}はこの機械が状態cからc'へ移行するなんらかの操作を表していると考えます。

• 小さい圏Dも同じように、別の機械(“リモコン”)だと考えます。

• RetrofunctorF : C \retroarr Dは、機械D(“リモコン”)が機械C(“本体”)の ユーザーインターフェースとして振る舞っていることを表します。

  • 対象についての写像F(-) : \Ob(C) \to \Ob(D)は、“本体”Cの状態から、 “リモコン”Dの状態が決まる、ということを表します。

  • 射についての写像F_c^{\sharp} : \homsetl{D}{Fc} \to \homsetl{C}{c}は、 “本体”の状態がcにあるとき、 “リモコン”の状態を現在のFcから別のdへ動かす操作gを “本体”に対する操作F_c^{\sharp} gに変換する写像です。

    • 恒等射を保つ性質は、リモコンに対して何もしない操作\id_{Fc}は、 本体に対しても何も変化させないことを表します。

    • 余域を保つ性質は、リモコンと本体に対する操作の結果としてたどりつく状態が、 状態の写像Fと整合していることを表します。

      リモコンの状態をdに変える操作g \in \homset{D}{Fc}{d}を本体への操作にした F_c^{\sharp}gが本体の状態をc'へと変えるものであるならば（\cod (F_c^{\sharp}g) = c'）、 その状態をリモコンに反映するとFc'=dとなり、リモコン単独で見たときの状態遷移と整合します。

    • 合成を保つ性質は、リモコン上の操作の合成が、本体に対する操作の合成と整合していることを表します。

Retrofunctorを射とする圏\CatC

圏\CatCの、圏論的な性質をいくつか見てみましょう。

余積+

任意の圏C_1とC_2から、それらの圏の余積C_1 + C_2を定義できます。 直観的には、C_1 + C_2はC_1とC_2の対象と射を、互いに関係のないまま足しただけの圏です。 もう少し丁寧に述べると、C_1 + C_2は次のような圏です。

• 対象はそれぞれの圏の対象の直和\Ob(C_1 + C_2) = \Ob(C_1) + \Ob(C_2)

• 射もそれぞれの圏の射の直和

  \begin{align*} \Mor(C_1 + C_2) &= \Mor(C_1) + \Mor(C_2) \\ \dom(\inl c_1) &= \inl (\dom c_1) \\ \dom(\inr c_2) &= \inr (\dom c_2) \\ \cod(\inl c_1) &= \inl (\cod c_1) \\ \cod(\inr c_2) &= \inr (\cod c_2) \end{align*}

• 射の合成は元の圏と同じものを使う。元の圏が異なる射どうしは合成可能でない。

小さい圏の余積は、名前が示唆するように、\Catにおける余積になっています。すなわち、 和を構成する関手I_1 : C_1 \to C_1 + C_2, I_2 : C_2 \to C_1 + C_2 と、和の普遍性を持ちます。すなわち任意の関手の組(G_i : C_i \to D)_iに対して、 G_i = G \comp I_iとなるような関手G : C_1 + C_2 \to Dが一意に存在します。

また、空な圏0、すなわち対象を全くもたない圏を”ゼロ個の圏の余積”とみなすことができます。

そして、+は\CatCにおいても余積になっています。

• 和を構成するretrofunctor\tilde{I}_1, \tilde{I}_2は以下のように定義できます。 （I_1の場合だけ示します）

  • 対象における写像は関手I_1と同じです。

    \tilde{I}_1(c_1) = \inl c_1

  • 射についての写像\tilde{I}_{1,c}^{\sharp} : \homsetl{(C_1+C_2)}{\tilde{I}_1(c)} \to \homsetl{C_1}{c} において、定義域となる射の集合\homsetl{(C_1+C_2)}{\tilde{I}_1(c)}は

    \begin{align*} \homsetl{(C_1+C_2)}{\tilde{I}_1(c)} &= \set{ f | f \in \Mor(C_1+C_2), \dom(f) = \inl c } \\ &= \set{ \inl f | f \in \Mor(C_1), \dom(f) = c } \\ &= \set{ \inl f | f \in \homsetl{C_1}{c} } \\ \end{align*}

    であり、これは単射\inlによる\homsetl{C_1}{c}の像です。 \tilde{I}_{1,c}^{\sharp}は\inlを外す写像として定義でき、 そうするとretrofunctorとなるために必要な性質を満たします。

普遍性については省略しますが、そちらも素直に定義できます。

また、ここでは2個の小さい圏の和を書きましたが、任意の和 （任意の大きさの集合Jで添字付けられた小さい圏の族C_jの和） も同様に定義できます。

並行積\otimes

任意の圏C_1, C_2に対して、圏の積C_1 \otimes C_2を以下のように定義します。⁴

• \Ob(C_1 \otimes C_2) = \Ob(C_1) \times \Ob(C_2)
• \homset{(C_1 \otimes C_2)}{(c_1,c_2)}{(c_1',c_2')} = \homset{C_1}{c_1}{c_1'} \times \homset{C_2}{c_2}{c_2'}

名前の通り、これは\Catにおける（圏論的）積になっており、 射影関手\pi_1 : C_1 \otimes C_2 \to C_1, \pi_2 : C_1 \otimes C_2 \to C_2と、 積の普遍性を持ちます。すなわち、任意の関手の組G_1 : D \to C_1, G_2 : D \to C_2に対して、 G_i = \pi_i \comp G(i=1,2)となる関手G : D \to C_1 \otimes C_2が一意に存在します。

ゼロ個の圏の積である終圏1も存在します。この圏は対象がただ1つで、射もその対象における恒等射を1つだけをもつ圏であり、 圏の同型C \otimes 1 \cong C \cong 1 \otimes Cが成り立ちます。

余積の場合と異なり、\CatCにおいてはC_1 \otimes C_2はC_1とC_2の（圏論的）積ではありません。⁵ 射影関手に相当する”射影retrofunctor”は作ることができますが、それらは積の普遍性を満たしません。 そこで、\CatCの文脈においては、圏の積\otimesのことを並行積(parallel product)と呼ぶことにします。

圏論的積でこそありませんが、並行積は\CatCにおけるモノイド積になっています。 \Catにおける同型は\CatCにおける同型でもあるので、 \otimesが\CatCにおいて(双)関手になってさえいれば、 \Catにおいて\otimes, 1がモノイド積になっている⁶ことから \CatCにおいてもモノイド積になっていることが従います。

そして、\otimesは関手\CatC \times \CatC \to \CatCにできます。 \otimesが関手であるとは、 \CatC \times \CatCの射であるretrofunctorの組(F : C_1 \retroarr D_1, G : C_2 \retroarr D_2) が与えられたとき、retrofunctor(F\otimes G) : C_1 \otimes C_2 \retroarr D_1 \otimes D_2が構成でき、 それが恒等retrofunctorとretrofunctorの合成を保つことです。

Retrofunctor(F\otimes G) : C_1 \otimes C_2 \retroarr D_1 \otimes D_2は次のように定義できます。

• 対象に関して (F\otimes G)(c_1,c_2) = (Fc_1, Gc_2)
• 射に関して (F\otimes G)_{(c_1,c_2)}^{\sharp} (h_1, h_2) = (F_{c_1}^{\sharp} h_1, G_{c_2}^{\sharp} h_2)

これがretrofunctorとしての性質をもつこと、恒等射と合成を保つことは証明が必要ですが省略します。

“射の分割をもつ圏” = 並行積\otimesに関する半群対象

以前の記事で述べた射の分割をもつ圏は、 圏\CatCを用いて簡潔に記述できます。 射の分割をもつ圏の定義を再度書くと、以下のようになります。

射の分割をもつ圏

射の分割をもつ圏とは、小さい圏Cであって、更に

• （対象の集合を半群にする）結合的な二項演算(\cdot) : \Ob(C) \times \Ob(C) \to \Ob(C)

• 各対象a,b \in \Ob(C)について 射の分割

  \begin{align*} \divleft{a}{b} &: \homsetl{C}{a\cdot b} \to \homsetl{C}{a} \\ \divright{a}{b} &: \homsetl{C}{a\cdot b} \to \homsetl{C}{b} \\ \end{align*}

をもち、以下の性質を満たすもののことである。

1. 射の分割が半群演算と両立する。Cの射t \in \homsetl{C}{a\cdot b\cdot c}に対して、

   \begin{align*} \divleft{a}{b} \left( \divleft{a\cdot b}{c} t \right) &= \divleft{a}{b \cdot c} t \\ \divright{b}{c} \left( \divright{a}{b\cdot c} t \right) &= \divright{a \cdot b}{c} t \\ \divright{a}{b} \left( \divleft{a\cdot b}{c} t \right) &= \divleft{b}{c} \left( \divright{a}{b\cdot c} t \right) \end{align*}

2. 射の分割は恒等射を保つ。

   \begin{align*} \divleft{a}{b}\id_{a\cdot b} &= \id_a \\ \divright{a}{b}\id_{a\cdot b} &= \id_b \end{align*}

3. 射の分割が終域を保つこと。Cの射t \in \homsetl{C}{a\cdot b}に対して、

   \begin{equation} \cod \left( \divleft{a}{b} t \right) \cdot \cod \left( \divright{a}{b} t \right) = \cod t \end{equation}

4. 射の分割が射の合成を保つこと。以下のように合成できる射t,uがあるとする。

   \begin{CD} {a\cdot b} @>t>> c @>u>> d \end{CD}

   このとき、以下が成り立つ。

   \begin{align*} 　　　　\divleft{a}{b} \left(t;u\right) &= \left(\divleft{a}{b} t\right); \left(\divleft{c_a}{c_b} u\right) \\ 　　　　\divright{a}{b} \left(t;u\right) &= \left(\divright{a}{b} t\right); \left(\divright{c_a}{c_b} u\right) \end{align*}\\ \begin{align*} \qquad \text{where} \begin{cases} c_a &= \cod\left(\divleft{a}{b} t\right) \\ c_b &= \cod\left(\divright{a}{b} t\right) \end{cases} \end{align*}

この定義の見方を少し変えると、これがretrofunctorを使って定義できることに気が付きます。 まず、二項演算(\cdot)を関数Mとして書きます。

\begin{align*} & M : \Ob(C) \times \Ob(C) \to \Ob(C) \\ & M(a,b) = a \cdot b \end{align*}

また、左右の射の分割を一つの関数M_{(a,b)}^{\sharp}にまとめて書きます。

\begin{align*} & M_{(a,b)}^{\sharp} : \homsetl{C}{M(a,b)} \to \homsetl{C}{a} \times \homsetl{C}{b} \\ & M_{(a,b)}^{\sharp}(t) = \left( \divleft{a}{b} t, \divright{a}{b}t \right) \end{align*}

並行積の定義から、これらの関数の型はretrofunctorM : C \otimes C \retroarr Cと一致しています。

\begin{align*} M &: \Ob(C \otimes C) \to \Ob(C)\\ M_{(a,b)}^{\sharp} &: \homsetl{C}{M(a,b)} \to \homsetl{(C\otimes C)}{(a,b)} \end{align*}

更に、射の分割の性質2.-4.はそのままMがretrofunctorC \otimes C \retroarr Cであるための条件に該当します。すなわち、Mはretrofunctorであり、逆にこのようなretrofunctorは射の分割のうち2.-4.だけを満たすものに合致します。

残りの条件である「演算\cdotが結合的であること」と「射の分割の性質1.」を合わせると、retrofunctor Mが結合法則を満たすという、(C,M)が半群対象であるための条件に合致します。すなわち、

射の分割をもつ圏

射の分割をもつ圏Cとは、\CatCにおける\otimesに関する半群対象 (C, M : C\otimes C \retroarr C)のことである。

と簡潔にまとめられます。単位的な射の分割をもつ圏も、同様にして

単位的な射の分割をもつ圏

単位的な射の分割をもつ圏Cとは、\CatCにおける\otimesに関するモノイド対象 (C, M : C\otimes C \retroarr C, E : 1 \retroarr C)のことである。

と簡潔に定義できます。