実用圏論： 2-圏、居住関係、プロファイリング - 檜山正幸のキマイラ飼育記 (はてなBlog)

$\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\twoto}{\Rightarrow } \newcommand{\In}{\text{ in } } \newcommand{\Iff}{\Leftrightarrow } \newcommand{\hyp}{\text{-} } \require{color} % 緑色 \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\For}{\Keyword{For } }% \newcommand{\Define}{\Keyword{Define } }%$ ここ何年かで、150分×10回で1クールのセミナーをシリーズとして行いました。話題は毎クール違うのですが、共通するテーマを一言でいえば「実用圏論」でしょう。ラムダ計算、プログラム意味論、論理、ベイズ確率論、データベース理論、システム設計などに“使う”ことを目的にした圏論です。

これらのセミナーの経験から「これは意外と重要」と感じたことを、思いつくままに述べてみます。

内容：

とりあえず2-圏
集合圏も2-圏とみなせる
2-圏としての埋め込み
居住関係とアビタ
プロファイルの追跡
おわりに

とりあえず2-圏

通常の圏（1次元の圏）をメインに扱う場合でも、なるべく早く高次圏〈higher category〉を導入したほうがいいと思います。一般的なn-圏は不要でも、2-圏はよく使います。

小さい圏の圏を ${\bf Cat}$ 、必ずしも小さくない（大きいかも知れない）圏の圏を ${\bf CAT}$ とします。今、“圏の圏”と言いましたが、 ${\bf Cat}$ も ${\bf CAT}$ も実は2-圏です。対象が圏、射が関手、そして2-射（2次元の射）として自然変換を持ちます。

順序集合の圏を ${\bf Ord}$ としましょう。対象は順序集合、射は単調写像〈{monotone | monotonic} map〉です。ホムセット ${\bf Ord}(A, B)$ は、単調写像のあいだの順序により順序集合になります。 $f, g \in {\bf Ord}(A, B)$ が $f \le g$ であるとき、2-射 $\alpha ::f \twoto g : A \to B \In {\bf Ord}$ が在るとみなします。そうすると、 ${\bf Ord}$ は2-圏となります。

順序集合を定義する条件達から、反対称性の条件を取り除くとプレ順序集合〈preordered set〉になります。プレ順序集合のあいだの単調写像も順序集合のときと同様に定義できるので、プレ順序集合と単調写像の全体は圏を形成します。これを ${\bf Preord}$ としましょう。 ${\bf Ord}$ の場合と同様な理由で ${\bf Preord}$ は2-圏になります。

${\bf Cat}, {\bf CAT}, {\bf Ord}, {\bf Preord}$ はいずれも2-圏の実例です。2-圏は浮世離れしたものではなくて、身近にあります。より多くの2-圏の事例は次の記事に書いてあります。

モナド論をヒントに圏論をする（弱2-圏の割と詳しい説明付き） // 2-圏の例 10選

集合圏も2-圏とみなせる

「集合圏は2-圏（2次元の圏）か？」と問われれば、答は「いや〈No〉、1-圏（1次元の圏）だ」となります。しかし、「集合圏に2-射（2次元の射）はあるか？」と問われれば、「ある〈Yes〉」です。また、「集合圏を2-圏とみなせるか？」に対する答は「みなせる〈Yes〉」です。

集合圏の2-射とは、射〈写像〉のあいだの等式です。つまり、2-射 $\alpha :: f \twoto g:A \to B \In {\bf Set}$ が存在するとは、 $f = g$ であることです。これは簡単な定義ですが、なかなかピンとこないようです。

次元を下げて、対象〈0-射〉と射〈1-射〉で考えてみましょう。次の2つの主張は同じことです。

対象 $A$ と $B$ が等しい。
対象 $A$ と $B$ のあいだに恒等射が存在する。

射 $f: A \to B$ が恒等射であることを $f: A \overset{\mrm{id}}{\to} B$ と書くことにします。この書き方を使うと、次の3つの主張は同じことです。

対象 $A$ と $B$ が等しい。
対象 $A$ と $B$ のあいだに恒等射が存在する。
$f: A \overset{\mrm{id}}{\to} B$ である射 $f$ が存在する。

これらの主張の次元を1つ上げると：

射 $f$ と $g$ が等しい。
射 $f$ と $g$ のあいだに恒等2-射が存在する。
$\alpha :: f \overset{\mrm{id}}{\twoto} g$ である2-射 $\alpha$ が存在する。

射〈1-射〉が等しいことと、射〈1-射〉のあいだに恒等2-射が存在することを同じことだと考えるのです。次元によらない一般原理としては、次の3つの主張は同じことです。

k-射 $x$ と $y$ が等しい。
k-射 $x$ と $y$ のあいだに恒等(k + 1)-射が存在する。
$z :^{k + 1} x \overset{\mrm{id}}{\to}\!\!{^{k + 1}}\, y$ である(k + 1)-射 $z$ が存在する。

ここで、 $:^{k + 1}$ はコロンが(k + 1)個並んでいることを示し、 $\to^{k + 1}$ は“太さ”が(k + 1)の矢印のつもりです。

k = 0, 1 の場合が、等しさが“恒等射（恒等(0 + 1)射）”と“恒等2-射（恒等(1 + 1)射）”で与えられる場合です。

通常は1-圏として扱われている集合圏も、2-射を持つのだから2-圏とみなすことができます。ただし、集合圏の2-射は恒等2-射だけなので、特殊な2-圏です。

ここまでの議論に集合圏固有なことは特にないので、一般的な圏〈1-圏〉 $\cat{C}$ は、2-圏とみなすことができます。

同じことは0-圏である集合に対しても言えます。通常は0-圏として扱われている集合も、要素の等しさを恒等1-射として、1-射を持つのだから1-圏とみなすことができます。ただし、集合（圏とみなした集合）の1-射は恒等1-射だけなので、特殊な1-圏（離散圏）です。

n-圏を(n + 1)-圏とみなすことのご利益は、次の記事を見てください。

圏の次元という概念が、実は融通がきくものだということは次の記事に書いています。

圏の離散化、切り捨て、次元調整

2-圏としての埋め込み

任意の順序集合はプレ順序集合とみなせるし、順序集合のあいだの単調写像はプレ順序集合のあいだの単調写像でもあります。このことから、次のような圏の埋め込みが存在します。

$\quad {\bf Ord} \hookrightarrow {\bf Preord}$

任意の集合は、離散順序により順序集合とみなせます。集合 $S$ 上の離散順序とは次のように定義される順序です。

$\For x, y\in S\\ \Define x \le y :\Iff x = y$

集合のあいだの任意の写像は離散順序に関して単調写像になるので、次の埋め込みが存在します。

$\quad {\bf Set} \hookrightarrow {\bf Ord}$

ところで、プレ順序集合はやせた圏とみなせました。つまり、次の埋め込みが存在します。

$\quad {\bf Preord} \hookrightarrow {\bf Cat}$

今までの埋め込みを並べてみると：

$\quad {\bf Set} \hookrightarrow {\bf Ord}\hookrightarrow {\bf Preord} \hookrightarrow {\bf Cat}$

集合圏、順序集合の圏、プレ順序集合の圏は、埋め込みを通じて小さい圏の圏の部分圏とみなせます。登場した圏はすべて2-圏とみなせるので、「小さい圏の2-圏の部分2-圏とみなせる」とも言えます。

例えば、集合圏の対象である集合は離散圏とみなされ、集合圏の射である写像は離散圏のあいだの関手とみなされ、集合圏の2-射である写像のあいだの等式は、恒等自然変換とみなされます。

${\bf Set}, {\bf Ord}, {\bf Preord}$ が2-射を持つことが納得いかないなら、典型的な2-圏である ${\bf Cat}$ 内に埋め込んで、対応する自然変換を考えてみれば実感がわくでしょう。

参考までに言うと、2-圏 ${\bf Cat}$ のなかで、 ${\bf Set}, {\bf Ord}, {\bf Preord}$ の埋め込み像を特徴づける性質は次のようになります。

${\bf Set}$ の埋め込み像：恒等1-射しか持たない圏〈離散圏〉を対象とする充満部分2-圏。
${\bf Ord}$ の埋め込み像：やせた骨格的圏〈thin skeletal category〉を対象とする充満部分2-圏。
${\bf Preord}$ の埋め込み像：やせた圏〈thin category〉を対象とする充満部分2-圏。

居住関係とアビタ

型理論において、たまに inhabit〈住む〉という言葉を使います。例えば、集合が空でないことを、その集合は inhabited だと言ったりします。inhabitation〈居住 | 生息〉の関係は、要素と集合の所属関係と同じことですから、記号 ' $\in$ ' を使って表せます。

$\quad \text{inhabitant}\;\in \;\text{habitat}$

inhabit, inhabitant, habitat の日本語は次を使うことにします。

inhabit：生息する、棲む、居住する
inhabitant：居住者、住人
habitat：アビタ、ハビタ、生息地

アビタ〈生息地〉が集合の場合は、居住関係〈生息関係〉 $\in$ の意味はハッキリしてますが、 $\cat{C}$ がn-圏のときの

$\quad x \in \cat{C}$

はちょっと曖昧です。それと言うのも、せめて $x$ の次元は知りたいからです。以下、n-圏の居住者（つまり射）の次元を話題にします。

$\cat{C}$ がn-圏のとき、 $\cat{C}$ のk-射の集合を考えることができます。このブログの過去記事を見てみると、k-射の集合に対して色々な書き方をしています。

$|\cat{C}|_k$ ：「2次元のコンピュータッド」
$k\hyp\mrm{Mor}(\cat{C})$ ：「任意の圏を等式により2-圏とみなす」
$\mrm{Mor}^k(\cat{C})$ ：「等式的推論と高次圏論」

ここでは、 $|\cat{C}|_k$ を使うことにします。

$|\cat{C}|_0$ ： 0-射〈対象〉の集合
$|\cat{C}|_1$ ： 1-射〈射〉の集合
$|\cat{C}|_2$ ： 2-射の集合

$x \in |\cat{C}|_k$ と書けば、 $x \in \cat{C}$ より曖昧さが減ります。 $x \in |\cat{C}|_k$ とまったく同じ意味で次の記法も使います。

$\quad x \in_k \cat{C}$

例えば、次のようです。

$\quad x \in_1 \cat{C} \in_0 {\bf Cat}$

上記の宣言から、 $x$ は、小さい圏 $\cat{C}$ の射〈1-射〉であるとわかります。また、

$\quad x \in_2 \cat{C} \in_0 {\bf CAT}$

これなら、 $x$ は、大きいかも知れない圏 $\cat{C}$ の2-射なので、射のあいだの等式ですね。

集合が集合圏に0-射として生息し、写像が1-射として生息しているのは簡単な事実です。が、複雑な構造になると、構造とその構成素達がどこに棲んでいるかはややこしくなります。

例えば、ベクトル空間 $V$ があるとき、その係数体 $K$ は体の圏に棲んでいます。ベクトルの足し算が載っているアーベル群 $A$ はアーベル群の圏に棲んでいます。アーベル群の台集合 $U$ は集合圏の対象〈0-射〉です。ベクトルの足し算は集合 $U\times U$ から $U$ への写像〈1-射〉なので、集合圏の住人です。足し算の交換法則〈可換律〉 $\mrm{comm}$ は写像のあいだの等式なので集合圏の2-射です。

$V \in_0 {\bf Vect}$
$K \in_0 {\bf Field}$
$A \in_0 {\bf Ab}$
$U \in_0 {\bf Set}$
$((+):U\times U \to U) \in_1 {\bf Set}$
$( \mrm{comm}:: \sigma_{U,U};(+) \twoto (+):U\times U \to U) \in_2 {\bf Set}$

構造とその構成素達のアビタ〈生息地〉をいちいち詮索していると鬱陶しいので、記号の乱用や同一視が多用されますが、ときにはそれぞれのアビタ〈生息地〉をハッキリさせる必要があります。

プロファイルの追跡

小学校低学年で掛け算九九を習いました。あの当時「数〈かず〉」と言えば自然数でしたから、掛け算記号 ' $\times$ ' の意味は次のようです。

$\quad (\times):{\bf N}\times {\bf N} \to {\bf N} \In {\bf Set}$

中置演算子記号を丸括弧で囲った $(\times)$ はその演算子記号が表す写像〈関数〉の意味です（いつも丸括弧を付けるわけでもないですが）。

上記の宣言は「 $(\times)\in_1 {\bf Set}$ （掛け算は集合圏の1-射）」より情報量が多く、掛け算の域〈domain〉と余域〈codomain〉まで明らかにしています。アビタと共に域・余域の情報まで揃うと、射の輪郭がだいぶ掴めるようになります。

さてところで、上のの宣言をよく見ると、掛け算記号が ${\bf N}\times {\bf N}$ にも出てきています。これは、掛け算九九で習った“あの掛け算”とは違うようです。そう、集合の直積ですね。

集合の直積を表す ' $\times$ ' は、2つの集合を引数にとる写像と考えられますから、そのプロファイル（域・余域の情報）は次のように書けるでしょう。

$\quad (\times):|{\bf Set}|_0 \times|{\bf Set}|_0 \to |{\bf Set}|_0$

この写像は、大きな集合〈類 | クラス〉のあいだの写像です。集合の直積である $(\times)$ はどこに棲んでいるのでしょう？ $(\times)$ のアビタはどこ？大きな集合も対象として含むような巨大な集合圏の居住者と考えざるを得ません。

$\quad (\times):|{\bf Set}|_0 \times|{\bf Set}|_0 \to |{\bf Set}|_0 \In {\bf SET}$

直積は、集合に対してだけではなくて写像に対する直積も定義できます。写像の直積も同じ記号 ' $\times$ ' で表します。そのプロファイルは次のようになります。

$\quad (\times):|{\bf Set}|_1 \times|{\bf Set}|_1 \to |{\bf Set}|_1 \In {\bf SET}$

集合の直積と写像の直積を一緒にすると、圏のデカルト積となります。デカルト積は二項関手〈双関手〉ですから、次のプロファイルを持ちます。

$\quad (\times):{\bf Set} \times {\bf Set} \to {\bf Set} \In {\bf CAT}$

すぐ上の $(\times)$ はもはや単なる写像ではなくて関手です。

二項関手〈双関手〉としての $(\times)$ のプロファイルに ${\bf Set} \times {\bf Set}$ が出てきますが、この掛け算記号は何でしょう？圏と圏の直積です。しかも、大きいかも知れない圏に対する直積ですね。そのプロファイルは：

$\quad (\times):{\bf CAT} \times {\bf CAT} \to {\bf CAT} \In \mathbb{2CAT}$

圏の次元も圏のサイズもさらに1レベル上げた世界で考える必要があります。なんだか不安な気分になりませんか？僕は不安で釈然としない気分になります。そのことは次の記事に書いています。

デカルト・タワーを求めて

不安になる話は一旦やめて、話題を変えます。数の掛け算を自然数の掛け算と解釈しましたが、整数の掛け算や実数の掛け算もあります。どの掛け算に対しても同じ掛け算記号 ' $\times$ ' がオーバーロード〈多義的使用〉されます。

自然数の掛け算、整数の掛け算、実数の掛け算を、下付き添字で区別することにします。

$\quad (\times_{\bf N}) :{\bf N}\times {\bf N} \to {\bf N} \In {\bf Set}\\ \quad (\times_{\bf Z}) :{\bf Z}\times {\bf Z} \to {\bf Z} \In {\bf Set}\\ \quad (\times_{\bf R}) :{\bf R}\times {\bf R} \to {\bf R} \In {\bf Set}$

オーバーロードされた掛け算記号は、次のような写像とみなせます。

$\quad (\times_{-}):\{{\bf N},{\bf Z}, {\bf R}\} \to |{\bf Set}|_1 \In {\bf SET}$

3つの要素（要素が集合）を持つ集合から、集合圏の射（つまり写像）の集合への写像です。具体的に書き下せば：

$\quad {\bf N} \mapsto (\times_{\bf N}) \in |{\bf Set}|_1\\ \quad {\bf Z} \mapsto (\times_{\bf Z}) \in |{\bf Set}|_1\\ \quad {\bf R} \mapsto (\times_{\bf R}) \in |{\bf Set}|_1$

もう少し精密に記述したいなら、「圏論的コンストラクタと圏論的オペレータ〈コンビネータ〉再論」で導入した記法を使って次のようになります。

$\quad (\times_{-}):: \_1 \times \_1 \overset{\mrm{comb}}{\twoto} \_1: \{{\bf N},{\bf Z}, {\bf R}\} \overset{\mrm{ctor}}{\to} |{\bf Set}|_0 \In {\bf CAT}^\mrm{lawless}$

ここで、

$\_1$ は無名ラムダ変数。 $(\_1 \times \_1) = \lambda\, X\in \{{\bf N},{\bf Z}, {\bf R}\}.(\, X\times X \,)$ 。
$\overset{\mrm{comb}}{\twoto}$ は、コンストラクタのあいだのコンビネータ〈オペレーター〉であることを示す。
$\overset{\mrm{ctor}}{\to}$ は、集合から圏の対象集合へのコンストラクタであることを示す。
${\bf CAT}^\mrm{lawless}$ は、関手性や自然性の法則を満たさない（無法則な）コンストラクタ／オペレーター〈コンビネータ〉も認めたナンデモアリの圏類似構造〈category-like structure〉。

この節で出てきたモノは、すべて掛け算記号 ' $\times$ ' で表せるモノでした。そのアビタとプロファイルを探ってみると、全然別な世界に棲んでいたり、異なった特性を持っていたりします。

モノに付けられたラベル（例えば掛け算記号）だけではモノの特徴は分かりません。プロファイルを調べること＝プロファイリングにより、対象物のおおよその特徴を掴むことが大事です。

おわりに

高次圏 -- とはいってもとりあえず2-圏まで考えましょう。すると、0-射〈対象〉、1-射〈射〉、2-射、3-射（2-射の等式は恒等3-射になる）が出てきます。登場する様々なk-射が同じn-圏に棲んでいるとは限らないので、それらのアビタ〈生息地〉を意識しましょう。そして射のプロファイルを追跡すれば、ある程度、射の特徴はわかります。

ときに、未定義部分がある関数、値が一意に決まらない関数もどき、関手とは呼べない対応、自然性を満たさない変換のような、出来そこないや無法者が登場します。それらも排除しないで利用していきましょう（「圏論的コンストラクタと圏論的オペレータ〈コンビネータ〉再論」参照）。

と、そんなことが「意外と重要」と感じます。