代数的定義形式とアンビエント構造

内容：

1. 代数的定義形式
2. 代数的定義形式の同義語群
3. アンビエント
4. 定義形式のアンカリング
5. 単位対象と格上げ
6. 値k-射と定義形式の格上げ
7. モデルとモデルの圏
8. TBD：ローヴェル・フレームワーク
9. TBD：族と抽象と脱抽象

代数的定義形式

n-圏と関連する圏論的実体〈categorical entities〉を定義する方法として：

1. 代数的定義〈algebraic definition〉
2. 非代数的定義〈non-algebraic definition〉

がある。短い解説は

• http://www.maths.ed.ac.uk/~tl/gurski_review/gurski_review.pdf

詳細な説明は

• Title: Comparing algebraic and non-algebraic foundations of n-category theory
• Author: Thomas Peter Cottrell.
• URL: http://etheses.whiterose.ac.uk/5324/1/CottrellThesis.pdf

代数的定義では、モノと操作を具体的・明示的に与える。非代数的なら存在だけを要求する。代数的定義の形式を、そのまんまだけど代数的定義形式〈algebraic definition form〉と呼ぶ。

代数的定義形式の同義語群

代数的定義形式に対して、次の同義語群ができる。次元nを付けて並べると：

1. n-代数(的)?定義(形式)?
2. n-定義(形式)?

nの省略も含めて展開すると：

1. n-代数的定義形式
2. n-代数定義形式
3. n-代数的定義
4. n-代数定義
5. n-定義形式
6. n-定義
7. 代数的定義形式
8. 代数定義形式
9. 代数的定義
10. 代数定義
11. 定義形式
12. 定義

こうして用語の爆発が生じる。次も同義語。

1. n-指標
2. n-仕様
3. n-セオリー

n = 1 の場合の計算科学での呼び名は：

1. 型クラス
2. インターフェイス
3. （仕様の）モジュール
4. セオリー

もちろん、色々と微妙に区別する人もいる。n-定義形式は、次元により(n+2)個のセクション〈{パーツ（パート） | ブロック | パーティション | セグメント}〉に区切られる。(n + 2)個のセクションの呼び名の流儀も：

1. 0からnまでは定義データ（英語では単にdata）セクションと呼び、(n + 1)-セクションを公理〈axiom〉セクションと呼ぶ。
2. すべて、定義データ〈data〉のセクションと呼ぶ。
3. 次元ごとに、それぞれの別な呼び名を与える。

n = 1 のときの、k次セクションとk-構成素〈k-constituent〉の呼び名の例：

• k = 0 0次セクションの構成素：型、集合、対象、ソート、種
• k = 1 1次セクションの構成素：関数、写像、演算、オペレーション、オペレーター、準同型、射
• k = 2 2次セクションの構成素：公理、条件、関係、表明、等式、恒等式、制約

(n + 1)-セクションの構成素〈(n + 1)-構成素〉には、「一貫性〈coherentce | coherent〉」という形容詞を付けることが多い。一貫性と同義で整合性〈consistency〉、統合性〈integrity〉、統一性〈compatibility〉、協調性〈cooperativity〉などがあるが、すべてが（自然言語として）類語で区別する根拠・基準はない。

k-セクションの構成素を圏論的には：

1. k-射
2. k-セル
3. k-生成射
4. k-アロー
5. k-オペレーション

などと呼ぶ。

アンビエント

同義語群から、とりあえず「n-定義形式」を選んで先を続ける。

n-定義形式は、n-アンビエントのなかで意味を持つ。実際的には、n-アンビエントが暗黙に仮定されている。n-アンビエントは、n-圏と対象とする(n + 1)-圏n-Cat、または、n-Cat上の具体圏（構造付きn-圏の圏）である。いずれにしても、アンビエントは(n + 1)-圏の構造を持ち、付加的な構造〈extra structure〉も持つかもしれない。

• n-アンビエント（包括的全体）は、少なくとも(n+1)-圏の構造を持つ。

例：

• 0-定義形式（離散グラフ＝点だけ＋等式）の解釈の場である0-アンビエントは、1-圏の構造を持つ。典型的には集合圏Setである。
• 1-定義形式（グラフ＋等式）の解釈の場である1-アンビエントは、2-圏の構造を持つ。典型的には圏の圏Catである。
• 2-定義形式（2-グラフ＋等式）の解釈の場である2-アンビエントは、3-圏の構造を持つ。典型的には2-圏の圏2-Catである。

暗黙的であれ明示的であれ、アンビエントは重要な概念である。アンビエントがなくてははじまらない！ 世界がないなら、モノもコトもない。

アンビエントを宇宙、世界、オーシャンなどとも呼ぶ。以下に同義語群：

1. アンビエント
2. 宇宙（単銀河の小宇宙、ワーキング宇宙）
3. 世界
4. オーシャン
5. レルム
6. ドクトリン
7. ブランド

n-アンビエント〈n-{小 | ワーキング}宇宙 | n-世界 | n-レルム | n-ドクトリン | n-ブランド〉のなかには、対象としてn-圏が入っている。

例：

• (-1)-アンビエント＝(-1)-ドクトリンには、(-1)-圏＝真偽値が入っている。→ アンビエント ＝ Bool
• 0-アンビエント＝0-ドクトリンには、0-圏＝集合が入っている。→ アンビエント ＝ Set
• 1-アンビエント＝1-ドクトリンには、1-圏＝圏が入っている。→ アンビエント ＝ Cat, CAT
• 2-アンビエント＝2-ドクトリンには、2-圏が入っている。→ アンビエント ＝ 2-Cat, 2-CAT

もう一度繰り返しておくと：

• n-定義形式〈n-指標 | n-仕様 | n-セオリー | n-型クラス〉は、n-アンビエント〈n-宇宙 | n-世界 | n-ドクトリン | n-レルム | n-ブランド〉なしにはあり得ない。暗黙的であれ、必ずアンビエントは存在している。

定義形式のアンカリング

n-定義形式として次の形を採用する。

definition {
 objects a, b, c;
 1-morphisms f, g:a->b;
 2-morphisms α::f -2> g, β::g -2> f;
 conditions α;β = f^;
}

詳細はどうでもいいのだが：

• 1-morphismの代わりにobjectを使った。
• (n + 1)-morphismの代わりにconditionを使った。

もちろん、definition, object, conditionの代替語（同義語）はいくらでもある。

• definition: signature, specification, theory, module, class, interface
• object: type, sort
• condition: assertion, equality, axiom, identity, relation, constraint

以上のような形式を非アンカー形式〈unanchored form〉と呼ぶ。次はアンカー形式〈anchored form〉の例。

definition [category Set]{
 objects a, b, c;
 1-morphisms f, g:a->b;
 2-morphisms α::f -2> g, β::g -2> f;
 conditions α;β = f^;
}

上記の[category Set]をアンカー指定〈anchor specification〉、Setのように具体的なアンビエントの対象をアンカー〈anchor〉と呼ぶ。定義形式〈指標 | 仕様 | 型クラス〉にアンカーを指定することをアンカリング〈anchoring〉と呼ぶ。

実際の定義形式〈指標 | 仕様 | 型クラス〉では、暗黙にアンカリングされていることが多い。多くの場合は圏Setでアンカリングされている。

暗黙的了解事項として、アンビエントとアンカーが特定されていることが多い。アンカーが特定されていて、さらにそのアンカー以外のアンビエント内対象を使わないなら、アンビエントは、単一対象と恒等射しかもたない自明圏（それでも(n+1)-圏）になる。この自明圏が省略されているケースが多い。重大な教訓として：

• 暗黙の了解事項と省略は諸悪の根源

一般に、n-定義形式のアンカーはn-アンビエントの特定対象なので、特定n-圏である。アンビエントが“構造付きn-圏〈structured n-category〉の圏”の場合、アンカーは構造付きn-圏になる。

定義形式〈指標 | 仕様 | 型クラス〉がアンカリングされると、解釈の宇宙〈semantic universe〉が限定される。固定されたアンカー上のオペレーション（次元1以上の生成射をオペレーションと呼ぶ）だけを考えることになる。

n-定義形式のアンカリングにより、インデックス付きn-圏の構造ができる。インデックス集合は、アンビエント（(n + 1)圏）の対象類である。このテのインデックス付きn-圏とファイバリングを調べるのは課題。

単位対象と格上げ

n-アンビエント〈n-ドクトリン | n-レルム | n-ブランド〉は、n-圏（または構造付きn-圏）からなる(n+1)-圏で、そこには特定された(n, 0)-シングルトン圏があるとする。特定された(n, 0)-シングルトン圏を単位対象〈unit object〉（それ自体n-圏である）と呼ぶ。n-アンビエントがモノイド圏かどうかわからないので、通常どおり終対象と呼ぶほうがいいが、次の理由（言い訳）がある。

1. n-アンビエントにはデカルト積が入ることを仮定するのが普通。そのとき、単位対象は実際にデカルト・モノイド積の単位対象である。
2. 単位型〈unit type〉と言葉をあわせる。

n-アンビエント（(n + 1)-圏）には、n-単位対象（特定された(n, 0)-シングルトン圏）を要求する。n-単位対象により、

• n-アンビエントの対象（それ自身はn-圏）の内部構造をアンビエントに引っ張り出す（抽出する、引き上げる）ことが出来る。

対象の中の人の立場では、対象内にある内部構成素（n-圏のk-射）が、アンビエントの射に格上げ〈promote | bump up〉されることになる。このとき、

• 対象内部のk-射は、アンビエントの(k + 1)-射になる。

格上げは、

• 内部のモノが外部のモノとなるので、脱出〈extrication | 開放 〉により格上げされる。
• 射の次元が1増えるので、次元的にも格上げされる。

アンビエントは、アンビエントの対象より次元が1大きいので、対象内のすべての射をアンビエントの射に格上げできる。

格上げによりできる錐体構造を格上げ錘〈promoted cone〉と呼ぶ。

n-アンビエント内対象（n-圏）の内部0-射（対象）の格上げを特に次のように呼ぶ。

1. 値〈value〉
2. 要素〈element〉
3. 点〈point〉
4. 標準点〈canonical point〉、大域的〈global point〉（一般化点〈generalized point〉に対して）

n	n-圏	その0-射	0-射の格上げ
0	集合	要素	値 ポインティング関数
1	圏	対象	対象 ポインティング関手
2	2-圏	対象	対象 ポインティング2-関手

n-アンビエント内対象（n-圏）の代わりに、その格上げ錐を使えば、内部射は格上げした外部射に変わるので、すべては外部（アンビエント）の言葉で記述できる。この論法を格上げ論法〈promotion argument〉と呼ぶことにする。

• 格上げ論法は重要だ。

格上げ論法を徹底するためには、n-アンビエント内対象（n-圏）がデカルト閉であること、そしてアンビエントそのものがデカルト閉であることが要求される。

nアンビエント自体のデカルト閉性（デカルト閉な(n + 1)-圏）、アンビエント内対象（n-圏）のデカルト閉性（デカルト閉なn-圏）のためには、対象（内部の(n - 1)圏とアンビエント内のn-圏）指数対象が必要になる。したがって、指数対象の構成が重要な課題。

値k-射と定義形式の格上げ

n-アンビエント内のn-定義形式があるとき、それを(n + 1)-定義形式に格上げ（または持ち上げ）できる。格上げされた(n + 1)-定義形式は、アンビエントにアンカーされる。アンビエント以外にアンカーするには、アンビエントの外の世界を考える必要がある。そのときは、アンビエントから脱出〈extricate | escape | move outside〉しなくてはならない。

アンビエントから脱出しないなら、アンビエントだけを対象とする1次元高い自明圏を考えて、それをアンビエントが所属するメタ宇宙とする。これを自明なメタアンビエント（trivial meta-ambient）と呼ぶ。追加情報なしで作れるメタアンビエントは、自明なメタアンビエントだけである。

n-アンビエント内のn-定義形式を格上げするには、当然に格上げ論法を使う。単位対象を域とするn-アンビエント内のk-射（(k - 1)-変換手）を値k-射〈value k-morphism〉と呼ぶ。

n	n-圏	単位対象	k	値k-射
0	集合	なし	0	なし
1	集合圏	単元集合	1	値ポインティング関数
2	圏の圏	単元圏	1	対象ポインティング関手
2	圏の圏	単元圏	2	射ポインティング自然変換

値n-射を単に値射〈value morphism〉とも呼ぶ。

n-定義形式を格上げするには、次の手順を使う。

1. n-定義形式のk-morphismをすべて(k+1)-morphismに直す。
2. valueを付けて、value k-morphismとする。
3. value k-morphismは域対象を省略してよいので、プロファイルはもとのまま。

この方法を繰り返し使うことにより、n＜n' である自然数に対して、低い次元のn-定義形式は、高い次元のn'-定義形式にそのまま格上げできる。

モデルとモデルの圏

アンビエントの別名は：

1. 宇宙
2. 世界
3. オーシャン（アンカーを投錨する先だから）
4. レルム
5. ドクトリン
6. ブランド

このなかから適当な対象（n-アンビエント内対象＝n-圏）を選ぶことがアンカリング。アンカーとして選ばれたn-圏を：

1. セマンティックn-圏
2. 意味n-圏
3. 標的n-圏〈target n-category〉

などと呼ぶ。アンビエント（(n+1)-圏）とセマンティック圏（n-圏）は混同される恐れがあるし、セマンティック圏をアンビエント圏と呼ぶこともある（あった）。

n-アンビエントをAと書くことにする。A∈|(n+1)-Cat| と考えてよい（少なくとも、忘却関手でそうみなせる）。また、C∈|A| ならば、C∈|n-Cat| である。これも、少なくとも忘却関手でみなせる、とする。正確な定義には、“具体的〈具象的〉n-圏”と“構造付きn-圏”の定義が必要。

Σがn-定義形式、Cがセマンティックn-圏のとき、ΣとCを同じ舞台に載せることができる。これは、ComCat-随伴を使う。n-コンピュータッド〈ポリグラフ〉の圏とn-圏の圏が随伴なので、n-Comかn-Catのどっちを共通舞台にしてもよい。

n-Com側で議論するときして、ΣからC（の忘却イメージ）へのコンピュータッド射をモデル〈model〉と呼ぶ。コンピュータッド射は（n-Cat側に移れば）関手と同じことだから、モデルの圏〈category of models〉を関手圏として作れる。n≧2 のときは、高次関手圏（変換手の圏）を作る。

n = 1 の場合、次は同義語である。

1. モデルとモデルの圏
2. 関手と関手圏
3. 代数と代数の圏
4. インスタンスとインスタンスの圏
5. 余前層と余前層の圏

モデルの圏の射は：

1. ××の射〈morphism〉
2. ××の準同型(射)?〈homomorphism〉
3. 模倣〈simulation〉
4. 変換〈transformation〉（実体は自然変換だから）

モデルには、反変モデルと共変モデルがある。それによって、前層か余前層かが変わる。n≧2だと、反対圏の作り方がイッパイあるので、反変・共変では片付かない。

Σをn-定義形式、Cをセマンティックn-圏とするとき、モデルの圏を[Σ, C]と書く。B(-. -) := [-, -] と置くと、Bはn-Comとn-Catが両側から作用する両側加群〈bimodule〉になると思う。豊饒圏とか米田埋め込みとも関係するだろうが、課題。

TBD：ローヴェル・フレームワーク

TBD: ローヴェル・セオリーのフレームワーク。アンビエントは使う。アンビエント内で特別な対象（コア対象）を指定するが、それはアンビエントが2-モナドの2-EM代数の2-圏として作られていることが前提になる。

TBD：族と抽象と脱抽象

TBD: 定義形式の格下げを定義したい。格上げして格下げするともとに戻るように。そのとき、パラメータ族／インデックス族〈parametrized/indexed family〉と変換手〈transfor〉の関係が問題になる。まだまとまってない。