このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

一般関手モデル:「圏の表示」の圏

プレーンな関手データモデルでは、スキーマ全体からなる圏Schは圏の圏Catの部分圏とみなせる圏です。Sch = Cat と考えてもいいでしょう。S∈|Sch| に対して、関手圏 [S, Set] がスキーマSインスタンスの圏となります。Schの選び方を変えたり、集合圏Setを別な圏に取り替えたりして、様々なバリアントを構成できます。

スキーマ全体からなる圏をドクトリンインスタンスを構成するための圏をアンビエントと呼ぶと、プレーンな関手データモデルでは「ドクトリン=Catアンビエント圏=Set」という設定になっています。CatSetもよく知られた圏なので、新しい概念を何も導入する必要がないところがミソですね。

ドクトリンとアンビエント圏以外に、関手データモデルにはもうひとつの圏が関与しています。スピヴァックはあまり強調してないのですが、圏の表示(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は PrsSch の関手となります。一方、S∈|Sch| に対して、Sの圏としての構造を忘れて表示とみなしたものを Uncat(S) とします。Uncatは、SchPrs の関手となります。

CatとUncatは随伴になります。つまり、次のホムセットのあいだの自然な同型を定義します。

  • Sch(Cat(P), T)
  • Prs(P, Uncat(T))

この随伴は、圏の圏Catと有向グラフの圏Graphのあいだの、FreeCat:GraphCat と Forget:CatGraph による随伴と似てますが、少し違いがあります。Prsの対象は単なる有向グラフではなくてパス同値関係(の集合)が付随してます。これにより、次が成立します。

  • Cat(Uncat(S)) は S上の恒等関手と同値になる。

おおよそ(up-to-equivalence)、Uncatは埋め込みだと言えます。この埋込みにより、SchPrsの部分圏と同一視すると、CatはPrs上の自己関手となり、関手の同値の意味でべき等になります。つまり、Catは「圏モドキを圏に正規化する」操作となります。正規化なので、二度やっても効果は一度分となるのです。

別な見方をしてみましょう; P|→Cat(P) という対応は、「変数の集合V |→ Vの変数を含む項の集合」という対応と類似のものです。Pは構文定義に近いものです。パス同値関係を持つので構文的な簡約規則も備えています。Uncat(Cat(P)) で定義されるモナドは、項の生成規則と簡約規則からなる型付き計算を表現していると言えます。

ドクトリンSchに対して、その表示の圏PrsとCat/Uncat随伴は、スピヴァック理論の重要な構成素だと思います。表示の圏により、ドクトリンを具体的に取り扱う手段が与えられるからです。また、Cat/Uncat随伴は、それ自身としてもなかなか興味深い構造です。