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

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

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

参照用 記事

ベキ集合ファイブレーション

インデックス付き圏(indexed category)を見つけたとき、とりあえずグロタンディーク構成(Grothendieck construction)をしてみると、なんか面白いことがあるかも知れません(いつも面白いとは保証しませんが)。

例えば、圏Cから圏Setへの関手 F:CSet があると、集合を離散圏とみなせば、Fは CCat となるのでインデックス付き圏となります(反変・共変の差は無視)。このインデックス付き圏にグロタンディーク構成を施すと要素の圏(category of elements)が得られます。

以下で、反変ベキ集合関手をインデックス付き圏とみなして、グロタンディーク構成をしてみます。出来上がった圏のファイブレーション(ファイバー圏*1)のセクション関手を考えると、けっこう実用性があると思います。

なお、インデックス付き圏とそのグロタンディーク構成については次の記事に書いてあります。


Iを集合圏の部分圏とします。Iの対象は集合で、射は写像です。A∈|I| に対して、Aのベキ集合を P(A) と書くことにします。f:A→B in I に対しては、P(f):P(B)→P(A) を次のように定義します。

  • V⊆B として、P(f)(V) := {x∈A | f(x)∈V}

Pの反変関手性はPの定義から確認できるので、P:ISet という反変関手(IopSet)が定義できました。

任意の集合Aに対して P(A) は部分集合の包含順序により順序集合になります。f:A→B に対する P(f):P(B)→P(A) は包含順序を保存します。つまり、順序集合の圏の射と考えることができます。Pが順序を保存するという性質(単調性)まで込めて考えると、Pは IOrd という関手になります。Ordは、順序集合と単調写像の圏です。

任意の順序集合はやせた圏なので、OrdCat と埋め込めます。この埋め込みを使うと、Pは ICat という関手となります。そうです、Pはインデックス付き圏ですね。

さて、「インデックス付き圏のグロタンディーク構成」の定義を参照しながら、具体的にグロタンディーク構成をしていきましょう。グロタンディーク構成の絵を参考にするといいですよ。

ファイブレーション(or バンドル)の全体圏(total category)をCとします。Cの対象は、ペア(A, U)で、A∈|I|、U⊆A となっているものです。Cの射で、(A, U)→(B, V) であるものは、f:A→B in I で、U⊆P(f)(V) を満たすものと考えることができます。

異なる台集合の上に乗った部分集合の包含比較はできませんが、台集合のあいだの写像で引き戻して包含比較をしています。つまり、部分集合のあいだの包含関係を一般化、あるいは大域化していることになります。(A, U) |→ A というファイブレーションの射影は、部分集合にその台(親)を対応させるものです。

U⊆P(f)(V) という条件は、「x∈U ならば f(x)∈V」なので、fをプログラムの実行と考えた場合のホーア表明になっています。述語と部分集合を同一視するなら、U⊆P(f)(V) はホーア式 U{f}V です。ベキ集合のグロタンディーク構成により得られた全体圏は、ホーア式を射とする圏とみなすことができて、ファイブレーション射影は、ホーア式にその制約記述の対象であるプログラムを対応させます。全体圏における結合は、2つのホーア式を前提とする含意の推論(カット規則)です。

最近、デイヴィッド・スピヴァック(David I. Spivak)は、データベースの定式化にインデックス付き圏(あるいは前層)を使う方法を開発しています。スピヴァックのデータモデルの文脈では、ベキ集合ファイブレーションにまた別の解釈が与えられます。ファイブレーションのセクション関手は、データベーススキーマに対する制約(の一種)を記述します。

圏のインデクシング、グロタンディーク構成、ファイブレーションは、まだまだ応用範囲を広げる気がします。

[追記]デイヴィッド・スピヴァックhttp://math.mit.edu/~dspivak/)がやっていることはすっごく面白いので、そのうち紹介したいと思います。[/追記][さらに追記]紹介しました。

[/さらに追記]

*1:fibred/fibered categoryのことですが、「ファイバー」がfiberのことかfibered(形容詞)のことか分かりにくいので「圏のファイブレーション」とします。