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

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

次に、 Chu(󰒚,⫫) にスター自律圏の構造を与える。 対象の第 1 成分と第 2 成分を入れ替える関手 -∗: Chu(󰒚,⫫)∘ ⟶ Chu(󰒚,⫫) (A,󰔄A,a) ⟼ (󰔄A,A,a∘σ󰔄AA) を考えると、 これが双対関手を定める。 なお、 σ󰔄AA:󰔄A⊗A→A⊗󰔄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(A⊗B)⊸⫫qp󰂗a󰂗b󰔄YC⊸󰔄BB⊸󰔄C(B⊗C)⊸⫫sr󰂗b󰂗c をともに引き戻しとし、 x と y をそれぞれの合成射の転置とすれば、 示すべき式は、 Hom((A⊗B,󰔄X,x),(󰔄C,C,c∘σ󰔄CC))≅Hom((A,󰔄A,a),(󰔄Y,B⊗C,y∘σ󰔄Y,B⊗C))♡ と書ける。 これを示す。

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

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