Avendia19
English

日記 (2020 年 4 月 8 日)

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

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

定義 4.1

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

定義 4.2

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

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

命題 4.3

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

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

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

定義 4.4

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

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

定理 4.5

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

まず、 Chu(󰒚,) に対称モノイダル圏の構造を定義する。 対象 (A,󰔄A,a),(B,󰔄B,b) に対し、 󰂗a := B󰔄AB(A)(AB)ida 󰂗b := A󰔄BA(B)(AB)idb とおく。 ここで、 a:󰔄AAb:󰔄BB はそれぞれ ab の転置であり、 ラベルのない射は標準的な同型射である。 これらの射を用いて、 引き戻し 󰔄XB󰔄AA󰔄B(AB)󰂗a󰂗b を計算すると、 その合成射として x:󰔄X(AB) が定まる。 この転置を x:󰔄X(AB) とおき、 (A,󰔄A,a)(B,󰔄B,b):=(AB,󰔄X,x) と定義する。 これにより、 Chu(󰒚,) のテンソル積が定まった。 このテンソル積は明らかに対称であり、 また単位元は :=(,,λ) で与えられる。 ここで、 λ: は標準的な同型射である。

次に、 Chu(󰒚,) にスター自律圏の構造を与える。 対象の第 1 成分と第 2 成分を入れ替える関手 -: Chu(󰒚,) Chu(󰒚,) (A,󰔄A,a) (󰔄A,A,aσ󰔄AA) を考えると、 これが双対関手を定める。 なお、 σ󰔄AA:󰔄AAA󰔄A はテンソル積の順序を入れ替える同型射である。 この関手は明らかに忠実充満であるから、 任意の対象 (A,󰔄A,a),(B,󰔄B,b),(C,󰔄C,c) に対し、 Hom((A,󰔄A,a)(B,󰔄B,b),(C,󰔄C,c))Hom((A,󰔄A,a),((B,󰔄B,b)(C,󰔄C,c))) が全ての変数に対して自然に成り立つことを示せば良い。 テンソル積の定義によって、 󰔄XB󰔄AA󰔄B(AB)qp󰂗a󰂗b󰔄YC󰔄BB󰔄C(BC)sr󰂗b󰂗c をともに引き戻しとし、 xy をそれぞれの合成射の転置とすれば、 示すべき式は、 Hom((AB,󰔄X,x),(󰔄C,C,cσ󰔄CC))Hom((A,󰔄A,a),(󰔄Y,BC,yσ󰔄Y,BC)) と書ける。 これを示す。

(f,󰔄f):(AB,󰔄X,x)(󰔄C,C,cσ󰔄CC) をとる。 図式 A󰔄YC󰔄BB󰔄C(BC)sr󰂗b󰂗cf(p󰔄f)g を考える。 ここで、 ff:AB󰔄C の転置であり、 (p󰔄f)p󰔄f:CA󰔄B と 2 回の転置で対応する射である。 この図式の外側は可換であることが示せるので、 この全体を可換にするような破線の射 g:A󰔄Y が一意に存在する。 さらに、 󰔄g:BC󰔄Aq󰔄f:CB󰔄A の転置として定める。 すると、 求めていた射 (g,󰔄g):(A,󰔄A,a)(󰔄Y,BC,yσ󰔄Y,BC) が得られる。 この逆の構成も、 同様に引き戻しの普遍性を用いて行うことができるので、 式 が示された。

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

定理 4.6

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

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

以上のことから、 乗法的論理積と指数的演算子を解釈する線型論理の圏論的モデル (すなわち線型圏) 󰒚 があるとして、 それに加えて否定結合子も解釈できるモデルが欲しいとなれば、 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