| この記事 | 10年後 |
|---|---|
| 圏の表示の圏 Prs | 形状の圏、または指標の圏 |
| 圏の表示（Prs の対象） | 1-コンピュータッド |
| ドクトリン（Sch） | ？ |
| アンビエント圏（Set） | ターゲット圏 |
「アンビエント」の意味・使用法は変わっています。ターゲット圏（この記事の“アンビエント圏”）が所属する2-圏がアンビエントです。今の場合、ターゲット圏（この記事の“アンビエント圏”）が $`{\bf Set}`$ なので、アンビエントは $`{\bf CAT}`$ になります。
「ドクトリン」という言葉は、色々な意味で使われて意味が曖昧になっているので、「極限ドクトリン」のように形容詞付きで使わないと意味不明です。裸の「ドクトリン」は使わないほうが吉。
この記事の最後にも解説の追記があります。
[/追記]
プレーンな関手データモデルでは、スキーマ全体からなる圏Schは圏の圏Catの部分圏とみなせる圏です。Sch = Cat と考えてもいいでしょう。S∈|Sch| に対して、関手圏 [S, Set] がスキーマSのインスタンスの圏となります。Schの選び方を変えたり、集合圏Setを別な圏に取り替えたりして、様々なバリアントを構成できます。
スキーマ全体からなる圏をドクトリン、インスタンスを構成するための圏をアンビエント圏と呼ぶと、プレーンな関手データモデルでは「ドクトリン＝Cat、アンビエント圏＝Set」という設定になっています。CatもSetもよく知られた圏なので、新しい概念を何も導入する必要がないところがミソですね。
ドクトリンとアンビエント圏以外に、関手データモデルにはもうひとつの圏が関与しています。スピヴァックはあまり強調してないのですが、圏の表示（presentation）の圏です。この圏をPrsと書くことにしましょう。
Prsの対象は、有向グラフとパス同値関係（path equivalence relation、可換図式と言っても同じ）の集合を組にしたものです。Prsの射は、パス同値関係を保存するような有向グラフの準同型写像です。圏の表示（有向グラフ＋パス同値関係）は、“生成系と関係”による圏の定義で、圏の表示から一意的に圏を構成できます。グラフから自由圏を作ってから、パス同値関係による商（quotient）をホムセットにします。
[追記]すぐ下に出てくるCatは関手です。圏の圏Catと、字の太さ以外は同じなので注意してください。[/追記]
P∈|Prs| に対して、上記の方法で作られた圏を Cat(P) とします。f:P→Q in Prs に対しても、Cat(f):Cat(P)→Cat(Q) in Sch を定義できるので、Catは Prs→Sch の関手となります。一方、S∈|Sch| に対して、Sの圏としての構造を忘れて表示とみなしたものを Uncat(S) とします。Uncatは、Sch→Prs の関手となります。
CatとUncatは随伴になります。つまり、次のホムセットのあいだの自然な同型を定義します。
- Sch(Cat(P), T)
- Prs(P, Uncat(T))
この随伴は、圏の圏Catと有向グラフの圏Graphのあいだの、FreeCat:Graph→Cat と Forget:Cat→Graph による随伴と似てますが、少し違いがあります。Prsの対象は単なる有向グラフではなくてパス同値関係（の集合）が付随してます。これにより、次が成立します。
- Cat(Uncat(S)) は S上の恒等関手と同値になる。
おおよそ（up-to-equivalence）、Uncatは埋め込みだと言えます。この埋込みにより、SchをPrsの部分圏と同一視すると、CatはPrs上の自己関手となり、関手の同値の意味でべき等になります。つまり、Catは「圏モドキを圏に正規化する」操作となります。正規化なので、二度やっても効果は一度分となるのです。
別な見方をしてみましょう； P|→Cat(P) という対応は、「変数の集合V |→ Vの変数を含む項の集合」という対応と類似のものです。Pは構文定義に近いものです。パス同値関係を持つので構文的な簡約規則も備えています。Uncat(Cat(P)) で定義されるモナドは、項の生成規則と簡約規則からなる型付き計算を表現していると言えます。
ドクトリンSchに対して、その表示の圏PrsとCat/Uncat随伴は、スピヴァック理論の重要な構成素だと思います。表示の圏により、ドクトリンを具体的に取り扱う手段が与えられるからです。また、Cat/Uncat随伴は、それ自身としてもなかなか興味深い構造です。
$`\quad \xymatrix@C+1pc{
{\bf Prs} \ar@/^1pc/[r]^{\mathrm{Cat}}
\ar@{}[r]|{\bot}
& {\bf Sch} \ar@/^1pc/[l]^{\mathrm{Uncat}}
}\\
\quad \text{ in } {\bf CAT}
`$
次は1-圏の2-圏への埋め込みです。
$`\quad \mathrm{Inc} : {\bf Sch} \to {\bf Cat} \subset {\bf CAT} \text{ in }\mathbb{2CAT}`$
$`J := \mathrm{Cat} * \mathrm{Inc}`$ と定義します。関手 $`J`$ は、形状〈指標〉の圏（今の場合は $`{\bf Prs}`$）からアンビエント2-圏 $`{\bf CAT}`$ への関手です。
$`\quad J : {\bf Prs} \to {\bf CAT} \text{ in }\mathbb{2CAT}`$
表示〈形状〉が $`P`$ であるデータベースインスタンスと自然変換の圏を $`\mathrm{Inst}(P)`$ とすると：
$`\quad \mathrm{Inst}(P) := {\bf CAT}\text{-}\mathrm{Diag}^{{\bf Prs}, J}[P] ({\bf Set})
= {\bf CAT}(J(P), {\bf Set})
\; \in |{\bf CAT}|
`$
[/追記]
