There is a strict 2-functor $\boxed{\big( ()\mathord-\Cat = ()_\ast \big) : \MONCAT \to \CAT : \calV \mapsto (\calV\mathord-\Cat = \calV_\ast)}$
between (the indicated strict 2-categories);
see CC II.6.3, also RE2C ¶1.3.2;
the notation $\calV\mathord-\Cat$ is now more standard, see e.g. BCECT,
but CC uses the briefer notations $\calV_\ast$, $\Phi_\ast$ and $\eta_\ast$ for the effect on monoidal categories, monoidal functors and monoidal natural transformations.
(Also, CC calls 2-categories “hypercategories”, a term no longer used for 2-categories.)
(The $()_\ast$ notation) is consistent with (other usages of $()_\ast$):
if we severely overload (the symbol $\setX$) so that it stands for (a) a $\calV$-category and (b) that $\calV$-category's set (or class) of objects, with (c) $\hom - \setX -$ denoting $\setX$'s hom-function,
then (the hom-function of $\setX\Phi_\ast$) is defined as:
\[ \hom - {(\setX\Phi_\ast)} - : \setX\times\setX \xrightarrow[\mkern2em]{\textstyle \hom - \setX -} \calV \xrightarrow[\mkern2em]{\textstyle \phi} \calV' : \langle \objectx,\objecty \rangle \mapsto \hom \objectx \setX \objecty \phi = \hom \objectx {(\setX\Phi_\ast)} \objecty \;. \]
For its brevity we adopt this notation for the effects of $\big( ()\mathord-\Cat = ()_\ast \big)$ on monoidal functors and monoidal natural transformations: thus $\functorF_\ast$ and $\eta_\ast$,
while using the notation $\calV\mathord-\Cat$ for the effect on monoidal categories.
[the image under the 2-functor $\big( ()\mathord-\Cat = ()_\ast \big)$]
of (the above adjunction in the 2-category $\MONCAT$)
is (an adjunction in the 2-category $\CAT$): \[\boxed{\begin{array}{} \functionh & \in & \mkern1em \hom \setX {\Set\mathord-\Cat} {\objectA \functorU_\ast} & \mkern2em \smash{\Rule {2px} {2ex} {11ex}} \mkern1em & && \langle \Set,\times,1 \rangle\mathord-\Cat && \xrightarrow{\mkern3em} && \langle \Set,\times,1 \rangle\mathord-\Cat && \xrightarrow{\mkern3em} && \langle \Set,\times,1 \rangle\mathord-\Cat \\ && \wr\Vert && & \llap\setX \nearrow & \llap\functionk \Big\Downarrow & \searrow \rlap{\functorF_\ast} & \Big\Downarrow \rlap{\eta_\ast} & \nearrow \rlap{\functorU_\ast} & \llap\Vert \Big\Downarrow \rlap{\epsilon_\ast} & \searrow \rlap{\functorF_\ast} & \Big\Downarrow \rlap{\eta_\ast} & \nearrow \rlap{\functorU_\ast = \langle \functoru,\tilde\functoru,\functoru^\circ \rangle _\ast} \\ \functionk & \in & \mkern.6em \hom {\setX \functorF_\ast} {\cattwo\mathord-\Cat} \objectA && \catI && \xrightarrow[\textstyle \objectA]{\smash{\mkern3em}} && \langle \cattwo,\land,\top \rangle\mathord-\Cat && \xrightarrow[\mkern3em]{\smash{}} && \langle \cattwo,\land,\top \rangle\mathord-\Cat \\ \end{array}}\] (The monoidal structures $\functoru^\circ$, $\tilde\functoru$, $\functorf^\circ$, and $\tilde\functorf$) combine with (the functors $\functoru$ and $\functorf$ themselves)
to produce ($\functorU_\ast$ and $\functorF_\ast$):
the units (CC I(6.3)) and compositions (CC II(6.1)) of ($\objectA\functorU_\ast$ and $\objectX\functorF_\ast$) are defined by: \[\mkern-3em \begin{array}{} && && && && & \hom \objecta {(\objectA\functorU_\ast)} \objectb \times \hom \objectb {(\objectA\functorU_\ast)} \objectc &&&& &&&& &&&& & \hom \objectx {(\objectX\functorF_\ast)} \objecty \land \hom \objecty {(\objectX\functorF_\ast)} \objectz \\ && && && && & \Vert &&&& &&&& &&&& & \Vert \\ && 1 & = & 1 && && & (\hom \objecta \objectA \objectb)\functoru \times (\hom \objectb \objectA \objectc)\functoru &&&&&& \top & = & \top &&&&& (\hom \objectx \objectX \objecty)\functorf \land (\hom \objecty \objectX \objectz)\functorf \\ && \llap{\wr\Vert} \big\downarrow & \functoru^\circ & \llap{\wr\Vert} \big\downarrow & && && \llap{\wr\Vert} \big\downarrow \rlap{\langle \hom \objecta \objectA \objectb, \hom \objectb \objectA \objectc \rangle \tilde\functoru} &&&& && \llap{\Vert} \big\downarrow & \functorf^\circ & \llap{\Vert} \big\downarrow &&&&& \llap{\Vert} \big\downarrow \rlap{\langle \hom \objectx \objectX \objecty, \hom \objecty \objectX \objectz \rangle \tilde\functorf} \\ \top & \mathop\mapsto\limits^\functoru& \top\functoru & = & \hom \top \cattwo \top &&& \hom \objecta \objectA \objectb \land \hom \objectb \objectA \objectc & \mathop\mapsto\limits^\functoru & \big( \hom \objecta \objectA \objectb \land \hom \objectb \objectA \objectc \big)\functoru &&&& 1 & \mathop\mapsto\limits^\functorf & 1\functorf & = & 1\cdot\top &&& \hom \objectx \objectX \objecty \times \hom \objecty \objectX \objectz & \mathop\mapsto\limits^\functorf & \big( \hom \objectx \objectX \objecty \times \hom \objecty \objectX \objectz \big)\functorf \\ \llap{\text{refl}} \big\downarrow & \mathop\mapsto\limits^\functoru & \llap{\text{refl}\functoru} \big\downarrow & = & \big\downarrow \rlap{\hom \top \cattwo {\text{refl}}} &&& \llap{\text{trans}} \big\downarrow & \mathop\mapsto\limits^\functoru & \llap{\text{trans}\functoru} \big\downarrow &&&& \llap{\objectx\arrowj} \big\downarrow & \mathop\mapsto\limits^\functorf & \llap{\objectx\arrowj\functorf} \big\downarrow & = & \big\downarrow \rlap{(\objectx\arrowj)\cdot\top} &&& \llap{\Mforcomp} \big\downarrow & \mathop\mapsto\limits^\functorf & \big\downarrow \rlap {\Mforcomp\functorf} \\ \hom \objecta \objectA \objecta & \mathop\mapsto\limits^\functoru & \hom \objecta \objectA \objecta \functoru & = & \hom \top \cattwo {\hom \objecta \objectA \objecta} &&& \hom \objecta \objectA \objectc & \mathop\mapsto\limits^\functoru & \hom \objecta \objectA \objectc \functoru &&&& \hom \objectx \objectX \objectx & \mathop\mapsto\limits^\functorf & \hom \objectx \objectX \objectx \functorf & = & \hom \objectx \objectX \objectx \cdot\top &&& \hom \objectx \objectX \objectz & \mathop\mapsto\limits^\functorf & \hom \objectx \objectX \objectz \functorf \\ && \Vert && && && & \Vert &&&& && \Vert && &&&& & \Vert \\ && {} \rlap{\mkern-2em \hom \objecta {(\objectA\functorU_\ast)} \objecta} && && && & {} \rlap{\mkern-2em \hom \objecta {(\objectA\functorU_\ast)} \objectc} &&&& && \hom \objectx {(\objectX\functorF_\ast)} \objectx && &&&& & \hom \objectx {(\objectX\functorF_\ast)} \objectz \\ \end{array}\]
Here of course ($\text{refl}$ and $\text{trans}$) are the implementations in ($\cattwo$-category theory)
of (the reflexive and transitive axioms for preorders);
in (the notation of CC) they would be denoted $\objecta\arrowj$ and $(\Mforcomp = \Mforcomp^\objectb_{\objecta\objectc})$ respectively.
References
CC, Eilenberg and Kelly, “Closed Categories”, 1966RE2C, Kelly and Street, “Review of the Elements of 2-Categories”, 1974
BCECT, Kelly, Basic Concepts of Enriched Category Theory, 1982/2005
No comments:
Post a Comment