Friday, December 17, 2021

The strong Yoneda lemma

Draft:
Kelly, ECT $\S\;$ 2.4 (2.31)

\[ \boxed{ \begin{array} {} && \hom {\hom K \calA -} {[\calA,\calV]} { \rightcat F} \\ && \Vert\kern-.1em\vert \\  && \rightadj{ \displaystyle \int_{\black A} \black{ [ \hom K \calA {\rightcat A}, {\rightcat F_A} ] } } \\ & \leftcat{ \llap{?? \exists!} \nearrow } & \rightadj{\Big\downarrow \rlap{\lambda_{\rightcat A}} } \\ \leftcat X & \rightcat{ \xrightarrow [\textstyle \alpha_A] {\kern3em} }  & [ \hom K \calA {\rightcat A}, {\rightcat F_A} ] \\ & \leftcat{ \llap{\exists! \eta} \searrow  }  & \rightadj{  \Big\uparrow \rlap{ \boxed{ \overline{ \rightcat{\hom {\black K} F A} } \equiv \phi_{\rightcat A} }  }   }  \\  && {\rightcat F}_K  \\  \hline \\  \leftcat X \tensor \hom K \calA {\rightcat A} & \xrightarrow{} &  \rightcat{F_A}  \\ \leftcat X \tensor \hom K \calA {\rightcat K} & \xrightarrow{} &  \rightcat{F_K} & {} \rlap{ \kern-3em \text{the instance } A=K } & \kern4em \\ \\  \hline \hom K \calA {\rightcat A} & \rightcat{  \xrightarrow { \textstyle \overline{\alpha_A} }  } &  [ \leftcat X, {\rightcat F_A} ] & \leftcat X  \\  & \rightcat{  \llap{\hom {\black K} F A} \searrow \rlap{ \leftcat{(1.48)} }  } & \Big\uparrow \rlap{ \kern -1.5em [\leftcat\eta, \rightcat{F_A}] } & \leftcat{ \Big\downarrow \rlap{ \boxed{\exists! \eta} }  }   \\   && [{\rightcat F}_K, \rightcat{F_A}] & {\rightcat F}_K \\ \\  \hline {} \rlap{ \kern-2em \text{instantiating the last triangle at } A=K \text{ gives} } \\ \hline \hom K \calA {\rightcat K} & \rightcat{  \xrightarrow { \textstyle \overline{\alpha_K} }  } &  [ \leftcat X, {\rightcat F_K} ] & \leftcat X  \\  & \rightcat{  \llap{\hom {\black K} F K} \searrow \rlap{ \leftcat{(1.48)} }  } & \Big\uparrow \rlap{ \kern -1.5em [\leftcat\eta, \rightcat{F_K}] } & \leftcat{ \Big\downarrow \rlap{ \boxed{\exists! \eta} }  } & \kern1em  \\ && [{\rightcat F}_K, \rightcat{F_K}] & {\rightcat F}_K  \\ \\  \hline {} \rlap{ \kern-2em \text{precomposing that triangle with } j_K \text{ gives } \eta = 1_K \overline{\alpha_K} }  \\ \end{array} } \]

To recover the weak version of the Yoneda lemma of Section 1.9,, 
take $\leftcat{X=I}$.

$\eta = \overline{\alpha_K} (1_K) $

<hr />

\[ \boxed{ \begin{array} {} \kern2em & \rightcat{\mathbf P} & \xrightarrow { \textstyle \rightcat{\hom q {\mathbf P} -} } & \leftcat{\mathbf V} \\ \hline  & p \\ &&& \nwarrow \rlap{ \hom q {\mathbf P} {p} } \\ & \rightcat{ \llap{ \hom p {\mathbf P} {p'} } \Bigg\downarrow } & \xrightarrow {  \textstyle \hom p { \big( \hom q {\mathbf P} - \big) } {p'}  } & \Big\downarrow & q \\. &&& \swarrow \rlap{ \hom q {\mathbf P} {p'} } \\ & p'  \end{array} } \]

\[ \boxed{ \begin{array} {} q,p \in {} & P \times P & \xrightarrow { \textstyle \text{hom}_{\mathbf P} = {\hom - {\mathbf P} -} } & V & {} \ni \hom q {\mathbf P} p = \overrightarrow{qp} \\   && \llap{ {\hom - P -} = \text{Hom}_P } \searrow & \Big\downarrow \rlap {U = \hom 0 V -}  \\  &&& \cattwo \\ & \theta: & \hom q P p & \cong & \hom 0 V {(\hom q {\mathbf P} p)} \\ && q = p & \iff & 0 = {\hom q {\mathbf P} p}  \\  \end{array} } \tag{tailored version of ECT (1.33)}  \]

Tuesday, December 7, 2021

Affine spaces as actegories

DRAFT:

Our goal here is to apply some of the concepts and notation of 
Janelidze-Kelly's treatment of actegories to
Mac Lane-Birkhoff's treatment of affine spaces.

There are four entities, or structures, which we shall be talking about.
An overview of those structures, together with some possible variable names for their elements/objects, is given in the following table:
\[ \boxed{ \begin{array} {c|c|c} & \text{discrete, i.e. enriched in monoidal closed } \cattwo = \{\leftadj\bot \lt \rightadj\top\} & \text{enriched in monoidal closed } \leftcat V  \\  \hline \leftcat{\text{actor}} & \leftcat{ V = \{u,v,w,X,Y,Z,\ldots\} \; \text{(monoidal closed)} \quad {(\mathcal V}_0) }  & \leftcat{\mathbf V \quad {(\mathcal V)} }    \\    & \leftcat{ \boxed{ \hom {\leftadj Y} V {\rightcat Z} \iff \leftadj Y = \rightcat Z } } \in \cattwo \quad ; \quad \leftadj{ \boxed{\leftcat X \tensor Y = \leftcat X + Y} } \quad ; \quad \rightadj{ \boxed{[\leftadj Y, \rightcat Ζ] = \rightcat Z - \leftadj Y} } & \boxed{ \begin{array} {} \leftadj Y \\ & \rightadj{  \searrow \rlap{ \boxed{ \hom {\leftadj Y} {\mathbf V} {\rightcat Z} = [\leftadj Y, \rightcat Ζ] = \rightcat Z - \leftadj Y } \leftcat{{} \in V} } }  \\ && \rightcat Z & \kern10em \\ \end{array} }   \\ \hline \rightcat{\text{actee}} & \rightcat{ P = \{p,q,r,\ldots\} \quad ({\mathcal P}_0 \text{ or } {\mathcal A}_0) } & \rightcat{ \mathbf P \quad (\mathcal P \text{ or } \mathcal A) } \\ &  \rightcat{ \boxed{ \hom {\leftadj q} P p  \iff {\leftadj q = p} } } \in \cattwo &  \boxed{ \begin{array} {} \leftadj q \\ & \rightadj{   \searrow \rlap{  \boxed{ \hom {\leftadj q} {\mathbf P} {\rightcat p} = \overrightarrow{\leftadj q, \rightcat p} = \rightcat p - \leftadj q } \leftcat{{} \in V}  }   } \\ && \rightcat p & \kern8em  \\ \end{array} } \\  \end{array} } \]
The category names in parentheses are my estimation of how Kelly would have denoted them using the naming conventions he used in his 1982 book <I>ECT</I>; 
those not in parentheses follow the conventions in JK.
This may be useful in comparing the two references.

\[ \hom {\leftadj Y} {\mathbf V} {\rightcat Z} = \rightadj{ [\leftadj Y, \rightcat Ζ] = \rightcat Z - \leftadj Y } \]

For the current discussion,
we are treating $\cattwo$, and M-B's $V$ and $P$, as <I>discrete</I> categories, the first two being discrete monoidal.
Thus in the following table
an isomorphism "in $\cattwo$" asserts an if-and-only-if relation between two statements; 
an isomorphism "In $V$" asserts equality of two vectors in the vector space $V$.

The right adjoints $\rightadj{\mathbf P}$ and $\rightadj{\mathbf V}$ defined by $\red\kappa$ and $\red k$ enrich $P$ and $V$ into $V$-categories, 
which get denoted by the names of their $V$-valued homs, namely $\mathbf P$ and $\mathbf V$.

\[ \boxed{ \begin{array} {ccrclc|ccc|cr} && \leftadj{ \big( \leftcat{?_V} \star q = \hat q \big) } & \red\dashv & \rightadj{ \boxed{  \big(  \hom  {\leftadj q} {\mathbf P} { \rightcat{?_P} } = (\rightcat{?_P} - \leftadj q) = \overrightarrow{ \leftadj q\rightcat{?_P} } \big) } }   \\   \red\kappa & \red : & \rightcat{ \hom { \leftadj{ (\leftcat v \star q = \leftcat v + q = \leftcat v \hat q) } } {P} p } & \red{ \buildrel \kappa \over \cong } & \hom {\leftcat v} {\leftcat V} { \rightadj{ \boxed{ ( \hom {\leftadj q} {\mathbf P} {\rightcat p} = (\rightcat p - \leftadj q) = \overrightarrow{\leftadj q\rightcat p} ) }     }   } & \kern1em & \kern1em & \text{in } \cattwo & \kern3em & \kern3em & \text{(MB 5, JK 2.1)}    \\    \red\pi & \red : &  \rightcat{ \hom { (\leftcat v \tensor w \mathrel = \leftcat v + w) } {V} u } & \buildrel \pi \over \cong & \hom v {V} { \boxed{ { ( \hom w {\mathbf V} {\rightcat u} = [w,\rightcat u] = (\rightcat u - w) ) }  }   } &&& \text{in } \cattwo &&& \text{(ECT 1.23, JK 2.2)}    \\   \red{ k = k_{\rightadj v, \leftadj q, \rightcat p} }   & \red : & \rightcat{ \hom { \leftadj{ (\leftcat v \star q = \leftcat v + q = \leftcat v \hat q) } } {\mathbf P} p } & \red{ \buildrel k \over \cong } & \hom {\leftcat v} {\leftcat{\mathbf V}} { \rightadj{  \boxed{ ( \hom {\leftadj q} {\mathbf P} {\rightcat p} = (\rightcat p - \leftadj q) = \overrightarrow{\leftadj q\rightcat p} ) }  } } & \kern1em & \kern1em & \text{in } V & \kern3em & \kern3em & \text{(JK 2.5)} \\  \red{ k = k_{\rightadj v, \leftadj q, \rightcat ?} } & : & \rightcat{ \hom { (\leftcat v \star q = \leftcat v + q) } {\mathbf P} ? } & \red{\buildrel k \over \cong} & \hom v {\mathbf V} { ( \hom q {\mathbf P} {\rightcat ?} = (\rightcat ? - q) = \overrightarrow{q\rightcat ?} ) } &&& \text{in } V &&& \text{(JK 2.8)}   \\  \red p & \red : & \rightcat{ \hom { \leftadj{ (\leftcat X \tensor Y = \leftcat X + Y) } } {\mathbf V} Z } & \red{\buildrel p \over \cong} & \leftcat{ \hom X {\mathbf V} { \rightadj{  \boxed{ ( \hom {\leftadj Y} {\mathbf V} {\rightcat Z} = [\leftadj Y,\rightcat Z] = (\rightcat Z - \leftadj Y) ) } } } } &&& \text{in } V &&& \text{(JK 2.9)}  \\   \\    \hline   \\       && \hom {v \star {\leftcat q}} P {\rightcat p} & \red\cong & \leftcat{   \hom q P {  \rightadj{ ( | \black v, \rightcat p | = (\rightcat p -\black v) ) }  }  }  &&& \text{in } \cattwo &&& \text{(JK 3.1)}    \\  && \rightcat{ \hom {\black X \tensor \leftcat Y} V  Z } & \red\cong & \leftcat{  \hom Y V { \rightadj{\rightcat Z - \black X} }  } &&& \text{in } \cattwo &&& \text{(JK 3.2)}    \\ & & \hom q {\mathbf P} {(|v, \rightcat p| = v \cotensor \rightcat p = -v + \rightcat p)}  &  \red\cong &  \hom v {\mathbf V} {  ( \hom q {\mathbf P} {\rightcat p}  = (\rightcat p-q) = \overrightarrow{q \rightcat p} )  } &&& \text{in } V &&& \text{(JK 3.7)} \\ \hline \red\kappa & \red : & \rightcat{ \hom { \leftcat T \leftadj A } \calA B }  & \red{ \buildrel \kappa \over \cong } & \hom {\leftcat T} { \leftcat{ [\calA, \calA] } } {   \rightadj{  \boxed{ \langle \leftadj A, \rightcat B \rangle = \hom ? {\black\calA} {\leftadj A} \cotensor \rightcat B}  }   } &&& \text{in } \cattwo &&& \text{(JK 5.1)} \\  \end{array} } \]

\[ \boxed{ \begin{array} {c|c|c} \rightcat P & \leftcat V & \rightcat P \\ \hline \leftadj q & \leftcat{ \xrightarrow [\kern4em] {\textstyle v} } & \leftcat v \leftadj{\hat q} = \leftadj{\leftcat v + q} \\ & \smash{ \leftcat{\Big\Vert} } & \smash{ \rightcat{\Big\Vert} \rlap{ \kern-4em \red{\mathop\Longleftrightarrow\limits_{\textstyle \kappa} } } } \\ & \hom {\leftadj q} {\rightadj{\mathbf P}} {\rightcat p} & \rightcat p \\ \end{array} } \]

\[ \boxed{ \begin{array} {cccccccccccc|ccccc|ccc} &&&& &&&& &&&& && \leftcat V &&&&& \red{ \text{$\kappa$'s} } \rightadj{ \text{ counit } \rightcat p \epsilon }   \\   && \leftcat V \rlap{ \leftcat{ \xrightarrow{\kern9em} } } &&&& \leftcat V \rlap{ \leftcat{ \xrightarrow{\kern9em} } } &&&& \leftcat V & \kern2em & \kern2em && v &&&& \leftadj q & \rightadj{ \xrightarrow [\kern4em] {\textstyle \overrightarrow{\leftadj q \rightcat p}} } & \rightadj{ (\overrightarrow{\leftadj q \rightcat p}) } \leftadj{\hat q} \\ & \leftcat{ \llap v \nearrow } && \leftadj{ \llap{ \hat q} \rightcat\searrow } & \leftadj{ \llap\delta \Vert } & \rightadj{ \nearrow \rlap{ \scriptstyle\kern-2em \overrightarrow{\leftadj q \rightcat ?} } } & \rightadj{\llap\epsilon \Vert} & \leftadj{ \llap{ \hat q} \rightcat\searrow } & \leftadj{ \llap\delta \Vert } & \rightadj{ \nearrow \rlap{ \scriptstyle \overrightarrow{\leftadj q \rightcat ?} } } &&&&& \leftadj{  \Bigg\Downarrow \rlap{ \boxed{\leftcat v (\eta = \delta)} }  } &&&&&& \rightadj{  \Bigg\Downarrow \rlap{ \boxed{\rightcat p \epsilon} }  }   \\   I \rlap{ \rightcat{ \xrightarrow[\textstyle p] {\kern9em} } } &&&& \rightcat{ P \rlap{ \xrightarrow {\kern9em} } } &&&& \rightcat P &&&&& \leftadj q & \rightadj{ \xrightarrow [\textstyle \overrightarrow{ \leftadj q , \leftcat v \leftadj{\hat q} }] {\kern4em} } & \leftadj{ \leftcat v \hat q = \leftcat v + q } & \kern2em & \kern2em &&& \rightcat p \\ &&&& &&&& &&&& && \red{ \text{$\kappa$'s} }  \leftadj{ \text{ unit } \leftcat v (\eta = \delta)} && &&&& \rightcat P  \\ \end{array} } \]

Compare $\red{ \pi_{\leftcat X, \leftadj Y, \rightcat Z} }$ to $\red{ p_{\leftcat X, \leftadj Y, \rightcat Z} }$.
$\red{ \pi_{\leftcat X, \leftadj Y, \rightcat Z} }$ asserts that, for all $\leftcat X, \leftadj Y, \rightcat Z \in V$,
\[ \rightcat{ ( \leftadj{\leftcat X + \leftadj Y} = \rightcat Z ) } \red{\text{ if and only if } } \leftcat{ ( \leftcat X = \rightadj{ \rightcat Z - \leftadj Y} ) } \, . \]
$\red{ p_{\leftcat X, \leftadj Y, \rightcat Z} }$ asserts that, for all $\leftcat X, \leftadj Y, \rightcat Z \in V$,
\[ \rightcat{  \overrightarrow{ \leftadj{\leftcat X +  Y}, \rightcat Z }  } \mathrel{\red=} \leftcat{ \overrightarrow{ \leftcat X,  \rightadj{ \overrightarrow{\leftadj Y, \rightcat Z} }  } } , \quad \text{ i.e., } \quad \rightcat{ Z - \leftadj{(\leftcat X + Y)} } \mathrel{\red=} \leftcat{ \rightadj{(\rightcat Z - \leftadj Y)} - X} \, . \]
Note that 
if we require the outer arrows, i.e. differences, in the $\red{ p_{\leftcat X, \leftadj Y, \rightcat Z} }$ assertion to be the zero vector in $V$, $0\in V$, 
we have a result equivalent to the $\red{ \pi_{\leftcat X, \leftadj Y, \rightcat Z} }$ assertion.
Thus, using Kelly's concepts and notation, $\boxed{{\mathbf V}_0 \cong V}$ (ECT 1.25).

And similarly for $\red{ \kappa = \kappa_{\rightadj v, \leftadj q, \rightcat p} }$ and $\red{ k = k_{\rightadj v, \leftadj q, \rightcat p} }$ in the external action case.
Thus, for $\rightcat P$, we have
\[ \boxed{ \begin{array} {} \theta & : & \rightcat{ \hom {\leftadj q} P {\rightcat p} } & \cong & \rightcat{ \hom { \leftadj{\leftcat 0+q} } P p } & \mathrel{ \red{\buildrel \kappa \over \cong} } & \leftcat{ \hom 0 V { \rightadj{ \hom {\leftadj q} {\mathbf P} {\rightcat p} } } } & \equiv & \hom {\leftadj q} {({\mathbf P}_0)} {\rightcat p} & \kern6em & \text{(ECT 1.25, JK 2.4)} \\ && \rightcat{ \leftadj q = \rightcat p } & \Leftrightarrow & \rightcat{ \leftcat 0 + \leftadj q = \rightcat p } & \red{ \buildrel \kappa \over \Leftrightarrow } & \leftcat{ 0 = \rightadj{(\rightcat p - \leftadj q) \equiv \overrightarrow{\leftadj q,\rightcat p} } } \\ \end{array} } \]

 Concerning (JK 2.8), a modification, to fit the $V,P$ situation, of what Janelidze and Kelly write is:

<blockquote>"The existence of the $V$-enriched representation (2.8) ... \[\hom { (v \star q = v+q) } {\mathbf P} ? \buildrel k \over \cong \hom v {\mathbf V} { ( \hom q {\mathbf P} ? = (?-q) = \overrightarrow{q?} ) }\] is expressed by saying that the $V$-category $\mathbf P$ is <em>tensored</em>, with $(v \star q = v+q)$ as the <em>tensor product</em> of $v$ and $q$."</blockquote>.

<hr />

<hr />
Compare Kelly's notations for monoidal categories:

\[ \boxed{ \begin{array} {l|cclc} \text{EK (1966) $\S$ II.1 and ECT (1982) $\S$ 1.1} & \calV & = & (\calV_0, \tensor, I, a, l, r) \\ \text{JK (2001) $\S$ 1} & \calV & = & (\calV, \tensor, I) \\ \end{array} } \]
Note the $\calV$-$\calV_0$ distinction is no longer being made at this level, 
i.e. we use the same symbol to denote both a monoidal category and its underlying mere (ordinary) category.

<hr />

\[ {\mathcal V}_0 (Y,Z) \cong {\mathcal V}_0 (I, [Y,Z]) \equiv V([Y,Z]) \tag*{ECT (1.25)} \]