n-セオリーとインスティチューション

やった、n-セオリーから自然にインスティチューションが出てくる。

n-セオリー

まず、n-セオリーのk-段階（k-階層、次元k）の定義：

• (At dimension k): Σ_k∈₀k-Spef[Σ_k+1], A_k∈₀k-Mod[Σ_k+1](Σ_k, A_k+1)
• C_k := k-Mod[Σ_k+1](Σ_k, A_k+1)
• k-Mod[Σ_k+1]:k-Spef[Σ_k+1]×C_k→C_k
• k-Mod[Σ_k+1](σ, X) := C_k+1↑[Free_k(σ), X]

ここで、C↑[X, Y] は、Cがデカルト閉n-圏だとしての指数（内部ホムn--圏）。Free_kはk-レイヤーの自由生成関手。レイヤーごとに、k-Spef[Σ_k+1] と C_k のあいだの随伴系が必要。

これが重要、つうかこれが全てと言ってもいい。事例を出すと：

...
(At dimension 3): Σ3∈03-Spef[Σ3+1],  A3∈03-Mod[Σ3+1](Σ3, A3+1)
(At dimension 2): Σ2∈02-Spef[Σ2+1],  A2∈02-Mod[Σ2+1](Σ2, A2+1)

次元kのこの構造を、k-レイヤーと呼ぶことにする。（k-パートは関手の場合に、0-パートとか1-パートとか使う。他の候補はk-ストレイタム。）k-レイヤーの定義には(k+1)-レイヤーが必要になる。k-レイヤーを(Σ_k, A_k)とも書く。

• Σ_kは、k-仕様と呼ぶ。k-仕様はk-圏の生成系である。
• A_kは、選ばれたk-インスタンスで、下の階層のアンビエントとなるのでk-アンビエントとも呼ぶ（やめるかも）。k-アンビエントの構造の台は(k-1)-圏である。ここが名前と実体の次元が感覚的にズレる（実際はズレてない）ので注意。k-アンビエント（k-構造）の台をアンビエント(k-1)-圏とも呼ぶ。
• k-Mod[Σ_k+1](Σ_k, A_k+1)は、k-圏からなる(k+1)-圏である。これをC_kとも書いて、セオリーのk-クラスと呼ぶ。k-クラスはk-インスタンス＝k-構造をホストするのでk-圏になる。
• C_k = k-Mod[Σ_k+1](Σ_k, A_k+1)の対象を、k-インスタンス（k-構造）と呼ぶ。アンビエントの場合と同じように、名前と実体の次元がズレる（ズレたような気分がする）。k-インスタンスの台は(k-1)-圏なので、台をインスタンス(k-1)-圏とも呼ぶ。

紛らわしいところをまとめると：

• k-アンビエントの台は、(k-1)-圏である。k-アンビエントはk-インスタンスでk-構造なのだから、台は次元が下がる。
• k-Modは、(k+1)-圏、対象はk-構造、対象（k-構造）の台は(k-1)-圏である。
• k-インスタンスはk-Modの対象（k-構造）なので、構造の台対象(k-1)-圏である。
• k-アンビエント（k-構造）は、特定されたk-インスタンス（k-構造）である。

下限次元（最小次元）がnであるセオリーをn-セオリーと呼ぶ。例えば、2-セオリーは、次元2までのレイヤーを持つ。上限はないので、いくらでも高い次元のレイヤーを持つ。次元はレイヤーのz-インデックス。

n-レイヤーの構成素は：

1. 指標／仕様のn-圏
2. クラスと呼ばれるデカルト閉n-圏
3. 仕様n-圏とクラスn-圏のあいだの自由生成・忘却スタイルの随伴系
4. 仕様n-圏から選ばれた対象（n-仕様）、一階層下のメタ仕様（教義のドクトリン）になる。
5. クラスn-圏から選ばれた対象（n-インスタンス）、一階層下のアンビエントになる。

インスティチューション

インスティチューションにも次元nがって、

• (n+1)-セオリーがあると、n-インスティチューションが作れる。
• n-インスティチューションを作るには、(n+1)-セオリーが必要。

かようにセオリーとインスティチューションは相互依存的で、お互いを必要としている。一心同体と言ってもいい。

単にインスティチューションと言った場合は1-インスティチューションを指す。したがって、インスティチューションは2-セオリー＝ドクトリンを必要とする。ドクトリンを、D = {(Σ_k, A_k) | k≧2}と書く。

ドクトリンDに対してインスティチューション (Sig, Mod, Sen, (-)^*, (-)_*, |=) を作る。

• Sig := 1-Sig[Σ₂]
• Mod := 1-Mod[Σ₂](-, A₂)
• For σ in Sig. Sen(σ) := (Super(σ) in 1-Spef[Σ₂])
• For φ:σ→σ' in Sig. For M:(Free(σ')→A₂. φ^*(M) := φ;M :σ→A₂ in (1-Mod[Σ₂](σ, A₂) = Sig)

(-)_*, |= は面倒なんで少し説明をする。

Sig = 1-Sig[Σ₂] と定義した。1-Sig[Σ₂] ⊆ 1-Spef[Σ₂] なので、作業用に、Spef := 1-Spef[Σ₂] と置く。既にSenは定義したが、

• Sen(σ) := (Super(σ) in Spef)

Super(σ)とは何かというと、圏Spefのなかで σ⊆τ となる inclusion map の全体からなるクラス SUPER(σ) を同値関係で割ったもので、Sub(σ)のある種の双対になる。

φ:σ→σ' in Sig に対して、φ_*:Sen(σ)→Sen(σ') in Set は前送り〈push-forward | pushout〉で定義する。σ⊆τ は i:σ→τ in Spef とみなして、

σ -φ→ σ'

i        ?

v        v

τ - ?→ ?τ'

上記の図式は可換に埋められる〈can be fulfilled〉とする。Spefを有限余完備と仮定するわけだ。埋められた対象(?τ')を φ_*(τ) とすると、

• mono ?:σ'→φ_*(τ) in Spef
• σ'⊆φ_*(τ)
• φ_*(τ)∈Super(σ')
• φ_*(τ)∈Sen(σ')

M' in Mod(σ'), τ∈Sen(σ) に対して、

• φ^*M' |=_σ τ ⇔ M' |=_σ' φ_*τ --(充足性条件)

が必要。N |=_σ τ の定義は：

• (σ⊆τ)^* : Mod(τ)→Mod(σ)
• N |=_σ τ :⇔ N in Im( (σ⊆τ)^* )

指標σと仕様τのあいだの包含 σ⊆τ in Spef があると、モデル圏（モデル1-圏）のあいだの関手が誘導される。誘導された関手は、部分圏の埋め込みだが、対象Nがその部分圏に入っているかどうかを判断するのが |= 。

Sen(σ)は最初からプレ順序構造を持ち、そのブレ順序はMod(σ)の部分圏の束構造に反映される。したがって、充足関係と充足条件（充足関係の公理）は、モデル圏の部分圏の束構造が、リダクト関手φ^*と強調していることを示す。

モデル・リダクト関手（モデルの単純引き戻し）と文翻訳関手（文の余ファイバー前送り）の定義から、これらは強調するようになっている。

• φ^*M' in Im( (σ⊆τ)^* ) ⇔ M' in Im( (σ'⊆φ_*)^* )
• φ;M' ∈₀ Mod(τ) ⇔ M' ∈₀ Mod(φ_*(τ))

形式理論は、構文論と意味論からなるが、構文論が指標／仕様のn-圏が担当し、意味論をクラスのn-圏が担当する。選ばれた仕様が構造の種別を決定して、その仕様に対するモデル圏が意味論を与える。ただし、モデル圏はアンビエントに依存して。そのアンビエントは一階層上の選ばれたインスタンスとなる。

一階層上で選ばれた仕様とインスタンスがあり、選ばれた仕様が下の階層のドクトリン仕様、選ばれたインスタンスが下の階層のアンビエントを与える。

クラス、型、型クラス、ドクトリン、セオリーなどが、構文側の存在（指標、仕様）を指すか、意味論側の存在（n-圏、アンビエント）を指すのかがマチマチ。