日記 (2021 年 2 月 4 日)
今日は、 安定写像のトレースという概念を導入して、 整合空間の冪を定義する。
定義 3.1.
整合空間 A,B の間の写像 f:A→B をとる。
各 a∈A および y∈|B| に対し、
fin(a) := {a∣a⊆a は有限集合} elfin(a,y) := {a∣a∈fin(a),y∈f(a)}
と定める。
なお、 fin(a) の元は a の 「有限近似 (finite approximant)」 と呼ばれる。
整合空間 A とその元 a∈A に対し、 明らかに fin(a)⊆A は有向であり、 a=⋃a∈fin(a)a である。
したがって、 別の整合空間 B への安定写像 f:A→B に対し、 f の連続性によって、 f(a)=⋃a∈fin(a)f(a) が成り立つ。
すなわち、 安定写像 f による a の像は fin(a) の元の像から一意に定まる。
この意味で fin(a) の元は a の近似なのである。
近似の概念を用いることで、 安定写像の特徴付けが得られる。
これを示すため、 補題を 2 つ用意しておく。
補題 3.2.
整合空間 A,B の間の写像 f:A→B をとり、 さらに a∈A および y∈|B| をとる。
このとき、 elfin(a,y) に極小元が存在するならば、 それは最小元である。
証明.
極小元 a∈elfin(a,y) をとる。
任意の a∈elfin(a,y) に対し、 a∪a⊆a かつ a∈A だから、 a∪a∈A である。
したがって、 f の安定性により、 f(a∩a)=f(a)∩f(a) が成り立つ。
a と a のとり方から y∈f(a) と y∈f(a) であるから、 今得られた等式によって、 y∈f(a∩a) を得る。
これより、 a∩a∈elfin(a,y) が成り立つ。
ここで、 a∩a⊆a であって a は極小だから、 a∩a=a でなければならない。
すなわち、 a⊆a である。
以上により、 a は最小である。
補題 3.3.
集合の集合 A とその有向部分集合 S⊆A をとる。
元 a∈A に対し、 a が有限集合で a⊆⋃a∈Sa ならば、 ある a∈S が存在して a⊆a が成り立つ。
証明.
各 x∈a に対し、 仮定からある ax∈S が存在して x∈ax が成り立つ。
a は有限集合で S は有向だから、 ある a∈S によって、 任意の x∈a に対して ax⊆a が成り立つようにできる。
すると、 任意の x∈a に対して x∈a が成り立つから、 a⊆a である。
以上の補題を用いると、 以下のような安定写像の特徴付けが得られる。
命題 3.4.
整合空間 A,B の間の写像 f:A→B をとる。
このとき、 2 条件
- f は安定である。
- f は単調である。
さらに、 任意の a∈A および y∈|B| に対し、 y∈f(a) であれば、 elfin(a,y) に包含関係に関する最小元が存在する。
は同値である。
証明.
条件 1 ⇒ 条件 2:まず、 定義から f は単調である。
そこで次に、 任意に a∈A および y∈|B| をとり、 y∈f(a) が成り立っているとする。
すでに述べたように、 f の連続性によって、 f(a)=⋃a∈fin(a)f(a) が成り立つ。
したがって、 ある a∈fin(a) が存在して y∈f(a) である。
すなわち、 a∈elfin(a,y) が成り立つ。
ここで elfin(a,y) を考えると、 a が有限集合であることから elfin(a,y) も有限集合である。
したがって、 elfin(a,y) には必ず極小元が存在するが、 補題 3.2 によってそれは最小元である。
a⊆a より elfin(a,y) の最小元は elfin(a,y) の最小元でもあるから、 これで示された。
条件 2 ⇒ 条件 1:仮定からすでに f は単調だから、 あとは f の連続性と安定性を示せば良い。
まず、 f の連続性を示す。
任意に有向部分集合 S⊆A をとると、 f の単調性によって ⋃a∈Sf(a)⊆f(⋃a∈Sa) は成り立つから、 この逆の包含関係を示せば良い。
そこで、 a:=⋃a∈Sa とおき、 y∈f(a) をとる。
仮定から最小元 a∈elfin(a,y) がとれるが、 a は有限集合で a⊆⋃a∈Sa であるから、 補題 3.3 によって、 ある a∈S が存在して a⊆a が成り立つ。
f の単調性から f(a)⊆f(a) なので y∈f(a) が得られ、 これより y∈⋃a∈Sf(a) が分かる。
以上により、 f(⋃a∈Sa)⊆⋃a∈Sf(a) である。
次に、 f の安定性を示す。
任意に元 a,a∈A をとり、 a∪a∈A であるとする。
f の単調性によって f(a∩a)⊆f(a)∩f(a) は成り立つから、 この逆の包含関係を示せば良い。
そこで、 y∈f(a)∩f(a) をとる。
仮定から、 最小元 a∈elfin(a,y) と a∈elfin(a,y) がとれるが、 a⊆a∪a かつ a⊆a∪a より、 この 2 元は elfin(a∪a,y) の最小元でもある。
最小元は一意であるから a=a が成り立つ。
したがって、 a⊆a∩a が得られ、 f の単調性から f(a)⊆f(a∩a) であるから、 y∈f(a∩a) が分かる。
以上により、 f(a)∩f(a)⊆f(a∩a) である。
この命題を踏まえて、 安定写像のトレースを以下のように定義する。
定義 3.5.
整合空間 A,B の間の安定写像 f:A→B をとる。
ある a∈A および y∈|B| に対し、 (a,y) が elfin(a,y) の最小元であるとき、 組 (a,y) を f の 「トレース (trace)」 という。
また、 f のトレース全体の集合を tr(f) で表す。
トレースからは元の安定写像を復元することができる。
定理 3.6.
整合空間 A,B の間の安定写像 f:A→B を考える。
任意の a∈A に対し、
f(a)={y∣ある a∈fin(a) に対して (a,y)∈tr(f)}
が成り立つ。
証明.
右辺の集合を g(a) と書くことにし、 両方の包含関係を示す。
任意の y∈f(a) に対し、 命題 3.4 によって、 最小元 a∈elfin(a,y) がとれる。
しかし a⊆a だから、 a は elfin(a,y) の最小元でもある。
これより (a,y)∈tr(f) であり、 y∈g(a) が得られた。
以上により、 f(a)⊆g(a) である。
逆に y∈g(a) をとると、 ある a∈fin(a) が存在して (a,y)∈tr(f) が成り立つ。
したがって特に y∈f(a) であるが、 f の単調性によって f(a)⊆f(a) だから、 y∈f(a) が成り立つ。
以上により、 g(a)⊆f(a) である。
さて、 今日の本題は、 整合空間 A,B に対してその冪 A⇀B を定義することであった。
これを素朴に安定写像 f:A→B 全体の集合としたいところだが、 安定写像自身は集合ではないので、 集合の集合である整合空間と見なすことはできない。
しかし、 定理 3.6 によって安定写像と 1 対 1 に対応することが分かったトレースは集合なので、 安定写像自身ではなくそのトレースの全体の集合を考えることで、 整合空間の枠組みに入れることができる。
すなわち、
A⇀B:={tr(f)∣f:A→B は安定}
と定義するのである。
幸運なことに、 これは整合空間になるための条件を満たしている。
これを定義として議論を終わりにしても良いのだが、 整合空間は反射的無向グラフとも見なせるので、 そのように見なしたときの A⇀B がどのように表せるかも気になるところである。
ここで、 A に属する有限集合全体を |!A| と書くことにすれば、 安定写像 f:A→B のトレース tr(f) は |!A|×|B| の部分集合である。
したがってこの問題は、 |!A|×|B| にどのような整合関係を定めれば、 その整合的な部分集合全体が上で定めた A⇀B に一致するか、 と言い換えることができる。
いきなり |!A|×|B| 上の整合関係を定めても良いが、 まず |!A| 上の整合関係を定め、 次にそれを用いて |!A|×|B| に整合関係を定めることにする。
定義 3.7.
整合空間 A に対し、
|!A|:={a∣a∈A は有限集合}
と定義する。
さらに、 |!A| 上の対称二項関係 !A を、 各トークン a,a∈|A| に対し、
a!Aa:⟺a∪a∈A
で定義する。
これによって定まる整合空間 !A を A の 「線型化 (linearisation)」 という。
定義 3.8.
整合空間 A,B に対し、
|A⇀B|:=|!A|×|B|
と定義する。
さらに、 |A⇀B| 上の対称二項関係 A⇀B を、 各トークン a,a∈|A| と y,y∈|B| に対し、
(a,y)A⇀B(a,y):⟺❲a!Aa⟹yBy❳AND❲a!Aa⟹yBy❳
で定義する。
これによって定まる整合空間 A⇀B を A と B の 「冪 (exponential)」 という。
これは実際に我々の欲しい空間になっている。
定理 3.9.
整合空間 A,B に対し、
A⇀B={tr(f)∣f:A→B は安定}
が成り立つ。
証明.
右辺の集合をここでは C と書くことにし、 両方の包含関係を示す。
証明は非常に素直にできるので、 ここでは方針を述べるに留める。
任意に c∈A⇀B をとり、
f: A ⟶ B a ⟼ {y∣ある a∈fin(a) に対して (a,y)∈c}
とおく。
すると、 これは矛盾なく定義された安定写像であり、 さらに定理 3.6 を使うと c=tr(f) が示せるので、 c∈C が分かる。
以上により、 A⇀B⊆C である。
逆に c∈C をとると、 ある安定写像 f:A→B が存在して c=tr(f) と書ける。
さらに、 tr(f)⊆|A⇀B| が整合的であることは容易に分かるから、 tr(f)∈A⇀B が分かる。
以上により、 C⊆A⇀B である。
これが実際に圏論的にも 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