圏論内で使う等式的推論を、圏論のなかで定式化してみます。等式的推論は高次射になるので、少しだけ高次圏論を使います。
内容:
関連する記事:
等式的推論
等式的推論〈equational reasoning〉は、幾つかの等式をもとに新しい等式を導き出す推論のことです。例えば次は、等式的推論における基本的な推論規則〈{inference | deduction} rule〉です。
この推論規則の意味は、上段の2つの等式から下段の等式が導き出せる、ということです。等値関係〈equality〉の推移性〈transitivity〉がその根拠です。
- 等値関係の推移性:
等式的推論は古典論理で統制されていて、ありとあらゆる分野で使われます。ただし、等号以外の関係記号/演算記号などの解釈は分野ごとに変わるでしょう。例えば、次の推論規則に出てくるセミコロンは“射の図式順結合記号”だとすれば、圏論における等式的推論になります。
圏論における等式的推論も当然に古典論理の統制下にあります。古典論理の統制から逃れることは不可能です。が、しかし、圏論内で使われる等式的推論を、できる限り(古典論理ではなく)圏論内で定式化することには意味があります。自律的に自給自足しようという企てです。
基本的なアイディアは、等式を恒等射で置き換える、というものです。
高次圏
等式的推論を圏論内で定式化するには、通常の圏だけでなく高次圏〈higher category〉=n-圏〈n-category〉の概念が必要です。とはいえ、厳密な定義や詳しい知識は不要で、次のことを認識していれば大丈夫です。
- 高次圏は、対象と射だけではなく、2次元の射、3次元の射、… など高次元の射を持つかも知れない。
- 対象は0次元の射、通常の射は1次元の射とみなす。
- k次元の射も、域と余域を持ち、域・余域は(k - 1)次元の射である。ただし、0次元の射=対象は例外で、域・余域を持たない。
k次元の射のことを短くk-射〈k-morphism〉と呼びます。0-射=対象、1-射=通常の射 です。
各次元の射を表す文字を次のように約束します。
射の次元 | 文字種 |
---|---|
0-射 | ラテン大文字 |
1-射 | ラテン小文字 |
2-射 | ギリシャ小文字 |
3-射 | ギリシャ大文字 |
例:
- 0-射:
- 1-射:
- 2-射:
- 3-射:
1-圏〈通常の圏〉 の1-射〈通常の射〉 のプロファイル(域と余域の仕様)は次のように書きます。
同様に、高次射〈k-射〉のプロファイルは次のように書きます。3-圏 内の射だとします。下の図を参照してください。
文字種の約束やプロファイルの書き方が広く合意されているわけではないので、他の約束・書き方があります。例えば、一番お馴染みの2-圏の例である“圏の圏” では:
- 0-射〈対象〉はラテン大文字だが、カリグラフィー体 などで書く場合が多い。
- 1-射〈射〉はラテン大文字 などで書く場合が多い。
このような約束・書き方は、次元が上がれば破綻します。4-圏ではもうウマクないです。致し方ないので、4-射は次元を右肩に添えて示すことにします。
ここで:
- : は4-射であることを示す。
- : のこと。
- : 矢印の“太さ”が4本分であることを示す。
色々な約束・記号を使わずとも、右肩に添えた次元だけでも識別できますが、ちょっと味気なくなります。
高次圏における結合
1-圏〈通常の圏〉の1-射〈通常の射〉は結合〈compose〉できます。しかし、勝手な1-射を2つ持ってきても結合できるとは限りません。結合できるためには、2つの射が隣接している、あるいは境界を接している必要があります。 と が(この順で)隣接していることをハッキリと書くと:
高次圏においても、隣接するk-射は結合できます。しかし、隣接の仕方が多様になります。次の図は、2つの2-射が隣接している様子を隣接境界部分を引き離して描いたものです。図の左側の場合は、1-射 を境界として隣接しています。図の右側の場合は、0-射 を境界として隣接しています。
プロファイルをハッキリと書くと:
図の左側では、 と は1次元の境界 を介して(この順で)隣接しています。一方、図の右側では、 と は0次元の境界 を介して(この順で)隣接しています。隣接条件を明示的に書くなら:
(k, j)-結合〈(k, j)-composition〉とは、j次元境界を介して隣接している2つのk-射に対して定義される結合です。今の例で言うなら:
- 2-射 と2-射 は、1-射 を介して隣接しているので、(2, 1)-結合可能である。(図の左側)
- 2-射 と2-射 は、0-射 を介して隣接しているので、(2, 0)-結合可能である。(図の右側)
3次元の場合も見ておきましょう。
図の意味は次のようです。
- 左側は、2-射 を介して隣接している2つの3-射
- 真ん中は、1-射 を介して隣接している2つの3-射
- 右側は、0-射 を介して隣接している2つの3-射
3-射のプロファイルを書きましょう。
この状況で、3-射の結合可能性は次のようになります。
- 3-射 と3-射 は、2-射 を介して隣接しているので、(3, 2)-結合可能である。(図の左側)
- 3-射 と3-射 は、1-射 を介して隣接しているので、(3, 1)-結合可能である。(図の真ん中)
- 3-射 と3-射 は、0-射 を介して隣接しているので、(3, 0)-結合可能である。(図の右側)
3-圏の場合は、(3, 2)-結合、(3, 1)-結合、(3, 0)-結合、(2, 1)-結合、(2, 0)-結合、(1, 0)-結合 の6つの結合を備えています*4。一般に、n-圏には 個の結合があります。
結合の演算子記号
結合は二項演算なので、(二項中置の)演算子記号を使うのが普通です。2-圏の場合3つの結合演算がありますが、僕は次のような記号を使っています。詳しくは「関手と自然変換の計算に出てくる演算子記号とか // 今後使う予定の演算子記号」を参照してください。煩雑さを避けて、図式順演算子記号だけを載せます。
2-射 | 1-射 | |
---|---|---|
1次元境界 | ||
0次元境界 |
新しい演算子記号 を下側(境界次元0)に挿入しているので、下側挿入方式と呼びましょう。これに対して、新しい演算子記号 を上側(境界次元1)に載せる方式を上側追加方式と呼びましょう。上側追加方式で演算子記号を決めると次のようになります。
2-射 | 1-射 | |
---|---|---|
1次元境界 | ||
0次元境界 |
演算子記号の選択として、下側挿入方式も上側追加方式も両方使われていて一長一短があります。
ここでは、下側挿入方式で決めた2-圏の演算子記号に対して、上側追加方式により3-圏の演算子記号を決めます。次のようになります。
3-射 | 2-射 | 1-射 | |
---|---|---|---|
2次元境界 | |||
1次元境界 | |||
0次元境界 |
この決め方が、これから話す話題 -- つまり、2-圏における等式的推論の圏論的定式化には向いています。
さて、演算子記号の決め方はともかくとして、高次圏の結合はどのように定義され、どのような性質をもつのでしょうか? これに関する一般論は必要ないので省略します。結合律、単位律、交替律は成立します。法則は厳密に〈strictly〉成立するとは限らず、だいぶ込み入った関係になります。ややこしいのでこれ以上は触れません。
恒等射
1-圏〈通常の圏〉では、0-圏〈対象〉に対して恒等射がただひとつだけ決まります。n-圏でも同様です。
- n-圏のk-射に対して、恒等(k + 1)-射がただひとつだけ決まる。
1-圏では、恒等射〈恒等1-射〉を のように書きますが、ここでは下付き添字ではなく と書きます。そうしないと のように下付きが入れ子になり読みにくくなるからです。
恒等射の次元が分かりにくくなることがあるので、必要なら右肩に次元を添えます。
- 0-射 の恒等1-射
- 1-射 の恒等2-射
- 2-射 の恒等3-射
- 3-射 の恒等4-射
また、プロファイルの矢印に、その射が恒等射であるという情報を含めた次の書き方も使います。
- 0-射 から への1-射があり、それは恒等1-射
- 1-射 から への2-射があり、それは恒等2-射
- 2-射 から への3-射があり、それは恒等3-射
- 3-射 から への4-射があり、それは恒等4-射
は、 という等式命題と同じ意味です。その他の次元でも、恒等k-射は(k - 1)-射の等式命題と同じ意味です。これは、等式命題の代わりに恒等射を使ってもいいことを示します。そう、最初の節で述べたアイディア
- 等式を恒等射で置き換える
です。
2-圏の3-射、4-射
「n-圏には、次元がnより大きい射は存在しない」と考えるのが普通の態度ですが、どうもこれは不便なようです。どんなn-圏でも(空n-圏でない限り)、任意の次元の射が存在すると考えたほうが便利だと思います。例えば、2-圏には3-射も4-射も存在します。
では、2-圏の3-射/4-射とはどういうものでしょうか? それは恒等射です。2-圏 の2-射 があるとき、 と のあいだの3-射とは次の恒等3-射だとします。
別な言い方をすると、 と のあいだの3-射とは という等式です。恒等射〈等式〉にラベルを付けてもかまわないので、次のようにラベル付けします。
この場合、3-射 と は同じなので、次の4-射が存在します。
この4-射は、「2-射 のあいだの等式のあいだの等式」と言えます。
このように考えれば、どんなn-圏でも、任意の次元の射が存在します。
恒等射だけの圏
n-圏 のすべてのk-射からなる集合を と書くことにします。特に:
の恒等射だけからなる部分n-圏を とします。また、
と約束します。次が成立します。
一般に:
ならば:
つまり、十分高い次元では、 と は区別がつきません。
恒等射だけからなるn-圏というと、非常につまらないn-圏のように思えますが、 には元のn-圏 と同じだけの結合演算が備わっています。それらの結合演算や演算法則を考えれば、 はそれなりに面白い構造を持ちます。
恒等射の計算と等式的推論
は2-圏だとして、 の3-射まで考えます。3-射は2-射のあいだの恒等射(2-射の等式)です。この状況で、3-圏としての結合演算は6つあり、それらの演算記号は先の表(下に再掲)のように決めます。
3-射 | 2-射 | 1-射 | |
---|---|---|---|
2次元境界 | |||
1次元境界 | |||
0次元境界 |
この表のなかで、3-射(2-射の等式)に対する3つの演算 とは何でしょうか? 結論を言ってしまうと、等式の推論規則です。以下に推論規則を列挙します。
2-射の等式の -推論規則:
2-射の等式の -推論規則:
2-射の等式の -推論規則:
これらの推論規則は分かりやすいと思いますが、射のプロファイル情報がハッキリしません。プロファイルを書き下します。
-推論規則を恒等射の記号を使って書けば:
3-射 と を-結合((3, 2)-結合)した結果は に等しいことを主張しています。「3-射が等しい」の等しさは4-射なので で書いています。つまり、-推論規則の圏論的対応物は3-射への演算と等式である恒等4-射だと言えます。
-推論規則を恒等射の記号を使って書けば:
3-射の-結合((3, 1)-結合)に関する等式(恒等4-射)ですが、2-射の-結合((2, 1)-結合、縦結合)に関する主張になっています。
-推論規則を恒等射の記号を使って書けば:
3-射の-結合((3, 0)-結合)に関する等式(恒等4-射)で、2-射の-結合((2, 0)-結合、横結合)に関する主張です。
以上の話は、 の部分高次圏 の3次元部分に注目して、その結合演算を見たわけです。2次元部分、1次元部分に注目すれば、1-射の等式、0-射の等式に関する推論規則が出てきます。
おわりに
圏論においても、何らかの条件や性質の記述には古典論理の論理式が使われますが、その一部分、特に等式は恒等射としての解釈を持ちます。等式的推論は恒等射の計算で代替できます。
古典論理による推論を排除することは出来ないにしろ、その一部分を圏論的計算で代替することは可能です。代替して嬉しいことは、算術計算と論理計算で別な計算体系を使う必要がなく、シームレスな計算になることです。
論理計算を圏論的計算で代替する試みは、やってみる価値があります。
*1:この図は「圏論的宇宙と反転原理と次元付きの記法」からです。
*2:この図は「おとぎ話としてのn-圏 -- 計算できる図形達の世界」からです。
*3:この図も「おとぎ話としてのn-圏 -- 計算できる図形達の世界」からです。
*4:次元が異なる射を結合するヒゲ結合を入れるともっと増えますが、本質的ではないので無視します。