generated at
内部homを用いた随伴系の自然同型
随伴系のhom自然同型を内部hom函手をもって
Adjunction.sig
signature Adjunction fixed-in Cat Data 0-morph C, D 1-morph leftAdjoint @ L : C -> D 1-morph rightAdjoint @ R : D -> C 2-morph unit @ η : C^ => L * R : C -> C 2-morph counit @ ε : R * L => D^ : D -> D Axioms 3-eq snaky-1 : (η * L^); (L^ * ε) ≡> L^ 3-eq snaky-2 : (R^ * η); (ε * R^) ≡> R^
sig
.0-morph in C c,c',.. .1-morph f : c .-> c',.. %0-morph in Cat %I, C, D %1-morph L : C %-> D R : D %-> C c%~ : %I %-> C d%~ : %I %-> D c%~ %1 L = (c.L)%~ : %I %-> D %2-morph η : C^ %=> L %1 R : C %-> C ε : R %1 L %=> D^ : D %-> D f%~ : c%~ %=> c'%~ f'%~ : c%~ %=> c"%~ f%~ %2 f'%~ = (f .1 f')%~ : c%~ %=> c"%~ : %I %-> C f%~ %1 L = (f.L)%~ : (c.L)%~ %=> (c'.L)%~ : %I %-> D where %1 = * &0-morph in CAT &I, Cat &1-morph (%I)&~, C&~, D&~# : &I &-> Cat &2-morph d%~&~: (%I)&~ &=> D&~ c%~&~: (%I)&~ &=> C&~ C^&~ : C&~ &=> C&~ L&~ : C&~ &=> D&~ R&~ : D&~ &=> C&~ : &I &-> Cat (L %1 R)&~ = L&~ &2 R&~ : C&~ &=> C&~ &3-morph? η&~ : C^&~ &3> L&~ &2 R&~ : C&~ &=> C&~ : &I &-> Cat
モノイダル閉圏における指数随伴系の自然性
表したいもの
\Phi \colon \hom_D(\_.L,\_) \Rightarrow \hom_C(\_,\_.R)
\colon C^\mathrm{op}× D \to \mathbf{Set}
sig
&2-morph [_*L,d]&~ = (L&~ &× d&~) &* &hom : [D&~,%I&~] &=> [C&~,D&~] : &I &× &I &-> Cat [_,dR]&~ = (C&~&^ &× dR&~) &* &hom : [C&~,%I&~] &=> [C&~,C&~] : &I &× &I &-> Cat -- &I &× &I &~= &I -- &I &-> Cat は大域要素 %1-morph [_*L,d] : [D,%I] %-> [C,D] -- [X,%I] ~= Const %I, : Const %I %-> [C,D] -- %I %-> [C,D] は大域要素 : C %-> D &Φ : [ _ * L, d] &=> [ _ , dR] ∀ c : %I -> C c.&Φ : [c * L,d] %=> [c , dR] : [ ∀ f : c * L => d (f)(c.&Φ) : c => dR ∀ g : c -> c' ((g*L);_) : [c' * L,d] =>[c * L,d]