日記 (2021 年 2 月 3 日)
今日は、 前回定義した整合空間と安定写像の圏 Coh における積を具体的に定義する。
整合空間の直積は以下のように定義する。
ここでは、 整合空間をトークンの反射的無向グラフだと見なし、 トークンの集合とそれ上の反射的対称二項関係を定めることで定義する。
以降、 集合 X,Y に対して、 記号の簡単のため X⊔Y:=({1}×X)∪({2}×Y) と書く。
定義 2.1.
整合空間 A,B に対し、
|A×B|:=|A|⊔|B|
と定義する。
さらに、 |A×B| 上の対称二項関係 A×B を、 各トークン x,x∈|A| と y,y∈|B| に対し、
(1,x)A×B(1,x) :⟺ xAx (2,y)A×B(2,y) :⟺ yBy (1,x)A×B(2,y) :⟺ True
で定義する。
これによって定まる整合空間 A×B を A と B の直積 (direct product) という。
すなわち、 2 つの整合空間の直積とは、 2 つの整合空間をグラフと見なして単純に並べ、 片方のグラフの全ての頂点からもう一方のグラフの全ての頂点への辺を追加したものである。
整合空間は特定の条件を満たす集合の集合とも見なせたのであったが、 この見方をすると、 整合空間の直積の次のように書ける。
命題 2.2.
整合空間 A,B に対し、
A×B={a⊔b∣a∈A,b∈B}
が成り立つ。
証明.
|A×B| の整合的な部分集合が、 ある a∈A と b∈B に対して a⊔b の形で書け、 さらにこのような形のものしかないことを示せば良い。
まず、 A×B の整合関係の定義により、 任意の a∈A と b∈B に対して、 部分集合 a⊔b⊆|A×B| が整合的なのは明らかである。
逆に、 任意に整合的な部分集合 c⊆|A×B| をとり、
a := {x∣(1,x)∈c} b := {y∣(2,y)∈c}
とおけば、 c=a⊔b であって、 部分集合 a⊆|A| および b⊆|B| はともに整合的である。
以上で示された。
以降、 これが圏論的な積になっていることを示すのだが、 そのためには直積から各成分への射影を定義する必要がある。
この準備として、 トークン集合の間の写像から誘導される整合空間の間の安定写像に関する一般論について先に述べておく。
命題 2.3.
整合空間 A,B に対し、 写像 u:|A|→|B| を考える。
u が単射であり、 さらに任意の x,x∈|A| に対して
xAx⟹u(x)Bu(x)
が成り立っているとき、 写像
u∗: A ⟶ B a ⟼ {u(x)∣x∈a}
は安定である。
証明.
定義に従って 3 つの条件を確かめれば良い。
命題 2.4.
整合空間 A,B に対し、 写像 u:|A|→|B| を考える。
任意の x,x∈|A| に対して
u(x)Bu(x)⟹xAx
が成り立っているとき、 写像
u∗: B ⟶ A b ⟼ {x∣u(x)∈b}
は安定である。
証明.
前の命題と同じく、 定義に従って 3 つの条件を確かめれば良い。
さて、 直積からの射影を定義しよう。
整合空間 A,B に対し、
u1: |A| ⟶ |A×B| x ⟼ (1,x) u2: |B| ⟶ |A×B| y ⟼ (2,y)
はともに命題 2.4 の条件を満たすから、 安定写像 π1:A×B→A と π2:A×B→B が誘導される。
具体的には、
π1: A×B ⟶ A a⊔b ⟼ a π2: A×B ⟶ B a⊔b ⟼ b
と書ける。
これが、 実際に積の普遍性をもつ。
定理 2.5.
整合空間 A,B に対し、 上記で定めた直積と射影 (A×B,π1,π2) は、 圏 Coh における積である。
証明.
積の普遍性を確かめれば良い。
任意の整合空間 C および安定写像 f:C→A と g:C→B に対し、
h: C ⟶ A×B c ⟼ f(c)⊔g(c)
と定義すると、 これは明らかに安定で、
CA×BABfgπ1π2h
は可換である。
さらに明らかに、 h はこれを可換にするような一意な射である。
さて、 整合空間をグラフとして見れば、 整合空間の直積とは、 グラフを単に並べた後に、 片方のグラフの頂点からもう一方のグラフの頂点への辺を全て追加したものであった。
これと同様に、 グラフを単に並べるだけで、 新しい辺を全く追加しないという演算も考えられる。
この演算は整合空間の直和と呼ばれる。
定義 2.6.
整合空間 A,B に対し、
|A+B|:=|A|⊔|B|
と定義する。
さらに、 |A×B| 上の対称二項関係 A×B を、 各トークン x,x∈|A| と y,y∈|B| に対し、
(1,x)A×B(1,x) :⟺ xAx (2,y)A×B(2,y) :⟺ yBy (1,x)A×B(2,y) :⟺ False
で定義する。
これによって定まる整合空間 A+B を A と B の直和 (direct sum) という。
集合の集合としては、 次のように書ける。
命題 2.7.
整合空間 A,B に対し、
A+B={{1}×a∣a∈A}∪{{2}×b∣b∈B}
が成り立つ。
直和への包含射は、 直積からの射影と同様に定義される。
ただし、 命題 2.4 ではなく命題 2.3 を用いる。
整合空間 A,B に対し、
u1: |A| ⟶ |A+B| x ⟼ (1,x) u2: |B| ⟶ |A+B| y ⟼ (2,y)
はともに命題 2.3 の条件を満たすから、 安定写像 ι1:A→A+B と ι2:B→A+B が誘導される。
具体的には、
ι1: A ⟶ A+B a ⟼ {1}×a ι2: B ⟶ A+B b ⟼ {2}×b
である。
さて、 残念なことに、 整合空間の直和は圏論的な余積ではない。
余積にならないことは以下の観察から分かる。
整合空間 A,B に対し、 命題 2.7 によって、
A+B={{1}×a∣a∈A}∪{{2}×b∣b∈B}
と書けるわけだが、 この右辺の 2 つの集合は実は非交ではなく、 ∅ が両方に属してしまっている。
そのため、 別の整合空間 C および安定写像 f:A→C と g:B→C に対して、 f(∅)=g(∅) が成り立っていない限り適切な写像 h:A+B→C を定義できない。
以上の理由から、 通常の論理の意味論を整合空間で展開する際に、 選言の解釈としては直和は役に立たない。
しかし、 後述する線型化と組み合わせることによって、 完璧とまでは言えないが十分意味のある選言の解釈が可能になる。
また、 通常の論理ではなく線型論理を考えるのであれば、 弱化規則と縮約規則が制限されているという制約 (いわゆる線型性) のおかげで、 この直和を加法的選言の解釈として使うことができる。
次回は、 安定写像のトレースという概念を導入し、 それを用いて整合空間の冪を定義することで、 Coh がカルテシアン閉であることを示す。
参考文献
- J. Y. Girard (1987) 「Linear logic」 『Theoretical Computer Science』 50:1–101
- J. Y. Girard, Y. Lafont, P. Taylor (1989) 『Proofs and Types』 Cambridge University Press