モノイダル閉圏における指数随伴系の自然性
from 内部homを用いた随伴系の自然同型
もくじ
というかページをダイエットさせたい
目的
モノイダル閉圏における指数随伴系\Sigma_L[A]=\left\lang A\otimes \_ \dashv A⊸\_ ,{}^A\mathrm{unit} ,{}^A\mathrm{eval} \right\rangの自然性をちゃんと考える
sigAdjunction
Cat Cat
A.&prod A.&hom
A.&unit A.&eval前提
左強モノイダル閉圏として扱う
デカルト積の対称性は使わない
Catの埋め込み先
& こっちは右強モノイダル閉圏として
& = CAT だと大きすぎ？Catとその仲間たちだけの圏でよさそう
Catから生成されるモノイダル閉圏？
sig% = L-S-C-MC Cat %× %I %⊸
& = R-S-C-MC ??? &× &I &⟜指数随伴対 A.\mathrm{prod} \dashv A.\mathrm{hom}
Cat P-1図式
ExpAdj.sig&1-morph
A.&prod = (A×_) : Cat &-> Cat
A.&hom = [A,_] : Cat &-> Cat左から掛けているやつ
(×)\colon \mathrm{Cat} × \mathrm{Cat} → \mathrm{Cat}
[,] = (⊸) \colon \mathrm{Cat}^\mathrm{op}× \mathrm{Cat} \to \mathrm{Cat}
[A,B] = A⊸B
ExpAdj.sig&1-morph
(%×) = \A B -> A %× B
: Cat &× Cat &-> Cat
(%⊸) = %[_,_] = \A B -> A %⊸ B
: Cat^{op} &× Cat &-> Catこいつらを一つ上(
& )から右カリー化するExpAdj.sig&1-morph
prod = (%×)&∩ = \A ->(\B -> A × B)
: Cat &-> (Cat &⟜ Cat)
hom = (%⊸)&∩ = \A ->(\B -> A ⊸ B)
: Cat^{op} &-> (Cat &⟜ Cat)単位、余単位
{^A}\mathrm{unit} \colon (\_) ⇒ A⊸(A×\_)
{^A}\mathrm{eval}\colon A×(A⊸\_)⇒(\_)
Cat P-1図式
& 1-2図式
ExpAdj.sig&1-morph
&2-morph
A.unit : Cat^ &=> [A,(A×_)]
A.eval : A × [A,_] &=> Cat^
: Cat &-> Cat
where
(*) = (&1)
[A,(A×_)] = A.prod * A.hom
A × [A,_] = A.hom * A.prodこれで随伴系の材料が揃った
sigAdjunction
Cat Cat
A.prod A.hom
A.unit A.evalまたこれはニョロニョロしてる
ExpAdj.sigAxioms
&3-eq snaky-1:
A.unit * A.prod^ ; A.prod^ * A.eval
== A.prod^
: A.prod => A.prod
&3-eq snaky-2:
A.hom^ * A.unit ; A.eval * A.hom^
== A.hom^
: A.hom => A.hom
where
(*) = (&1), (;) = (&2), (^) = (&^)Cat P-1図式
& 1-2図式
自然性
単位と余単位のI-スライダー性
成分Bについては自然変換なので
自然変換のエレベーター性がそのまま
Cat P-1図式
I-slider.sig%1-morph
G: B -> B'
G.A.unit
== B.A.unit ; [A,(A×G)]
== G ; B'.A.unit
G.A.eval
== B.A.eval ; G
== (A×[A,G]) ; B'.A.eval
where
(;) = (%1)いつもは
* にしてる函手の結合だけど、今回はCatが最下層なのでこうした方が見やすい& 1-2図式
左内部hom函手の構成から自動的に導かれる
Cat P-1図式
U-slider.sigF : A %-> A'
&3-eq
F.unit : Cat^ &=> [A,(A'×_)]
:= A.unit; [A,(F×_)]
== A'.unit; [F,(A'×_)]
F.eval : A × [A',_] &=> Cat^
:= (A×[F,_]); A.eval
== (F×[A',_]); A'.eval
where
(*) = (&1), (;) = (&2){^A}\Lambda \colon \mathbf{Cat}[A×\_,\_] \Rightarrow \mathbf{Cat}[\_,A⊸\_]
{^∩}P=P.{^A}\Lambda^B_{B'} = {^A}\mathrm{unit}_{B};(A⊸P)
{_∪}Q=Q.({^A}\Lambda^B_{B'})^{-1} = (A×Q);{^A}\mathrm{eval}_{B'}
where
P : A×B→B'
Q : B→A⊸B'
内部homでやってみる
Cat P-1図式
curry.sig&2-iso
A.%ΛL : (A×_)⊸_ &=> _⊸(A⊸_)
: Cat^{op} &× Cat &-> Cat
%1-iso
(B,B').A.%ΛL : (A×B)⊸B' %-> B⊸(A⊸B')
%1-morph
P : A×B -> B'
Q : B -> A⊸B'
∩P = P.(B,B').A.%ΛL
= B.A.unit %1 P.A.hom
: B -> A⊸B'
∪Q = Q.[(B,B').A.%ΛL]^{-1}
= Q.A.prod %1 B.A.eval
: A×B -> B'うまくいかない……
随伴系のなす圏への函手にしたかった
しかしスライディングの同値が噛み合わない
付録
計算途中に使ったやつ
ExpAdj.sig%0-morph
A, B
A %⊸ B , A %× B
&0-morph
Cat(%)[F,G] : [A',B] → [A,B']
where
F\colon A→A' G\colon B→B'
想定される成分は\colon H \mapsto F;H;G
スライディング.sig&2-morph
A.unit : Cat^ &=> [A,(A×_)]
A.eval : A × [A,_] &=> Cat^
[A,(F×_)] = (F.prod) * (A.hom)
: [A,(A×_)] &=> [A,(A'×_)]
[F,(A'×_)] = (A'.prod) * (F.hom)
: [A',(A'×_)] &=> [A,(A'×_)]
A × [F,_] = (F.hom) * (A.prod)
: A × [A',_] &=> A × [A,_]
F × [A',_] = (A'.hom) * (F.prod)
: A × [A',_] &=> A' × [A',_]
sig Cat[A×B,B'] = (A×B)⊸B'
Cat[B,A×B'] = B⊸(A⊸B')