「有向コンテナと多項式コモナド」にて:
モノイド類似構造である有向コンテナ〈圏〉構造が、多項式自己関手を台とするコモノイド構造として反映されるわけです。面白いですね。
面白そうなので、アーマン/ウウスタル〈Danel Ahman, Tarmo Uustalu〉以外の論文もチラチラと眺めてみました(ちゃんと読んではいない)。
Agdaのようなプログラミング言語じゃなくても、コミュニティごとにジャーゴン〈隠語・方言の体系〉が形成されているようで、内容以前に言語的解釈で骨が折れます。ちょっとこれはコミュニケーションが困難だな、と感じました。
コンテナ/多項式界隈の錯綜した概念・用語・記法を整理します。一般的な問題意識・観点からの話は別記事「分かりにくさへの対処」に切り出しました -- 事前に、あるいは必要に応じて目を通してみてください。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\hyp}{\text{-} }
\newcommand{\id}{\mathrm{id}}
\newcommand{\In}{\text{ in } }
\newcommand{\Dwn}{\downarrow }
\newcommand{\Comp}{\mathop{;} }
\newcommand{\o}[1]{\overline{#1}}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\coef}[1]{ {\langle #1 \rangle} }
\newcommand{\lcomp}{ \triangleleft }
\newcommand{\base}[1]{ {{#1}\!\lrcorner} }
\require{color} % 緑色
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
\newcommand{\Define}{\Keyword{Define } }%
\newcommand{\Subject}{\Keyword{Subject } }%
\newcommand{\Where}{\Keyword{Where } }
\newcommand{\And}{\Keyword{And } }
\newcommand{\Let}{\Keyword{Let } }
\newcommand{\KWB}[1]{ \textcolor{blue}{\text{#1}} }% KeyWord Blue
\newcommand{\if}{\KWB{if } }
\newcommand{\then}{\KWB{ then } }
\newcommand{\else}{\KWB{else } }
`$
内容:
多項式
圏論的コンテナ/多項式は昔からある概念です。例えば次は、圏論的多項式の嚆矢のひとつとされています。
- [GH03]
- Title: Wellfounded Trees and Dependent Polynomial Functors
- Authors: Nicola Gambino and Martin Hyland
- Date: 2003
- Pages: 15p
- URL: https://www.dpmms.cam.ac.uk/~martin/Research/Publications/2004/gh04.pdf
最近の応用圏論〈ACT | Applied Category Theory〉では、多項式の利用が盛んです。スピヴァック〈David I. Spivak〉を中心とするMITのグループ(MIT以外の所属の人もたくさんいますが)が応用多項式論を展開しています。このグループの多項式論をMIT流多項式論〈polynomial theory à la MIT〉と呼ぶことにします。
中学・高校の多項式では(「分かりにくさへの対処 // 係数列と多項式関数」参照)、多項式の係数列とそれが定義する多項式関数はあまり区別されずに曖昧に扱われますが、係数列と関数は別物です。圏論的コンテナ/多項式でも、多項式関手とそれを定義する係数データはもちろん別物です。本来、コンテナ/多項式とは係数データのことであって、関手のことではありません。が、実際にはけっこうゴッチャになります。
ここでは、関手ではなくて係数データであることを強調するために、(多項式の)係数系〈coefficient system〉という言葉を導入します。「圏論的コンテナ」でも同様な注意を述べています。
コンテナの圏論的な定式化では、“関手を定義するデータ”と“定義される関手”を同一視してそれをコンテナと呼ぶことが多いのですが、同一視すると分かりにくいので、コンテナスキーマとコンテナ関手に分けて説明します。コンテナ関手はコンテナスキーマから定義されます。あるいは(同じことですが)、コンテナスキーマから定義される関手がコンテナ関手だ、と言えます。
ここでの用語運用をまとめると:
- 多項式 = (多項式の)係数系
- 多項式 ≠ 多項式関手
- コンテナ = コンテナスキーマ
- コンテナ ≠ コンテナ関手
コンテナ( = コンテナスキーマ = 多項式 = 係数系)の圏を $`{\bf Cont}`$ 、多項式関手(= コンテナ関手)の圏を $`{\bf PolyFtor}`$ とします。コンテナに多項式関手を対応させる関手は $`\mrm{Ftor}`$ としましょう。
$`\quad \mrm{Ftor} : {\bf Cont} \to [{\bf Set}, {\bf Set}] \In {\bf CAT}\\
\Where\\
\quad [{\bf Set}, {\bf Set}] = {\bf CAT}({\bf Set}, {\bf Set}) \;\in |{\bf CAT}|
`$
関手 $`\mrm{Ftor}`$ の本質像〈essential image〉が圏 $`{\bf PolyFtor}`$ です。本質像を $`\mrm{EssImg}(\hyp)`$ と書くと:
$`\quad {\bf PolyFtor} = \mrm{EssImg}(\mrm{Ftor})\subseteq [{\bf Set}, {\bf Set}] \;\in |{\bf CAT}|`$
関手 $`\mrm{Ftor}`$ の余域圏を $`{\bf PolyFtor}`$ に狭めて考えることもあります。余域の制限の違いしかないので、同じ名前をオーバーロードします。
$`\quad \mrm{Ftor} : {\bf Cont} \to {\bf PolyFtor} \In {\bf CAT}`$
これが基本的な枠組みです。
参考文献
MIT流多項式論の教科書・論文を紹介します*1。
- [NS20-]
- Title: Polynomial Functors: A Mathematical Theory of Interaction
- Authors: Nelson Niu, David I. Spivak
- Date: Dec 1, 2020 (initial), Oct 11, 2023 (latest)
- Pages: 2023-10-20 時点で 352p
- URL: https://topos.site/poly-book.pdf
- URL: https://github.com/ToposInstitute/poly
[↑] MIT流多項式論の包括的な教科書です。この文書は更新され続けています。変更履歴や最新バージョンの情報は、github で公開されています。
- [LSS23-]
- Title: All Concepts are Cat^♯
- Authors: Owen Lynch, Brandon T. Shapiro, David I. Spivak
- Submitted: 4 May 2023 (v1), 19 May 2023 (v3)
- Pages: 32p
- URL: https://arxiv.org/abs/2305.02571
[↑] 「圏 =多項式コモナド」の教義に基づいて、新しいスタイルの圏論を展開しています。
- [SS23-]
- Title: Structures on Categories of Polynomials
- Authors: Brandon T. Shapiro, David I. Spivak
- Submitted: 29 Apr 2023 (v1), 18 May 2023 (v2)
- Pages: 50p
- URL: https://arxiv.org/abs/2305.00167
[↑] [LSS23-] から参照されているので挙げておきます。多項式の圏(コンテナの圏と多項式関手の圏)について詳しく調べたものらしいです(読んでない)。
- [AU16-]
- Title: Directed Containers as Categories
- Authors: Danel Ahman, Tarmo Uustalu
- Submitted: 5 Apr 2016
- Pages: 10p
- URL: https://arxiv.org/abs/1604.01187
[↑] MITグループではありませんが、「圏 =多項式コモナド」の発端となった論文です。「有向コンテナと多項式コモナド」参照。
多項式コモナド
多項式コモナド〈polynomial comonad〉は、多項式関手を台とするコモナドです。コモナド余乗法とコモナド余単位は自然変換です。つまり、集合圏上の多項式自己関手達のモノイド圏におけるコモノイド対象が多項式コモナドです。これは次のように書けます。
$`\quad \text{polynomial comonads} = \mrm{Comon}( ({\bf PolyFtor}, *, \mrm{Id}) )`$
ここで、$`*`$ は関手の結合、$`\mrm{Id} = \mrm{Id}_{\bf Set}`$ で、$`({\bf PolyFtor}, *, \mrm{Id})`$ は(厳密な)モノイド圏です。$`\mrm{Comon}(\hyp)`$ は、モノイド圏内のコモノイド対象からなる圏を作る構成です。
「有向コンテナと多項式コモナド」における多項式コモナドは上記の定義に基づいています。ところが、多項式関手を定義するデータであるコンテナ〈多項式の係数系〉の圏 $`{\bf Cont}`$ も、関手の結合に相当する結合積〈composition product〉でモノイド圏になります。よって、次の定義も可能です。
$`\quad \text{polynomial comonads} = \mrm{Comon}( ({\bf Cont}, \lcomp, \mrm{I}) )`$
ここで、$`\lcomp`$ はコンテナの結合積(反図式順)、$`\mrm{I}`$ は結合積に対する単位対象です(MIT流では、小文字一文字 $`y`$ で単位対象を表しますが)。この場合、コモノイドの台はコンテナであり、コモノイドの余乗法/余単位はコンテナの射(後述)です。
MIT流多項式論では、多項式コモナドは、コンテナのモノイド圏内のコモノイド対象を指しているようです。もっとも、コンテナの圏と多項式関手の圏は同一視する傾向があるので、同時に自己関手圏内のコモノイド(通常のコモナド)をも意味しているかも知れません。概念的には同一視可能であっても、実際の計算は違うので、解釈を間違えるとサッパリ計算ができません -- 文脈を見て解釈を変える必要があります。
アーマン/チャップマン/ウウスタル〈Danel Ahman, James Chapman, Tarmo Uustalu〉の有向コンテナ〈directed container〉は、概念的には(小さい)圏と同じものであり、多項式コモナドを定義します。この事実から、MIT流多項式論では、(場合により)多項式コモナドの別名として圏〈category〉が使われます。この意味での圏(多項式コモナド)は、
$`\quad c = (c, \epsilon, \delta) \:\text{ category}`$
のように書かれます。
圏(多項式コモナド)のあいだの射は通常の関手ではないので余関手〈cofunctor〉と呼びます。
$`\quad \phi : c \to d\:\text{ cofunctor}`$
余関手 $`\phi`$ は、原則的には $`\mrm{Comon}( ({\bf Cont}, \lcomp, \mrm{I}) )`$ の射です。下部構造としての実体は $`{\bf Cont}`$ の射になります(条件で縛られる)。
ファミリー
「ファミリー」は「コンテナ」と同義語です。したがって、「ファミリー」と「多項式(の係数系)」も同義語です。ただし、射に関しては逆向きの射を採用します。
$`\quad {\bf Cont} = {\bf Fam}_{\leftarrow}`$
ファミリーと逆向きの射に関しては、以下の過去記事の節をみてください。
ファミリー〈family〉と(集合論的な)バンドル〈bundle〉は一対一(正確には up-to-iso で一対一)に対応します。適当な条件のもとで、逆向きの射をバンドルに定義することも可能です*2。バンドルはファイバー付き集合〈{fibred | fibered} set〉とも呼びます。ファミリー/バンドル/ファイバー付き集合については、次の過去記事で触れています。
「ファミリーの圏とシグマ関手・パイ関手 // ファミリーの圏の変種: 逆向き」と「2-コンテナ // 1-コンテナ」の記法を組み合わさると、次のように書けます。'$`\simeq`$' は圏同値を表します。
$`\quad {\bf Cont} = {\bf Fam}_{\leftarrow}\\
\quad {\bf Fam}_\alpha \simeq {\bf Bun}_\alpha\: (\alpha \in \{\to, \leftarrow\})\\
\quad {\bf Bun}_\alpha = {\bf FibSet}_\alpha\: (\alpha \in \{\to, \leftarrow\})
`$
様々な概念・用語
「圏論的コンテナ」において、形状〈shape〉、位置〈position〉などのコンテナ独自の用語を紹介しました。より具体的な話は、「ツリーデータ型のモナド」を見るといいかも知れません。ツリーデータ型の例では、ツリーの形状が“コンテナの意味で形状”で、ツリーのリーフノードが“コンテナの意味での位置”になります。この例 -- リーフ値付きツリー〈leaf valued tree〉では、コンテナの用語が具体例とマッチしています。
しかし、圏の対象が“コンテナの意味で形状”で、圏の射が“コンテナの意味での位置”だとなると(「有向コンテナと多項式コモナド」)、違和感をいだくでしょう。とはいえ、この違和感の正体は、テクニカルタームに対して国語辞書的意味を連想しているからです。余計な連想をしなければいいだけのことです*3。
異なる出自の様々な概念・用語がありますが、形式的・抽象的には同義語になります。同義語を表にまとめると以下のとおり。以下で、“有向コンテナ・改”は「有向コンテナと多項式コモナド」で導入した用語のことです。下の表の 2, 3, 4 列を縦に見ると、それらは同義語の並びです。
コンテナ | 形状 | 位置の集合 | 位置 |
圏 | 対象 | 片方向ホムセット | 射 |
有向グラフ | 頂点 | カローラ | 辺 |
有向コンテナ・改 | ポイント | カローラ | アロー |
MIT流多項式 | 位置 | カローラ | 方向 |
ファミリー | インデックス | 値、成分 | 成分の要素 |
バンドル | ベース空間の点 | ファイバー | ファイバーの点 |
コンテナとコンテナ射の書き方
コンテナ〈多項式の係数系 | ファミリー〉のインスタンス -- つまり、圏 $`{\bf Cont}`$ の対象を書き表す方法を決めます。「分かりにくさへの対処 // 記号の乱用を緩和する方法」で述べた方法を使います。
コンテナの実体は、集合 $`X`$ から“集合の集合” $`|{\bf Set}|`$ への写像に過ぎません。
$`\quad A : X \to |{\bf Set}| \In {\bf SET}`$
通常、写像の域も添えて次のように書きます。
$`\quad A = (X, A) \text{ where } X \in |{\bf Set}|,\, A\in \mrm{MAP}(X, |{\bf Set}|)`$
これは、記号の乱用ではなくて、冗長な書き方、あるいは依存ペアとしての書き方です。
$`X, A`$ を(「有向コンテナと多項式コモナド」における)コンテナとしての $`A`$ の構成素とみなせば:
$`\quad A = \mrm{Cont}(\mrm{Pt}(A), \mrm{Corol}^A )`$
構成素の名前は、「有向コンテナと多項式コモナド」で導入した用語に基づきます。
- $`\mrm{Pt}(A)`$ : コンテナ $`A`$ の、ポイント〈point〉の集合
- $`\mrm{Corol}^A`$ : コンテナ $`A`$ の、ポイントにカローラ〈corolla〉(半径は 1)を対応させる写像
「ポイント」「カローラ」以外の呼び名は前節の表を参照してください。幾つかの記法の規約〈notational convention〉を設けます。
- $`\mrm{Pt}(A)`$ を $`|A|`$ と書いてもよい。これは、圏の対象の集合/グラフの頂点の集合/リストの長さなどと、記法的に整合性を持つ。
- $`\mrm{Corol}^A`$ を $`A`$ と書いてもよい(記号の乱用)。ただし、引数渡しはブラケットを使う。$`\mrm{Corol}^A(a) = A[a]`$ 。
- 区切り記号にカンマではなくて縦棒を使うことにより、コンテナであることを示唆する。$`\mrm{Cont}(X , A[\hyp] ) = (X \mid A[\hyp])`$ 。
次に、コンテナのあいだの射 $`\phi: A \to B \In {\bf Cont}`$ の書き方です。コンテナ射は2つのパート〈構成素〉を持つので、次のようにします。
$`\quad \phi = \mrm{MorCont}(\phi_\mrm{ptPart}, \phi_\mrm{corolPart})`$
- $`\phi_\mrm{ptPart}`$ : 射 $`\phi`$ の、ポイントパート〈point part〉 $`\phi_\mrm{ptPart} : |A| \to |B| \In {\bf Set}`$
- $`\phi_\mrm{corolPart}`$ : 射 $`\phi`$ の、カローラパート〈corolla part〉 $`\phi_\mrm{corolPart} \in \prod_{x\in |A|}\mrm{Map}(B[\phi_\mrm{ptPart}(x)], A[x])`$
カローラパートをアローパート〈arrow part〉と呼んでもよいだろうし、ベースパート/ファイバーパート〈base part / fiber part〉でもかまいません。幾つかの記法の規約〈notational convention〉を設けます。
- $`\phi_\mrm{ptPart}`$ を $`\base{\phi}`$ と書いてもよい。
- $`\phi_\mrm{corolPart}`$ を $`\phi^\sharp`$ と書いてもよい。このとき、最初の引数は下付きインデックスとして渡す。$`\phi^\sharp_a : B[\base{\phi}(a)] \to A[a] \In {\bf Set}`$ 。
$`\base{\phi}`$ は「Diag構成の変種とその書き方」で導入したベースパートの書き方です。圏の対象集合に合わせて絶対値記号 $`|\phi|`$ でもいいかと思いましたが、$`|\phi|`$ が関数 $`\phi`$ のノルムに見えてしまうのが難点です。$`\base{\phi}`$ でも $`|\phi|`$ でも、最初は違和感あるでしょうが、要は慣れの問題です。
コンテナの圏とその周辺
コンテナ〈ファミリー | 多項式の係数系〉と関連する概念がいくつかあります。それらは同一視されたり、オーバーロード(同じ名前で呼ばれる)可能性があります。いったんはそれらを区別して、相互の対応関係を把握しましょう。
全体像は次のようになります。
$`\require{AMScd}
\quad \begin{CD}
{\bf Bun}_{\leftarrow}@. {}\\
@A{\mrm{Groth}}AA @.\\
{\bf Cont} @>{\mrm{Ftor}}>>{\bf PolyFtor}\\
@V{\mrm{Formal}}VV @. \\
{\bf FormalPoly} @. {}
\end{CD}\\
\In {\bf CAT}
`$
図式内に出てくる関手 $`\mrm{Groth}, \mrm{Ftor}, \mrm{Formal}`$ はいずれも圏同値を与えます。4つの圏は事実上同じで同一視可能となります。
中学・高校で習った多項式との類比で言うと(「分かりにくさへの対処 // 係数列と多項式関数」参照):
- $`{\bf Cont}`$ の対象は、実数の有限列に相当。
- $`{\bf FormalPoly}`$ の対象は、記号的な形式に相当。
- $`{\bf PolyFtor}`$ の対象は、関数に相当。
$`{\bf FormalPoly}`$ を、$`{\bf Cont}`$ とは別な圏としてキチンと定義するのは難しいでしょう。また、キチンと定義する必要があるわけでもありません。$`{\bf FormalPoly}`$ と $`{\bf Cont}`$ は同じ圏だが、気持ちの上で(心理的に)区別する、くらいでもいいでしょう。
心理的にであっても $`{\bf FormalPoly}`$ の存在を認めると、話は分かりやすくなります。
[/補足]
コンテナ $`A = (X \mid A[\hyp])`$ がコンテナのとき、$`\mrm{Formal}(A)`$ は次の記号的形式のことです。
$`\quad \sum_{x\in X} y^{A[x]}`$
$`(X \mid A[\hyp])`$ と $`\sum_{x\in X} y^{A[x]}`$ は、ほんとに同一視してしまってもかまいません(上の補足参照)。形式的総和記号を使った $`\sum_{x\in X} y^{A[x]}`$ は、コンテナの別表示だとみなせます。別表示のメリットは記号的・機械的計算に向いていることです。
$`\mrm{Ftor}(A)`$ は、多項式関手です。ラムダ記法を使って次のように書けます。
$`\quad \mrm{Ftor}(A) = \lambda\, y\in_* {\bf Set}.(\, \sum_{x\in X} y^{A[x]} \;\in_* {\bf Set}\,)`$
ここで、
- $`y`$ は対象〈集合〉でも射〈関数〉でも代入できる形式的変数〈不定元〉
- $`\in_*`$ は、対象として、または射として所属すること。
「有向コンテナと多項式コモナド」でそうしたように、次の略記(記法の規約)を使います。
$`\quad \widehat{A} := \mrm{Ftor}(A)`$
コンテナとバンドルのあいだを結ぶ関手 $`\mrm{Groth}`$ はグロタンディーク構成です。本来のグロタンディーク構成の退化バージョンで、コンテナ $`A = (X \mid A[\hyp])`$ に次のようなパイ型で作ったバンドルを対応させます。
$`\quad \pi : \sum_{x\in X}A[x] \to X \In {\bf Set}`$
バンドルの構成素名を $`\mrm{Tot}`$(全空間)、$`\mrm{Base}`$(底空間)、$`\mrm{proj}`$(射影)とすると:
$`\Let B = \mrm{Groth}(A) = \mrm{Groth}( (X \mid A[\hyp]) ) = \mrm{Groth}(\mrm{Cont}(X, A) )\\
\quad B = \mrm{Bun}(\mrm{Tot}(B), \mrm{Base}(B), \mrm{proj}^B)
= \mrm{Bun}(\sum_{x\in X}A[x], X, \pi)
`$
コンテナとバンドルの関係で重要なことは、コンテナのカローラ $`A[a]`$ が、バンドル射影の逆像で再現することです。
$`\For A \in |{\bf Cont}|\\
\For a \in X = |A|\\
\quad A[a] = \pi^{-1}(a)\\
\Where\\
\quad \pi = \mrm{proj}^{\mrm{Groth}(A)}
`$
MIT流のオーバロード
先に紹介したMIT流多項式論の参考文献、特に [LSS23-] で使用されている記法を紹介します。
原則的に、対応するコンテナ/多項式関手/バンドルの三者はオーバーロード(同じ名前で参照)します。「多項式 $`p`$」と言ったとき、最初の解釈はバンドルとしての多項式です。[SS23-] の記法では:
$`\quad p : P_* \to P`$
これは次の意味です(記号の乱用あり)。
$`\quad p = \mrm{Bun}(\mrm{Tot}(p), \mrm{Base}(p), \mrm{proj}^p) = \mrm{Bun}(P_*, P, p)`$
射影の名前を大文字にすると底空間(射影の余域)、大文字に下付きアスタリスクで全空間(射影の域)という記法の規約です。
バンドル $`p`$ に対応するコンテナのカローラ写像は、名前は同じですが $`p[\hyp]`$ とします。
$`\quad p[\hyp] : P \to |{\bf Set}| \In {\bf SET}`$
コンテナ $`p`$ から得られる記号的形式と関手は区別せずに次のように書きます。
$`\quad p = \sum_{I \in P} y^{p[I]}`$
インデックス〈ポイント〉を大文字で書くのも記法の規約です。
[LSS23-] では、名前を大文字にするのはやめて、次のように書きます。
$`\quad p : p_* \to p(1)`$
$`p(1)`$ と書いたときの $`p`$ は関手とみなしています。つまり、次のようなことです。
$`\quad p(1) = (\mrm{Ftor}(p))({\bf 1})`$
多項式関手とみなした $`p`$ に単元集合を渡すと、コンテナ〈ファミリー〉のポイント〈インデックス〉の集合が得られます(計算すれば分かります)。
$`\quad p(1) = (\mrm{Ftor}(p))({\bf 1})\cong \mrm{Pt}(p) = |p|`$
コンテナ $`p`$ から得られる記号的形式/関手は次の形に書けます。
$`\quad p = \sum_{I \in p(1)} y^{p[I]}`$
この例から察せられるように、MIT流多項式論では、かなりえげつないオーバーロードが使われています。
*1:オンラインに公開されている文書・論文の略称は [Web14-15], [DH18-20] (「コレクション改めクラスターの圏」に登場)のように、初投稿年と最新更新年をハイフンで結ぶことにします。更新がない場合でも、オンラインなら更新の可能性はあるのでハイフンだけ入れます。
*2:余域側のバンドルを底写像に沿って引き戻してから、逆向きの写像を作ります。バンドルの射としては不自然な気はしますが。
*3:実際のところ「連想をしない」は無理です。特定の連想に拘らない/引きずられないようにしましょう。