左指数随伴系
ある対象からの左指数対象が任意に存在するときに
left_exponential_adjunction.siga.LExpAdjs
= Adjunction C C (a⊗) (a⊸) a.unit a.eval
where
MonoidalCategory C ⊗ _ _ _ _ in &
&1-morph
(a⊸) : C -> C
&2-morph
a.unit : C^ => (a⊗) * (a⊸)
a.eval : (a⊸) * (a⊗) => C^モノイダル圏Cにおける
\mathrm{LExpAdjs}[a]
=\left\langle (a⊗) \dashv (a⊸) ,{}^a\mathrm{unit} ,{}^a\mathrm{eval} \right\rangle
随伴対
(a⊗) \colon C→C
(a⊸) = {}^a\_\colon C→C
^a\mathrm{unit} \colon C^\wedge ⇒ (a⊗) * (a⊸)
i.e.
{}^a\mathrm{unit}_z\colon z→a⊸(a\otimes z)
^a\mathrm{eval} \colon (a⊸) * (a⊗) ⇒ C^\wedge
i.e.
{}^a\mathrm{eval}_z\colon a\otimes (a⊸z)→z
対象a\in Cを固定して
i.e.
随伴系の自然同型、転置、反転置
{^a}\Lambda \colon \hom_C(a\otimes \_,\_) \Rightarrow \hom_C(\_,a⊸\_)
\colon C^\mathrm{op}× C \to \mathbf{Set}
{}^\cap\_ \coloneqq (x,y).\Lambda'^a
\colon \hom_C(a\otimes x,y) → \hom_C(x,{}^ay)
{}_{\cup}\_ \coloneqq (x,y).(\Lambda'^a )^{-1} =({}^{\cap}\_)^{-1}
\colon \hom_C(x,{}^ay) → \hom_C(a\otimes x,y)