\gdef\Set{\mathrm{\mathbf{Set}}} \gdef\Cat{\mathrm{\mathbf{Cat}}} \gdef\CatC{\Cat^\sharp} \gdef\Ob{\mathrm{Ob}} \gdef\Mor{\mathrm{Mor}} \gdef\id{\mathop{\mathrm{id}}} \gdef\dom{\mathop{\mathrm{dom}}} \gdef\cod{\mathop{\mathrm{cod}}} \gdef\homset#1#2#3{#1 \left\lbrack {#2}, {#3} \right\rbrack} \gdef\homsetl#1#2{#1 \left\lbrack {#2} \right\rbrack} \gdef\map{\mathop{\mathrm{map}}} \gdef\divleft#1#2{\frac{{#1}, \_}{{#1}, {#2}}} \gdef\divright#1#2{\frac{\_, {#2}}{{#1}, {#2}}} \gdef\setcompre#1#2{\left\lbrace {#1} \middle\vert {#2} \right\rbrace}
背景
前回の記事謎構造・「射の分割」ができる圏1で、 射の分割という演算を備えた圏を定義しました。
この定義を考えるモチベーションは、
小さい圏とComonad
が1対1に対応する2という事実から、
Comonad
でもApplicative
でもある関手f
を小さい圏で表現したとき、そのApplicative
の演算(pure
, <*>
)が圏においてどんな演算に対応するのか、という疑問です。
「Comonad
かつApplicative
」ではないですが、それ近い「Comonad
かつApply」はcomonadパッケージにて定義されており、
ComonadApplyという名前が与えられています。
この型クラスはもともと3において”symmetric (semi)monoidal comonad”として形式化されたものがベースになっているようです。
さて、前回の記事ではこの構造について謎ですとだけ言ったのですが、進展がありました。前記事でいうproperな射の分割をもつ圏は、
- 小さい圏を対象、retrofunctorを射として持つ圏\CatC4において、圏の直積に関するモノイド対象
であると考えられます。 このことを説明する記事を書きたいと思ったのですが、まずはその準備として、前記事とは異なる”射の分割を持つ圏”を再定義します。 定義を変えたい理由は4つあります:
- 前記事では横着して可換バージョンだけを定義したが、別にその必要はないこと
- 記法の変更がしたいこと
- properでない射の分割について考えたくなくなったのでproperなものだけを指して単に”射の分割を持つ圏”と呼びたいこと
Comonad
かつApply
であるものに対応する、半群に関する射の分割を考えたいこと
本記事は射の分割を持つ圏の新しい定義を行います。
射の分割の定義
局所小圏Cのホムセットを\homset{C}{a}{b}と書くことにします。 また、各ホムセットはそれぞれ共通部分を持たないとします。すなわち
\homset{C}{a}{b} \cap \homset{C}{a'}{b'} \neq \emptyset \implies \left( a = a' \wedge b = b' \right)
を仮定します。
小さい圏Cにおいて、始域がaである射を集めた集合を\homsetl{C}{a}と書くことにします。 各ホムセットは共通部分を持たないため、次式が成り立ちます。
\begin{equation} \begin{split} \homsetl{C}{a} &= \setcompre{t \in \Mor(C)}{\dom t = a} \\ &= \biguplus_{b \in \Ob(C)} \homset{C}{a}{b} \end{split} \end{equation}
射の分割を持つ圏 Cを、小さい圏Cであって、追加で
対象の集合上の半群演算(\cdot) : \Ob(C) \times \Ob(C) \to \Ob(C)
射の分割と呼ばれる、対象の組a,bそれぞれについて定まる関数の族
\begin{equation} \divleft{a}{b} : \homsetl{C}{a\cdot b} \to \homsetl{C}{a} \end{equation}
および
\begin{equation} \divright{a}{b} : \homsetl{C}{a\cdot b} \to \homsetl{C}{b} \end{equation}
を備え、それらが以下の条件をすべて満たすものと定義します。
射の分割が半群演算と両立すること。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}
射の分割が恒等射を保つこと。
\begin{align} \divleft{a}{b} \id_{a\cdot b} &= \id_{a} \\ \divright{a}{b} \id_{a\cdot b} &= \id_{b} \end{align}
射の分割が終域を保つこと。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}
射の分割が射の合成を保つこと。以下のように合成できる射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}
ただし、c_a, c_bはtの射の分割それぞれの終域とする。
\begin{align*} c_a &= \cod\left(\divleft{a}{b} t\right) \\ c_b &= \cod\left(\divright{a}{b} t\right) \end{align*}
単位的な射の分割を持つ圏Cを、射の分割を持つ圏Cであって、 対象1 : \Ob(C)を持ち、以下の条件を満たすものと定義します。
1が\Ob(C)のなす半群の単位元である(すなわち(\Ob(C),1,\cdot)はモノイドである)こと。
単位元による分割は「何もしない」こと。
\begin{align} \divleft{a}{1} t &= t \\ \divright{1}{b} t &= t \end{align}
1からそれ以外の対象への射を持たないこと。
射の分割をもつ圏の例
離散圏における射の分割
離散圏Dにおいて、 離散圏は恒等射以外を持たないため、「射の分割は恒等射を保つ」という性質から射の分割は完全に固定されており、 \Ob(D)上の半群(\cdot)(またはモノイド(1,\cdot))が与えられるだけで Dを射の分割を持つ圏(単位的な射の分割を持つ圏)にすることができます。
任意の圏の左零分割
任意の集合は、x\cdot y = xという2項演算によって半群とみなすことができます。 任意の小さい圏Cも、対象の上にこの2項演算を与え、射の分割を
\begin{align} \divleft{a}{b} t &= t \\ \divright{a}{b} t &= \id_{b} \end{align}
とするとこれは前節の条件をすべて満たし、Cを射の分割を持つ圏にできます。
Cがひとつの対象とひとつの恒等射のみを持つ圏\mathbb{1}でない限り、 これは単位的な射の分割を持つ圏にはなりません。
前順序である場合、特に結び半束(join-semilattice)である場合
任意の前順序を備えた集合(X,\sqsubseteq)は小さい圏とみなすことができます。 この圏の射をa\sqsubseteq bなる順序対(a,b)で表すことにすると、射の分割は
\begin{align} \divleft{a}{b} (a\cdot b, c) &= (a, \divleft{a}{b}(c)) \\ \divright{a}{b} (a\cdot b, c) &= (b, \divright{a}{b}(c)) \end{align}
と表されます。ただし、\divleft{a}{b}, \divright{a}{b}という記法を多義的に用いて、 対象を引数にとる関数として用いられている場合は以下のような型を持つ関数であるとします。
\begin{align} \divleft{a}{b} &: \setcompre{d}{a \cdot b \sqsubseteq d} \to \setcompre{d}{a \sqsubseteq d} \\ \divright{a}{b} &: \setcompre{d}{a \cdot b \sqsubseteq d} \to \setcompre{d}{b \sqsubseteq d} \end{align}
これらが満たすべき性質は以下のようになります。
射の分割が半群演算と両立すること。a\cdot b\cdot c \sqsubseteq dなるa,b,c,dに対して、
\begin{align} \divleft{a}{b} \left( \divleft{a\cdot b}{c} d \right) &= \divleft{a}{b \cdot c} d \\ \divright{b}{c} \left( \divright{a}{b\cdot c} d \right) &= \divright{a \cdot b}{c} d \\ \divright{a}{b} \left( \divleft{a\cdot b}{c} d \right) &= \divleft{b}{c} \left( \divright{a}{b\cdot c} d \right) \end{align}
射の分割が恒等射を保つこと。
\begin{align} \divleft{a}{b} (a\cdot b) &= a \\ \divright{a}{b} (a\cdot b) &= b \end{align}
射の分割が終域を保つこと。a\cdot b \sqsubseteq cなるa,b,cに対して、
\begin{equation} \left( \divleft{a}{b} c \right) \cdot \left( \divright{a}{b} c \right) = c \end{equation}
射の分割が射の合成を保つこと。a\cdot b \sqsubseteq c \sqsubseteq dなるa,b,c,dに対して、
\begin{align} \divleft{a}{b} d &= \left(\divleft{c_a}{c_b} d\right) \\ \divright{a}{b} d &= \left(\divright{c_a}{c_b} d\right) \end{align}
ただし、c_a, c_bは以下の通りとする。
\begin{align*} c_a &= \divleft{a}{b} c \\ c_b &= \divright{a}{b} c \end{align*}
自分自身これの具体例はいまいち思いついていないのですが、 前順序集合(X,\sqsubseteq)が実際には結び半束である場合、すなわち
- \sqsubseteqが半順序でもある、すなわちx \sqsubseteq yかつy \sqsubseteq xならばx = yである
- 結び(2元の最小上界)\veeを持つ
という場合には、次のように射の分割を与えることができます。
まず、\setcompre{d}{a \vee b \sqsubseteq d}は\setcompre{d}{a \sqsubseteq d}や\setcompre{d}{b \sqsubseteq d}の部分集合です。 射の分割を定める関数は以下の型をしているので、どちらも包含写像としてみます。
\begin{align*} \divleft{a}{b} &: \setcompre{d}{a \vee b \sqsubseteq d} \to \setcompre{d}{a \sqsubseteq d} \\ \divright{a}{b} &: \setcompre{d}{a \vee b \sqsubseteq d} \to \setcompre{d}{b \sqsubseteq d} \end{align*}
すなわち
\begin{align*} \divleft{a}{b} c &= c\\ \divright{a}{b} c &= c \end{align*}
と定義すると性質1~4を満たします。
次回予告
順番は考えていないのですが、
多項式Comonadと小さい圏が対応すること、多項式Comonadの間の準同型が小さい圏の間の関手とは一致しないこと
- “Directed Containers as Categories.” https://arxiv.org/abs/1604.01187
- ほぼ完全にこの論文の話
- “Directed Containers as Categories.” https://arxiv.org/abs/1604.01187
小さい圏の間のretrofunctorの定義と、多項式Comonadの間の準同型が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
- Nelson Niu and David I. Spivak, “Polynomial Functors: A Mathematical Theory of Interaction,” https://github.com/ToposInstitute/poly/blob/pdf/poly-book.pdf
圏の
積直積がRetrofunctorを射とする圏\CatCにおける直積モノイド積であること、 射の分割を持つ圏Cが\CatCにおける半群対象であること- 多分まだ書かれてない?
などを解説していきたいと思っています。上2つは実際には参考文献の日本語での再解説でしかないので、 自分がそれらをうまく書けなかったら「これを読んでね」として一番下だけ書く可能性があります。
追記
- 2024-08-30 参考文献がめちゃくちゃだったのを修正
- 2024-10-19 圏としての直積は\CatCにおけるモノイド積だが直積ではないのに、「直積である」と言ってしまっていたのを訂正
なんと1年も経ってる・・・↩︎
Daniel Ahman and Tarmo Uustalu, “Directed Containers as Categories.” https://arxiv.org/abs/1604.01187↩︎
Tarmo Uustalu and Varmo Vene, “Comonadic Notions of Computation” https://www.sciencedirect.com/science/article/pii/S1571066108003435↩︎
Nelson Niu and David I. Spivak, “Polynomial Functors: A Mathematical Theory of Interaction,” https://github.com/ToposInstitute/poly/blob/pdf/poly-book.pdf↩︎