Avendia19
English

日記 (2021 年 2 月 4 日)

今日は、 安定写像のトレースという概念を導入して、 整合空間の冪を定義する。

定義 3.1

整合空間 A,B の間の写像 f:AB をとる。 各 aA および y|B| に対し、 fin(a) := {󰔊a󰔊aa は有限集合} elfin(a,y) := {󰔊a󰔊afin(a),yf(󰔊a)} と定める。 なお、 fin(a) の元は a有限近似finite approximant と呼ばれる。

整合空間 A とその元 aA に対し、 明らかに fin(a)A は有向であり、 a=󰔊afin(a)󰔊a である。 したがって、 別の整合空間 B への安定写像 f:AB に対し、 f の連続性によって、 f(a)=󰔊afin(a)f(󰔊a) が成り立つ。 すなわち、 安定写像 f による a の像は fin(a) の元の像から一意に定まる。 この意味で fin(a) の元は a の近似なのである。

近似の概念を用いることで、 安定写像の特徴付けが得られる。 これを示すため、 補題を 2 つ用意しておく。

補題 3.2

整合空間 A,B の間の写像 f:AB をとり、 さらに aA および y|B| をとる。 このとき、 elfin(a,y) に極小元が存在するならば、 それは最小元である。

極小元 󰔊aelfin(a,y) をとる。 任意の a󰎘elfin(a,y) に対し、 󰔊aa󰎘a かつ aA だから、 󰔊aa󰎘A である。 したがって、 f の安定性により、 f(󰔊aa󰎘)=f(󰔊a)f(a󰎘) が成り立つ。 󰔊aa󰎘 のとり方から yf(󰔊a)yf(a󰎘) であるから、 今得られた等式によって、 yf(󰔊aa󰎘) を得る。 これより、 󰔊aa󰎘elfin(a,y) が成り立つ。 ここで、 󰔊aa󰎘󰔊a であって 󰔊a は極小だから、 󰔊aa󰎘=󰔊a でなければならない。 すなわち、 󰔊aa󰎘 である。 以上により、 󰔊a は最小である。

補題 3.3

集合の集合 A とその有向部分集合 SA をとる。 元 󰔊aA に対し、 󰔊a が有限集合で 󰔊aaSa ならば、 ある aS が存在して 󰔊aa が成り立つ。

x󰔊a に対し、 仮定からある axS が存在して xax が成り立つ。 󰔊a は有限集合で S は有向だから、 ある aS によって、 任意の x󰔊a に対して axa が成り立つようにできる。 すると、 任意の x󰔊a に対して xa が成り立つから、 󰔊aa である。

以上の補題を用いると、 以下のような安定写像の特徴付けが得られる。

命題 3.4

整合空間 A,B の間の写像 f:AB をとる。 このとき、 2 条件

  1. f は安定である。
  2. f は単調である。 さらに、 任意の aA および y|B| に対し、 yf(a) であれば、 elfin(a,y) に包含関係に関する最小元が存在する。

は同値である。

条件 1 条件 2:まず、 定義から f は単調である。 そこで次に、 任意に aA および y|B| をとり、 yf(a) が成り立っているとする。 すでに述べたように、 f の連続性によって、 f(a)=󰔊afin(a)f(󰔊a) が成り立つ。 したがって、 ある 󰔊afin(a) が存在して yf(󰔊a) である。 すなわち、 󰔊aelfin(a,y) が成り立つ。

ここで elfin(󰔊a,y) を考えると、 󰔊a が有限集合であることから elfin(󰔊a,y) も有限集合である。 したがって、 elfin(󰔊a,y) には必ず極小元が存在するが、 補題 3.2 によってそれは最小元である。 󰔊aa より elfin(󰔊a,y) の最小元は elfin(a,y) の最小元でもあるから、 これで示された。

条件 2 条件 1:仮定からすでに f は単調だから、 あとは f の連続性と安定性を示せば良い。

まず、 f の連続性を示す。 任意に有向部分集合 SA をとると、 f の単調性によって aSf(a)f(aSa) は成り立つから、 この逆の包含関係を示せば良い。 そこで、 󰔄a:=aSa とおき、 yf(󰔄a) をとる。 仮定から最小元 󰔊aelfin(󰔄a,y) がとれるが、 󰔊a は有限集合で 󰔊aaSa であるから、 補題 3.3 によって、 ある aS が存在して 󰔊aa が成り立つ。 f の単調性から f(󰔊a)f(a) なので yf(a) が得られ、 これより yaSf(a) が分かる。 以上により、 f(aSa)aSf(a) である。

次に、 f の安定性を示す。 任意に元 a,a󰎘A をとり、 aa󰎘A であるとする。 f の単調性によって f(aa󰎘)f(a)f(a󰎘) は成り立つから、 この逆の包含関係を示せば良い。 そこで、 yf(a)f(a󰎘) をとる。 仮定から、 最小元 󰔊aelfin(a,y)󰔊a󰎘elfin(a,y) がとれるが、 aaa󰎘 かつ a󰎘aa󰎘 より、 この 2 元は elfin(aa󰎘,y) の最小元でもある。 最小元は一意であるから 󰔊a=󰔊a󰎘 が成り立つ。 したがって、 󰔊aaa󰎘 が得られ、 f の単調性から f(󰔊a)f(aa󰎘) であるから、 yf(aa󰎘) が分かる。 以上により、 f(a)f(a󰎘)f(aa󰎘) である。

この命題を踏まえて、 安定写像のトレースを以下のように定義する。

定義 3.5

整合空間 A,B の間の安定写像 f:AB をとる。 ある 󰔊aA および y|B| に対し、 (󰔊a,y)elfin(󰔊a,y) の最小元であるとき、 組 (󰔊a,y)fトレースtrace という。 また、 f のトレース全体の集合を tr(f) で表す。

トレースからはもとの安定写像を復元することができる。

定理 3.6

整合空間 A,B の間の安定写像 f:AB を考える。 任意の aA に対し、 f(a)={yある 󰔊afin(a) に対して (󰔊a,y)tr(f)} が成り立つ。

右辺の集合を g(a) と書くことにし、 両方の包含関係を示す。

任意の yf(a) に対し、 命題 3.4 によって、 最小元 󰔊aelfin(a,y) がとれる。 しかし 󰔊aa だから、 󰔊aelfin(󰔊a,y) の最小元でもある。 これより (󰔊a,y)tr(f) であり、 yg(a) が得られた。 以上により、 f(a)g(a) である。

逆に yg(a) をとると、 ある 󰔊afin(a) が存在して (󰔊a,y)tr(f) が成り立つ。 したがって特に yf(󰔊a) であるが、 f の単調性によって f(󰔊a)f(a) だから、 yf(a) が成り立つ。 以上により、 g(a)f(a) である。

さて、 今日の本題は、 整合空間 A,B に対してその冪 AB を定義することであった。 これを素朴に安定写像 f:AB 全体の集合としたいところだが、 安定写像自身は集合ではないので、 集合の集合である整合空間と見なすことはできない。 しかし、 定理 3.6 によって安定写像と 1 対 1 に対応することが分かったトレースは集合なので、 安定写像自身ではなくそのトレースの全体の集合を考えることで、 整合空間の枠組みに入れることができる。 すなわち、 AB:={tr(f)f:AB は安定} と定義するのである。 幸運なことに、 これは整合空間になるための条件を満たしている。

これを定義として議論を終わりにしても良いのだが、 整合空間は反射的無向グラフとも見なせるので、 そのように見なしたときの AB がどのように表せるかも気になるところである。 ここで、 A に属する有限集合全体を |!A| と書くことにすれば、 安定写像 f:AB のトレース tr(f)|!A|×|B| の部分集合である。 したがってこの問題は、 |!A|×|B| にどのような整合関係を定めれば、 その整合的な部分集合全体が上で定めた AB に一致するか、 と言い換えることができる。

いきなり |!A|×|B| 上の整合関係を定めても良いが、 まず |!A| 上の整合関係を定め、 次にそれを用いて |!A|×|B| に整合関係を定めることにする。

定義 3.7

整合空間 A に対し、 |!A|:={󰔊a󰔊aA は有限集合} と定義する。 さらに、 |!A| 上の対称二項関係 󰖬!A を、 各トークン 󰔊a,󰔊a󰎘|A| に対し、 󰔊a󰖬!A󰔊a󰎘:⟺󰔊a󰔊a󰎘A で定義する。 これによって定まる整合空間 !AA線型化linearisation という。

定義 3.8

整合空間 A,B に対し、 |AB|:=|!A|×|B| と定義する。 さらに、 |AB| 上の対称二項関係 󰖬AB を、 各トークン 󰔊a,󰔊a󰎘|A|y,y󰎘|B| に対し、 (󰔊a,y)󰖬AB(󰔊a󰎘,y󰎘):⟺󰔊a󰖬!A󰔊a󰎘y󰖬By󰎘AND󰔊a󰖫!A󰔊a󰎘y󰖫By󰎘 で定義する。 これによって定まる整合空間 ABABexponential という。

これは実際に我々の欲しい空間になっている。

定理 3.9

整合空間 A,B に対し、 AB={tr(f)f:AB は安定} が成り立つ。

右辺の集合をここでは C と書くことにし、 両方の包含関係を示す。 証明は非常に素直にできるので、 ここでは方針を述べるに留める。

任意に cAB をとり、 f: A B a {yある 󰔊afin(a) に対して (󰔊a,y)c} とおく。 すると、 これは矛盾なく定義された安定写像であり、 さらに定理 3.6 を使うと c=tr(f) が示せるので、 cC が分かる。 以上により、 ABC である。

逆に cC をとると、 ある安定写像 f:AB が存在して c=tr(f) と書ける。 さらに、 tr(f)|AB| が整合的であることは容易に分かるから、 tr(f)AB が分かる。 以上により、 CAB である。

これが実際に圏論的にも Coh における冪になっているのだが、 長くなったのでその証明は次回に回すことにする。

参考文献

  1. J. Y. Girard (1987) 「Linear logic」 『Theoretical Computer Science』 50:1–101
  2. J. Y. Girard, Y. Lafont, P. Taylor (1989) 『Proofs and Types』 Cambridge University Press