順序付き関係の圏

型の計算をしているうちに、“順序付き関係の圏”とでも呼ぶべきものに出会いました。Ordered Relations でORelと書くことにします。集合の圏Set、順序集合の圏Ord、関係の圏Relと、圏ORelのあいだには次のような関係があります。

  Set -- Gr --> Rel
   |             |
  Disc          Disc
   |             |
   v             v
  Ord - OGr --> ORel

矢印はいずれも関手です。Grはグラフ化、OGrは順序付きのグラフ化（グラフの順序的閉包を取る）、縦方向の矢印は集合に離散順序を入れる関手です。2本の縦矢印は違う関手を表しますが、似ているので同じ名前Discをラベルにしています。これらの圏と関手について説明します。プロ関手との関係とかにも触れますが、とても急ぎ足です。

内容：

関係の圏の素早い復習
順序集合の圏の素早い復習
反対順序と直積
上方閉集合と下方閉集合
順序付き関係の圏
順序付き関係の圏は面白い

関係の圏の素早い復習

関係の圏Relは“集合の全体”を対象類とする圏です。つまり、|Rel| = |Set| 。ホムセットは、Powをベキ集合だとして、Rel(A, B) = Pow(A×B) です。R:A→B in Rel とは、R∈Rel(A, B) ですから、これは R∈Pow(A×B) なので、R⊆A×B です。射の結合（合成）と恒等射の定義は以下のとおりです。

R:A→B, S:B→C in Rel に対して、R;S := {(x, z)∈A×C | ∃y.[(x, y)∈R ∧ (y, z)∈S]}
A in |Rel| に対して、id_A := {(x, x')∈A×A | x = x'}

さて、SetからRelへの関手Grを定義しましょう。Setの対象（集合）Aに関しては、そのままRelの対象とみなします；つまり、Gr(A) = A 。f:A→B in Set があるとき、Gr(f) = {(x, y)∈A×B | y = f(x)} と定義すると、Gr(f)∈Pow(A×B) なので、Gr(f):A→B in Rel です。このようにして定義された対応Grは関手になります。Gr(f)は写像fのグラフです。

順序集合の圏の素早い復習

集合Xとその上の順序関係≦の組 (X, ≦) を対象とする圏を考えます。記号の乱用をして、X = (X, ≦) と書きます。つまり、順序集合の構造全体とその台集合を同じ記号で表します。X = (X, ≦_X) のような書き方も使います。

(X, ≦)、(Y, ≦) が2つの順序集合だとして、写像 f:X→Y が単調（monotone, monotonic）とは、「x≦x' ならば f(x)≦f(x')」のことです。順序集合を対象として、単調写像を射とする圏ができるので、それをOrdとします。

Aが集合のとき、A上の順序関係≦を次のように定義します。

x≦y ⇔ x = y

順序関係とはいいながら、実際はイコールのことです。イコールにより定義される順序関係を離散順序（discrete order）と呼びます。実際はイコールなので、集合A上に離散順序（イコールね！）を入れた構造を (A, =) と書きましょう。任意の写像 f:A→B は、(A, =)→(B, =) とみて単調になります。この事実を利用すると、Discという関手が定義できます。

Disc(A in Set) = ((A, =) in Ord)
Disc(f:A→B in Set) = (f:(A, =)→(B, =) in Ord)

関手 Disc:Set→Ord は、順序集合にその台集合を対応させる忘却関手 U:Ord→Set と随伴の関係になります。

反対順序と直積

(X, ≦)が順序集合のとき、同じ台集合Xに、新しい順序≦^opを次のように定義します。

x≦^opx' ⇔ x'≦x

新しい順序≦^opは、もとの順序≦の反対（逆向き）です。順序集合 (X, ≦^op) をもとの順序集合の反対（opposite）の順序集合と呼びます。X = (X, ≦) と書くとき、(X, ≦^op) はX^opと書きます。

X = (X, ≦) と Y = (Y, ≦) が2つの順序集合のとき、直積集合 X×Y 上に順序を入れることができます； (x, y)≦(x', y') ⇔ (x≦x' ∧ y≦y') とすればいいですね。こうして作った順序集合も（記号を乱用して） X×Y と書きます。

次の事実があります。

(X^op)^op = X
(X×Y)^op = X^op×Y^op
X^op = X ⇔ Xは離散順序集合

これらを使うと例えば、(X^op×Y)^op = (X^op)^op×Y^op = X×Y^op が言えます。

上方閉集合と下方閉集合

(X, ≦)が順序集合で、A⊆X のとき：

「x∈A、x≦x' ならば、x'∈A」のとき、Aを上方閉集合（upper close/closed set, upper set）と呼ぶ。
「x∈A、x'≦x ならば、x'∈A」のとき、Aを下方閉集合（lower close/closed set, lower set）と呼ぶ。

上方／下方閉集合は（順序集合の）イデアルとかフィルターとかとも呼ばれますが、どっちがどっちだか忘れてしまうのでここでは使わないことにします。X = (X, ≦) の全ての上方閉集合の集合を Pow↑(X) と書くことにします。同様に、下方閉集合の全体は Pow↓(X) です。

(X, ≦)が順序集合で、A⊆X が上方閉とは限らない部分集合のとき、Aを含む最小の上方閉集合があります（定義してみてください）。これをA↑と書きましょう。A↑をAの上方閉包（upper closure）と呼びます。A↓は下方閉包（lower closure）ですね。

単項集合演算↑と↓はベキ等です。(A↑)↑ = A↑、(A↓)↓ = A↓ であり、「Aが上方閉集合 ⇔ A↑ = A」、「Aが下方閉集合 ⇔ A↓ = A」が成立します。Pow↑(A) = Pow↓(A^op)、Pow↓(A) = Pow↑(A^op) も成立します。

いよいよ、圏ORelを定義しましょう。まず対象は、|ORel| = |Ord| です。圏Relが、圏Setと対象を共有するのと似たような状況です。次にホムセットですが、ORel(X, Y) = Pow↑(X^op×Y) です。これも、Rel(A, B) = Pow(A×B) と似ています。ホムセットの要素（射です）は、関係の圏と同じくR, S, Tなどの文字で表すことにします。

ORelにおける射の結合と恒等射は次のように定義します。

R:X→Y, S:Y→Z in ORel に対して、R;S := {(x, z)∈X×Z | ∃y.(x, y)∈R ∧ (y, z)∈S]}
X in |ORel| に対して、id_X := {(x, x')∈X×X | x ≦ x'}

これらの定義がwell-definedで、結合律と単位律を満たすことの証明は、関係の圏のときと同様です（多少めんどくさくなりますけど）。結合の定義は関係の圏とまったく同じですが、次のように書いたほうがふさわしいような気がします、気分の問題ではありますが。

R:X→Y, S:Y→Z in ORel に対して、R;S := {(x, z)∈X×Z | ∃y, y'.[y≦y' ∧ (x, y)∈R ∧ (y', z)∈S]}

関手 Disc:Rel→ORel は、Disc:Set→Ord と同様に定義できます。OGr:Ord→ORel は、OGr(f) = Gr(f)↑ として定義できます。

順序付き関係の圏は面白い

大急ぎで圏ORelを定義しました。圏ORelは、いくつかの観点から興味深いものです。まず、定義から明らかなように、圏ORelは、圏Relと圏Ordの拡張になっています。圏Relと圏Ordは圏ORelに埋め込むことができます。

圏ORelはコンパクト閉圏になります。圏Relもコンパクト閉圏なのですが、双対が自明（すべての対象が自己双対）という点でイマヒトツ楽しくないですね。ですが、圏ORelの双対は (-)^op なので、自己双対ではない対象がたくさんあります。

ORelの射はプロ関手（profunctor）と似ています。豊饒圏の枠組みを使えば、おそらくプロ関手とみなせるでしょう。Profを圏とプロ関手の圏として、Ord : Cat = ORel : Prof という“比例式”が成り立っていそうです。

もともと僕がORelに行き着いたのは型の計算なので、ORelの状況が分かると型の計算に役立ちます。ORelの部分圏で、具体的な計算が実用的に出来るものが見つかるとトテモうれしいです。

といった事情で、圏ORelをもっと調べる価値はあると思っています。