Avendia19
English

日記 (2020 年 4 月 8 日)

4 月 5 日4 月 6 日で扱った 3 種類のモデルは、 乗法的論理積 (とその単位元 ) と指数的演算子 ! のみを解釈するものであった。 線型論理にはこれ以外にも論理結合子があるので、 それらも解釈しようとすると追加の構造が必要になる。 ここでは、 否定結合子の解釈について触れようと思う。

否定結合子の解釈には、 スター自律圏の構造を使うのが一般的である。 これは Barr1 によって導入された構造で、 圏の全ての対象がその圏の中に双対をもつようなものである。 スター自律圏の記述には、 以下の 2 種類の方法がある。

1

対称モノイダル圏 󰒚 を考える。 ここに、 次の条件を満たすような忠実充満関手 -:󰒚󰒚 が定まっているとする。 すなわち、 任意の対象 A,B,C に対して、 全ての変数に対して自然な全単射 Hom(AB,C)Hom(A,(BC)) が成り立つ。 このとき、 󰒚スター自律圏star-autonomous category という。 また、 関手 -双対関手dualising functor と呼ぶ。

2

対称モノイダル圏 󰒚 を考える。 󰒚 がモノイダル閉であり、 次の条件を満たすような対象 が定まっているとする。 すなわち、 任意の対象 A に対して、 モノイダル閉性の余単位 εA:A(A) の転置 κA:A(A) は同型射である。 このとき、 󰒚スター自律圏star-autonomous category という。 また、 対象 大域的双対対象global dualising object と呼ぶ。

これら 2 つの定義は同値である。

3

上記のスター自律圏の 2 つの定義は同値である。

思ってたほど単純ではなくまだ証明ができていないので、 証明ができたときに加筆する。

スター自律圏とは任意の対象が双対をもつような圏であるわけだが、 もとの圏がモノイダル閉で引き戻しをもつならば、 全ての対象が双対をもつとは限らない場合でも、 双対をもつように圏を拡大できることが知られている。 この操作は Chu2 によるもので、 Chu 構成と呼ばれる。

4

モノイダル閉圏 󰒚 の対象 を 1 つ固定し、 圏 Chu(󰒚,) を以下のように定義する。

この圏 Chu(󰒚,) を、 󰒚 による Chu 構成— construction という。

5

モノイダル閉圏 󰒚 およびその対象 をとる。 󰒚 が引き戻しをもつならば、 Chu(󰒚,) はスター自律圏の構造をもつ。

まず、 Chu(󰒚,) に対称モノイダル圏の構造を定義する。 対象 (A1,A2,a),(B1,B2,b) に対し、 󰂗a := B1A2B1(A1)(A1B1)ida 󰂗b := A1B2A1(B1)(A1B1)idb とおく。 ここで、 a:A2A1b:B2B1 はそれぞれ ab の転置であり、 ラベルのない射は標準的な同型射である。 これらの射を用いて、 引き戻し X2B1A2A1B2(A1B1)󰂗a󰂗b を計算すると、 その合成射として x󰎘:X2(A1B1) が定まる。 この転置を x:X2(A1B1) とおき、 (A1,A2,a)(B1,B2,b):=(A1B1,X2,x) と定義する。 これにより、 Chu(󰒚,) のテンソル積が定まった。 このテンソル積は明らかに対称であり、 また単位元は :=(,,λ) で与えられる。 ここで、 λ: は標準的な同型射である。

次に、 Chu(󰒚,) にスター自律圏の構造を与える。 対象の第 1 成分と第 2 成分を入れ替える関手 -: Chu(󰒚,) Chu(󰒚,) (A1,A2,a) (A2,A1,aσA2A1) を考えると、 これが双対関手を定める。 なお、 σA2A1:A2A1A1A2 はテンソル積の順序を入れ替える同型射である。 この関手は明らかに忠実充満であるから、 任意の対象 (A1,A2,a),(B1,B2,b),(C1,C2,c) に対し、 Hom((A1,A2,a)(B1,B2,b),(C1,C2,c))Hom((A1,A2,a),((B1,B2,b)(C1,C2,c))) が全ての変数に対して自然に成り立つことを示せば良い。 テンソル積の定義によって、 X2B1A2A1B2(A1B1)qp󰂗a󰂗bY2C1B2B1C2(B1C1)sr󰂗b󰂗c をともに引き戻しとし、 xy をそれぞれの合成射とすれば、 示すべき式は、 Hom((A1B1,X2,x),(C2,C1,cσC2C1))Hom((A1,A2,a),(Y2,B1C1,yσY2,B1C1)) と書ける。 これを示す。

(f1,f2):(A1B1,X2,x)(C2,C1,cσC2C1) をとる。 図式 A1Y2C1B2B1C2(B1C1)sr󰂗b󰂗cf1(pf2)g1 を考える。 ここで、 f1f1:A1B1C2 の転置であり、 (pf2)pf2:C1A1B2 と 2 回の転置で対応する射である。 この図式の外側は可換であることが示せるので、 全体を可換にするような破線の射 g1:A1Y2 が一意に存在する。 さらに、 g2:B1C1A2qf2:C1B1A2 の転置として定める。 すると、 求めていた射 (g1,g2):(A1,A2,a)(Y2,B1C1,yσY2,B1C1) が得られる。 この逆の構成も、 同様に引き戻しの普遍性を用いて行うことができるので、 式 が示された。

命題 3 の証明によって、 スター自律圏の対象 A,B に対し、 モノイダル閉圏の構造と双対関手は AB(AB) という関係で結びついていることが分かる。 このことから、 Chu(󰒚,) の対象 (A1,A2,a),(B1,B2,b) に対し、 引き戻し X1B2A2A1B1(A1B2)󰂗a󰂗b を計算し、 得られる合成射の転置を x:X1(A1B2) とすれば、 (A1,A2,a)(B1,B2,b):=(X1,A1B2,x) と書けることが分かる。 また、 大域的双対対象については、 であることから、 (,,ρ) と書ける。

6

モノイダル閉圏 󰒚 およびその対象 をとる。 このとき、 󰒚Chu(󰒚,) の余反射的部分圏と見なせる。 すなわち、 忠実充満関手 i:󰒚Chu(󰒚,) が存在して、 これに右随伴関手が存在する。

まず、 包含関手は、 i: 󰒚 Chu(󰒚,) ABf (A,A,εA)(B,B,εB)(f,fid) によって与えられる。 ここで、 εA:A(A) はモノイダル閉性の余単位である。 これが忠実充満なのは明らかである。 さらに、 この右随伴関手は、 第 1 成分への射影 r: Chu(󰒚,) 󰒚 (A1,A2,a)(B1,B2,b)(f1,f2) A1B1f1 である。 このことは容易に示せる。

以上のことから、 乗法的論理積と指数的演算子を解釈する線型論理の圏論的モデル (すなわち線型圏) 󰒚 があるとして、 それに加えて否定結合子も解釈できるモデルが欲しいとなれば、 Chu 構成 Chu(󰒚,) を作るというのが 1 つの方法として考えられる。 しかし、 Chu(󰒚,) が線型圏になるように関手 !:Chu(󰒚,)Chu(󰒚,) を定めるのは容易ではない。 これに関しては、 また別の機会で触れようと思う。

参考文献

  1. M. Barr (1979) 『Star-Autonomous Categories』 Springer-Verlag
  2. P.-H. Chu (1978) 『Constructing -Autonomous Categories』 Ph. D. thesis of McGill University