Kelly ECT displayed formulae and diagrams

PRELIMINARY DRAFT --- CUSTOMIZED, NON-STANDARD

This is just a beginning on that project. 

Currently only a few selected formulae and diagt are listed. Also some of the Kelly's words have been included.

The formulae are not exactly what Kelly wrote in ECT. I have transformed them somewhat. 

\begin{align} \boxed{\int_{A\in\calA} \hom A T A} & {\mkern2em} \xrightarrow{\text{equalizer}} {} & \prod_{A\in\calA} \hom A T A  & {\mkern2em} \mathop\rightrightarrows\limits^\rho_\sigma {} & \prod_{A,A'\in\calA} [ \hom A \calA {A'}, \hom A T {A'} ] \\ & \mkern2em  \llap{\boxed{\lambda_A}} \searrow & \downarrow \rlap{\text{proj}_A} \\ && \hom A T A \tag{2.2} \end{align}

\begin{gather} \Big[X, \int_{A\in\calA} \hom A T A \Big] \xrightarrow{\textstyle [X,\lambda_A]} [X, \hom A T A] \text{ makes its source the end of lts targets, inducing}\\ \Big[ X, \int_{A\in\calA} \hom A T A \Big] \cong \int_{A\in\calA} [X, \hom A T A ] \tag{2.3} \end{gather}

\[ \int_{(A,B)\in\calA\tensor\calB} \hom {A,B} T {A,B} \cong \int_{B\in\calB} \int_{A\in\calA} \hom {A,B} T {A,B} \tag{2.8} \]

\begin{align} \boxed{\hom T {[\calA,\calB]} S} & \mkern2em \cong & \int_{A\in\calA} \hom {AT} \calB {AS} & {\mkern2em} \xrightarrow{\text{equalizer}} & \prod_{A\in\calA} \hom {AT} \calB {AS}  & {\mkern2em} \mathop\rightrightarrows\limits^\rho_\sigma  & \prod_{A,A'\in\calA} [ \hom A \calA {A'} , \hom {AT} \calB {A'S}  ] \\ &  \mkern2em \llap{\boxed{E_A}} \searrow & \downarrow \rlap{\text{proj}_A}  \mkern1em \\ && \hom {AT} \calB {AS} \tag{2.10} \end{align}

\[\big[ X, \hom T {[\calA,\calV]} S \big] \cong \hom T {[\calA,\calV]} {[X,S]} \tag{2.13} \]

Given a $\calV$-functor $\boxed{F:\calA\to\calV}$ and an object $\boxed K$ of $\calA$ as in 1.9, 

we have the map (arrow in $\calV_0$) $\hom K F A : \hom K \calA A \to [F_K,F_A]$, 

which is.$\calV$-natural in $A$ by 1.8(b).

The transform \[ \phi_A : F_K \to [\hom K \calA A, F_A] \tag{2.30} \] of $\hom K F A$ under the (symmetry) adjunction $\hom X {\calV_0} {[Y,Z]} \cong \hom Y {\calV_0} {[X,Z]}$

is ($\calV$-natural in $A$) by 1.8(m).

(The stronger Yoneda lemma) is 

the assertion that (2.30) expresses $F_K$ as the end $ \boxed{\textstyle \int_A [\hom K \calA A, F_A]}$, 

so that we have an isomorphism (natural in $K$) \[\boxed{ \phi : F_K \cong \hom {\hom K \calA -} {[\calA,\calV]} F }. \tag{2.31} \]

$F_K$ was a single-variable functor; Kelly generalizes to a functor $\hom C P K$ of two variables in the (natural in the "extra" variable $C$, as well as in $K$):

\[ \boxed{ \phi = \hom C \phi K : \hom C P K  \cong \hom {\hom K \calA -} {[\calA,\calV]} {\hom C P -} } \tag{2.33} \]

\begin{align} \boxed{\hom B \calB {\{\hom K \calK - , G\}}} & \mkern2em \mathop\cong\limits^{(3.1)} & \hom {\hom K \calK -} {[\calK,\calV]} {\hom B \calB G} && \Rule 2px 3ex 1ex && \boxed{\hom {(\hom - \calK K * G)} \calB B} & \mkern2em \mathop\cong\limits^{(3.5)} & \hom {\hom - \calK K} {[\calK\op,\calV]} {\hom G \calB B}  \\ &&  {\wr\Vert} \rlap {(2.33) \text{ Yoneda}} \mkern2em && \Rule 2px 3ex 1ex && && \mkern3em {\wr\Vert} \rlap {(2.33) \text{ Yoneda}} \mkern2em \\ &&  \boxed{\hom B \calB {G_K}} \mkern2em && \Rule 2px 3ex 1ex && && \boxed{\hom {G_K} \calB B} \mkern2em \tag{3.10} \end{align}

\begin{align} \hom C Q {\{F,G\}} & \mathop\cong\limits^{Q \text{ preserves}}_{\text{limit}} & {\{F,\hom C Q G\}} & \mathop\cong\limits^{ (3.7)} & \hom F {[\calK,\calV]} {\hom C Q G} \\ \llap{\text{defn of $T$ }} {\wr\Vert} \\ \boxed{\hom C \calC {\{F,G\}T}} &&&& {\wr\Vert} \rlap{\text{ defn of $T$}}  \\ \\ \boxed{\hom C \calC {\{F,GT\}}} && \mathop\cong\limits^{(3.1)} && \hom F {[\calK,\calV]} {\hom C \calC {GT}} \tag{3.15} \end{align}

Kelly ECT on limits and colimits

We begin by considering the most classical case, that of conical limits for (categories enriched in a <i>cartesian closed base category</i> $\calV$). This encompasses both (the case $\calV = \Set$ considered by Kelly in section 3.4 of ECT, i.e. ordinary or "mere" category theory), and (the case $\calV = \bftwo$, so important to Boolean logic and basic mathematics (where it yields infima and suprema)). Recall that for $\calV = \Set$, (the unit object $I$ is $1$, the (a) one-element set), while for $\calV = \bftwo$ (it is $\top$, the object representing "true").

When ($\calV$ is cartesian closed), then for any ($\calV$-category $\calK$) and any (object $B$ of another $\calV$-category $\calB$) there is a unique (constant functor $B\Delta : \calK \to \calI \to \calB$). See section 3.9 for a discussion of this. In particular, $I \in \calV$ determines $I\Delta : \calK \to \calV$.

We recall a fundamental isomorphism (1.26): $\boxed{i: X \cong [I,X]}$, which is natural in $X \in \calV$.

 Next we introduce the basic ingredients for the limit or colimit: (an indexing category $\calK$), (a target category $\calB$), and a functor $\boxed{G: \calK \to \calB}$.

Then we have (the following proof of (3.29)) 

\[\begin{array} {} \text{comment} &&& \text{internal} && \text{weighting} \\  &&& X & \mathop\cong\limits^i & [I,X] \rlap{\mkern2em X\in\calV} \\ \text{individual hom object} &&& \hom B \calB {G_K} & \mathop\cong\limits^i & [I,\hom B \calB {G_K}] \\ \text{cones in $\calB$  }  & \int_{K\in\calK} \hom B \calB {G_K} & \mathop\equiv\limits^{(2.10)} & \hom {B\Delta} {[\calK,\calB]} {G} & \mathop\cong\limits^{(3.24)} &  \hom {I\Delta} {[\calK,\calV]} {\hom B  \calB G} & \mathop\cong\limits^{\text{(3.1)}} & \boxed{\hom B \calB {\{I\Delta,G\}}}   \\ (3.25) \text{ defn of $\lim$ } &&&  {\wr\Vert} \\  &&& \boxed{\hom B \calB {(G\lim)}} && {\wr\Vert} \rlap{\, (3.25) \text{ defn of $\lim$}} \\  \text{To Be Proved: }(3.29) \\  &&&  \boxed{(\hom B \calB G)\lim} & \mathop\cong\limits^i & \hom I \calV {\big((\hom B \calB G)\lim\big)} \\  \end{array}\]

The composite of the last two isomorphisms (going clockwise) is (3.28); the total composite of all four isomorphisms (not counting (3.1)) is (3.29).  Note that, per the third paragraph of section 1.6, $\hom X \calV Y$ and $[X,Y]$ both denote the same object of $\calV$. Note that the composite of the left  isomorphism and both of the top isomorphisms implies (3.26): $G\lim \mathop\cong\limits^{\text{(3.26)}} \{I\Delta, G\}$ (for a cartesian closed base category $\calV$).

A key definition in basic mathematics is a special case of the above. Specifically, let $\calV = \bftwo$, so $I=\top$, and consider $\boxed{a:\N\to\R : n \mapsto a_n}$, where ($\N$ is the natural numbers considered as a discreet $\bftwo$-caregory), while ($\R$ is the real numbers with their usual ordering, considered also as a $\bftwo$-category). I.e. we are considering a sequence of real numbers as a $\bftwo$-functor.

Here we specialize (the names of the variables) in (the general $\calV$-cat situation) to (the above special case).

\[\begin{array} {} \text{internal} && \text{weighting} \\  X & \mathop\cong\limits^i & [\top,X] \rlap{\mkern1em X\in\calV=\bftwo} \\  \hom x \R {a_n} & \mathop\cong\limits^i & [\top,\hom x \R {a_n}] \\ \llap{\text{cones, i.e. lower bounds, in $\R$   } \mkern1em }  \hom {x\Delta} {[\N,\R]} {a} & \mathop\cong\limits^{(3.24)} &  \hom {\top\Delta} {[\N,\bftwo]} {\hom x  \R a} & \mathop\cong\limits^{\text{(3.1)}} & \boxed{\hom x \R {\{\top\Delta,a\}}}   \\ \llap{(3.25) \text{ defn of $\lim$ }}  {\wr\Vert} \\  \boxed{\hom x \R {(a\lim)}} && {\wr\Vert} \rlap{\, (3.25) \text{ defn of $\lim$}} \\  \llap{\text{To Be Proved: }(3.29)} {} \\   \boxed{(\hom x \R a)\lim} & \mathop\cong\limits^i & \hom \top \bftwo {\big((\hom x \R a)\lim\big)} \\  \end{array}\]

Here we go a step further and translate (the operators) from (those used in category theory) to (those used in basic math).

\[\begin{array} {} \text{comment} & \text{basic math} & \text{categorical} && \text{weighting} \\ X\in\calV=\bftwo && X & \mathop\cong\limits^i & [\top,X]  \\ \text{individual inequality or hom object} &  x \le a_n & \hom x \R {a_n} & \mathop\cong\limits^i & [\top,\hom x \R {a_n}] \\ \text{$x$ is a lower bound for $a$} & \boxed{(\forall n\in \N) (x \le a_n)} & \hom {x\Delta} {[\N,\R]} {a} & \mathop\cong\limits^{(3.24)} &  \hom {\top\Delta} {[\N,\bftwo]} {\hom x  \R a} & \mathop\cong\limits^{\text{(3.1)}} & \boxed{\hom x \R {\{\top\Delta,a\}}}  \\ (3.25) \text{ defn of infimum / limit }  & \Updownarrow &  {\wr\Vert} \\ & \boxed{x \le (a \inf)} &  \boxed{\hom x \R {(a\inf)}} && {\wr\Vert} \rlap{\, (3.25) \text{ defn of $\lim$}} \\ \text{To Be Proved: }(3.29)  \\  && \boxed{(\hom x \R a)\lim} & \mathop\cong\limits^i & \hom \top \bftwo {\big((\hom x \R a)\lim\big)} \\  \end{array}\]

There is also a "dual" version of the above that applies to colimits and suprema. Here we only show the general version:

\[\begin{array} {} \text{comment} &&& \text{internal} && \text{weighting} \\  &&& X & \mathop\cong\limits^i & [I,X] && X\in\calV \\ \text{individual hom object} &&& \hom {G_K} \calB B & \mathop\cong\limits^i & [I, \hom {G_K} \calB B ] \\ \text{cocones in $\calB$ }  & \int_{K\in\calK} \hom {G_K} \calB B & \mathop\equiv\limits^{(2.10)} & \hom G {[\calK,\calB]} {B\Delta} & \mathop\cong\limits^{(3.24)} &  \hom {I\Delta} {[\calK\op,\calV]} {\hom G  \calB B} & \mathop\cong\limits^{\text{(3.5)}} & \boxed{\hom {(I\Delta * G)} \calB B}  \\ (3.25) \text{defn of colimit } &&&  {\wr\Vert} \\ &&& \boxed{\hom {(G\colimit)} \calB B} && {\wr\Vert} \rlap{\, (3.25) \text{ defn of $\lim$}} \\  \text{To Be Proved: }(3.29) \\  &&&  \boxed{(\hom G \calB B)\lim} & \mathop\cong\limits^i & \hom I \calV {\big((\hom G \calB B)\lim\big)} \\    \end{array}\]

(3.29) has the following significant interpretation. The hom functor $\hom - \calB -$ is continuous in both its variables. I.e. $\hom B \calB -$ takes (limits in $\calB$) to (limits in $\calV$), while $\hom - \calB B$ takes (colimits in $\calB$) (i.e. limits in $\calB\op$) to (limits in $\calV$). (3.29) shows (this to be true for conical limits when $\calV$ is cartesian closed), but in fact (it is true for not merely conical limits but also the more general weighted limits, for a wide range of base categories $\calV$). See (3.8).  Thus we have <em>necessary</em> conditions for $\calV$-valued functors to be representable. The "Representablity Theorems" identify conditions which, when added to continuity, ensure representablity.

(3.29) is Theorem V.4.1 in Mac Lane's CWM, which works at the level of individual cones and arrows, i.e. elements of hom sets, rather than at the level of hom sets. I find the proof at the level of hom sets clearer, and also more capable of generalization, but both are instructive.

========

Here we present a summary of the weighted limit situation. On the right of the display below is a proof of (3.7) for $\calV$-functors $F,G : \calK \to \calV$. On the left we use (3.7) for ($F$ and $\hom B \calB G$) to get (3.8).

\[\begin{array} {} & \boxed{\hom B \calB {\{F,G\}}} & \mathop\cong\limits^{(3.1)} & \hom F {[\calK,\calV]} {\hom B \calB G} &  \mkern5em & \Rule {2px} {3ex} {1ex}  & & \big[ X, \boxed{\hom F {[\calK,\calV]} G} \big] & \mathop\equiv\limits^{(2.10)}  & \big[ X, \int_K  [F_K,G_K] \big] & \xrightarrow{[X,\lambda_K]} & \big[ X, [F_K,G_K] \big] \\  \text{TBP } (3.8) & &&  {\wr\Vert} \rlap{(3.7) \text{ for } F, \hom B \calB G } && \Rule {2px} {3ex} {1ex}  & \text{TBP } (3.7) &&& \wr\Vert \rlap{(2.3)} && \Vert \\   &&& \boxed{\{F, \hom B \calB G\}} && \Rule {2px} {3ex} {1ex} & & \big[ X, \boxed{\{F,G\}} \big] && {\displaystyle \int_K} \big[ X, [F_K,G_K] \big] & \xrightarrow{\lambda_K} & \big[ X, [F_K,G_K] \big] \\   &&&&& \Rule {2px} {3ex} {1ex} & &  \wr\Vert \rlap{(3.1)}  && \wr\Vert \rlap{\text{sym}} && \wr\Vert \rlap{\text{sym}}  \\ &&&&& \Rule {2px} {3ex} {1ex} & & \hom F {[\calK,\calV]} {[X,G]} & \mathop\equiv\limits^{(2.10)} & {\displaystyle \int_K} \big[ F_K, [X,G_K] \big] & \xrightarrow{\lambda_K}  & \big[ F_K, [X,G_K] \big] \\  \end{array}\]

Thus $\hom B \calB -$ preserves not merely conical limits, but weighted limits, and this for a general base category $\calV$ meeting the requirements spelled out in the earlier sections of ECT.

It remains to prove (2.3), which applies to any $\calV$- bifunctor $T : \calK\op, \calK \to \calV$ (the above was the case  $T= [F,G]$, i.e. $\hom K T L = [F_K,G_L]$). For arbitrary $X,Y \in \calV$, the horizontal arrows shown below are in bijection, natural with respect to $Y$ and $X$:

\[\begin{array} {} Y & \longrightarrow & [X, \hom K T K] \\ Y \tensor X & \longrightarrow & \hom K T K \\ \Vert && \uparrow \rlap{\lambda_K} \\  Y \tensor X & \longrightarrow & \int \hom K T K \\ Y & \longrightarrow & [X, \int \hom K T K] \\ \end{array}\]

In the above, (the integal signs) represent (ends as in ECT $\S$ 2.1). (The arrows going into targets WITHOUT an integral sign) represent (extranatural transformations as in ECT $\S$ 1.7). (The arrows having targets WITH an integral sign) are merely (arrows in $\calV_0$). (The vertical arrow $\lambda_K$) is (the universal arrow of the end) and mediates (one of the bijections); (the other two bijections) are mediated by (the monoidal closed structure of $\calV$).

===========

The ingredients for the following ((3.16) etc.) are: \begin{align} \calK \xrightarrow[\kern3em]{F} \calV & \kern2em & \calK\tensor\calA & \xrightarrow[\kern3em]{P} & \calB &\kern2em & \calA \xrightarrow[\kern3em]{H} \calB \\ && \calK & \xrightarrow[\kern3em]{G} & [\calA,\calB] \end{align}

\begin{align} \boxed{\hom H {[\calA,\calB]} {\{F,G\}}} && \boxed{\hom F {[\calK,\calV]} {(\hom H {[\calA,\calB]} G)}} & \mathop\equiv\limits^{(2.10)^2} & \int_K \big[ F_K, {\textstyle\int_A}\, \hom {H_A} \calB {(P_{K,A})} \big] & \xrightarrow[\mkern3em]{\lambda_K} & \big[ F_K, {\textstyle\int_A}\, \hom {H_A} \calB {(P_{K,A})} \big] & \xrightarrow[\mkern3em]{[F_K, \lambda_A]} & \big[ F_K, \hom {H_A} \calB {(P_{K,A})} \big] \\ \llap{(2.10)} {\vert\kern-.1em\Vert} &&&&  \llap{\int_K (2.3)} {\wr\Vert}\rlap{\text{ for $F_K$ and $\textstyle \int_A$}} && \llap{(2.3)} {\wr\Vert} \rlap{\text{ for $F_K$ and $\textstyle \int_A$}} && \Vert \\ \int_A \hom {H_A} \calB   {\{F,G\}_A} &&&& \int_K \int_A \big[ F_K, \hom {H_A} \calB {(P_{K,A})} \big] & \xrightarrow[\mkern3em]{\lambda_K} & \int_A \big[ F_K, \hom {H_A} \calB {(P_{K,A})} \big]  & \xrightarrow[\mkern3em]{\lambda_A} & \big[ F_K, \hom {H_A} \calB {(P_{K,A})} \big]  \\ \llap{(3.16)}{\vert\kern-.1em\Vert} &&&& \llap{(2.9)} {\wr\Vert} \rlap{\text{Fubini}} &&&& \Vert \\ \int_A \hom {H_A} \calB {\{F,P_{(-A)}\}} & \mathop\cong\limits^{\int_A (3.1)} & \int_A \hom F {[\calK,\calV]} {\hom {H_A} \calB {(P_{-A})}} & \mathop\equiv\limits^{(2.10)} &  \int_A \int_K \big[ F_K, \hom {H_A} \calB {(P_{K,A})} \big] & \xrightarrow[\mkern3em]{\lambda_A} & \int_K \big[ F_K, \hom {H_A} \calB {(P_{K,A})} \big]  & \xrightarrow[\mkern3em]{\lambda_K} & \big[ F_K, \hom {H_A} \calB {(P_{K,A})} \big]  \\ \hom B \calB {X\cotensor C} & \mathop\cong\limits^{(3.1)}_{(3.42)} & [X, \hom B \calB C] \tag{3.16} \end{align}

There is a notational issue in the above: 

Kelly uses $G:\calK\to [\calA,\calB]$ for the curried version of $P:\calK\tensor \calA \to \calB$, writing $(GK)A$ for $P(K,A)$, or as he puts it, $(G-)A = P(-,A)$ (which I tend to write as $P_{-A}$). 

In the above I alternate between the two notations, using whatever seems most appropriate for the particular context.