Consider a
monoidal closed category, with objects and the
labeled arrows as in any of the three diagrams below
(the only differences between them are (
affine transformations, a reflection, a
horizontal shear and a rotation) on the diagrams).
The unlabeled arrows should be understood to be either
(unnamed variables) of (the specified source-target type), or, alternatively,
[the hom objects, e.g. $[\objectA\backslash\objectB]$] determined by (the source and target of (the unlabeled arrows)).
$\begin{array}{}
\objectA' & {}\rlap{\xrightarrow{\mkern6em}} &&& \objectB && &&&&
&& \objectA & {}\rlap{\xrightarrow{\mkern6em}} &&& \objectB' &&&&
\objectA' & \xrightarrow{\smash{\textstyle \;\arrowf\;}} & \objectA \\
& \llap\arrowf \searrow && \nearrow && \searrow \rlap\arrowh & & \mkern2em & \text{reflection} & \mkern2em &
& \llap\arrowf \nearrow && \searrow && \nearrow \rlap\arrowh & & \mkern2em & \text{h.s. and rotation} & \mkern2em &
\big\downarrow & \swarrow & \big\downarrow \\
&& \objectA & {}\rlap{\xrightarrow{\mkern6em}} &&& \objectB' &&&&
\objectA' & {}\rlap{\xrightarrow{\mkern6em}} &&& \objectB && &&&&
\objectB & \xrightarrow[\smash{\textstyle \;\arrowh\;}]{} & \objectB' \\
\end{array}$
In such a situation, we have the following commutative cubical diagram:
$\begin{array}{}
&&&&& 1 & 2 & 3 & 4 & 5 & 6 \\
1 & \objectA' &&&& \boxed{ \begin{array}{} \elta'&&\arrowg \\ {\objectA'}&\tensor&[\objectA\backslash\objectB]\\ \end{array} } & {}\rlap{ \mkern-1em\xrightarrow[\mkern14em]{\textstyle {\objectA'} \tensor \boxed{[\arrowf\backslash\objectB]}} } && \boxed{ \begin{array}{} \elta'&&\arrowf\arrowg \\ {\objectA'} & \tensor & [{\objectA'}\backslash\objectB]\\ \end{array} } \\
2 && \llap\arrowf \searrow &&& & \llap{\arrowf \tensor [\objectA\backslash\objectB]} \searrow & {}\rlap{ \mkern1em\boxed{\boxed{\hom \arrowf \arrowe \objectB = \text{U}}} } && \searrow \rlap{\hom {\objectA'} \arrowe \objectB} \\
3 &&& \objectA & \mkern2em & && \boxed{ \begin{array}{} \elta'\arrowf&&\arrowg \\ \objectA&\tensor&[\objectA\backslash\objectB]\\ \end{array} } & {} \rlap{ \mkern-4em\xrightarrow[\mkern14em]{\smash{\textstyle \hom \objectA \arrowe \objectB} } } && \boxed{ \begin{array}{} \elta'\arrowf\arrowg \\ \objectB\\ \end{array} } \\
4 &&&&& \llap{{\objectA'} \tensor [\objectA\backslash\arrowh]} \Bigg\downarrow & {} \rlap{ \mkern1em \boxed{\boxed{{\objectA'} \tensor [\arrowf\backslash\arrowh] = \text{B}}} } && \Bigg\downarrow \rlap{{\objectA'} \tensor \boxed{[{\objectA'}\backslash\arrowh]}} \\
5 &&&&& & {} \rlap{ \mkern-3.5em \boxed{\boxed{\arrowf \tensor [\objectA\backslash\arrowh] = \text{L}}} } & {} \rlap{ \mkern2em \smash{\boxed{\boxed{\boxed{\hom \arrowf \arrowe \arrowh}}} \mkern7em \boxed{\boxed{\hom {\objectA'} \arrowe \arrowh = \text{R}}}} } \\
6 &&&&& && \llap{\objectA \tensor \boxed{[\objectA\backslash\arrowh]}} \Bigg\downarrow & \boxed{\boxed{\hom \objectA \arrowe \arrowh = \text{F}}} && \Bigg\downarrow\rlap\arrowh \\
7 &&&&& \boxed{ \begin{array}{} \elta'&&\arrowg\arrowh \\ {\objectA'}&\tensor&[\objectA\backslash{\objectB'}]\\ \end{array} } & {}\rlap{ \mkern-1em\xrightarrow[\mkern14em]{\textstyle {\objectA'} \tensor \boxed{[\arrowf\backslash{\objectB'}]}} } && \boxed{ \begin{array}{} \elta'&&\arrowf\arrowg\arrowh \\ {\objectA'}&\tensor&[{\objectA'}\backslash{\objectB'}]\\ \end{array} } \\
8 &&&&& & \llap{\arrowf \tensor [\objectA\backslash{\objectB'}]} \searrow & {}\rlap{ \mkern1em\boxed{\boxed{\hom \arrowf \arrowe {\objectB'} = \text{D}}} } && \searrow \rlap{\hom {\objectA'} \arrowe {\objectB'}} \\
9 &&&&& && \boxed{ \begin{array}{} \elta'\arrowf&&\arrowg\arrowh \\ \objectA&\tensor&[\objectA\backslash{\objectB'}]\\ \end{array} } & {} \rlap{ \mkern-4em\xrightarrow[\mkern14em]{\smash{\textstyle \hom \objectA \arrowe {\objectB'} } } } && \boxed{ \begin{array}{} \elta'\arrowf\arrowg\arrowh \\ {\objectB'}\\ \end{array} } \\
\end{array}$
The boxes (other than those enclosing the eight vertices of the cube) have the following meanings:
A single box, e.g. $\boxed{[\arrowf\backslash\objectB]}$, denotes an arrow determined by the universal condition on a universal arrow, $\hom {\objectA'} \arrowe \objectB$ in this case.
A double box, e.g. $\boxed{\boxed{\hom \arrowf \arrowe \objectB = \text{U}}}$, denotes a commuting square = commuting face of the cube;
we use “Rubik’s cube” abbreviations to designate the faces of the cube: Up/Down, Left/Right, Front/Back.
The triple box, $\boxed{\boxed{\boxed{\hom \arrowf \arrowe \arrowh}}}$, denotes the total cube determined by $\arrowf$ and $\arrowh$.
The commutative squares (faces of the cube) labeled $\boxed{\boxed{\hom \objectA \arrowe \arrowh = \text{F}}}$ and $\boxed{\boxed{\hom {\objectA'} \arrowe \arrowh = \text{R}}}$
define the covariant arrows $\boxed{[\objectA\backslash\arrowh]}$ and $\boxed{[{\objectA'}\backslash\arrowh]}$, and then witness the ordinary naturality of $\arrowe$ WRT (with respect to) $\arrowh$.
The commutative squares labeled $\boxed{\boxed{\hom \arrowf \arrowe \objectB = \text{U}}}$ and $\boxed{\boxed{\hom \arrowf \arrowe {\objectB'} = \text{D}}}$
define the contravariant arrows $\boxed{[\arrowf\backslash\objectB]}$ and $\boxed{[\arrowf\backslash{\objectB'}]}$, and then witness the extraordinary naturality of $\arrowe$ WRT $\arrowf$.
The commutativity of $\boxed{\boxed{\arrowf \tensor [\objectA\backslash\arrowh] = \text{L}}}$ is simply because $\tensor$ is a bifunctor.
The commutativity of the $[\arrowf\backslash\arrowh]$ square (a $\tensor$-factor of the $\boxed{\boxed{{\objectA'} \tensor [\arrowf\backslash\arrowh] = \text{B}}}$ square)
is determined by the commutativity of the $\text{R}, \text{U}, \text{F}, \text{L}, \text{D}$ faces, plus the uniqueness clause applied to $\hom {\objectA'} \arrowe {\objectB'}$.
The cube itself, labeled $\boxed{\boxed{\boxed{\hom \arrowf \arrowe \arrowh}}}$, witnesses the joint (simultaneous) naturality of $\arrowe$ WRT both $\arrowf$ and $\arrowh$.
This is a variation on a diagram in paragraph 1.3.2 of MVFC.
References
MVFC, Max Kelly,
“Many-variable functorial calculus”, 1972
Draft stuff:
No comments:
Post a Comment