「マイクロコスモ原理と構造の無限タワー」に、yamさんからコメントをいただきました。yamさんの疑問(モヤモヤ)は、少し前に僕が持っていた疑問(モヤモヤ)とたぶん同種のものでしょう。その疑問(モヤモヤ)は、「もう、無限に続くタワーを登るしかないんだな」と僕が覚悟を決めた動機のひとつでした。
順序対(ペア) (a, b) はどっから来るのでしょう? その起源、故郷はどこにあるのでしょうか? -- これがその疑問(モヤモヤ)です。順序対(ペア)は無限の彼方、天空の世界からやって来ると考えざるを得ず、順序対(ペア)の故郷を訪ねるには、デカルト構造の無限タワーを登るしかないようです。(下の絵はタワーじゃなくて豆の木)
内容:
記法の変更と追加
「マイクロコスモ原理と構造の無限タワー」と記法を少し変えます。それについては、メモ編の次の記事に書きました。
太字や下線などの装飾を使うのが辛い(欠点もある)ので、ダッシュ(プライム、シングルクォートで代用)を使うことにしたのが大きな変更点*2。例えば、Y(U, U) は Y'(U, U) とします。それと、単位対象(0-射)と単位射(1-射)を区別します。
- 単位対象は1(イチ)と書く。とある圏Cに注目してるなら、1∈|C|。
- 単位射はi(小文字アイ)と書く。i:1'→C なので、iはCの外にある射。
さらにいくつかの約束をここで追加します。
中置演算子記号を前置演算子記号(関数記号)にしたいときは、Haskellのセクション記法と同様に丸括弧で囲みます。例えば、掛け算 a×b は (×)(a, b) とも書きます。僕は、(×)をしばしばYと書いてました。Yを使う理由は「モノイドやモノイド圏の指標 補足解説」に書いています。
n-圏の結合〈composition〉はイッパイあり得ますが、それらを一律に「#」で表すことは「マイクロコスモ原理と構造の無限タワー」でやりました。このとき、上下の添字(#nk の n, k)は省略することがあります。自然変換(成分表示)の下添字も明らかなら省略することがあります。省略は好ましくないけど、簡潔さのため(めんどうだしさぁ)。
なにか対象A(アトムかも知れないし、集合かも知れないし、圏かも知れないし、関手かも知れないし、2-圏かも知れないし、…)があるとき、その恒等を一律にA^と書きます。これはDOTNの流儀です。AとA^を同一視してしまう流儀もあります -- 簡潔だけどちょっと分かりにくいので採用しません。
デカルト構造
小さいデカルト圏 C = (C, ×, 1, α, λ, ρ) を考えます。圏論的直積がデカルト・モノイド積×で与えられます。デカルト・モノイド積の単位対象1は、Cの終対象になっています。α, λ, ρ は、モノイド圏としての律子(律子に関しては「律子からカタストロフへ」を参照)です。
- (×):C×C→C in Cat
んっ? … オイオイオイオイ、C×C の×って何だよ? -- これは2-圏Catに備わったデカルト・モノイド積です。Catは単なる2-圏ではなくて、デカルト2-圏だったのです。Cの構造の一部である×とCatの構造の一部である×を区別するにはダッシュ記法(「モノイドやモノイド圏の指標 補足解説」参照)を使います。
- (×):C×'C→C in Cat
- (×'):Cat×''Cat→Cat in 2-CAT
2-CATは、必ずしも小さくない2-圏からなる3-圏とします。2階層分だけ書きましたが、(×''), (×'''), (×''''), ... の定義は無限に続きます。この無限性から逃れようがないです。でも、安定するなら平気です。
ここであやしいことを口走りますが; 「安定するなら平気」と思うことが、無基底・無限階層の世界における「悟り」なんだと思います。無限性を拒絶せずに受け入れるのです。
デカルト圏に話を戻します; デカルト圏は単なるモノイド圏以上のものです。デカルト構造を記述するには、モノイド構造に対し、さらに構成素を付け加える必要があります。追加の構成素は、終射 !、射影 π1, π2、対角 δ です。集合圏は小さな圏ではないですが、説明のために集合圏で言えば:
!, π1, π2, δ は自然変換ですが、そのプロファイルは、2-圏Catのなかで次のように書けます。
- ! :: C^⇒!'C#i : C→C in Cat (i:1'→C in Cat)
- π1 :: (×)⇒(π'1)C,C : C×'C→C in Cat
- π2 :: (×)⇒(π'2)C,C : C×'C→C in Cat
- δ :: C^⇒δ'C#(×) : C→C in Cat
ここで:
- !' :: Cat^⇒!''Cat#i' : Cat→Cat in 2-CAT (i':1''→Cat in 2-CAT)
- π'1 :: (×')⇒(π''1)Cat,Cat : Cat×''Cat→Cat in 2-CAT
- π'2 :: (×')⇒(π''2)Cat,Cat : Cat×''Cat→Cat in 2-CAT
- δ' :: Cat^⇒δ''Cat#(×') : Cat→Cat in 2-CAT
デカルト圏Cをホストする2-圏であるCatがデカルト圏であり、×', 1', α', λ', ρ', !', π'1, π'2, δ' を備えているのです。そのデカルト圏Catをホストする3-圏である2-CATもまたデカルト圏の構造(×''など)を持つのです。
「デカルト圏をホストする(より高次の)圏はデカルト圏である」というマイクロコスモ原理は無限に適用できるので、デカルト構造という構造は(上方)無限タワーを形成し、この無限タワーを通してしかデカルト構造の包括的理解は得られません。
幸いにも、デカルト構造の無限タワーは安定し、Catより上の次元(階層)では同じことの繰り返しになります。構造をホストする環境の次元はどんどん上がりますが、その環境の2-構造(0射, 1射, 2射 までの構造)しか関与しないので、神ならぬ我々でも無限の彼方まで見通すことができます。それが「安定する」の意味です。
無限タワーを恐れず、積極的に登ろうという気分を盛り上げるには、「高次圏: 無基底・無限階層 補足」、特にスザウィールの言葉を参照。
二項演算とペアリング
二項演算とペアリング(ペアを作る操作)は密接に関連しています。この二者の相関が、ジグザグ状の軌跡を描いて無限タワーを登っていくことになります。その様子を見てみましょう。
なんかの二項演算の中置演算子記号を・とします。a, b に対して a・b を考えることができます。とある範囲Aのなかでしか a・b は定義できないでしょう。つまり、a∈A, b∈A に対して(のみ)、a・b ∈A が定義される。
記号・を前置演算子記号(関数記号)に変更すると、a・b は (・)(a, b) と書けます。これはまた、ペア (a, b) を関数 (・) に入れた (・)((a, b)) とみなされて、次のプロファイルを得ます。
- (・):A×A→A
集合の直積記号×は中置演算子記号です。集合 A, B に対して、A×B を考えることができます。直積といえども、とある範囲C(多くの場合はSet)でしか A×B は定義できないでしょう。つまり、A∈0C, B∈0C に対して(のみ)、A×B ∈0C が定義される。x∈0Y は、x∈|Y| と同じ意味です。
記号×を前置演算子記号(関数記号)に変更すると、A×B は (×)(A, B) と書けます。これはまた、ペア (A, B) を(二項)関手 (×) に入れた (×)((A, B)) とみなされて、次のプロファイルを得ます。
- (×):C×'C→C
圏の直積記号×'は中置演算子記号です。圏 C, D に対して、…[以下省略]…
今述べたような文面は、いつまでもいつまでも続くのです。しかし、「同じことを言ってるだけじゃないか」となります。無限に続くが循環する、安定するのです。循環も含めてデカルト構造の無限タワーを構成します。
ここで重要な注意は、これぞデカルト構造の無限タワー〈The infinite tower of cartesian structures〉と呼べるモノは特にないことです。集合圏以外にデカルト圏はいくらでもあります。ひとつ選んだデカルト圏をホストする“より高次の圏”もいくらでもあります。いくらでもある選択肢の無限階層があり、そのなかから我々は目的や好みに応じてひとつの無限タワーを選ぶだけです。無限タワーが無限にあり、特別な基底はなく、それらは相互依存しています。
おわりに
デカルト構造の無限タワーは安定します。安定するので、ある階層から先は同じことの繰り返しになります。別な言い方をすると、指標と等式的法則により、あからさま〈explicitly〉に循環定義を書き下せるってことです。
循環定義を書き下す作業は、やれば出来ることですが自明ではありません。記法・図法の工夫をしないと、なかなかうまく書き下せないですし、意外に量があるんですよね。僕が見た範囲では、デカルト構造のキチンとした循環定義は公開されてないようです。内容的には“当たり前のことの再確認”なので、誰もやりたがらない作業なのかな? できれば、デカルト構造の全貌(=無限タワーの総体)を晒したいと思っています。
*1:画像: https://fanart.tv/movie/81005/jack-the-giant-slayer/ 映画『ジャックと天空の巨人』
*2:手書きのときは、オーバーラインがいいかも知れません。オーバーラインなら、2本、3本重ねることが出来て、比較的に視認性もいいですから。