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)} \]

Tuesday, November 16, 2021

Dimensional analysis as change of base

This is a preliminary draft!

An important topic in linear algebra is "change of basis", i.e., what happens to the representation of individual vectors, and of linear transformations, when bases of vector spaces are changed.
See, for example, Chapter VII, Section 7 of <I>Algebra, Third Edition</I> by Mac Lane and Birkhoff.
The machinery developed there applies to finite-dimensional vector spaces.
We can best understand that machinery by first considering the one-dimensional case.
In that case, the machinery is directly applicable to the elementary topic of "dimensional analysis":
https://en.wikipedia.org/wiki/Dimensional_analysis

Let us illustrate 'dimensional analysis" with an example.
Start with an approximation:
\[  \boxed{    \begin{array} {ccl|l}  \source{ (1 \text{ inch}) } & = & \target{ (2.54 \text{ cm}) }  &  \text{the familiar statement of the approximation}   \\   & = & \target{  \black{2.54} \times (1 \text{ cm}) }  &  \text{factoring out the conversion factor}   \\   \source b & = & \target{ \black P \times  c } = \target{ \black P \hat  c } &  \text{abstracting}  \\   & = & \target{ (\source b \target y) \times c } = (\source b \target y) \target{\hat c} = \source b \target{(y \hat c)} = \source b  & \text{see below for an explanation}  \\  \end{array}    } \]                 \[ \begin{array} {} &&& {} \rlap{ \kern-3em \target{ \text{(centimeters)} } } \\ &&& \target\R \\ &&& \target{ \llap{ \hat c = \text{centimeters} } \Bigg \downarrow } & \searrow \rlap{ P\inv = \text{($\target{\text{centimeters}}$ to $\source{\text{inches}}$) conversion} } \\ \source{ \text{(inches)} } & \source\R & \source{ \xrightarrow [\kern6em] { \textstyle \hat b = \text{inches} } } & V & \source{ \xrightarrow [ {} \rlap{ \kern-3em \textstyle x = (\hat b)\inv = \hom b V - = \langle b,- \rangle = \text{inches} } ] {\kern6em} } & \source\R & \source{ \text{(inches)} } \\ && \llap{ P = \text{($\source{\text{inches}}$ to $\target{\text{centimeters}}$) conversion} } \searrow & \target{ \Bigg \downarrow \rlap{ y = (\hat c)\inv = \hom c V - = \langle c,- \rangle = \text{centimeters} } } \\ &&& \target\R \\ &&& {} \rlap{\kern-3em \target{ \text{(centimeters)} } } \\ \end{array} \]

The method of dimensional analysis uses this equality to convert $\source{\text{measurements in inches}}$ to $\target{\text{measurements in centimeters}}$, e.g.
\[ \boxed{  \source{ 5 \text{ inches} } \times { \target{ 2.54 \text{ cm} } \over \source{ 1 \text{ inch} } } = \source 5 \times \target{ 2.54 \text{ cm} }  } . \]

We now make a prolonged segue into mathematics, eventually to see how the above can be viewed as a special case of some general mathematical considerations.
So let us now move into the realms of geometry and algebra. 

First, in geometry, we might consider a line $L$, extending infinitely in both directions, with points $P,Q$ etc.
We might assign (a base point, call it $0$, on the line), and wish to measure off distances along the line. But what units to use? The choice is up in the air.

Next, in algebra, more specifically linear algebra, 
we may view the line as a 1-dimensional real vector space, consisting of vectors $v,w$ etc.
Being a vector space means that certain operations are defined on its elements (vectors):
A nullary operation, $0$, selecting the origin of the vector space,
addition of vectors, yielding $v+w$, 
and scalar multiplication by reals, yielding $v \xi$ (we here, following Mac Lane and Birkhoff, use Greek letters to denote scalars).
All of these may be defined geometrically, given a bijection between (the line $L$) and (the 1-dimensional real vector space $V$).

Note that while reals (scalars) can <I>act</I> on $V$: $\langle v,\xi \rangle \mapsto v\xi$, 
we do not yet have a <i>bijection</i> between the 1-dimensional real vector spaces $V$ and $\R$, the vector space of the scalars themselves.
I.e., we have no sense of scale within $V$.
We get that by $\source{ \text{choosing one non-zero vector } \boxed{b} \text{ in $V$ to be the <i>unit vector</i> or <I>base</I>.} }$
Given (the vector $\source b$), we have a function denoted $\source{ \boxed{ \hat b } }$:
\[ \source{  \boxed{ \hat b : \R \to V : \xi \mapsto b\xi }  } , \]
taking (a scalar $\xi$) (which we may regard as a coordinate relative to the unit, or base, vector $\source b$) to (the vector $\source b \xi$).

Since ($\source b$ is a non-zero vector in a 1-dimensional vector space), (the function $\source{ \hat b }$) is in fact a bijection.
We denote the  inverse to $\source{ \hat b }$ by $\source{ \boxed{x} }$, so $\source{ x = (\hat b)\inv }$. Thus 
\[ \source{ \boxed{ x = (\hat b)\inv : V \to \R } } ; \]
it takes a ($v\in V$) to (the unique $\source{x}(v) = \xi \in\R$ such that $v = \source b \xi = \source b \source x (v) = \source{\hat b x}(v) $), 
which we naturally regard as (the coordinate of $v$) relative to (the base vector $\source b$).

Since $\source{\hat b}$ and $\source x$ are inverse to each other, we have $\source{\hat b x = 1_\R}$ and $\source{x \hat b} = 1_V$ (note the order of composition being used).


<hr />

Some diagrams for future use:

For an explanation of the following diagram, see Thm. 11 in M-B VI.4
\[ \begin{array} {} 1 \\ &&&& \searrow \rlap {v \in V} \\ & \llap{ n\op \backslash F \ni \mathbf\xi} \searrow & n \rlap{ \xrightarrow [\kern 11em] {\kern 1em \textstyle \mathbf b} } &&&& V \\ &&& \llap{ \hom - n - \lambda } \searrow  && \llap{ \mathbf\mu } \searrow && \searrow \rlap{ f \in V^\star } \\ &&&& n\op \backslash F \rlap{ \kern.5em \xrightarrow [\textstyle \mathbf\mu \star -] {\kern 8em} } &&&& F \\ \end{array} \]
The short (1-2) diagonal (not shown) in the diagram is $\mathbf b \star -$), i.e. the extension of $\mathbf b$ over $\hom - n - \lambda$.

A special case of the the change of base diagram.
Here we consider a line,
with a given origin or base point, 
as a one dimensional vector space,
and consider how it may be measured in either inches or centimeters.
\[  \begin{array} {}   {} \rlap{ \source { m=1 } } &&&&&&& {} \rlap{  \target{ n=1} }  \\ & \source{ \llap{\mathbf b} \searrow \rlap{\text{inch}} } &&&&&&& \kern-2em \target{ \llap{\mathbf c}  \searrow \rlap{\text{centimeter}} }  \\ && \source{  V \rlap{ \kern.5em \xrightarrow {\kern9em} }  } &&&& \source V & \kern-.5em \xrightarrow{\kern6em} & \target{  V \rlap{ \kern.5em \xrightarrow {\kern9em} }  } &&&& \target V  \\ &&& \source{  \llap{ \mathbf x = \hom {\mathbf b} V - } \searrow  }  & \source \Vert &\source{  \nearrow \rlap{ \mathbf b \star - }  }  &&&& \target{  \llap{ \mathbf y = \hom {\mathbf c} V -} \searrow  }  & \target\Vert & \target{  \nearrow \rlap{ \mathbf c \star - }  }  \\  &&&& \source{ m\calP } \rlap{ \kern.5em \xrightarrow [ \textstyle (P =  \hom {\target{\mathbf c}} {\target V} {\source{\mathbf b}} ) \star {\source -} ] {\kern18em} } &&&&&& \target{n\calP} \\ \end{array} \]

Several of these arrows represent mappings which have significant verbal descriptions.
The diagonal arrows, taking them from left to right, may be described verbally as:

Selecting the point corresponding to one inch ; selecting a unit (an inch).
The coordinate (in inches) of a point ; converting points to numbers (of inches); this is the act of <I>measurement</I>, in inches.
The point determined by a specific number of inches ; converting numbers (of inches) to points.

The next (and last) three diagonal arrows do the same for centimeters.


\[ \begin{array} {} \source n &&&&&&& {} \rlap{ \target n } \\ & \source{ \llap{\mathbf b} \searrow } &&&&&&& \kern-2em \target{ \searrow \rlap{\mathbf c} } \\ && \source{ V \rlap{ \kern.5em \xrightarrow {\kern9em} } } &&&& \source V & \kern-.5em \xrightarrow{\kern6em} & \target{ V \rlap{ \kern.5em \xrightarrow {\kern9em} } } &&&& \target V \\ &&& \source{ \llap{ \mathbf x = \hom {\mathbf b} V - } \searrow } & \source \Vert &\source{ \nearrow \rlap{ \mathbf b \star - } } &&&& \target{ \llap{ \mathbf y = \hom {\mathbf c} V -} \searrow } & \target\Vert & \target{ \nearrow \rlap{ \mathbf c \star - } } \\ &&&& \source{ n\calP } \rlap{ \kern.5em \xrightarrow [ \textstyle (P = \hom {\target{\mathbf c}} {\target V} {\source{\mathbf b}} ) \star {\source -} ] {\kern18em} } &&&&&& \target{n\calP} \\ \end{array} \]

The change of base diagram, modified in two ways. 
First, for a linear transformation $t$ from a $m$-dimensional vector space $V$ to an $n$-dimensional vector space $W$.
Second, specializing to one dimensional vector spaces (so $\source{m=1}$ and $\target{n=1}$), 
and assuming the bases for the two vector spaces are, respectively, 
points at a distance of one inch and one centimeter from the origin.
\[  \begin{array} {} {} \rlap{ \source { m=1 } } &&&&&&& {} \rlap{  \target{ n=1} }  \\ & \source{ \llap{\mathbf b} \searrow \rlap{\text{inch}} } &&&&&&& \kern-2em \target{ \llap{\mathbf c}  \searrow \rlap{\text{centimeter}} } \\ && \source{  V \rlap{ \kern.5em \xrightarrow {\kern9em} }  } &&&& \source V & \kern-.5em \xrightarrow[\kern8em] {\textstyle t} & \target{  W \rlap{ \kern.5em \xrightarrow {\kern9em} }  } &&&& \target W  \\ &&& \source{  \llap{ \mathbf x = \hom {\mathbf b} V - } \searrow  }  & \source \Vert &\source{  \nearrow \rlap{ \mathbf b \star - }  }  &&&& \target{  \llap{ \mathbf y = \hom {\mathbf c} W -} \searrow  }  & \target\Vert & \target{  \nearrow \rlap{ \mathbf c \star - }  }  \\ &&&& \source{ m\calP } \rlap{ \kern.5em \xrightarrow [ \textstyle (P =  \hom {\target{\mathbf c}} {\target W} {\source{\mathbf b}t} ) \star {\source -} ] {\kern20em} } &&&&&& \target{n\calP} \\ \end{array} \]

----------------

THIS IS DRAFT FOR A RATHER DIFFERENT SUBJECT 
(Mac Lane-Birkhoff affine spaces a la Janelidze-Kelly).

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

<hr />

\[ \kappa : \hom {v+q} {P} p \buildrel \kappa \over \cong \hom v {V} { ( \hom q {\mathbf P} p = (p-q) ) } \tag{MB 5, JK 2.1} \]

Friday, September 24, 2021

The categorical comprehension schema

One ingredient in (the categorical comprehension situation), as considered by Lawvere, Street, Walters, et al is (the factorization of functors) in (  (a categorical version) of ( (the classic epi-mono factorization of functions) in (the category of sets) )  ).
That factorization, in $\Set$, uses the notion of image, which in turn uses the logical notion of existence: $(f : X \to Y) \, \leftadj{ \text{Image} } = \{ y\in Y | (\leftadj\exists x\in X)(xf=y) \}$.
Note how comprehension is used in the above definition.

A version of this can be produced in an arbitrary category, using certain standard categorical notions.
(When applied to $\Set$, one does not recover the subset of $Y$ defined above.)
The diagram below, an expansion of 
(the general categorical definition in Theorem 3 of [Street-Walters 1973]), 
shows how this is done.
Here $f : A \to B$ is in general a functor between categories.
But the best introduction to this result is to take $A$ and $B$ to be discrete, i.e. essentially just sets, and $f$ merely a set-theoretic function between them, 
then to interpret the various constructs in that simple situation, i.e. in $\Set$.
Note (the result) 
is NOT even isomorphic to 
(the standard epic-monic factorization of $f$).

\[ \boxed{ \begin{array} {}    & {} \rlap{  \kern-2em \rightadj{ \text{left fiber} }  }   \\   &  \rightadj{ \llap{(2) \;} \boxed{(\black f \downarrow \black b)} }   &   \rightadj{ \xrightarrow [\smash{}] {\textstyle a} }  & A \rlap{ \kern.5em \xrightarrow [\smash{\kern13.5em}] {\textstyle !_A} } &&&& \calI \rlap{ \kern0em \xrightarrow [\smash{\kern6em}] {\textstyle \ulcorner 1 \urcorner} } && & \Set   \\   &&&& \leftcat{ \searrow \rlap{\kern-.1em e \; (5)} }  && \rightadj\nearrow \\    &   \smash{   \rightadj{\llap ! \Bigg\downarrow} } & \smash{ \rightadj{ \llap\beta \Bigg\Downarrow} } & \smash{    \llap f \Bigg\downarrow \rlap{   \kern0em \scriptstyle \red{  { \calE-\calM \atop \text{factorization} }  }  }   }   &&  \rightadj{ \boxed{(\black 1 \downarrow \leftadj k) \; (4)} } \rlap{    \kern0em \smash{   \leftadj{  \Bigg\Downarrow { \text{for the $\Lan$} \atop \textstyle \leftadj{\iota \; (3)} }  }   }    } &&& \smash{ \rightadj{ \Bigg\Downarrow \rlap{ \kern-.25em { \text{for the} \atop \text{comma cat} } } } } & & \smash{\Bigg\Vert}     \\   &&&& \rightadj{ \swarrow \rlap{\kern-.1em p} }   \\     &   \calI & \xrightarrow [\textstyle b \; (1)] {\smash{\kern3em}}  &   B \rlap{    \kern.5em \leftadj{   \xrightarrow [ \textstyle \boxed{ \textstyle \black{(!_A \ulcorner 1 \urcorner)} \Lan_{\black f} = k } \; (3) \; \text{(fiber colimit)} ] {\smash{\kern21em}}  }   } &&&&&& \kern1em & \Set    \\     \kern1em   &&&&  {} \rlap{  \kern-1em B\text{-indexed} \leftadj{ \text{ family of left-fiber colimits} }  } \\    \end{array} } \]

<hr />
-----------
An instructive, very concrete, example of this situation is:

\[ \boxed{ \begin{array} {} & {} \rlap{  \kern-4em \rightadj{ \text{left fiber (pullback)} }  } \\ \text{e.g.:} & \rightadj{  \text{Mike}[\text{Mike}g=\text{M}]  }  & \mapsto & \text{Mike} && \mapsto && \star & \mapsto && 1       \\      & \rightadj{   \llap{(2) \;} \boxed{  \begin{array} {} (\black g \downarrow \black{ \text{M} })  \\  \text{Mike}[\text{Mike}g=\text{M}], \text{etc.}  \\  \end{array}  }    } & \rightadj{   \xrightarrow [\smash{}] { \textstyle \text{names}_{ \black{\text{M}} }  }   } & \boxed{ \begin{array} {}  \text{Names}   \\  \text{Mike, Marty, Mo, Fran, Flo} \\  \end{array} }  \rlap{   \kern.5em \xrightarrow [\smash{\kern24em}] {  \textstyle !_{ \text{Names} }  }   } &&&& \calI \rlap{ \kern0em \xrightarrow [\smash{\kern6em}] {\textstyle \ulcorner 1 \urcorner} } && & \Set     \\     &&&& \leftcat{ \searrow \rlap{\kern-.1em e \; (5)} } && \rightadj\nearrow     \\        & \smash{ \rightadj{\llap ! \Bigg\downarrow} } & \smash{ \rightadj{\Bigg\Downarrow} } & \smash{ \llap g \Bigg\downarrow \rlap{ \kern1em \red{ { \calE-\calM \atop \text{factorization} } } } } && \rightadj{   \boxed{  \begin{array}{} (\black 1 \downarrow \leftadj k) \; (4) \\  \text{M}[0], \text{M}[1], \text{M}[2], \text{F}[0], \text{F}[1] \\  \end{array} }   } \rlap{    \kern0em \smash{   \leftadj{  \Bigg\Downarrow { \text{for the $\Lan$} \atop \textstyle \leftadj{\iota \; (3)} }  }   }    } &&& \smash{ \rightadj{ \Bigg\Downarrow \rlap{ \kern-.25em { \text{for the} \atop \text{comma cat} } } } } & & \smash{\Bigg\Vert}        \\    &&&& \rightadj{ \swarrow \rlap{\kern-.2em p} }     \\    & \calI \rlap{   \xrightarrow [\textstyle \text{M} \; (1)] { \smash{\kern20em} }   }  && \boxed{ \begin{array} {}  \text{Genders}   \\  \text{M, F, N} \\    \end{array} }  \rlap{ \kern.5em \leftadj{ \xrightarrow [ \textstyle \boxed{ \textstyle \black{(!_{\text{Names}} \ulcorner 1 \urcorner)} \Lan_{\black g} = k } \; (3) \; \text{(fiber colimit)} ] {\smash{\kern37em}} } } &&&&&& \kern1em & \Set   \\    &&& {} \rlap{  \leftadj{ \kern0em \black{\text{M}}k = \black 1 + \black 1 + \black 1 = 3 = \{0,1,2\} ; \;  \black{\text{F}}k = \black 1 + \black 1 = 2 = \{0,1\} ;  \; \black{\text{N}}k = \leftadj\emptyset } .}     \\     \kern1em &&&& {} \rlap{ \kern-5em \text{Genders-indexed} \leftadj{ \text{ family of left-fiber colimits} } } \\ \end{array} } \]

The national transformation $\leftadj\iota$ of the $\leftadj\Lan$ deserve a closer look.
The key point is that 
it is (the natural transformation $\leftadj\iota$) that links 
each (individual name) with 
( a specific element of (the sets that are colimits) that form (the image of the $\leftadj\Lan$ in $\Set$) ).

\[  \boxed{    \begin{array} {ccccccccc|cc} \kern1em & \rightadj{   \llap{(2) \;} \boxed{  \begin{array} {} (\black g \downarrow \black{ \text{M} })  \\  \text{Mike}[\text{Mike}g=\text{M}], \text{etc.}  \\  \end{array}  }    } & \rightadj{   \xrightarrow [\smash{}] { \textstyle \text{names}_{ \black{\text{M}} }  }   }  & \boxed{ \begin{array} {}  \text{Names}   \\  \text{Mike, Marty, Mo, Fran, Flo} \\  \end{array} }  \rlap{   \kern.5em \xrightarrow [\smash{\kern6em}] {  \textstyle !_{ \text{Names} }  }   } && \calI \rlap{ \kern0em \xrightarrow [\smash{\kern8em}] {\textstyle \ulcorner 1 \urcorner} } && & \Set   & 1  &  \kern3em  \\    &  & \smash{ \rightadj{\llap ! \searrow} } & \smash{ \rightadj{\bigg\Downarrow} } &   \llap g \searrow   & \smash{ \leftadj{\bigg\Downarrow \rlap\iota} }  &  \leftadj{  \nearrow \rlap{ \boxed{ \textstyle \black{(!_{\text{Names}} \ulcorner 1 \urcorner)} \Lan_{\black g} = k } \; (3) \; \text{(fiber colimit)} }  }   &&& \smash{   \leftadj{\Bigg\downarrow} \rlap{  \raise3ex { \leftadj\iota _{\text{Mike}} }  }   } \\  & && \calI \rlap{   \xrightarrow [\textstyle \text{M} \; (1)] { \smash{\kern12em} }   }  &&  \boxed{ \begin{array} {}  \text{Genders}   \\  \text{M, F, N} \\  \end{array} }  &&&&  \leftadj{ \black{\text{Mike}g}k = \black{\text{M}} k = 3 }  \\   \end{array}   }  \]

Using the notation and setup of the above, we then have

\[ { \black{\text{Mike}} }e  =  (\black{\text{Mike}}g = \text{M}) \big[ \leftadj{  \iota_{\black{\text{Mike}}} : \black 1 \to  \black{ (\text{Mike}g) } k = \black{\text{M}} k = 3  }  \big]   \]

<hr />
Very preliminary draft!! (A work in progress) :

Categorical Comprehension Schema:

Street-Walters:

The general case in Street-Walters requires the following:
Here 
(${\bf T}$ is a (possibly large) category, of "types" or "contexts"),
($P : {\bf T}\op \to \Cat$ is a functor, a "hyperdoctrine"), and
($X\in {\bf T}$ is a "type" or "context").

\[  \boxed{  \begin{array} {} \leftcat{ ({\bf T}\downarrow X) } & \mathop\rightleftarrows\limits^{\leftadj\Omega}_{\rightadj\Theta} & \rightcat{ XP } & \rightcat{=} & \rightcat{  (\calM \downarrow X) } & \rightcat{\approx} & \rightcat{ \hom X {\bf T} \Omega }   \\    \end{array}   } \]

Examples: 

\[ \boxed{ \begin{array} {ccc|ccccccc}     {\bf T} & \ni & \Omega &   \leftcat{ ({\bf T}\downarrow X) } & \mathop\rightleftarrows\limits^{\leftadj\Omega}_{\rightadj\Theta} & \rightcat{ XP } & \rightcat{=} & \rightcat{ (\calM \downarrow X) } & \rightcat{\approx} & \rightcat{ \hom X {\bf T} \Omega } \\ &&&&&   \rightcat{ \text{attributes} }   \\   \hline \Set & \ni & 2 &  \leftcat{ (\Set\downarrow X) } & \mathop\rightleftarrows\limits^{\leftadj\Omega}_{\rightadj\Theta} & \rightcat{ XP } & \rightcat{=} & \rightcat{ ( \text{(monics)} \downarrow X) } & \rightcat{\approx} & \rightcat{ \hom X \Set 2} & \rightcat{=} & \rightcat{ [X,2] }   \\  &&&  \leftcat{ \text{oversets} } && \rightcat{ \text{attributes} } &&  \rightcat{ \text{monics} } && {} \rlap{ \rightcat{ \kern2em \text{predicates} } }     \\      \hline  \Set  &  & \Set  &  \leftcat{ (\Set \downarrow X) } & \mathop\rightleftarrows\limits^{\leftadj\Omega}_{\rightadj\Theta} & \rightcat{ XP } & \rightcat{=} & \rightcat{ (\text{(dofs)} \downarrow X) } & \rightcat{\approx} & \rightcat{ \hom X \SET \Set} & \rightcat{=} & \rightcat{ [X,\Set] }   \\  &&&  \leftcat{ \text{oversets} } && \rightcat{ \text{attributes} } && {} \rlap{ \kern-4em \rightcat{ \text{} } } &&  {} \rlap{ \rightcat{ \kern2em \text{indexed families} } }       \\        \hline  \CAT  & \ni & \Set  &  \leftcat{ (\CAT \downarrow X) } & \mathop\rightleftarrows\limits^{\leftadj\Omega}_{\rightadj\Theta} & \rightcat{ XP } & \rightcat{=} & \rightcat{ ( \text{(dofs) } \downarrow X) } & \rightcat{\approx} & \rightcat{ \hom X \CAT \Set} & \rightcat{=} & \rightcat{ [X,\Set] }   \\  &&&  \leftcat{ \text{overcategories} } && \rightcat{ \text{attributes} } && {} \rlap{ \kern-4em \rightcat{ \text{discrete op-fibrations (dofs)} } } && {} \rlap{ \rightcat{ \kern2em \text{indexed families} } } \\ \end{array} } \]

References:

https://ncatlab.org/nlab/show/hyperdoctrine
https://ncatlab.org/nlab/show/axiom+of+separation

\boxed{ \begin{array} {} \text{ } \\ \text{ } \\ \end{array} } 

\[ 3 = 1+1+1 = {0} + {0} + {0} = {0,1,2} = [2] \]

Sunday, July 25, 2021

Kan extensions

Draft of just one, but key, diagram concerning the pointwise right Kan extension at (one object $\leftcat{ \boxed{1} \;  l\in\calL}$).


\[ \leftcat{      \boxed{     \begin{array} {}    &&  \calI & \xrightarrow[\smash{\kern4em}]{\textstyle \boxed{1} \; l}  &  \calL  \\ &&  \rightadj{  \llap{ \boxed{11} \; ! } {\Bigg\uparrow}  }  &  \leftcat{  \llap{ \boxed{11} \; \lambda }   {\Bigg\Downarrow} }   &  \rightadj{  \llap{ \boxed{0} R } {\Bigg\uparrow}   }  &  \kern2em \llap{  \llap{ \rightcat{\boxed{31} \, \alpha} \kern-.2em } \Downarrow \kern1em  }  \leftcat{  \searrow \rlap {S \; \boxed{30} }  }     \\    \leftcat\calI  &  \xrightarrow[  \smash{ \textstyle \leftcat{\boxed{12}} \; \rightcat r \leftcat{[\lambda]} }  ]{  \smash{ \textstyle \text{right lax fiber} }  }  &  \leftcat{     ( l \downarrow {\rightadj R} ) \smash{    \rlap{  \lower2.7ex{   \kern-2.1em \boxed{10}  }  }   }    }  &    \rightcat{   \xrightarrow[ \smash{\textstyle \boxed{11}  \; Q=r}  ]{}   }    &  \rightcat\calR  &  \xrightarrow[  \smash{ \textstyle \boxed{0} \;  G \; (\text{e.g., }\rightadj R) }  ]{\kern8em}  &  \calC       \\   \leftcat\Vert  &&&&  \rightcat\Vert  \\  \leftcat\calI \rlap{ \xrightarrow[ \textstyle \rightcat r ]{\kern24em} }  &&&&  \rightcat\calR    \\ \end{array}     }      } \]

Given the initial data, the span $\Big( \rightadj{  \boxed{0} \; R  : {\leftcat\calL} \leftarrow {} } {\rightcat\calR}  \to \calC :  { G \; \boxed{0} } \Big) $, 
we wish to form 
(the right Kan extension $\rightadj{ \boxed{20} \; { \Ran_R {\black G} } : {\leftcat\calL} \to {\black\calC} }$) 
of $G$ over $\rightadj R$.
We do this "pointwise".
Given (an object $\leftcat{ \boxed{1} \;  l\in\calL }$),
form (its right lax fiber $\leftcat{  \boxed{10} \; ( l \downarrow {\rightadj R} )   }$) as shown in the diagram above.
Then form 
(the limit ${\rightadj{  \boxed{20} \; \rightcat{\big( (Q=r) \black G\big)} \lim_{\black\calC}  }}$ in $\calC$), 
an arrow running from the top left in the above diagram southeast to the somewhat lower right,
together with 
(its universal cone $\rightadj{ \boxed{21} \; \pi : \rightcat{\big( (Q=r) \black G\big)}   {\rightadj\lim}_{\black\calC} \Rightarrow \rightcat{(Q=r) \black G}  } $), 
a 2-cell just below the just-mentioned arrow.


\[ \leftcat{ \boxed{ \begin{array} {} && \calI & \xrightarrow[\smash{\kern4em}]{\textstyle \boxed{1} \; l} & \calL \\ && \rightadj{ \llap{ \boxed{11} \; ! } {\Bigg\uparrow} } & \leftcat{ \llap{ \boxed{11} \; \lambda } {\Bigg\Downarrow} } & \rightadj{ \llap{ \boxed{0} R } {\Bigg\uparrow} } & \kern2em \rightadj{     \llap{  \llap{ \boxed{31} \, 1_R  \kern-.3em  } \Downarrow \kern1em  }   }  \leftcat{ \searrow \rlap {1_\calL \; \boxed{30} } } \\ \leftcat\calI & \xrightarrow[ \smash{ \textstyle \leftcat{\boxed{12}} \; \rightcat r \leftcat{[\lambda]} } ]{ \smash{ \textstyle \text{right lax fiber} } } & \leftcat{ ( l \downarrow {\rightadj R} ) \smash{ \rlap{ \lower2.7ex{ \kern-2.1em \boxed{10} } } } } & \rightcat{ \xrightarrow[ \smash{\textstyle \boxed{11} \; Q=r} ]{} } & \rightcat\calR &   \rightadj{    \xrightarrow[ \smash{ \textstyle R \; \boxed{0} } ]{\kern8em}    }   & \calL \\ \leftcat\Vert &&&& \rightcat\Vert \\ \leftcat\calI \rlap{ \xrightarrow[ \textstyle \rightcat r ]{\kern24em} } &&&& \rightcat\calR \\ \end{array} } } \]

Tuesday, July 20, 2021

Algebraic set theory versus ETCS

Very much a preliminary draft, with errors!

This is a first cut at lining up and comparing various set theories and their models.

\[  \boxed{  \begin{array} {l|c|c|ccc}   \text{reference}  &  \text{Awodey}  &  \text{Leinster}  &  \text{SGL VI.10}    \\   \hline    \text{theories}  &  \text{BIST: Basic Intuitionistic Set Theory}  & \text{ETCS: Elementary Theory of the Category of Sets}   &  \text{RZC}  \\   \hline    \text{models}   &  \text{categories of classes}  &  &  \text{WPTNNC}   \\    \end{array}    }    \]

Awodey-Butz-Simpson-Streicher 2014 BIST APAL
https://www.sciencedirect.com/science/article/pii/S0168007213000730

Saturday, July 17, 2021

Spaces, frames, locales

Here are some of the key concepts from Mac Lane and Moerdijk's SGL related to the above.

$\mathbf{(Spaces)}$ (arrows go in geometric direction), 
$\mathbf{(Frames)}$ (arrows go in algebraic direction), 
$\mathbf{(Locales)} = {\mathbf{(Frames)}}\op$ (arrows go in geometric direction),

Quoting Mac Lane-Moerdijk, Section IX.1,

For a map $f : S \to T$ of spaces, the locale-map $\Loc(f) : \Loc(S) \to \Loc(T)$ is given by the frame morphism $f\inv : \calO(T) \to \calO(S)$, 
i.e.
$ \Big(f :S \to T\Big) \in \mathbf{(Spaces)} \xrightarrow{\textstyle \Loc} \mathbf{(Locales)} \ni \Big( \Loc(f) : \Loc(S) \to \Loc(T) \Big) = \Big( { \big( f\inv: \mathcal{O}(T) \to \calO(S) \big) }\op \Big) \in { \mathbf{(Frames)} }\op $.

Thursday, June 24, 2021

Draft : Comma category notation

First note that, for all $x,y$,  either $x\lt y$ or $y\lt x$ since $h(x,y)$ has to be one of $x,y$.

Suppose $x,y,z$ are distinct elements such that $x\lt y$, $y\lt z$, and $z\lt x$. This last is equivalent to $h(x,z) = z$.  
We write $h(x,z) =??? z$ to indicate this hypothesis is in question.

Then, using the assumption that $h$ is a consistent choice function, we have

\[ \begin{array} {}  x & = & h(x,y) & = & h\big( h(x,y),h(y,z) \big)  \\  &&&& \Vert  \\  &&&&  h(x,y,z)  \\   &&&& \Vert  \\  y & = & h(y,z) & =??? & h\big( h(y),h(x,z) \big)  \\  \end{array} \]

contradicting $x,y$ are distinct.




\[ \leftcat{  \boxed{   \begin{array} {cc|ccccc l|ccccccccc}    \calJ \rlap{\kern.5em \xrightarrow[\kern15em]{\textstyle G} }  &&&  &&  \leftcat{(l\downarrow \calL)}  {} \rlap{  \kern.5em \rightcat{ \xrightarrow[\kern39em]{\textstyle Q = r} }  }   &&&  && &&&  \calL   &&        \\                    \hline     &&&     &&   \llap{\boxed{1}\;} G  &&& \kern1em  & \kern1em   &  \boxed{2}  & G\rightcat Q &&     \\  &&&     &&    &  \rightadj{\nwarrow \rlap\pi}  & \rightadj{\boxed{5}}  &&   & \llap{G\lambda} \nearrow & \smash{ \lower1ex{ \boxed{43=2} } }  &  \rightadj{ \nwarrow \rlap\pi }  & \rightadj{\boxed{3}}     \\     &&&     &&   &&  \rightadj{\big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)}[\overline{G\lambda}]    &&   \leftcat{\llap{\boxed{0}\kern1em}  l} & {} \rlap{\kern-1em \xrightarrow[\textstyle \exists!\overline{G\lambda} \; \boxed{4}]{\kern12em} }  &&&  \rightadj{(\black G\rightcat Q)\lim_{\leftcat\calL}}   \\  &&&    &&   {} \rlap{ \kern3em \text{a single cone} }   &&&& {} \rlap{\kern0em \text{mediating arrow, a morphism of cones} } &&&&   \\                   \hline    &&&    \forall \; \boxed{6} \; k[\kappa]  &  {} \rlap{ \kern-1em \xrightarrow[\kern17em]{\textstyle \forall \mu \; \boxed{7}}  }  &&&  \black G  \rlap{\; \boxed{1}}    \kern1em  &  \kern1em  &  & \boxed{6\rightcat Q} &  k & {} \rlap{ \kern-1em \xrightarrow [\kern12em] {\textstyle \mu\rightcat Q =  \mu \; \boxed{7}} } &&& \black G\rightcat Q  & \boxed{2}      \\  &&&    &    \llap{ \exists! \; \boxed{8'} \; \bar\mu} \searrow  && \rightadj{ \nearrow \rlap{\pi} }   &     &     && \llap{\kappa} \nearrow && \llap{\black G\lambda} \nearrow \rlap{\boxed{2}} && \rightadj{ \nearrow \rlap{\pi} } &   \\   &&&   &&  \rightadj{ \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big) } [\overline{\black G\lambda}]     & \rightadj{\boxed{5}}  &   &&   \llap{\boxed{0}\kern1em}  l & {} \rlap{ \kern-1em \xrightarrow [\textstyle \exists!\overline{\black G\lambda} \; \boxed{4}] {\smash{\kern12em}} } &&& \rightadj{(\black G\rightcat Q)\lim_{\leftcat\calL}}  &  \rightadj{\boxed{3}}  &   \\   \end{array}  }   } \]





\[ \leftcat{ \boxed{ \begin{array} {c|cc|c|cccc|c|cccccc}             \calJ \rlap{ \xrightarrow[\kern12em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} } }  & \boxed{ (l\downarrow {\rightadj R}) } \rlap{ \rightcat{ \kern.5em \xrightarrow[ \textstyle \kern4.5em \text{faithful} \kern4.5em ]{\textstyle Q=r} } } & & \rightcat\calR \rlap{ \rightadj{ \kern.5em \xrightarrow[\kern7em]{\textstyle R} } } & & \calL &&  \kern2em &&&&  \CAT   \\       \hline j & X = j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda] = \rightcat r [\kappa] && \kern2em j\black G\rightcat Q = \rightcat r \kern1em &&& j\black G\rightcat Q\rightadj R = \rightcat r \rightadj R      \\        & &&&& \llap{j \black G \lambda = \kappa} \nearrow &   \\       \llap\iota \Bigg\downarrow & \llap{\iota \black G = {}} \Bigg\downarrow \rlap{ {} = \iota \black G \rightcat Q = \rightcat\rho } && \llap{ \iota \black G \rightcat Q \; } \Bigg\downarrow \rlap{ {} = \rightcat\rho} &  \kern1em l &  {} \rlap{\kern0em \iota \black G = \rightcat\rho}  &  \Bigg\downarrow \rlap{\iota \black G \rightcat Q\rightadj R = \rightcat\rho \rightadj R } & & & &  \boxed{ (l\downarrow {\rightadj R}) }  &  \rightcat{ \kern.5em \xrightarrow[ \textstyle \text{faithful} ]{\textstyle Q=r} } & \rightcat\calR  \\      && && & \llap{j' \black G \lambda = \kappa'} \searrow & \\       j' & X' = j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda] = \rightcat{r'} [\kappa'] && j' \black G\rightcat Q = \rightcat{r'} &&& j' \black G\rightcat Q\rightadj R = \rightcat{r'} \rightadj R   \\            \hline              &  \rightadj{   \Bigg\downarrow \rlap{  \kern1em {{\rightcat r} [\kappa]} \mathrel{\rightadj\mapsto} {{(\rightcat r \rightadj R)} [\kappa]} }  }   &&&&&&  &&& \Bigg\downarrow  & \rightadj{ \text{p.b.} } & \rightadj{ \Bigg\downarrow\rlap{R} }   &  \\                 \hline      \calJ \rlap{ \xrightarrow[\kern12em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} } }  & \boxed{ (l\downarrow\calL) } \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern10em \text{faithful} \kern6em ]{\textstyle Q=r} } } & & & &\calL &&    \\ \hline      j & X = j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda] = k[\kappa]  &&&&& j\black G\rightcat Q = k   \\   & &&&& \llap{j \black G \lambda = \kappa} \nearrow & & &  \\   \llap\iota \Bigg\downarrow & \llap{\iota \black G = {} } \Bigg\downarrow \rlap{ {} = \iota \black G \rightcat Q = \mu } & && l &  {} \rlap{\kern0em \iota \black G = \mu}  & \Bigg\downarrow \rlap{\iota \black G \rightcat Q = \mu} & & & & \boxed{ (l\downarrow\calL) } & \rightcat{ \xrightarrow[ \textstyle \text{faithful} ]{\textstyle Q=r} }  &   \leftcat\calL  \\     && && & \llap{j' \black G \lambda = \kappa'} \searrow &    &&&& \llap{!} \downarrow & \Uparrow \rlap\lambda & \Vert \rlap{1_\calL}  \\   j' & X' = j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda] = k'[\kappa']  &&&&& j' \black G\rightcat Q = k'   &&&&  \calI  & \xrightarrow[\textstyle l]{}  &  \calL \\     \end{array} } } \]

\[ \leftcat{ \boxed{ \begin{array} {cc|c|ccc|ccccc|c|cc|cccc} \R^2 & \kern2em && \kern2em & \boxed{ (l\downarrow\calL) } \rlap{ \kern.5em \rightcat{ \xrightarrow[ \textstyle \kern2.6em \text{faithful} \kern2.6em ]{\textstyle Q=r} } } & & & & \calL &&9 \kern2em &&11 & \rightcat\calR \rlap{ \xrightarrow[\kern3.5em]{\textstyle \rightadj R } } & \kern0em & \kern0em &\calL &&9 \\ \hline X = \langle X\pi_1,X\pi_2 \rangle = \langle x,y \rangle &&&& \black X = \black X \rightcat Q [\black X \lambda] = k[\kappa] && &&& X\rightcat Q = k &&&& \rightcat r &&&& \rightcat r \rightadj R \\ && && &&& & \llap{X\lambda = \kappa} \nearrow & &&&&& && \llap\kappa \nearrow & \\ && && \Bigg\downarrow \rlap\mu & & \kern2em & l & \mu & \Bigg\downarrow \rlap{\mu\rightcat Q = \mu} &&&& \rightcat{ \llap\rho } \Bigg\downarrow && l & & \rightcat{ \Bigg\downarrow \rlap{\rho \rightadj R} }& \\ & &&&&&& & \llap{X'\lambda = \kappa'} \searrow & &&&& &&& \llap{\kappa'} \searrow & \\ &&&& X' = X' \rightcat Q [X' \lambda] = k' [\kappa'] &&&&& X'\rightcat Q = k' &&&& \rightcat{r'} &&&& \rightcat{r'} \rightadj R \\ \end{array} } } \]

\[ \leftcat{ \boxed{ \begin{array} {cccccc|ccccccc|cccccc} && 1 && \rightadj{\boxed{3}} &    \hskip1em & \hskip1em  &  && 1 && \rightadj{\boxed{3}} &     \\    & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &        \\     \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL)  \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }   } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.55em]{\textstyle Q = r} }  & \calL &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL) \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }     } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.5em]{\smash{\textstyle Q = r} }  }  & \calL    \\    {} \rlap{\kern-2em \text{CWM Exercise V.1.1}}  &&  \Bigg\downarrow & \llap{\boxed{0}\;\lambda} \Bigg\Uparrow  & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{\boxed{3}\;\pi}  \bigg\Uparrow} } } & \rightadj{   \nearrow \rlap{\kern-6.2em \lower1ex{\boxed{3}\;(\black G\rightcat Q)\lim}}   }   & {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{4} } }   } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  & \kern1em    \\     && 1 & \xrightarrow[\textstyle \boxed{0} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{0} \; l]{\kern21em} }  &&&& \calL  \\   \end{array} } } \]





\[ \leftcat{ \boxed{ \begin{array} {cccccc|ccccccc|cccccc} && 1 && \rightadj{\boxed{3}} &    \hskip1em & \hskip1em  &  && 1 && \rightadj{\boxed{3}} &     \\    & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &        \\     \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL)  \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }   } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.55em]{\textstyle Q = r} }  & \calL &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL) \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }     } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.5em]{\smash{\textstyle Q = r} }  }  & \calL    \\    {} \rlap{\kern-2em \text{CWM Exercise V.1.1}}  &&  \Bigg\downarrow & \llap{\boxed{0}\;\lambda} \Bigg\Uparrow  & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{\boxed{3}\;\pi}  \bigg\Uparrow} } } & \rightadj{   \nearrow \rlap{\kern-6.2em \lower1ex{\boxed{3}\;(\black G\rightcat Q)\lim}}   }   & {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{4} } }   } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  & \kern1em    \\     && 1 & \xrightarrow[\textstyle \boxed{0} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{0} \; l]{\kern21em} }  &&&& \calL  \\ \end{array} } } \]


\[ \leftcat{ \boxed{ \begin{array} {cccccc|ccccccc|cccccc}   &&&&  \rightcat y     &&&&&   \\     1 & \xrightarrow[\kern3em]{\textstyle  \boxed{  X = \langle X\pi_1,X\rightcat{\pi_2}\rangle = \langle x,\rightcat y \rangle }  } & \leftcat{ {\mathbf R}^2 \rlap{ \lower2.8ex{ \kern-1.3em \boxed{0} } } } & \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.55em]{\textstyle \pi_2} } & \mathbf R & \hskip1em & \hskip1em & \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{ (l \downarrow \calL) \rlap{ \lower2.8ex{ \kern-2em \boxed{0} } } } & \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.5em]{\smash{\textstyle Q = r} } } & \calL \\ && \llap{\pi_1} \Bigg\downarrow \rlap{\boxed{0}} & & & \hskip1em & \hskip1em & \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{\boxed{3}\;\pi} \bigg\Uparrow} } } & \rightadj{ \nearrow \rlap{\kern-6.2em \lower1ex{\boxed{3}\;(\black G\rightcat Q)\lim}} } & {} \rlap{ \kern-5.4em \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{4} } } } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} } & \kern1em \\ &   x  & \mathbf R & & & \hskip1em & \hskip1em & 1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{0} \; l]{\kern21em} } &&&& \calL            \\  \hline   \\   \hline          && 1 && \rightadj{\boxed{3}} &    \hskip1em & \hskip1em  &  && 1 && \rightadj{\boxed{3}} &     \\    & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } &   \smash{   \lower3ex {\rightcat k}  }  &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &        \\     \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle \boxed { G =  G\rightcat Q [G\lambda]  =  \rightcat k[\kappa] }}} & \leftcat{   (l \downarrow \calL)  \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }   } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.55em]{\textstyle Q = r} }  & \calL &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL) \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }     } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.5em]{\smash{\textstyle Q = r} }  }  & \calL    \\    &   \text{CWM Exercise V.1.1}  & \llap{!} \Bigg\downarrow \rlap{\boxed{0}}     & \llap{\boxed{0}\;\lambda} \Bigg\Uparrow  & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{\boxed{3}\;\pi}  \bigg\Uparrow} } } & \rightadj{   \nearrow \rlap{\kern-6.2em \lower1ex{\boxed{3}\;(\black G\rightcat Q)\lim}}   }   & {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{4} } }   } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  & \kern1em    \\        && 1 & \xrightarrow[\textstyle \boxed{0} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{0} \; l]{\kern21em} }  &&&& \calL  \\ \end{array} } } \]


<hr />

\[ \leftcat{ \boxed{ \begin{array} {cc|ccc|cccc}  & \kern0em & \kern0em & (l\downarrow\calL) \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern4.5em \text{faithful} \kern4.5em ]{\textstyle Q=r} } } & & & & &\calL &9  \\    \\   \hline  &&& \black X = \black X \rightcat Q [\black X \lambda] = k[\kappa]     &&&&& k   \\    &&& &&&& \llap\kappa \nearrow &    \\       &&&  \Bigg\downarrow \rlap\mu & && l & \mu  & \Bigg\downarrow \rlap\mu & \\ &&&& && & \llap\kappa' \searrow &    \\    &&& X' = X' \rightcat Q [X' \lambda] = k' [\kappa']     &&&&& k'  \\             \\  \hline  \\ \hline  \calJ \rlap{ \xrightarrow[\kern11em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} }   } & \kern0em & \kern0em & (l\downarrow\calL) \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern4.5em \text{faithful} \kern4.5em ]{\textstyle Q=r} } } & & & & &\calL &9  \\    \\   \hline j &&& j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda]     &&&&& j\black G\rightcat Q   \\    &&& &&&& \llap{j \black G \lambda} \nearrow &    \\      \llap\iota \Bigg\downarrow &&&  \llap{\iota \black G = {} }   \Bigg\downarrow \rlap{ {} =   \iota \black G \rightcat Q    } & && l & \iota \black G  & \Bigg\downarrow \rlap{\iota \black G \rightcat Q} & \\ &&&& && & \llap{j' \black G \lambda} \searrow &    \\    j' &&& j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda]     &&&&& j' \black G\rightcat Q   \\     \end{array} } } \]




<hr />

\[ \leftcat{ \boxed{ \begin{array} {cc|ccc|cccc}  & \kern0em & \kern0em & (l\downarrow\calL) \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern4.5em \text{faithful} \kern4.5em ]{\textstyle Q=r} } } & & & & &\calL &9  \\    \\   \hline  &&& \black X = \black X \rightcat Q [\black X \lambda] = k[\kappa]     &&&&& k   \\    &&& &&&& \llap\kappa \nearrow &    \\       &&&  \Bigg\downarrow \rlap\mu & && l & \mu  & \Bigg\downarrow \rlap\mu & \\ &&&& && & \llap\kappa' \searrow &    \\    &&& X' = X' \rightcat Q [X' \lambda] = k' [\kappa']     &&&&& k'  \\     \end{array} } } \]



\[ \leftcat{ \boxed{ \begin{array} {cc|ccc|cccc} \calJ \rlap{ \xrightarrow[\kern11em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} }   } & \kern0em & \kern0em & (l\downarrow\calL) \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern4.5em \text{faithful} \kern4.5em ]{\textstyle Q=r} } } & & & & &\calL &9  \\    \\   \hline j &&& j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda]     &&&&& j\black G\rightcat Q   \\    &&& &&&& \llap{j \black G \lambda} \nearrow &    \\      \llap\iota \Bigg\downarrow &&&  \llap{\iota \black G = {} }   \Bigg\downarrow \rlap{ {} =   \iota \black G \rightcat Q    } & && l & \iota \black G  & \Bigg\downarrow \rlap{\iota \black G \rightcat Q} & \\ &&&& && & \llap{j' \black G \lambda} \searrow &    \\    j' &&& j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda]     &&&&& j' \black G\rightcat Q   \\     \end{array} } } \]


Naturality at those arrows amounts to showing commutativity of the following diagram in $\SET$:

\[ \boxed{ \begin{array} {}  \kern0em & && [\homst d \catD -, {\rightcat X}]  &&  \kern1em  \\   & &  \llap{ [\homst \delta \catD -, \rightcat\phi] } \swarrow &&  \searrow \rlap{ \check {()} }  \\   & [ \homst {d'} \catD -, \rightcat Y ] &&&&  {\rightcat X}_{\leftcat d}  \\  && \llap{ \check{()} } \searrow  && \swarrow \rlap{ {\rightcat\phi}_{\leftcat\delta} }   \\   & && {\rightcat Y}_{ \leftcat{\delta'} }   \\    \end{array}  }  \]

Wednesday, June 16, 2021

Certain preserved limits give left adjoints

WORK IN PROGRESS!

Here we use the fact that (the cone  $\boxed{    \pi : \leftcat{1_{(l \downarrow \rightadj R)} }\lim \Rightarrow \leftcat{1_{(l \downarrow \rightadj R)} }: \leftcat{(l \downarrow \rightadj R)} \to \leftcat{(l \downarrow \rightadj R)}    }$) is (a natural transformation). 
Hence (the following triangles) commute for all ($\rightcat r \leftcat{[\lambda]}\in \leftcat{(l \downarrow \rightadj R)}$) and ($\rightcat f$ as shown):
\[  \boxed{  \begin{array}  {c|cccccc|cccccc}  \leftcat{1_{(l \downarrow \rightadj R)} } & \kern0em   &  \leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)} &  {} \rlap{   \kern-1em \xrightarrow[\smash{\kern15em}]{\textstyle \rlap{\pi_{\rightcat r[\lambda]}} }  }   &&&  \rightcat r \leftcat{[\lambda]} & \kern0em   &  \leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)} &  {} \rlap{   \rightcat{  \kern-1em \xrightarrow[\smash{\kern15em}]{\textstyle f }  }  }   &&&  \rightcat r  \leftcat{[\lambda]}     \\      \llap{\pi} \Big\Uparrow &  &&  \llap{ \pi_{\rightcat{ (\black Q\lim_\calR) } \leftcat{ \big[\overline{\lambda}\big] }}  } \nwarrow  &  \pi_{\pi_{\rightcat r \leftcat{[\lambda]}}}  &  \nearrow \rlap{\pi_{\rightcat r[\lambda]}} &&  &&  \llap{ \pi_{\rightcat{ (\black Q\lim_\calR) } \leftcat{ \big[\overline{\lambda}\big] }}  } \nwarrow  &  \pi_{\rightcat f}  &  \nearrow \rlap{ \pi_{\rightcat r[\lambda]} }  \\    \leftcat{   1_{(l \downarrow \rightadj R)} \lim_{(l \downarrow \rightadj R)  }   }  & & &&  \leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)}  & & && &&    \leftcat{  1_{(l \downarrow \rightadj R)} \lim_{(l \downarrow \rightadj R)}  }    \\ \end{array}  }  \]

To reiterate, (the two triangles above) commute for all ($\rightcat r \leftcat{[\lambda]}\in \leftcat{(l \downarrow \rightadj R)}$) and ($\rightcat f$ as shown) because ($\rightcat\pi$ is a cone).

Using (naturality of $\pi$ at $\pi_{\rightcat r \leftcat{[\lambda]}}$), i.e. $ \pi_{\pi_{\rightcat r \leftcat{[\lambda]}}}$,  plus 
(the uniqueness clause in the universal property of $\leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)}$), 
we get that $\pi_{\rightcat{ (\black Q\lim_\calR) } \leftcat{ \big[\overline{\lambda}\big] }} = 1_{  \leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)}  }$.
This, plus (naturality of $\pi$ at $\rightcat f$), i.e. $\pi_{\rightcat f}$,
gives $\rightcat f = \pi_{\rightcat r[\lambda]}$.

This in turn gives us that 
$\leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)}$ is 
(an initial object in ${(l \downarrow \rightadj R)}$},
which is equivalent to
$\rightcat{ (Q\lim_\calR) } \leftcat{ \big[\overline{\lambda}\big] }$ being 
(a universal arrow from $\leftcat l$ to $\rightadj\calR$) 
which is equivalent to
$\rightcat{ (Q\lim_\calR) }$ being (a left adjoint $\leftcat  l \leftadj L$ for $\leftcat  l$) with ($\leftcat{ \overline{\lambda} }$ its unit).

<hr />

\[ \boxed{ \begin{array} {c|c|c} \kern2em & \kern2em & \kern2em \\ xx & yy & zz \\ \end{array} } \]

\[ \boxed{ \begin{array} {} && r \\ & \llap{\pi_r} \nearrow & \pi_{\pi_r} & \nwarrow \rlap{\pi_r} \\ \leftcat l\leftadj L & {} \rlap{ \kern-1em \xrightarrow[\pi_{\leftcat l\leftadj L}] {\kern8em} } &&& \leftcat l\leftadj L \\ \end{array} } \]

Saturday, June 5, 2021

The creation of limits in comma categories

DRAFT:
WARNING: There are several different systems that one can come up with
to number the various categories, objects, arrows, and 2-cells we need to introduce and discuss. 
Different numbering systems are in use in different places in the following, 
while I think about which, if any, should be the primary numbering system.


This is a somewhat technical, nitty-gritty, topic, involving some fine details,
but it plays a crucial role in proofs of adjoint functor theorems (see Chapter X, Section 1, of Mac Lane's CWM; also its Chapter V, Section 6, both the Lemma stated there and the exercises to that section), and is worth a close look, where details get filled in, to see what is entailed.
$\calK$
Much of this post is an experiment in presentation, experimenting with different ways of presenting the proof, 
in particular different diagrams that present different aspects, parts, or views of what is going on.

<h3>Comma categories: review and notation</h3>
The notation in the proof gets a bit sticky.
There are both notational and conceptual issues.

Let us introduce this topic by comparing 
(the universal 1-cone $\rightadj{ \langle \pi_{\rightcat 1}, \pi_{\rightcat 2} \rangle }$ of a very familiar categorical product, $\R\times\R \cong \R^2$), to 
(the universal 2-diagrams ($\rightcat Q [\leftcat\lambda]$) for $(l \downarrow \calL)$ and $(l \downarrow \rightadj R)$, the comma categories in question).
(For the 1-universal property of those, see Exercise II.6.4 of CWM. 
For a characterization of those as  weighted limits (cylinders) see Kelly 1989 [EO2CL] (4.2) .)

The diagram at left below, for $\R\times\R \cong \R^2$, is in the 1-category of real vector spaces $\Vect$,
the other diagrams are 2-diagrams in the 2-category $\CAT$.
{Further diagrams are below that top diagram.)

\[ \leftcat{ \boxed{ \begin{array} {ccccc|ccccc|ccccc|ccccc}  &  \leftcat{ \boxed{ \R\times\R \cong \R^2 } \rlap{ \lower2.8ex{ \kern-3.2em \boxed{10} } } } & \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.55em]{\textstyle \pi_2} } & \R & \hskip.5em & \hskip.5em & \leftcat{ \boxed{ (l \downarrow \calL) }  \rlap{ \lower3ex{ \kern-2.2em \boxed{10} } } } & \rightcat{ \xrightarrow[\kern2em\boxed{11} \; \text{faithful} \kern2em]{\textstyle Q = r} } & \calL   &   \hskip.5em & \hskip.5em & \leftcat{ \boxed{ (l \downarrow \rightadj R) }  \rlap{ \lower3ex{ \kern-2.2em \boxed{10} } } } & \rightcat{ \xrightarrow[\kern1.5em\boxed{11} \; \text{faithful} \kern1.5em]{\textstyle Q = r} } & \rightcat\calR   &   \hskip.5em & \hskip.5em &  \boxed{  ( l \downarrow {\rightadj R})  }  &  \xrightarrow[\kern4em]{\textstyle \text{fiber}}  &  \leftcat{ \boxed{ (\Delta \Downarrow {\rightadj R}) }  }  & \rightcat{ \xrightarrow[\kern4em]{\textstyle !} } & \calI     \\       & \llap{\pi_1} \Bigg\downarrow \rlap{\boxed{11}} & & & \hskip0em & \hskip0em & \llap ! {\Bigg\downarrow} \rlap{\boxed{11}} & \llap{\boxed{11}\;\lambda} \Bigg\Uparrow & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} } & \hskip1em & \hskip0em   & \llap ! {\Bigg\downarrow} \rlap{\boxed{11}} & \llap{\boxed{11}\;\lambda} \Bigg\Uparrow & \Bigg\downarrow \rlap{ \rightadj R \; \boxed{0} } & \hskip1em & \hskip0em   &   \llap{!} {\Bigg\downarrow}  & \rightadj{\text{p.b.}}  & \leftcat{\Bigg\downarrow}  & \Bigg\Uparrow  & \rightadj{  \Bigg\downarrow \rlap{ \ulcorner R \urcorner }  }&       \\       & \R & & & \hskip0em & \hskip0em & \calI & \xrightarrow[\textstyle \boxed{1} \; l]{} & \calL & \hskip0em & \hskip0em   & \calI & \xrightarrow[\textstyle \boxed{1} \; l]{} & \calL & \hskip0em & \hskip0em  &  \calI  &  \xrightarrow[\textstyle l]{}  &  \leftcat\calL & \xrightarrow[\textstyle \Delta]{} & [\rightcat\calR,\leftcat\calL]     \\      \end{array} } } \]

\[ \leftcat{ \boxed{ \begin{array} {cc|c|ccc|ccccc|c|ccc|ccc|cccc}  \R^2   \rlap{  \lower3.2ex{ \kern-1.4em \boxed{10} }  } & \kern0em && \kern0em &  (l\downarrow\calL)  \rlap{  \lower3.2ex{ \kern-2.3em \boxed{10} }  }  \rlap{ \kern.5em \rightcat{ \xrightarrow[ \textstyle \kern4em \boxed{11} \; \text{faithful} \kern4em ]{\textstyle Q=r} } } & & & & &  \calL \rlap{  \lower3.2ex{ \kern-1em \boxed{0} }  }   & \kern1em  &&  \kern0em   & \calJ \rlap{ \xrightarrow[\kern4.7em \boxed{12} \kern4.7em] {\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} }  } & \kern0em & \kern0em & (l\downarrow\calL) \rlap{  \lower3.2ex{ \kern-2.3em \boxed{10} }  } \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern3.8em \boxed{11} \; \text{faithful} \kern3.8em ]{\textstyle Q=r} } }  & \kern0em & & & &  \calL \rlap{  \lower3.2ex{ \kern-1em \boxed{0} }  }  &    \\      \\   \hline   X = \langle X\pi_1,X\pi_2 \rangle = \langle x,y \rangle &&&&     \black X = \black X \rightcat Q [\black X \lambda] = k[\kappa]     &&&&&  X\rightcat Q = k   &&&&  j &&& j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda] &&&&& j\black G\rightcat Q    \\    && && &&& & \llap{X\lambda = \kappa} \nearrow & &&&&& &&&&&& \llap{j \black G \lambda} \nearrow &  \\   &&    &&  \Bigg\downarrow \rlap\mu & & \kern2em   & l & \mu  & \Bigg\downarrow \rlap{\mu\rightcat Q = \mu} &&&& \llap\iota \Bigg\downarrow &&& \llap{\iota \black G = {} } \Bigg\downarrow \rlap{ {} = \iota \black G \rightcat Q } & && l & \iota \black G & \Bigg\downarrow \rlap{\iota \black G \rightcat Q} &  \\  & &&&&&& & \llap{X'\lambda = \kappa'} \searrow & &&&& &&&&& && \llap{j' \black G \lambda} \searrow &   \\     &&&&  X' = X' \rightcat Q [X' \lambda] = k' [\kappa']     &&&&& X'\rightcat Q = k'  &&&&  j' &&& j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda] &&&&& j' \black G\rightcat Q    \\     \end{array} } } \]

\[ \leftcat{ \boxed{ \begin{array} {c|cc|c|cccc|c|cccccc} \calJ \rlap{ \xrightarrow[\textstyle \kern2em \boxed{12} \; \text{right lax fiber} \kern2em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} } } & \boxed{ (l\downarrow {\rightadj R}) } \rlap{ \lower3.2ex{ \kern-2.5em \boxed{10} } } \rlap{ \rightcat{ \kern.5em \xrightarrow[ \textstyle \kern5.5em \boxed{11} \; \text{faithful} \kern5.5em ]{\textstyle Q=r} } } & & \rightcat\calR \rlap{ \rightadj{ \kern.5em \xrightarrow[\kern8em \boxed{0} \kern8em]{\textstyle R} } } & & \calL && \kern2em &&&& \CAT \\ \hline j & X = j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda] = \black X\rightcat Q [\black X \lambda] = \rightcat r [\kappa] && \kern2em \black{X} \rightcat Q = j\black G\rightcat Q = \rightcat r \kern1em & \kern7em && \black{X} \rightcat Q \rightadj R = j\black G\rightcat Q\rightadj R = \rightcat r \rightadj R = k \\ & &&&& \llap{\black{X} \lambda = j \black G \lambda = \kappa} \nearrow & \\ \llap\iota \Bigg\downarrow & \llap{\iota \black G = {}} \Bigg\downarrow \rlap{ {} = \iota \black G \rightcat Q = \rightcat\rho } && \llap{ \iota \black G \rightcat Q \; } \Bigg\downarrow \rlap{ {} = \rightcat\rho} & \kern1em l & {} \rlap{\kern0em \iota \black G = \rightcat\rho} & \Bigg\downarrow \rlap{\iota \black G \rightcat Q\rightadj R = \rightcat\rho \rightadj R = \mu} & & & & \boxed{ (l\downarrow {\rightadj R}) } & \rightcat{ \kern.5em \xrightarrow[ \textstyle \boxed{11} \; \text{faithful} ]{\textstyle Q=r} } & \rightcat\calR \\ && && & \llap{\black{X'} \lambda = j' \black G \lambda = \kappa'} \searrow & \\ j' & X' = j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda] = \black{X'} \rightcat Q [\black{X'} \lambda] = \rightcat{r'} [\kappa'] && \black{X'} \rightcat Q = j' \black G\rightcat Q = \rightcat{r'} &&& \black{X'} \rightcat Q \rightadj R = j' \black G\rightcat Q\rightadj R = \rightcat{r'} \rightadj R = k' \\ \hline & \rightadj{ \Bigg\downarrow \rlap{ \kern1em {{\rightcat r} [\kappa]} \mathrel{\rightadj\mapsto} {{(\rightcat r \rightadj R)} [\kappa]} } } &&&&&& &&& \Bigg\downarrow & \rightadj{ \text{p.b.} } & \rightadj{ \Bigg\downarrow\rlap{R \; \boxed{0}} } & \kern1em \\ \hline \calJ \rlap{ \xrightarrow[\textstyle \kern2em \boxed{12} \; \text{right lax fiber} \kern2em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} } } & \boxed{ (l\downarrow\calL) } \rlap{ \lower3.2ex{ \kern-2.5em \boxed{10} } } \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern13em \boxed{11} \; \text{faithful} \kern13em ]{\textstyle Q=r} } } & & & &\calL && \\ \hline j & X = j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda] = \black X\rightcat Q [\black X \lambda] = k[\kappa] &&&&& \black{X} \rightcat Q = j\black G\rightcat Q = k \\ & &&&& \llap{\black{X} \lambda = j \black G \lambda = \kappa} \nearrow & & & \\ \llap\iota \Bigg\downarrow & \llap{\iota \black G = {} } \Bigg\downarrow \rlap{ {} = \iota \black G \rightcat Q = \mu } & && l & {} \rlap{\kern0em \iota \black G = \mu} & \Bigg\downarrow \rlap{\iota \black G \rightcat Q = \mu} & & & & \boxed{ (l\downarrow\calL) } & \rightcat{ \xrightarrow[ \textstyle \boxed{11} \; \text{faithful} ]{\textstyle Q=r} } & \leftcat\calL \\ && && & \llap{\black{X'} \lambda = j' \black G \lambda = \kappa'} \searrow & &&&& \llap{\boxed{11} \; !} \downarrow & \llap{ \boxed{11} \; \lambda } \Uparrow & \Vert \rlap{1_\calL \; \boxed{0}} \\ j' & X' = j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda] = \black{X'} \rightcat Q [\black{X'} \lambda] = k'[\kappa'] &&&&& \black{X'} \rightcat Q = j' \black G\rightcat Q = k' &&&& \calI & \xrightarrow[\textstyle \boxed{1} \; l]{} & \calL \\ \end{array} } } \]

\[ \leftcat{ \boxed{ \begin{array} {cccccc|ccccccc|cccccc}   &&&&  \rightcat y     &&&&&   \\     1 & \xrightarrow[\kern3em]{\textstyle  \boxed{  X = \langle X\pi_1,X\rightcat{\pi_2}\rangle = \langle x,\rightcat y \rangle }  } & \leftcat{ {\R}^2 \rlap{ \lower2.8ex{ \kern-1.3em \boxed{10} } } } & \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.55em]{\textstyle \pi_2} } & \R & \hskip1em & \hskip1em &  &  &  &  &  \\   && \llap{\pi_1} \Bigg\downarrow \rlap{\boxed{11}} & & & \hskip1em & \hskip1em &  &  & &  &  & \kern1em       \\ &   x  & \R & & & \hskip1em & \hskip1em &      &&&&   \\                          \hline                   && 1 && \rightadj{\boxed{3}} &    \hskip1em & \hskip1em  &  && 1 && \rightadj{\boxed{3}} &     \\    & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((X\pi_2)\lim_{\leftcat\R}\big)[\overline{X\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black X \rightcat{\pi_2})\lim_{\leftcat\R}} } &   &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((X\pi_2)\lim_{\leftcat\R}\big)[\overline{X\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black X \rightcat \pi_2)\lim_{\leftcat\R}} } & &        \\     &&&&  \rightcat y     &&&&&   \\     (\leftcat a, \rightcat b )   & \xrightarrow[\kern3em]{\textstyle  \boxed{  X = \langle X\pi_1,X\rightcat{\pi_2}\rangle = \langle x,\rightcat y \rangle }  } & \leftcat{ {\mathbf R}^2 \rlap{ \lower2.8ex{ \kern-1.3em \boxed{10} } } } & \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.55em]{\textstyle \pi_2} } & \mathbf R & \hskip1em & \hskip1em & \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{ (l \downarrow \calL) \rlap{ \lower2.8ex{ \kern-2em \boxed{10} } } } & \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.5em]{\smash{\textstyle Q = r} } } & \calL \\ && \llap{\pi_1} \Bigg\downarrow \rlap{\boxed{11}} & & & \hskip1em & \hskip1em & \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{ \boxed{21}\;\pi_{\black G \rightcat Q} } \bigg\Uparrow} } } & \rightadj{   \nearrow \rlap{  \kern-6.2em \lower1ex{ \boxed{20}\;(\black G\rightcat Q)\leftcat{\lim_\calL} }  }    } & {} \rlap{ \kern-5.4em \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{32} } } } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} } & \kern1em \\ &   x  & \mathbf R & & & \hskip1em & \hskip1em & 1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{1} \; l]{\kern21em} } &&&& \calL   \\          \hline   \\         && 1 && \rightadj{\boxed{20}} &    \hskip1em & \hskip1em  &  && 1 && \rightadj{\boxed{20}} &     \\    & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{22}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } &   \smash{   \lower3ex {\rightcat k}  }  &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{22}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &        \\     \calJ & \xrightarrow [\kern3.5em\boxed{12}\kern3.5em]{\smash{\textstyle \boxed { G =  G\rightcat Q [G\lambda]  =  \rightcat k[\kappa] }}} & \leftcat{   (l \downarrow \calL)  \rlap{  \lower2.8ex{ \kern-2em \boxed{10} }  }   } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.5em]{\textstyle Q = r} }  & \calL &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{12}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL) \rlap{  \lower2.8ex{ \kern-2em \boxed{10} }  }     } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.5em]{\smash{\textstyle Q = r} }  }  & \calL    \\    &   \text{CWM Exercise V.1.1}  & \llap{!} \Bigg\downarrow \rlap{\boxed{11}}     & \llap{\boxed{11}\;\lambda} \Bigg\Uparrow  & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightadj{    {} \rlap{   \kern4em \raise3.6ex{  \llap{ \boxed{21} \; \pi_{\black G\rightcat Q} } \bigg\Uparrow  }   }    } & \rightadj{   \nearrow \rlap{\kern-6.2em \lower1ex{\boxed{20}\;(\black G\rightcat Q)\lim_{\leftcat\calL}}}   }   & {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{32} } }   } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  & \kern1em    \\        && 1 & \xrightarrow[\textstyle \boxed{1} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{1} \; l]{\kern21em} }  &&&& \calL  \\          \hline   \\   \hline        &&&&  \rightcat k  &&&&&  \\      \calI & \xrightarrow [\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle \boxed { X =  X\rightcat Q [X\lambda]  =  \rightcat k[\kappa] }}} & \leftcat{   (l \downarrow \calL)  \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }   } &  \rightcat{ \xrightarrow [\kern3.5em\boxed{0}\kern3.55em]{\textstyle Q = r} }  & \calL &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL) \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }     } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.5em]{\smash{\textstyle Q = r} }  }  & \calL    \\    & & \llap{!} \Bigg\downarrow \rlap{\boxed{0}}     & \llap{\boxed{0}\;\lambda} \Bigg\Uparrow  & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{\boxed{3} \; \pi_{\black G\rightcat Q}}  \bigg\Uparrow} } } & \rightadj{   \nearrow \rlap{\kern-6.2em \lower1ex{\boxed{3}\;(\black G\rightcat Q)\lim}}   }   & {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{4} } }   } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  & \kern1em    \\        && 1 & \xrightarrow[\textstyle \boxed{0} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{0} \; l]{\kern21em} }  &&&& \calL  \\           \hline   \\         && 1 && \rightcat{\boxed{20}} &    \hskip1em & \hskip1em  &  && 1 && \rightcat{\boxed{20}} &     \\    & \llap{!} \nearrow & \red{     \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{22} \; \rightcat{ \big( (\leftcat G  Q)\lim_\calR \big) } \leftcat{ [\overline{G\lambda}] } } }  } & \rightcat{ \searrow \rlap{ (\leftcat G  Q)\lim_\calR }     } &   \smash{   \lower3ex {\rightcat s}  }  &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{     \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{22} \; \rightcat{ \big( (\leftcat G  Q)\lim_\calR \big) } \leftcat{ [\overline{G\lambda}] } } }  } & \rightcat{ \searrow \rlap{ (\leftcat G  Q)\lim_\calR }     } & &        \\     \calJ & \xrightarrow[\kern3.5em\boxed{12}\kern3.5em]{\smash{\textstyle \boxed { G =  G\rightcat Q \leftcat{[G\lambda]}  =  \rightcat s \leftcat{[\kappa]} }}} & \leftcat{   (l \downarrow \rightadj R)  \rlap{  \lower2.8ex{ \kern-2em \boxed{10} }  }   } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.55em]{\textstyle Q = r} }  & \rightcat\calR &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{12}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \rightadj R) \rlap{  \lower2.8ex{ \kern-2em \boxed{10} }  }     } &  \rightcat{ \xrightarrow [\kern3.5em\boxed{11}\kern3.5em]{\smash{\textstyle Q = r} }  }  &  \rightcat\calR   \\    &   \text{CWM Lemma V.6}  & \llap{!} \Bigg\downarrow \rlap{\boxed{11}}     & \llap{\boxed{11}\;\lambda} \Bigg\Uparrow  & \rightadj{     \Bigg\downarrow \rlap{ R \; \boxed{0} }     }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightcat{ {} \rlap{ \kern4em \raise3.6ex{\llap{\boxed{21} \; \pi_{\black G\rightcat Q} }  \bigg\Uparrow} } } & \leftadj{   \nearrow \rlap{  \kern-6.2em \lower1ex{ \boxed{20}\;(\black G\rightcat Q)\lim_{\rightcat\calR} }  }   }   & \leftadj{      {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \leftcat{ \overline{\black G\leftcat\lambda} } \; \boxed{32} } }   }     }   &   \rightadj{     \Bigg\downarrow \rlap{ R \; \boxed{0} }     }  & \kern1em    \\        && 1 & \xrightarrow[\textstyle \boxed{1} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{1} \; l]{\kern21em} }  &&&& \calL  \\ \end{array} } } \]

To understand those categories, 
a necessary starting point is to see what the objects and arrows in each look like 
in relation to
the objects and arrows in their constituent categories. 
To that end, consider the above diagrams: 

<hr />

(Repitious repeat, to be edited :-)
Before wading into (the existence proof) for (a limit) in (a comma category), 
it is useful to review the definitions of (the objects and arrows in comma categories), 
and (their relations) to (those in the related categories).
(This is material in Section II.6, Comma Categories, of CWM, adopted with notation tailored to 
(a putative right adjoint functor $\rightadj{ \boxed{0} \; R : \rightcat\calR \to \leftcat\calL }$).)

To that end, consider the above (rather large display).
This display accomplishes several things.
First, it shows (objects and arrows in several different categories and how they relate to each other).
Second, it shows how (objects in comma categories) can be broken into (their components) ($X \mapsto X\rightcat Q, X\leftcat\lambda$), 
and conversely how (compatible entities) can be combined into (an object in a comma category) ($k, \kappa \mapsto k[\kappa]$),
and, moreover, this not just for (individual objects), but also for (functors into comma categories) (variable objects).

<hr />

Suppose we have a path, a function of time, in $\R^2$
Such a path could be denoted as a single variable, say a single letter like $X$, 
or in terms of its coordinates, say $\langle x_1,x_2 \rangle$, or $\langle x,y \rangle$, 
or we could introduce explicit coordinate functions on ${\mathbf R}^2$, say $\pi_1$ and $\pi_2$ 
and view the coordinates as composites $X\pi_1$ and $X\pi_2$, 
which can be combined to give $X$ by: $\boxed{  X = \langle X\pi_1,X\pi_2 \rangle }$.
(I.e., do we show the coordinates of $X$, or merely $X$ as a single entity?)
The same choices arise for functors into comma categories.
($\leftcat{  (l\downarrow\calL) }$) has its "coordinate functions"
($\rightcat Q : \leftcat{  (l\downarrow\calL) } \to \calL$) and ($   \leftcat{  \lambda : {!l} \Rightarrow \rightcat Q :  {(l\downarrow\calL)} \to \calL  }   $).
Thus below I speak about (a functor $G : \calJ \to {(l\downarrow\calL)} $), and its "coordinates" $G\rightcat Q$ and $G\leftcat\lambda$, 
which can be put back together to get $G$ by: $\boxed{  G = G\rightcat Q \leftcat{ [\black G\lambda] }  }$, 
which acts as follows on ($\iota : j \to j'$ in $\calJ$):

\[ \leftcat{ \boxed{ \begin{array} {cc|ccc|cccc} \calJ \rlap{ \xrightarrow[\kern11em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} }   } & \kern0em & \kern0em & (l\downarrow\calL) \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern4.5em \text{faithful} \kern4.5em ]{\textstyle Q=r} } } & & & & &\calL &9  \\    \\   \hline j &&& j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda]     &&&&& j\black G\rightcat Q   \\    &&& &&&& \llap{j \black G \lambda} \nearrow &    \\      \llap\iota \Bigg\downarrow &&&  \llap{\iota \black G = {} }   \Bigg\downarrow \rlap{ {} =   \iota \black G \rightcat Q    } & && l & \iota \black G  & \Bigg\downarrow \rlap{\iota \black G \rightcat Q} & \\ &&&& && & \llap{j' \black G \lambda} \searrow &    \\    j' &&& j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda]     &&&&& j' \black G\rightcat Q   \\     \end{array} } } \]

<hr />

In the simplest situation (CWM Exercise V.1.1), 
we start with (a single category $\leftcat{ \boxed{0} \; \calL }$) and (an object $\leftcat{ \boxed{1} \; l \in \calL }$).
We can then form (the comma category $\leftcat{ \boxed{\boxed{10}\;(l\downarrow \calL)} }$)
with its universal 2-diagram in the 2-category $\CAT$,
one leg of which is the (canonical faithful, but not full, forgetful functor 
$\rightcat{  \boxed{\leftcat{(l\downarrow \calL)} \xrightarrow[\kern1em\boxed{11}\kern1em]{\textstyle Q = r} \leftcat\calL : \leftcat{k[\kappa : l \to k] \mathrel{\rightcat\mapsto} k}}  }$).
(The boxed numbers are used in some diagrams below.)

Suppose now we have 
(a functor $\boxed{ \boxed{12} \; G : \calJ \to \leftcat{(l\downarrow \calL)} }$) such that 
(the composite $\boxed{ 12; \rightcat{11} } \; \black G\rightcat Q$) has
(a limit cone $\rightadj{    \boxed{\textstyle \boxed{21}\; \pi_{\black G \rightcat Q} : \boxed{20} \; (\black G\rightcat Q)\lim_{\leftcat\calL} \Rightarrow \black G\rightcat Q}    }$ in $\leftcat\calL$).

\[ \leftcat{ \boxed{ \begin{array} {cccccc|ccccccc|cccccc} && 1 && \rightadj{\boxed{20}} &    \hskip1em & \hskip1em  &  && 1 && \rightadj{\boxed{20}} &     \\    & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{22} \; \big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{22}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &        \\     \calJ & \xrightarrow [\kern3.5em \boxed{12} \kern3.5em] {\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL)  \rlap{  \lower2.8ex{ \kern-2em \boxed{10} }  }   } &  \rightcat{ \xrightarrow [\kern3.5em\boxed{11}\kern3.55em]{\textstyle Q = r} }  & \calL &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{12}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL) \rlap{  \lower2.8ex{ \kern-2em \boxed{10} }  }     } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.5em]{\smash{\textstyle Q = r} }  }  & \calL    \\    {} \rlap{\kern-2em \text{CWM Exercise V.1.1}}  &&  \Bigg\downarrow & \llap{\boxed{11}\;\lambda} \Bigg\Uparrow  & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{ \boxed{21} \; \pi_{\black G \rightcat Q} }  \bigg\Uparrow} } } & \rightadj{   \nearrow \rlap{  \kern-6.2em \lower1ex{ \boxed{20}\;(\black G\rightcat Q)\lim_{\leftcat\calL} }  }   }   &  {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{32} } }   }    & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  & \kern1em    \\     && 1 & \xrightarrow[\textstyle \boxed{1} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{1} \; l]{\kern25em} }  &&&& \calL  \\ \end{array} } } \]

See (the external 2-diagrams in $\CAT$ above), also (the internal diagrams in two functor categories) in (the first row below).
Ignore for the moment (the second row).
 
\[ \leftcat{  \boxed{   \begin{array} {cccc l|ccccccccc}    &&    [ \calJ, \leftcat{(l\downarrow \calL)} ]  {} \rlap{  \kern.5em \rightcat{ \xrightarrow[\kern37em]{\textstyle [ \leftcat\calJ, (Q=r) ] } }  }   &&&  && &&&  [ \calJ, \calL ]   &&        \\                    \hline     &&   \llap{\boxed{1 | 12}\;} G  && & \kern1em  & \kern1em   &&  \llap{  \boxed{2 | 12;\rightcat{11}} \kern1em }   G\rightcat Q &&     \\     &&    &  \rightadj{  \nwarrow \rlap{ \pi_{\black G} \; \boxed{5 | 121} }  }  &  &&   & \llap{G\lambda} \nearrow & \smash{   \lower1ex{  \boxed{ \scriptstyle \text{defn } \overline{G\lambda} }  }   }  &  \rightadj{  \nwarrow \rlap{ \pi_{\black G \rightcat Q} \; \boxed{3 | 21} }  }     \\       &&   &&  \rightadj{\big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)}[ \overline{G\lambda} ] \; \boxed{5 | 132}  &&   \leftcat{\llap{\boxed{0}\kern1em}  l} & {} \rlap{\kern-1em \xrightarrow[ \textstyle \boxed{ \exists!\overline{G\lambda} \; \boxed{4 | 32} } ]{\kern12em} }  &&&  \rightadj{  (\black G\rightcat Q)\lim_{\leftcat\calL} \; \boxed{3 | 20}  }   \\   &&   {} \rlap{ \kern3em \text{a single $\calJ$-cone in $(l\downarrow \calL)$} }   &&&& {} \rlap{\kern0em \text{mediating arrow, a morphism of $\calJ$-cones in $\calL$} } &&&&   \\                   \hline        \forall \; \boxed{6} \; k[\kappa]  &  {} \rlap{ \kern-1em \xrightarrow[\kern17em]{\textstyle \forall \mu \; \boxed{7}}  }  &&&  \black G  \rlap{\; \boxed{1}}    \kern1em  &  \kern1em  &  & \boxed{6\rightcat Q} &  k & {} \rlap{ \kern-1em \xrightarrow [\kern12em] {\textstyle \mu\rightcat Q =  \mu \; \boxed{7}} } &&& \black G\rightcat Q  & \boxed{2}      \\     &    \llap{ \exists! \; \boxed{8'} \; \bar\mu} \searrow  && \rightadj{  \nearrow \rlap{ \pi_{\black G} \; \boxed{5 | 121} }  }   &     &     && \llap{\kappa} \nearrow && \llap{\black G\lambda} \nearrow \rlap{\boxed{2 | 12;11}} && \rightadj{  \nearrow \rlap{ \pi_{\black G \rightcat Q \;  \boxed{3 | 21}} }  } &   \\   &&  \rightadj{ \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big) } [\overline{\black G\lambda}]     & \rightadj{\boxed{5 | 120}}  &   &&   \llap{\boxed{0}\kern1em}  l & {} \rlap{ \kern-1em \xrightarrow [\textstyle \exists!\overline{\black G\lambda} \; \boxed{4 | 32}] {\smash{\kern12em}} } &&& \rightadj{(\black G\rightcat Q)\lim_{\leftcat\calL}}  &  \rightadj{\boxed{3 | 20}}  &   \\   \end{array}  }   } \]
Then ($\boxed{2}\; G\leftcat\lambda$ is a cone over $\boxed{2}\; G\rightcat Q$), 
($\rightadj{ \boxed{3} \; \pi_{\black G \black Q} }$ is a universal cone over $\boxed{2}\; G\rightcat Q$), 
so there is a unique (mediating arrow $\leftcat{   \boxed{  \boxed{4} \; \overline{{\black G}\lambda}  }   }$) such that $\leftcat{    \boxed{   {  {\overline{\black G\lambda}} \cdot {  \rightadj{ \pi_{\black G \rightcat Q} }  } = {\black G\lambda}   }    }       }$.
Note that ($\rightadj{ \boxed{5}\; \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)\leftcat{[\overline{\black G\lambda}]} }$ is an object in the comma category $\leftcat{\boxed{0}\; (l\downarrow \calL)}$), and 
**** (the universal cone $\rightadj{\boxed{3} \; \pi_{\black G \rightcat Q} : (\black G\rightcat Q)\lim_{\leftcat\calL} \Rightarrow \black G\rightcat Q}$ in $\leftcat\calL$) 
may also be viewed as 
(a cone $\rightadj{  \boxed{\textstyle \boxed{5}\; \pi_{\black G} : \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)[\overline{\black G\lambda}] \Rightarrow G}  }$ in $\leftcat{(l\downarrow \calL)}$) ****.

To show ($\rightcat{\boxed{0}\; Q}$ created a limit) we must show 
(the above lift ${\rightadj\pi}_{\rightcat G}$) is (unique as a lift) and (universal as a cone).

For (uniqueness as a lift)
suppose (a cone $\rho : k[\kappa] \Rightarrow G$ in $\leftcat{(l\downarrow \calL)}$) 
is (a lift through $\rightcat Q$) of (the cone $\rightadj{\pi_{\black G \rightcat Q} : (\black G\rightcat Q)\lim_{\leftcat\calL} \Rightarrow \black G\rightcat Q}$ in $\calL$). 
\[ \leftcat{ \boxed{ \begin{array} {cccc|cccccc} {} \rlap{ \kern2em (l \downarrow \calL) \kern.5em \rightcat{ \xrightarrow[\kern24em]{\textstyle Q = r} } } &&&& & && \calL \\ \hline G &&& \kern1em & \kern1em & && G\rightcat Q && \\ & \nwarrow \rlap\rho && \text{a single cone in } \leftcat{(l\downarrow \calL)} && & \llap{G\lambda} \nearrow && \nwarrow \rlap{ \rho\rightcat Q = \rightadj{ \pi_{\black G \rightcat Q} } } & \\ && k[\kappa] &&& \leftcat l & {} \rlap{\kern-1em \xrightarrow[\textstyle \kappa]{\kern9em} } &&& (k[\kappa])\rightcat Q = \rightadj{ (\black G\rightcat Q)\lim_{\leftcat\calL} } \\ &&&&& {} \rlap{\kern0em \text{a morphism of cones in } \leftcat\calL} &&&& \\ \end{array} } } \]
Then $k \xlongequal{ \text{ defn. of } \rightcat Q \, } (k[\kappa])\rightcat Q \xlongequal{ \text{ lift } } \rightadj{  (\black G\rightcat Q)\lim_{\leftcat\calL}  }$
and $\rho = \rho\rightcat Q = \rightadj\pi_{\black G \rightcat Q}$
so $\Big(  \rho : k[\kappa] \Rightarrow G  \Big)$ equals $\rightadj{ \Big( \pi_{\black G} : \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)[\kappa] \Rightarrow G  \Big)  }$  as (cones in $\leftcat{(l\downarrow \calL)}$).

The only variable yet to be determined is $\kappa$.
But, like $\overline{G\lambda}$,
($\kappa$ is a morphism of cones from $G\lambda$ to $\pi_{\black G \rightcat Q}$), 
and (the uniqueness clause of the universal property of the latter) gives 
$\kappa = \overline{G\lambda}$.



Our job now is to show 
(the cone  $\rightadj{    \boxed{   \textstyle   \boxed{5} \; \pi_{\black G} : \leftcat{   \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)\Big[\overline{\black G\lambda}\Big]   }  \Rightarrow  \black G   }    }$)
is (a universal cone to $G$ in $\leftcat{(l\downarrow \calL)}$), thus 
$\red{   \boxed{  \textstyle \leftcat{ \big((\black G\rightcat Q) \lim_{\leftcat\calL}\big) \Big[\overline{\black G\lambda}\Big] } = \black G\lim_{ \leftcat{(l\downarrow \calL)} }  }   }$.
(Consult the internal diagrams below; 
numbers in boxes refer to entities in the categories $\leftcat\calL$ and $\leftcat{(l\downarrow \calL)}$.)

\[ \leftcat{ \boxed{ \begin{array} {ccc|c  rcccccl}   \kern1em && \kern-10em &  \kern1em  &&& &&  \llap{ \boxed{1 | 12} \; } \black G &&   \\  &  \leftcat{ \llap{ \boxed{10} \; } (l\downarrow \calL)  }  &&&    && && & \rightadj{ \nwarrow \rlap{\pi_{\black G} \; \boxed{5 | 121}} }  &  \kern4em  \text{(a single cone) in } \leftcat{(l\downarrow \calL)}  \\  &  \smash{   \lower2ex{  \rightcat{ \llap{ \boxed{11} \; Q } \Bigg\downarrow }  }   } &&&     &&&   && & \rightadj{ \big((\black G\rightcat Q) \lim_{\leftcat\calL}\big) } \Big[\overline{\black G\lambda}\Big]  \rightadj{  {} = \black G \lim_{ \leftcat{(l\downarrow \calL)}   } \; \boxed{5 | 120}    }   \\         \hline          &&&& && &&  \llap{ \boxed{2 | 12;11} \; } G\rightcat Q &&   \\     &&&&   && &  \leftcat{  \llap{\boxed{2 | 12;11 , 31} \; G\lambda} \nearrow  }  && \rightadj{ \nwarrow \rlap{\pi_{\black G \black Q} \; \boxed{3 | 21}} } &  \kern4em \rightadj{ \text{(a single, universal, cone) in } \leftcat\calL }   \\    &  \leftcat{  \llap{ \boxed{0} \; } \calL  }   &&&    && \leftcat{  \boxed{0 | 1 , 30} \; l  }   & {} \rlap{\kern-1em \xrightarrow[\textstyle \llap{\boxed{4 | 32} \;} \exists!\overline{G\lambda}] {\kern19em} } &&& \rightadj{  (\black G\rightcat Q)\lim_{\leftcat\calL} \rlap{ \; \boxed{3 | 20} }  }     \\     &&&&& {} \rlap{    \kern0em \text{definition of $\leftcat{\overline{\black G\lambda}}$ makes it (a morphism of cones in  $\leftcat\calL$) : $\leftcat{  \overline{\black G\lambda} : \black G \lambda \to \rightadj{ \pi_{\black G \rightcat Q} }  }$  }     }  &&&&&       \\ \hline \\ \hline       &&&&&  {} \rlap{   \text{($\mu : k[\kappa] \Rightarrow G$ an arbitrary cone) in } \leftcat{(l\downarrow \calL)} \text{ to the base } G  }  \\    &&&& &  & \forall \; \boxed{6} \; k[\kappa] & {} \rlap{ \kern-1em \xrightarrow[\kern18em] {\textstyle \forall\mu \kern1em \boxed{7}} } &&& \black G \rlap{\; \boxed{1 | 12}} \\ &  \leftcat{  \llap{ \boxed{10} \; } (l\downarrow \calL)  } &&& && & \llap{\boxed{8'} \kern1em \exists!\bar\mu} \searrow && \rightadj{ \nearrow \rlap{ \pi_{\black G} \; \boxed{5 | 121} } } &   \kern4em  \text{(a single cone) in } \leftcat{(l\downarrow \calL)}   \\   & \smash{   \lower2ex{   \rightcat{  \llap{ \boxed{11} \; Q} \Bigg\downarrow  }   }    }      &&& && && \rightadj{ \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big) } \Big[\overline{\black G\lambda}\Big]  \rlap{  \; \rightadj{ \boxed{5 | 120} }  }  &&   \\             \hline              &&&  {} \rlap{   \text{(the $\rightcat Q$-image of (the above cone $\mu : k[\kappa] \Rightarrow  G$)) in $(l\downarrow \leftcat\calL)$ is (a cone $\mu\rightcat Q = \mu : k \Rightarrow G\rightcat Q$) in } \leftcat\calL,    }  \\     &&&  {} \rlap{  \text{thus there exists a unique mediating arrow $\boxed{   \textstyle \boxed{8}\; \bar\mu : k \to \rightadj{ (\black G\rightcat Q)\lim_{\leftcat\calL} }    }$ (not shown) in $\calL$}  }   \\     &&& {} \rlap{   \text{such that $\boxed{8}\; \bar\mu : \mu\rightcat Q \to {\rightadj\pi}_{\black G\rightcat Q}$  is a morphism of cones in $\leftcat\calL$}   }       \\  &&&&   & \boxed{6 \rightcat Q} & k & {} \rlap{ \kern-2em \xrightarrow [\kern20em] {\textstyle \mu \rightcat Q = \mu \kern1em \boxed{7 \rightcat Q}} } &&& \black G\rightcat Q \rlap{  \;  \boxed{ 2 | 12;\rightcat{11} }  }     \\    &  \llap{ \boxed{0} \; } \calL   &&&  & \llap{\kappa} \nearrow \rlap{   \kern-.5em { \text{$\leftcat\mu$ is} \atop \text{a cone in $\leftcat{(l\downarrow\calL)}$} }   }   && {} \rlap{ \kern0em \black G\lambda \nearrow \kern0em \boxed{2} \kern0em { \text{$\overline{\black G\leftcat\lambda}$ is an arrow} \atop \text{between cones in } \calL }   } && \rightadj{  \nearrow \rlap{ \pi_{\black G \rightcat Q} \; \boxed{3 | 21} }  } &  \kern4em  \rightadj{ \text{(a single, universal, cone) in } \leftcat\calL }    \\      &&& \kern0em &  \llap{ \boxed{0} \; } l & {} \rlap{ \kern-1em \xrightarrow [\textstyle \exists!\overline{\black G\lambda} \rlap{\; \boxed{4 | 32}}] {\kern15em} } &&& \rightadj{   (\black G\rightcat Q)\lim_{\leftcat\calL} \rlap{ \; \boxed{3 | 20} }   } && \\   \end{array} } } \]

To that end, let ($\leftcat{\boxed{6} \; k[\kappa]}$ be an object in $\leftcat{(l\downarrow \calL)}$), 
and ($\leftcat{\boxed{7}\; \mu : k[\kappa] \Rightarrow G}$ be a cone in $\leftcat{(l\downarrow \calL)}$).
Then ($\boxed{7 \rightcat Q}\; \mu \rightcat Q = \leftcat{\mu :  k \Rightarrow \black G\rightcat Q}$ is a cone in $\leftcat\calL$), 
so there is a unique (mediating arrow $\leftcat{   \boxed{  \textstyle  \boxed{8}\; \bar\mu : k \to  \rightadj{ (\black G\rightcat Q)\lim_{\leftcat\calL} }  }   }$) 
(not shown in the diagram) such that ($\leftcat{ \bar\mu : \mu \to \rightadj\pi }$ is a morphism of cones in $\leftcat\calL$). 
It remains to show ($\leftcat{ \bar\mu : k \to \rightadj{(\black G\rightcat Q)\lim_{\leftcat\calL}} }$ in $\leftcat\calL$) 
is (an arrow $\leftcat{ \bar\mu : k[\kappa] \to \rightadj{\big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)} \leftcat{\Big[\overline{\black G\lambda}\Big]} }$ in $\leftcat{(l\downarrow \calL)}$).
 Since $\leftcat{ \kappa\bar\mu \rightadj\pi = \kappa\mu = \black G\lambda = \overline{\black G\lambda}\rightadj\pi }$, 
the uniqueness clause in the universal property of $\rightadj\pi$ gives $\leftcat{ \kappa\bar\mu = \overline{\black G\lambda}}$, 
so $\leftcat{ \bar\mu : \mu \to \rightadj\pi}$ is an arrow in $\leftcat{ (l\downarrow \calL) }$
and $\leftcat{ \boxed{8'} \; \bar\mu : \mu \to \rightadj\pi }$ is a morphism of cones in $\leftcat{(l\downarrow \calL)}$ (see the diagram).
Further $\leftcat{ \bar\mu : k[\kappa] \to \rightadj{\big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)}\leftcat{[\overline{\black G\lambda}]} }$ in $\leftcat{(l\downarrow \calL)}$ 
is the unique arrow in $\leftcat{(l\downarrow \calL)}$ such that $\leftcat{\bar\mu} \rightadj\pi = \rightcat\mu$.
Thus $\rightadj{    \pi : \big((\black G \rightcat Q)\lim_{\leftcat\calL}\big) \leftcat{  \big[ \overline{\black G \lambda} \big) ]   } \Rightarrow \black G    }$ is a universal cone in $\leftcat{(l\downarrow \calL)}$.

In those circumstances $\leftcat{ G : \calJ \to (l\downarrow \calL) }$ 
has a limit $\rightadj{\pi : \big((\black G \rightcat Q)\lim_{\leftcat\calL}\big)\leftcat{  [ \overline{\black G \lambda} ]  } \Rightarrow \black G}$  in $\leftcat{(l\downarrow \calL)}$ 
which is preserved by the canonical forgetful functor $\leftcat{(l\downarrow \calL) \to \calL}$.

The above diagrams were internal to respectively $\leftcat\calL$ and $\leftcat{(l\downarrow \calL)}$.
There is an external diagram (in $\CAT$) that is useful in showing relations between the limits:
\[ \leftcat{ \begin{array} {} && 1 \\ & \llap{!} \nearrow & \red{ \Bigg\downarrow \rlap{ \kern-4em \boxed{\textstyle \big((GQ)\lim_{\leftcat\calL}\big)  \big[\bar\lambda\big]} } } &  \searrow \rlap{ (G\rightcat Q)\lim_{\leftcat\calL} }  \\      \calJ & \xrightarrow[\textstyle G]{\kern4em} & \boxed{(l \downarrow \calL)} &  \rightcat{ \xrightarrow[\textstyle Q = r]{\kern4em} }  & \calL  \\    \big\Vert  &&&&  \big\Vert   \\    \calJ &  {} \rlap{ \kern-2em \xrightarrow[\textstyle G\rightcat Q]{\kern17em} } &&& \calL\end{array}  }  \]




<hr />





For the adjoint functor theorems we need a two-category, or "relative," version of the above.
(The boxed numbers below are used in both the text and the diagrams.
They give a sense of the order in which various constructions are made.)
Thus we start with a functor $\rightadj{ \boxed{ {\leftcat\calL} \leftarrow {\rightcat\calR} : R \; \boxed{0} }  }$ 
from ($\rightcat{ \boxed{0} \calR} $, the "right category") (that is my terminology; I do not know how common that terminology is) 
to ($\leftcat{ \boxed{0} \calL }$, the "left category").
Given $\rightadj R$ and (an object $\leftcat{ \boxed{0|1} \; l \in \calL }$ in the left category $\leftcat\calL$),
we consider (the comma category $\leftcat{   \boxed{ \boxed{0|10} \; (l \downarrow {\rightadj R})}   }$) 
and its relations (in the 2-category $\CAT$) to several other entities:

\[   \leftcat{       \boxed{     \begin{array} {cccccc|cc}      &&  1  & \rightcat{ \boxed{3 | 20} }  & & \kern2em & \kern2em  &   &&  1  & \rightcat{ \boxed{3 | 20} } &   \kern2em    \\    &  \llap{!} \nearrow  &  \red{    \Bigg\downarrow \rlap{   \kern-2.5em \boxed{  \textstyle \leftcat G\lim_{ \leftcat{(l \downarrow {\rightadj R})} }  }   }    }   &  \rightcat{ \searrow \rlap{(\leftcat G Q)\lim_\calR} }  & &     &      &     &  \llap{!} \nearrow  &  \red{    \Bigg\downarrow \rlap{   \kern-2.5em \boxed{  \textstyle \leftcat G\lim_{ \leftcat{(l \downarrow {\rightadj R})} }  }   }    }   &  \rightcat{ \searrow \rlap{(\leftcat G Q)\lim_\calR} }  &     \\      \calJ  &  \xrightarrow[\kern1em \boxed{1 | 12} \kern1em]{\textstyle G}  &  \boxed{(l \downarrow {\rightadj R})} \rlap{  \lower3ex{ \kern-2.6em \boxed{0 | 10} }  }   &  \rightcat{ \xrightarrow[\kern1em \boxed{0 | 11} \kern1em]{\textstyle Q = r} }  &  \rightcat\calR    &     &      & \calJ  &  \xrightarrow[\kern1em \boxed{1 | 12} \kern1em]{\textstyle G}  &  \boxed{ (l \downarrow {\rightadj R}) } \rlap{  \lower3ex{ \kern-2.6em \boxed{0 | 10} }  }   &  \rightcat{ \xrightarrow[\kern1em \boxed{0 | 11} \kern1em]{\textstyle Q = r} }   &  \rightcat\calR    &     \\       &&   \Bigg\downarrow   & \llap{ \boxed{0 | 11} \;  \lambda }  \Bigg\Uparrow &  \rightadj{\Bigg\downarrow \rlap{ R \;  \boxed{0} }  } &   {} \rlap{\kern1em \cong}   &      &    {} \rlap{ \kern-2em { \textstyle\text{CWM} \atop \textstyle\text{Exercise V.6.3} }  }    &&   \Bigg\downarrow   &  \rightadj{  \llap{ \boxed{0 | 10} \; } \text{p.b.}  }   &  \rightadj{\Bigg\downarrow  \rlap{ R \;  \boxed{0} } }     \\   &&  1  & \xrightarrow[\smash{\textstyle \boxed{0 | 1} \; l}]{}   &  \calL   &       &       &   &&  \leftcat{(l \downarrow \calL)}  &  \rightcat{ \xrightarrow{} } &  \calL   \\    {} \rlap{\kern1em \text{CWM Lemma V.6, Exercise V.6.1} } &&&&&&&     {} \rlap{ \kern-2em { \textstyle\text{CWM} \atop \textstyle\text{Exercise V.1.1} }  }  &&  \Bigg\downarrow   &  \llap{ \boxed{0 | 11} \; \lambda } \Bigg\Uparrow &  \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }      \\   &&&&&&&&& 1  &  \xrightarrow[\textstyle \boxed{0 | 1} \; l]{}  &  \calL   \\  \end{array}     }       }    \]

Whereas the diagram above was (an external diagram, in $\CAT$), 
the diagrams below are (internal to the three categories).

\[ \leftcat{ \boxed{ \begin{array} {cccccc c|cccccc c|cccccc} &&& (l\downarrow \rightadj R) \; \boxed{10} \rlap{ \kern.5em \rightcat{ \xrightarrow[\kern28em]{\textstyle Q = r \; \boxed{11}} } } &&&&& &&  \rightcat{ \calR \; \boxed{0} } \rlap{  \kern.5em \rightadj{ \xrightarrow[\kern35em]{\textstyle R \; \boxed{0}} }  } &&&&&&&&&   \calL \; \boxed{0}    \\        \hline      & \forall \; \boxed{6 | 130} \; \rightcat r \leftcat{[\kappa]} & \rightcat{ {} \rlap{ \kern-1em \xrightarrow[ \textstyle \kern3em \text{a cone in } \leftcat{(l\downarrow \rightadj R)} \kern3em ]{\textstyle \forall \rho \; \boxed{7 | 131}} } } &&&   G\;\boxed{1 | 12}  & \kern1em & \kern1em & \boxed{6 \rightcat Q | 30}\;\rightcat{r} & \rightcat{   {} \rlap{  \kern-1em \xrightarrow[ \textstyle \kern2.5em \text{a cone in } \calR \kern2.5em ]{    \textstyle \rho Q = \rho\;\boxed{7Q | 31} }  }   } &&& G \rightcat{ Q \; \boxed{2} } & \kern1em & \kern1em &&&  \llap{ \boxed{6 \rightcat Q \rightadj R | 30 \rightadj R} \; } {\rightcat r}{\rightadj R} &  \rightcat{  {} \rlap{ \kern-3em \xrightarrow [\kern19em] {\textstyle \rho Q \rightadj R = \rho \rightadj R \; \boxed{7 \rightcat Q  \rightadj R | 31\rightadj R} } }  } &&&  G \rightcat{Q} {\rightadj R} \; \boxed{2\rightadj R}  & 8      \\          && \rightcat{ \llap{\exists! \; \boxed{8' | 132} \; \bar\rho} \searrow } && \rightcat{  \nearrow \rlap{ \pi_{\black G} \; \boxed{5 | 121} }  } & &&& & \rightcat{ \llap{\exists! \; \boxed{8 | 32} \; \bar\rho} \searrow } && \rightcat{  \nearrow \rlap{ \pi_{\black G\rightcat Q} \; \boxed{3 | 21} }  } &&&&    &     \llap{ \boxed{6\lambda} \; \kappa } \nearrow   &  \kern-1em { \text{$\rightcat\rho$ is a} \atop \text{cone in $\leftcat{ (l\downarrow{\rightadj R}) }$}  }  \kern1em   & \llap{\black G\lambda} \nearrow \rlap{ \boxed{2} } & { \text{$\overline{\black G\leftcat\lambda}$ is an arrow} \atop \text{between cones in $\leftcat\calL$} }   &   \rightadj{  \nearrow \rlap{ \pi_{\black G\rightcat Q} R  \; \boxed{\rightcat 3 R | 21 R} }  }  && \kern1em \rightadj{ \text{(a single, universal, cone) in } \leftcat\calL }      \\     &&& \rightcat{\big((\black G Q)\lim_\calR\big)}[\overline{\black G\lambda}] \rlap{  \; \rightadj{ \boxed{5 | 120} }  }  &&  && &&&    \rightcat{(\black G Q)\lim_\calR} \rlap{ \rightcat{\; \boxed{3 | 20} }  }  &&&&& l & {} \rlap{ \kern-1em \xrightarrow [ \textstyle \exists!\overline{\black G\lambda} \; \boxed{4 | 22} ] {\kern14em} } &&& \rightadj{ \big(\rightcat{(\black G Q)\lim_\calR}\big) R } \rlap{  \; \boxed{ \rightcat 3 \rightadj R | \rightcat{20} \rightadj R }  }    \\   \end{array} } } \] 

The following combines (an external diagram) with (four internal diagrams) in (one large display). 
The created limits are colored $\red{\text{red}}$.
\[   \boxed{   \begin{array} {c|ccccc|ccccccc|ccccc}  1&  \forall \; \boxed{6 | 130} \; {\rightcat r} \leftcat{[\kappa]} & {} \rightcat{  \rlap{ \kern-2em \xrightarrow[\kern26em]{\textstyle \forall\rho \; \boxed{7 | 131}} }  }   &&&  G = \rightcat{ (\black G Q) } \leftcat{ [{\black G} \lambda] } \; \boxed{1 | 12}  &  \kern0em  & &  &&  &&   && & \rightcat{\boxed{6Q | 30}} & \rightcat r & \rightcat{  {} \rlap{ \kern-1em \xrightarrow [\kern26em] { \textstyle \rho\rightcat Q \; \boxed{7Q | 31}} }  }   &&& \black G\rightcat Q \rlap{\; \rightcat{\boxed{2}}}  & \kern2em    \\           2&  & \leftcat{  \llap{ \exists! \; \boxed{8' | 132} \; \bar\rho} \searrow  }    &    &  \rightadj{  \nearrow \rlap{\pi_{\black G} \; \rightcat{\boxed{3' | 121}} }  }   &&&   \rightcat{ {} \rlap{   \xrightarrow[\textstyle \kern8em \boxed{0 | 11} \kern8em]{\textstyle Q = r} }   }    &  &&  &&  && & & &  \rightcat{ \llap{ \boxed{8 | 32} \; \exists!\overline{\rho Q} } \searrow  }   &   &   \rightcat{ \nearrow \rlap{\pi_{\black G\rightcat Q} \; \boxed{3 | 21} } } &    \\         3&   &&     \smash{ \raise7ex{    \red{ \boxed{  \textstyle \text{limit in } \leftcat{ (l \downarrow {\rightadj R}) } \over {  \textstyle {\black G}\lim_{ \leftcat{ (l \downarrow {\rightadj R}) }  }   =    \atop \textstyle \rightcat{ \big    ((\black G Q)\lim_\calR\big) } \leftcat{ \Big[\overline{\black G \lambda}\Big] }  }   }    }     }      }     & \rightadj{ \boxed{5 | 120} }  &&&&  &&&&     & & & &&&   \smash{     \raise4ex{  \rightcat{  \boxed{ \textstyle \text{limit in } \calR  \over \textstyle (\black G\rightcat Q)\lim_\calR = \leftcat l\leftadj L  }   }    }     }    &  \rightcat{\boxed{3 | 20}}  &       \\    \hline   4&   &&   \leftcat{ (l \downarrow {\rightadj R}) }   &   &&&  \calJ  &  \xrightarrow[\smash{\textstyle \kern1em \boxed{1 | 12} \kern1em}]{\textstyle G}  &  \leftcat{ (l \downarrow {\rightadj R}) } \rlap{   \smash{  \lower3ex{ \kern-2.5em \boxed{0 | 10} }  }   }  & \rightcat{ \xrightarrow[\textstyle \kern1em \boxed{0 | 11} \kern1em]{\textstyle Q = r} } & \rightcat\calR    & & & & &&&   \rightcat\calR  &&       \\      5&   &&  \Bigg\downarrow  &&&&   &&  \leftcat{ \llap ! \Bigg\downarrow }  &  \leftcat{ \llap{\boxed{0 | 11} \; \lambda} {\Bigg\Uparrow} }  &  \rightadj{  \Bigg\downarrow \rlap{ R \; \boxed{0} }  }  &&&&&&&    \rightadj{  \Bigg\downarrow \rlap{ R \; \boxed{0} }  }    \\   6&  && \leftcat{ (l \downarrow \calL) }   &&&& && 1 & \leftcat{ \xrightarrow[\textstyle \boxed{0 | 1} \; l]{} } & \leftcat\calL && & && &&  \leftcat\calL   &  \\   \hline   7&   \forall \; \boxed{6' | 130'} \; \leftcat{  ({\rightcat r}{\rightadj R}) [\kappa]  } & {} \rightcat{  \rlap{ \kern-1em \xrightarrow[\kern27em]{\textstyle \forall\rho \; \boxed{7 | 131} }  }  }   &&&  \leftcat{    (\black G\rightcat Q\rightadj R) [{\black G} \lambda] \rlap{\; \boxed{2 | 11}}    }  & &&& &&&&&& \leftcat{  \boxed{ \rightcat{6Q}\rightadj{R} | \rightcat{30}\rightadj{R} }  } & \rightcat r\rightadj R & {} \rlap{   \kern-1em \xrightarrow [\kern25em] {  \textstyle \rightcat{\rho Q}\rightadj R \; \boxed{ \rightcat{7Q}\rightadj R | \rightcat{31}\rightadj R }  }   }   &&& \black G\rightcat Q\rightadj R \rlap{\; \leftcat{\boxed{2 \rightadj{R}}}}     \\       8&      & \leftcat{   \llap{  \exists! \; \boxed{ {8'\rightadj R | 32 \rightadj R} } \; {\bar\rho}'  } \searrow   }   &&  \rightadj{    \nearrow  \rlap{    {\rightcat\pi}_{\black G\rightcat Q} \rightadj R \; \leftcat{  \boxed{ {\rightcat 3 \rightadj R | \rightcat{21} \rightadj R} }  }   }    }    &&&  \rightcat{ {} \rlap{   \xrightarrow [\textstyle \kern8em \boxed{0 | 11} \kern8em] {\textstyle Q = r} }   } & && && && & \leftcat{ \llap{\boxed{6\lambda} \; \kappa} \nearrow } & \leftcat{ {} \rlap{ \kern0em \black G\lambda \nearrow \kern0em \boxed{2 | \black G 11} } } &&& \rightcat{    \nearrow \rlap{   \rightcat{ \pi_{\black G Q} }  \rightadj{R} \; \leftcat{ \boxed{ \rightcat{3}\rightadj{R} | \rightcat{21}\rightadj R }  }   }    } &   \\    9&         && \smash{ \raise2ex{    \red{ \boxed{  \textstyle \text{limit in } \leftcat{ (l \downarrow \calL) } \over { \textstyle \leftcat{   \Big( \rightcat{\big((\black G Q)\lim_\calR\big)} {\rightadj R} \Big)  } \leftcat{\Big[\overline{\black G \lambda}\Big]} }   }    }     }      }        & \rightadj{ \boxed{5' | 120'} }  &&&& && && \kern1em & \kern1em & \leftcat{ \llap{\boxed{0 | 1}\;} l } & \leftcat{ {} \rlap{ \kern-1em \xrightarrow [ \textstyle \exists!\overline{\black G\lambda} \kern1em \boxed{4 | 32} ] {\kern9em} } } &&&  \smash{     \raise0ex{  \leftcat{  \boxed{ \textstyle \text{limit in } \calL  \over \textstyle  \rightcat{  \big((\black G\rightcat Q)\lim_\calR\big) \rightadj R  } = \leftcat l\leftadj L\rightadj R}   }    }     }   & \leftcat{  \boxed{ \rightcat 3\rightadj R | \rightcat{20}\rightadj R }  }  &  \\   \end{array}  }  \]

Now suppose we have a functor $\boxed{ \boxed{1 | 12} \; G : \calJ \to \leftcat{(l \downarrow {\rightadj R})} }$ (see the center diagram in the large display above).
We form the components of $\boxed{1 | 12} \; G$ by composition, namely
a functor $\rightcat{  \boxed{ \boxed{2} \; {\black G}Q : {\black\calJ} \to \calR }  }$ into $\rightcat\calR$, and
a natural transformation (a cone) $\leftcat{  \boxed{ \boxed{2} \; {\black G}\lambda : l \Rightarrow {\black G}{\rightcat Q}{\rightadj R} : {\black\calJ} \to \calL }  }$ in $\leftcat\calL$.
Suppose now that (the functor $\rightcat{ \boxed{2} \; {\black G}Q : {\black\calJ} \to \calR}$) has
a limiting cone $\rightcat{   \boxed{  \textstyle  \boxed{3 | 21} \; \pi_{\black G Q} : {  \boxed{3|20} \; ({\black G}Q)\lim_\calR  } \Rightarrow {\black G} Q : {\black\calJ} \to \calR   }   }$ in $\rightcat\calR$ (at the upper right of the above large display),
and that (that limiting cone in $\rightcat\calR$) is preserved by $\rightadj R$ (so we are now in the lower right of the above display).
Then there exists a unique (mediating arrow $\leftcat{   \boxed{\textstyle  \boxed{4 | 22} \; {\overline{{\black G}\lambda}} :  l \to \rightadj{ \big(\rightcat{(\black G Q)\lim_\calR}\big) R }  }   }$ in $\leftcat\calL$),  
which is also (a <u>morphism of cones in $\leftcat\calL$</u>)
$\leftcat{    \boxed{  \boxed{4 | 22} \;{\overline{{\black G}\lambda}} : {\black G}\lambda \to {  \rightcat{ \pi_{\black G Q}  }  }{\rightadj R} }    }$ (in the lower right of the display).
But, and here is a crucial but somewhat tricky, perhaps subtle, point, 
(that same data) may.be viewed as (<u><i>a single cone</i> in $(l\downarrow \rightadj R)$</u>)
$\rightadj{  \boxed{\textstyle \boxed{5 | 121} \; \pi_{\black G} : \boxed{5|120} \; \rightcat{\big((\black G Q)\lim_\calR\big)} \leftcat{[\overline{\black G \lambda}]} \Rightarrow \leftcat{ G  :  \calJ \to (l\downarrow \rightadj R) }  }   }$ (shown at the upper left of the above display).
Thus the same arrow $\leftcat{   \boxed{\textstyle  \boxed{4 | 22} \; { \overline{{\black G}\lambda} }  }   }$ plays three different roles:

mediating arrow $\leftcat{   \boxed{\textstyle  \boxed{4 | 22} \; {\overline{{\black G}\lambda}} :  l \to \rightadj{ \big(\rightcat{(\black G Q)\lim_\calR}\big) R }  }   }$ in $\leftcat\calL$

morphism of cones $\leftcat{ \boxed{     \textstyle  \boxed{4 | 22} \; {  \overline{ {\black G}\lambda }  } : \leftcat l [{\black G}\lambda] \to  \Big(  \rightadj{ \big( \rightcat{(\black G Q)\lim_\calR} \big) R }  \Big) [{ \rightcat{ \pi_{\black G Q} } }{\rightadj R} ] }    }$ in $(\Delta \downarrow \ulcorner G\rightcat Q\rightadj R\urcorner)$

a component of the object $ \rightadj{  \boxed{     \textstyle  \boxed{120} \; \rightadj{ \big( \rightcat{(\black G Q)\lim_\calR} \big) }   \leftcat{  \big[ \, \overline{\black G \lambda} \, \big]  }    }     } $  in $\leftcat{  (l \downarrow \rightadj R)  }$

<hr />

Same data but different notation:

\[ \leftcat{ \begin{array} {} && 1 \\ & \llap{!} \nearrow & \red{ \Bigg\downarrow \rlap{ \kern-2.8em \boxed{(G_i[\lambda_i])\lim} } } & \rightcat{ \searrow \rlap{ G_i\lim } }      \\         \calJ & \xrightarrow[\kern3em]{\textstyle {\rightcat G}_i[\lambda_i]} & \boxed{(l \downarrow {\rightadj R})} & \rightcat{ \xrightarrow[\kern3em]{\textstyle Q = r} } & \rightcat\calR \\ && \Bigg\downarrow & \buildrel \textstyle \lambda \over \Longrightarrow & \rightadj{\Bigg\downarrow \rlap R} \\ && 1 & \xrightarrow[\textstyle l]{} & \calL \\ \end{array} } \]

\[ \leftcat{ \boxed{ \begin{array} {cccccc c|cccccc c|cccccc} {} \rlap{ \kern7em (l\downarrow \rightadj R) \kern.5em \rightcat{ \xrightarrow[\kern20em]{\textstyle Q = r} } } &&&&& && {} \rlap{ \kern6em \rightcat\calR \kern.5em \rightadj{ \xrightarrow[\kern27em]{\textstyle R} } } &&&&&&& {} \rlap{ \kern11em \calL }     \\    \hline & \forall \rightcat r[\kappa] & \rightcat{ {} \rlap{ \kern-1em \xrightarrow[\kern12em]{\textstyle \forall \rho_i} } } &&& {\rightcat G}_i[\lambda_i] & \kern1em & \kern1em & \rightcat{\forall r} & \rightcat{ {} \rlap{ \kern-1em \xrightarrow[\kern10em]{\textstyle \forall \rho_i} } } &&& \rightcat{ G_i} & \kern1em & \kern1em &&& {\rightcat r}{\rightadj R} & \rightcat{ {} \rlap{ \kern-1em \xrightarrow [\kern11em] {\textstyle \rho_i \rightadj R } } } &&& \rightcat{G_i} {\rightadj R} & \\ && \rightcat{ \llap{\exists!\rho} \searrow } && \rightcat{ \nearrow \rlap{\pi_i} } & &&& & \rightcat{ \llap{\exists!\rho} \searrow } && \rightcat{ \nearrow \rlap{\pi_i} } &&&&& \llap{\kappa} \nearrow && \llap{\lambda_i} \nearrow && \rightcat{ \nearrow \rlap{\pi_i \rightadj R} } \\ &&& \rightcat{ G_i\lim}[\lambda] && && &&& \rightcat{G_i\lim} &&&&& l & {} \rlap{ \kern-1em \xrightarrow [\textstyle \exists!\lambda] {\kern8em} } &&& \rightcat{G_i\lim}\rightadj R \\ \end{array} } } \] 
We start with a functor ${\rightcat G_i[\leftcat\lambda_i]} : \calJ \to \leftcat{(l\downarrow {\rightadj R})}$, so $\rightcat{ G : \calJ \to \calR}$ is a functor landing in $\rightcat\calR$, while $\{ \leftcat{ \lambda_i : l \rightarrow {\rightcat G_i \rightadj R} } \}_{i\in\calJ}$ is a cone in $\leftcat\calL$.
Suppose $\rightcat G$ has a.limit $\rightcat{\pi_i : G\lim \to G_i}$ in $\rightcat\calR$ which is preserved by $\rightadj R$.
In these circumstances the limit $\rightcat{\pi_i : G\lim \to G_i}$ in $\rightcat\calR$ lifts to a limit in $\leftcat{(l\downarrow \rightadj R)}$.


\[ \leftcat{ \boxed{ \begin{array} {ccccccc c|cccccc c|cccccc} {} \rlap{ \kern8em \calL \kern8em \rightadj{ \xleftarrow[\kern4em]{\textstyle R} } } &&&&&&&&& {} \rlap{ \kern5em \rightcat{ \calR \kern5em \xleftarrow[\kern4em]{\textstyle Q = r} } } &&&&&&& {} \rlap{ \kern4.5em (l\downarrow \rightadj R) } &&&&& test \\ \hline && {\rightcat r}{\rightadj R} & \rightcat{ {} \rlap{ \kern-1em \xrightarrow [\kern11em] {\textstyle \rho_i \rightadj R } } } &&& \rightcat{G_i} {\rightadj R} & \kern1em & \kern1em & \rightcat{\forall r} & \rightcat{ {} \rlap{ \kern-1em \xrightarrow[\kern10em]{\textstyle \forall \rho_i} } } &&& \rightcat{ G_i} & \kern1em & \kern1em & \forall \rightcat r[\mu] & \rightcat{ {} \rlap{ \kern-1em \xrightarrow[\kern12em]{\textstyle \forall \rho_i} } } &&& {\rightcat G}_i[\lambda_i] & test \\ & \llap{\kappa} \nearrow && \llap{\lambda_i} \nearrow && \rightcat{ \nearrow \rlap{\pi_i \rightadj R} } & &&& & \rightcat{ \llap{\exists!\rho} \searrow } && \rightcat{ \nearrow \rlap{\pi_i} } &&& && \rightcat{ \llap{\exists!\rho} \searrow } && \rightcat{ \nearrow \rlap{\pi_i} } && test \\ l & {} \rlap{ \kern-1em \xrightarrow [\textstyle \exists!\lambda] {\kern8em} } &&& \rightcat{G_i\lim}\rightadj R && &&& && \rightcat{G_i\lim} &&& && && \rightcat{ G_i\lim}[\lambda] &&& test \\ \end{array} } } \] 

<hr />
<h3>References</h3>
Kelly 1989 "Elementary observations on 2-categorical limits"
https://doi.org/10.1017%2FS0004972700002781


Below this line is just excess material, basically earlier draft stuff that I am keeping around in case I want to use them again.
<hr />
---------------------

\[ \leftcat{ \boxed{ \begin{array} {cc|ccc|cccc} \calJ \rlap{ \xrightarrow[\kern4.5em \boxed{12} \kern4.5em] {\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} }   } & \kern0em & \kern0em & (l\downarrow\calL)  \rlap{  \lower3.2ex{ \kern-2.3em \boxed{10} }  }   \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern3.6em \boxed{11} \; \text{faithful} \kern3.6em ]{\textstyle Q=r} } } & & & & &\calL &   \\      \\      \hline j &&& j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda] &&&&& j\black G\rightcat Q \\ &&& &&&& \llap{j \black G \lambda} \nearrow & \\ \llap\iota \Bigg\downarrow &&& \llap{\iota \black G = {} } \Bigg\downarrow \rlap{ {} = \iota \black G \rightcat Q } & && l & \iota \black G & \Bigg\downarrow \rlap{\iota \black G \rightcat Q} & \\ &&&& && & \llap{j' \black G \lambda} \searrow & \\ j' &&& j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda] &&&&& j' \black G\rightcat Q \\ \end{array} } } \]