Two squares formulas

This is the start of a VERY ROUGH draft.

Assume $\blue{w = u+iv}, \green{z = x+iy} \in \mathbb C$.

It is interesting to compare the two formulas.

In the Two Squares Equality, first we square each of the numbers, 

then add pairs of the squares, 

then multiply the resulting binary sums.

In the triangle inequality, 

first we add matching components, 

then square each binary sum, 

then add the squares.

\[ \boxed{ \begin{array} {} \text{The Two Squares Equality} \\ \hline \blue w\green z = \blue{(u + iv)} \green{(x + iy)} = \blue u\green x - \blue v\green y +i(\blue v\green x + \blue u\green y)   \\  \blue w \green{\bar z} = \blue{(u + iv)} \green{(x - iy)} = \blue u\green x + \blue v\green y + i(\blue v\green x - \blue u\green y)  \\ \blue{\bar w} \green{\bar z} = \blue{(u - iv)}\green{(x - iy)} = \blue u\green x - \blue v\green y - i(\blue u\green y + \blue v\green x) = \overline{\blue w\green z}  \\ \hline   \blue{{|w|}^2} \green{{|z|}^2} = \blue w \blue{\bar w}  \green{z \bar z} = \blue w \green {z \bar z} \blue{\bar w} = \blue w\green z \overline{\blue w\green z} = {|\blue w\green z|}^2  \\ \hline \boxed{ \blue{{|w|}^2} \green{{|z|}^2} = \blue{(u^2 + v^2)} \green{(x^2 + y^2)}  } = \blue{u^2}\green{x^2} + \blue{u^2}\green{y^2} + \blue{v^2}\green{x^2} + \blue{v^2}\green{y^2} \\  {|\blue w\green z|}^2 = {(\blue u\green x - \blue v\green y)}^2 + {(\blue v\green x + \blue u\green y)}^2 \\ \blue{u^2}\green{x^2} - 2\blue u\green x\blue v\green y + \blue{v^2}\green{y^2} \\ \blue{v^2}\green{x^2} + 2\blue v\green x\blue u\green y + \blue{u^2}\green{y^2} \\ \end{array} } \]

Triangle inequality

\[ \boxed{ \begin{array} {} \text{The Triangle Inequality} \\ \hline |\blue W + \green Z| \leq \blue{|W|} + \green{|Z|} \\ {|\blue W+\green Z|}^2 \leq \blue{{|W|}^2} +2\blue{|W|}\green{|Z|} + \green{{|Z|}^2} \\ \boxed{{{|\blue W+\green Z|}^2 = (\blue u+\green x)}^2 + {(\blue v+\green y)}^2} \leq \blue{u^2 + v^2} + 2\blue{\sqrt{u^2 + v^2}}\green{\sqrt{x^2 + y^2}} + \green{x^2 + y^2} \\ 2(\blue u\green x+\blue v\green y) \leq  2\blue{\sqrt{u^2 + v^2}}\green{\sqrt{x^2 + y^2}} \\ {(\blue u\green x+\blue v\green y)}^2 \leq \blue{(u^2+v^2)} \green{(x^2+y^2)} \\ 2\blue u\green x\blue v\green y \leq \blue{u^2}\green{y^2} + \blue{v^2}\green{x^2} \\ 0 \leq \blue{u^2}\green{y^2} - 2\blue u\green x\blue v\green y + \blue{v^2}\green{x^2} = {(\blue u\green y - \blue v\green x)}^2 \\ \end{array} } \]

Universal element, universal arrows, initial/terminal objects, left/right lifts

Preliminary and incomplete!

The common and central (to category theory) notion of <I>universal element</I> has at least four definitions.

Here we aim to present and compare the definitions.

They all assume we start with a functor

\[ \boxed{ \rightadj{ \leftcat{(\Set = \calL)} \longleftarrow \rightcat\calR } : R }  \, . \]

Here the designations of what is "left" and what is "right" 

is determined by

what is on the left and right within the hom sets of each category in the definition of adjunction (or representable).

In the first two definitions there are certain (hopefully) familiar ${\rightadj\forall}{\leftadj{\exists!}}$ conditions that form part of the definition; 

I am not going to repeat those conditions -- you can look them up, 

or read about them later in this blog

In the last two definitions those conditions are built into 

the definitions of "initial object" and "left lift".

The rightmost columns are works in progress, 

dual to the column next to them.

\[ \boxed{ \begin{array} {cll|ccccc|ccccc|ccccc} 1. & \text{universal element} & \leftadj{ \lambda_0 \in \rightcat{r_0} \rightadj R }  \\ \hline 2. & \text{universal arrow} & \leftadj{\lambda_0 \in \leftcat{   \hom 1 \Set { \rightcat{r_0} \rightadj R }  }  } \text{, i.e.,} \\ &&  \leftadj { \lambda_0 : \leftcat{1} \to \rightcat{r_0} \rightadj R } \text{ in } \leftcat\Set  \\ \hline  &&& {} \rlap{ \kern2em \target{ \text{covariant form} } } &&&&& {} \rlap{ \kern8em  \source{ \text{contravariant form} } } \\ &&& {} \rlap{ \kern1em \leftadj{ \text{universal element} } } &&&&& {} \rlap{ \kern8em  \rightadj{ \text{opuniversal element} } } \\ \hline &&& \leftcat{ \calI \rlap{ \kern.5em  \xleftarrow [\kern11em] {!} }  } &&&& \leftcat{1 \downarrow {\rightadj R} } & \rightcat{ {\leftadj L} \downarrow 1  \rlap{ \kern.5em   \xrightarrow [\kern11em] {!} }  } &&&& \rightcat{\calI} & \leftcat{ 1 \downarrow {\rightadj L}  \rlap{ \kern.5em   \xrightarrow [\kern10em] {!} }  } &&&& \rightcat{\calI}  \\ 3. & \text{initial object} & \leftadj{r_0 \langle \lambda_0\rangle} & \leftcat{ \llap 1 \big\downarrow }  && \smash{  \leftcat{ \stackrel \lambda \Longrightarrow } } && \rightcat{\big\downarrow \rlap r } & \leftcat{\llap l \big\downarrow }  && \smash{  \rightcat{ \stackrel \rho \Longrightarrow } } && \rightcat{ \big\downarrow \rlap 1 }  & \leftcat{\llap l \big\downarrow }  && \smash{  \rightcat{ \stackrel \rho \Longleftarrow } } && \rightcat{ \big\downarrow \rlap 1 }   \\   &&  \text{is an initial object in $\leftcat{ 1 \downarrow {\rightadj R} }$} & \leftcat\Set \rlap{ \kern.5em \rightadj{ \xleftarrow[\textstyle R]{\kern12em} } } &&&& \rightcat\calR & \leftcat\calL \rlap{ \kern.5em \leftadj{ \xrightarrow[\textstyle L]{\kern12em} } } &&&& \rightcat{\Set\op} & \leftcat{\calL\op} \rlap{ \kern.5em \leftadj{ \xrightarrow[\textstyle L]{\kern10em} } } &&&& \rightcat{\Set}  \\ \hline &&&&& \leftcat \calI &&&&& \leftcat \calI  &&&&& \leftcat \calI  \\ 4. & \text{left lift} &  \leftadj{ \lambda_0 : {\leftcat 1} \Rightarrow r_0 \rightadj R }  && \leftcat{ \llap 1 \swarrow } & \smash{ \lower1ex{ \leftadj{ \stackrel {\lambda_0 = \eta} \Longrightarrow } } } & \leftadj{ \searrow \rlap{r_0 = \leftcat 1 L} } &&& \rightadj{ \llap{ \rightcat 1 R = l_0 } \swarrow } & \smash{ \lower1ex{ \rightadj{ \stackrel {\rho_0 = \epsilon} \Longrightarrow } } } & \rightcat{ \searrow \rlap 1 } &&& \rightadj{ \llap{ \rightcat 1 R = l_0 } \swarrow } & \smash{ \lower1ex{ \rightadj{ \stackrel {\rho_0} \Longleftarrow } } } & \rightcat{ \searrow \rlap 1 }   \\  && \text{is a left lift of $\leftcat 1$ through $\rightadj R$ } & \leftcat\Set  \rlap{ \kern.5em \rightadj{ \xleftarrow[\textstyle R]{\kern12em} } } &&&& \rightcat\calR  & \leftcat\calL \rlap{ \kern.5em \leftadj{ \xrightarrow[\textstyle L]{\kern12em} } } &&&& \rightcat{\Set\op}   & \leftcat{\calL\op} \rlap{ \kern.5em \leftadj{ \xrightarrow[\textstyle L]{\kern10em} } } &&&& \rightcat{\Set}  \\ \hline &&& {} \rlap{ \kern3em \leftadj{ \text{left adjoint} } } &&&&& {} \rlap{ \kern3em  \rightadj{ \text{right adjoint} } }  \\ \hline &&& \leftcat{ \calI \rlap{ \xleftarrow [\kern11em] {!} } } &&&& \leftcat{l \downarrow {\rightadj R} } & \rightcat{  { {\leftadj L} \downarrow r } \rlap{ \xrightarrow [\kern11em] {!} } } &&&& \rightcat{\calI} \\ 5. & \text{left adjoint} & \leftadj{ (r_0 = \leftcat l L) \langle \lambda_0\rangle } & \leftcat{ \llap l \big\downarrow } && \smash{ \leftcat{ \stackrel \lambda \Longrightarrow } } && \rightcat{\big\downarrow \rlap r } & \leftcat{ \llap l \big\downarrow } && \smash{ \rightcat{ \stackrel \rho \Longrightarrow } } && \rightcat{\big\downarrow \rlap r } \\ && \text{is an initial object in $\leftcat{ l \downarrow {\rightadj R} }$} & \leftcat\calL \rlap{ \kern.5em \rightadj{ \xleftarrow[\textstyle R]{\kern12em} } } &&&& \rightcat\calR & \leftcat\calL \rlap{ \kern.5em \leftadj{ \xrightarrow[\textstyle L]{\kern13em} } } &&&& \rightcat\calR  \\ \hline &&&&& \leftcat \calI &&&&& \rightcat \calI \\ 6. & \text{left lift} & \leftadj{ \lambda_0 : {\leftcat l} \Rightarrow r_0 \rightadj R } && \leftcat{ \llap l \swarrow } & \smash{ \lower1ex{ \leftadj{ \stackrel {\lambda_0 = \eta} \Longrightarrow } } } & \leftadj{ \searrow \rlap{r_0 = \leftcat l L} }  &&& \rightadj{ \llap {\rightcat r R = l_0} \swarrow } & \smash{ \lower1ex{ \rightadj{ \stackrel {\rho_0 = \epsilon} \Longrightarrow } } } & \rightcat{\searrow \rlap r} \\ &&  \text{is a left lift of $\leftcat l$ through $\rightadj R$ } & \leftcat\calL \rlap{ \kern.5em \rightadj{ \xleftarrow[\textstyle R]{\kern12em} } } &&&& \rightcat\calR & \leftcat\calL \rlap{ \kern.5em \leftadj{ \xrightarrow[\textstyle L]{\kern13em} } } &&&& \rightcat\calR \\ \hline &&& \leftcat{ \hom l \calL {\rightcat r \rightadj R} } \rlap{ \kern.5em \leftcat{  \xleftarrow [ \leftadj{ \widehat{\lambda_0 = \eta} } ] {\kern10em} }  } &&&&  \rightcat{ \hom { \leftadj{ (r_0 = \leftcat l L) }  } \calR r } & \leftcat{ \hom l \calL { \rightadj { (\rightcat r  R = l_0) } } } \rlap{ \kern.5em \rightcat{  \xrightarrow [ \rightadj{ \widehat{\rho_0 = \epsilon} } ] {\kern10em} }  } &&&& \rightcat{ \hom {\leftcat l \leftadj L} \calR r  }  \\ &&&  {} \rlap{ \kern-2em { \leftadj{(\lambda_0 = \eta)} } \cdot {\rightadj{ (\rightcat\rho  R) } } }  && \leftcat{\leftarrow\kern-.2em \shortmid} && \rightcat\rho & \leftcat\lambda && \rightcat\mapsto && {} \rlap{ \kern-4em \leftadj{(\leftcat\lambda L)} \cdot \rightadj{(\rho_0 = \epsilon)} }  \\  \end{array} } \]

Orbits as natural transformations

This a very incomplete, preliminary document.

$\newcommand\lZ {{\leftadj \Z}}$

$\newcommand\gG {{\rightcat G}}$

$\newcommand\lm {{\leftcat m}}$

$\newcommand\rn {{\rightcat n}}$

It could equally well have been titled "Orbits and the Yoneda lemma".

The connection between orbits and natural transformations is that, 

given a monoid, 

<I>the exponential law relating (a power to a product of natural numbers) to (an iterated power) 

is precisely (an instance of naturality)</I>.

We assume we are working in the familiar category of abelian groups and group homomorphisms.

Let $G$ be an abelian group.

The group's binary operation allows us to define an action of (the integers $\lZ$) on (that group $G$) by exponentiation.

A careful development of this is in many texts on algebra; 

e.g., <i>Algebra</i>, Third Edition, by Mac Lane and Birkhoff, 

in its Chapter II, Groups, Section 3, Cyclic Groups (M-B II.3), 

where they define exponentiation ("powers") in an arbitrary group $G$, 

using the group's operations and recursion:

$$ g^0 = e, \kern3em g^{(n+1)} = g^n g, \kern3em g^{(-n)} = (g^n)^{(-1)} $$

Once that is done one may prove "exponential laws" giving relationships between 

the exponentiation operation giving an action of $\lZ$ on $\gG$ and 

the algebraic operations on $\lZ$ and $\gG$:

\[ \boxed{ \begin{array} {ccc|l|c}  &&&& \text{M-B II.3}    \\  \hline   g^{(n+n')} & \leftadj{  \xlongequal [\text{sum}] {\text{integer}}  }  & g^n g^{n'}  &  \text{exponentiation by } \leftadj{ \text{(a sum of integers)} } &  (6)  \\ g^0 & \xlongequal{} & e \\ \hline \\  g^{(\source n \target p)} & \rightadj{  \xlongequal [\text{product}] {\text{integer}}  } & (g^{\source n})^{\target p} & \text{exponentiation by } \rightadj{ \text{(a product of integers)} }   &  (7) \\ g^1 &  \xlongequal{} & g \\ \hline  \\    (\source g \target h)^n & \target{ \xlongequal [\text{operation}] {\text{group}} } & \source{g^n} \target{h^n} & { \textstyle \text{exponentiation of } \target{ \text{(a product of group elements)}} \atop \textstyle \text{(this is the only law that assumes } \target{ \text{$G$ is abelian} ) }  }  &  (12)    \\ e^n & \xlongequal{} & e \\ \end{array} } \]

Since $\Set$ is cartesian closed, the action may be given in three equivalent ways:

\[ \boxed{  \begin{array} {ccccccc|l}  \lZ & \longrightarrow & [G,G] & : & n & \mapsto & {()}^n & \text{exponentiation by $n$} \\  G \times \lZ & \longrightarrow & G & : & \langle g,n \rangle & \mapsto & g^n  & \text{the usual action map} \\  G & \longrightarrow & [\lZ,G] & : & g & \mapsto & \hat g = g^? & \text{the orbit of $g$}  \\ \end{array}  }  \]

Here is a preliminary, incomplete diagram in that category:

\[ \boxed {  \begin{array} {ccccccccccc|cc} \kern10em & 1   \\    &&   \llap{ \text{either $1$ or, more generally, $m$} } \searrow    \\     &&&   \llap{  \leftcat{ 1 \in {} }   } \rightcat{ \hom {r_0} {\rightadj{\Z^×}} {r_0} }  \rlap{   \red{  \xrightarrow [\kern11em] { {g^?} = {\alpha_{\rightcat{r_0}}} }  }   }  &&&&  \hom {} {\leftcat G} {\rightcat{r_0}}   \rlap{   {} \ni \red{  \boxed{ \source 1\alpha = \leftcat g }  }   }   &&&&  {\source g} {\target h}    \\     &&& \lower10ex{  \source{ \llap{\rightcat{ \hom {r_0} {\rightadj{\Z^×}} {n} } } \smash{\Bigg\downarrow} } }  & \rightcat{ \searrow \rlap{ \kern-4em \hom {r_0} {\rightadj{\Z^×}} {{\leftcat n}{\rightcat p}} }  } & \lower10ex{ {\red\alpha}_{\leftcat n}  } && \lower10ex{  \smash{ \source{ \Bigg\downarrow \rlap{G_n = ()^n} } }  }  & \searrow \rlap{G_{(\leftcat n \rightcat p)} = ()^{(\leftcat n \rightcat p)} }       \\      &&&   \llap{ \leftcat{ 1+\cdots +1 = 1\cdot n = 1 \tensor n =  n  \in {} }  }   \rightcat{ \hom {r_0} {\rightadj{\Z^×}} {r} }  \rlap{   \red{  \xrightarrow [\kern11em]{ {g^?} = {\alpha_{\rightcat{r}}} }  }   }   &&&& \hom {} {\leftcat G} {\rightcat r}   \rlap{ \ni      \boxed{ \begin{array} {ccc|c} \red{ \big( \leftcat{ 1+\cdots +1 } \big) \alpha  }  & \xlongequal{\text{$n$-ary homomorphism}} &  (1\red\alpha) \cdots (1\red\alpha)  & \text{$n$-ary operations}   \\   \red{ (\leftcat{1\cdot n}) \alpha  }  &  \xlongequal [ \text{$\rightadj{\Z^×}$-natural transformation } 1{\red\alpha}_n ] {\text{$\leftadj\Z$-homomorphism}} && \text{$\rightadj{\Z^×}$-actions}  \\  \red{ (\leftcat{1 \tensor n)} \alpha } \\  \red{ \boxed{\black n \alpha} }   & \xlongequal{\text{definition of $\red\alpha$ (given $\leftcat g$)}} & \red{  \boxed{ \black{(1\red\alpha)^n} = {\leftcat g}^{n} }  } \\    \hline  {} \rlap{\kern-2em \text{the general homomorphism property:}}  \\   \red{ (\black{n+n'}) \alpha } &  \xlongequal{\text{homomorphism}}  &  (n \red\alpha)   (n' \red\alpha)  \\  g^{n+n'}  &  \xlongequal{\text{exponential law}}  &  g^n g^{n'}  \\   \end{array} }  }        &&&  \kern30em  &    ({\source g} {\target h})^n = {\source{g^n}} {\target{h^n}}         \\            &&&&  \rightcat{  \llap{ \hom {r_0} {\rightadj{\Z^×}} {p} } \searrow  }  &&   {\red\alpha}_{\rightcat p}  &&  \target{  \searrow \rlap{G_p = ()^p} }   \\    &&&&& \rightcat{ \hom {r_0} {\rightadj{\Z^×}} {r'} } \rlap{ \red{ \xrightarrow [\kern10em] { {{\leftcat g}^?} = {\alpha_{\rightcat{r'}}} }  }   }  &&&& \hom {} {\leftcat G} { \rightcat{r'} }  \\  \end{array}  }  \]

\[ \boxed { \begin{array} {} & &  \red{    \big( \leftadj m \rightcat{ (\leftcat n p) } \big) \alpha_{\rightcat{r'}}   }   &   \red{   \xlongequal {   \leftadj m \alpha_{ (\leftcat n \rightcat p) }  }   }   &  ( \leftadj m {\red\alpha}_{\rightcat{r_0}} )^{   \rightcat {  ( \leftcat n p )  }   }  &  \kern1em   \\  & &  \llap{  \red{( \rightadj{\text{assoc.}} ) \alpha_{\rightcat{r'}} }  } \Vert   \\ \red{    \big( \leftcat n \rightcat p \big) \alpha_{\rightcat{r'}}   }   &  \xlongequal{ \leftadj{m=1} }   & \red{    \big( \leftcat{  (\leftadj m  \leftcat n)  }  \rightcat p \big) \alpha_{\rightcat{r'}}   }  &&  \smash{ \raise1.5ex{\Bigg\Vert \rlap{  ( \leftadj m {\red\alpha}_{\rightcat{r_0}})^{ \rightadj{\text{assoc.}}} }  } }   \\  &  \red{  (\leftadj m \leftcat n) \alpha_{\rightcat p}  }       \\ \rightcat{   \big( \red{  (\leftcat n) \alpha_{\rightcat{r}}  }  \big)^{\rightcat p}  }  & \xlongequal{ \leftadj{m=1} } &    \rightcat{   \big( \red{  (\leftadj m \leftcat n) \alpha_{\rightcat{r}}  }  \big)^{\rightcat p}  }  &  \red{   \xlongequal [  \rightcat{ ( \leftadj m {\red\alpha}_{\leftcat n} )^p }  ] {}  }   &  \rightcat{  \big( \leftcat{ (\leftadj m {\red\alpha}_{\rightcat{r_0}})^n } \big)^p  }  \\    \end{array}  }  \]

The next diagram is a work in progress.

It is being modified from a previous diagram.

\[ \boxed { \begin{array} {ccccccccccc|cc} \kern10em & 1 \\ && \llap{ \text{either $0$ or, more generally, $m$} } \searrow \\ &&& \llap{ \leftcat{ 0 \in {} } } \rightcat{ \hom {r_0} {\leftadj{\Z^+}} {r_0} } \rlap{ \red{ \xrightarrow [\kern11em] { {g^?} = {\alpha_{\rightcat{r_0}}} } } } &&&& \hom {} {\leftcat G} {\rightcat{r_0}} \rlap{ {} \ni \red{ \boxed{ \source 0 \alpha = \leftcat g } } } &&&& {\source g} {\target h} \\ &&& \lower10ex{ \source{ \llap{\rightcat{ \hom {r_0} {\leftadj{\Z^+}} {n} } } \smash{\Bigg\downarrow} } } & \rightcat{ \searrow \rlap{ \kern-5em \hom {r_0} {\leftadj{\Z^+}} {( \leftcat n + \rightcat p )} } } & \lower10ex{ {\red\alpha}_{\leftcat n} } && \lower10ex{ \smash{ \source{ \Bigg\downarrow \rlap{G_n = ()^n} } } } & \searrow \rlap{G_{(\leftcat n + \rightcat p)} = ()^{(\leftcat n + \rightcat p)} }        \\       &&& \llap{ \leftcat{ 0 + n = n \in {} } } \rightcat{ \hom {r_0} {\leftadj{\Z^+}} {r} } \rlap{ \red{ \xrightarrow [\kern11em]{ {g^?} = {\alpha_{\rightcat{r}}} } } } &&&& \hom {} {\leftcat G} {\rightcat r} \rlap{ \ni \boxed{ \begin{array} {ccc|c} \red{ \big( \leftcat{ 1+\cdots +1 } \big) \alpha } & \xlongequal{\text{$n$-ary homomorphism}} &  (1\red\alpha) \cdots (1\red\alpha)  & \text{$n$-ary operations}   \\   \red{ (\leftcat{1\cdot n}) \alpha  }  &  \xlongequal [ \text{$\leftadj{\Z^+}$-natural transformation } 1{\red\alpha}_n ] {\text{$\lZ$-homomorphism}} && \text{$\leftadj{\Z^+}$-actions}  \\  \red{ (\leftcat{1 \tensor n)} \alpha } \\  \red{ \boxed{\black n \alpha} }   & \xlongequal{\text{definition of $\red\alpha$ (given $\leftcat g$)}} & \red{  \boxed{ \black{(1\red\alpha)^n} = {\leftcat g}^{n} }  } \\    \hline  {} \rlap{\kern-2em \text{the general homomorphism property:}}  \\   \red{ (\black{n+n'}) \alpha } &  \xlongequal{\text{homomorphism}}  &  (n \red\alpha)   (n' \red\alpha)  \\  g^{n+n'}  &  \xlongequal{\text{exponential law}}  &  g^n g^{n'}  \\   \end{array} }  }        &&&  \kern30em  &    ({\source g} {\target h})^n = {\source{g^n}} {\target{h^n}}         \\            &&&&  \rightcat{  \llap{ \hom {r_0} {\leftadj{\Z^+}} {p} } \searrow  }  &&   {\red\alpha}_{\rightcat p}  &&  \target{  \searrow \rlap{G_p = ()^p} }   \\    &&&&& \rightcat{ \hom {r_0} {\leftadj{\Z^+}} {r'} } \rlap{ \red{ \xrightarrow [\kern10em] { {{\leftcat g}^?} = {\alpha_{\rightcat{r'}}} }  }   }  &&&& \hom {} {\leftcat G} { \rightcat{r'} }  \\  \end{array}  }  \]

------

Proofs by induction of (the exponential laws for powers),

using (the definition of powers by recursion).

\[ \boxed{ \begin{array} {ccc|ccc} a^{(\lm + \rn)\sigma} & \xlongequal { \text{defn. $a^{(\lm+\rn)\sigma}$} } & a a^{(\lm + \rn)} & \boxed{ a^{\big(\lm(\rn\sigma)\big)} } & \xlongequal { \text{defn. $\lm(\rn\sigma)$} } & a^{(\lm\rn + m)}  \\  \llap{ \text{defn. $\lm+(\rn\sigma)$} } \Vert && \Vert \rlap{ \text{ind.} }  &&& \Vert \rlap{ \text{homo. for plus} }   \\  \boxed{ a^{\lm+(\rn\sigma)} }  && a a^\lm a^\rn &&& a^{\lm\rn} a^\lm \\  && \Vert \rlap{ \text{comm.} } &&& \Vert \rlap{ \text{ind.}}  \\  \boxed{ a^\lm a^{\rn \sigma} } & \xlongequal [\text{defn. $a^{\rn\sigma}$}] {}  & a^\lm a a^\rn & \boxed{ (a^\lm)^{(\rn\sigma)} } & \xlongequal [ \text{defn. $(a^\lm)^{(\rn\sigma)}$} ] {}  & (a^\lm)^\rn a^\lm   \\  \end{array} } \]

Duals as right adjoints

This is extremely incomplete and preliminary.

\[ \boxed { \begin{array} {}  &&&& \leftcat 1  &&&&  {\rightadj t}_{\rightcat{C^n}}     \\  & \leftadj v && \rightadj{b^i}  && \leftadj{b_i} &&&   \\  \hline   &&  \leftcat{  k^1 \rlap{ \xleftarrow [\kern 10em] {\displaystyle 1\in k^1} }  } &&&& \leftcat{ k^1} \rightadj{   \rlap{  \xleftarrow [\kern 10em] { \displaystyle t_{\rightcat{C^n}} \in [\leftadj{B^m},\rightcat{C^n}]  }  }   } &&&& \leftcat{ k^1 }   \\     & \leftadj{ \swarrow  \rlap{\kern-4em v\in B^m}  }  &  \rightadj{ \big\Downarrow \rlap{\epsilon_{\rightcat{k^1}}}  }  &   \rightadj{ \nwarrow \rlap{ \kern-.5em B^* } } & \leftadj{ \big\Downarrow \rlap\eta }  & \leftadj{ \swarrow  \rlap{\kern-.5em B^m}  }  &  \rightadj{ \big\Downarrow \rlap{\epsilon_{\rightcat{k^1}}}  }  &   \rightadj{ \nwarrow \rlap{ \kern-.5em B^* } }   &  \rightcat{ \swarrow \rlap{\kern-.5em C^n} }    &   \rightcat{ \swarrow \rlap{C^n} }   \\   \rightcat{ k^1 \rlap{\xleftarrow {\kern 10em} }  } &&&& \rightcat{ k^1 \rlap{\xleftarrow {\kern 10em} }  } &&&& \rightcat{ k^1 }    \end{array} } \]

\[ \boxed { \begin{array} {} && \leftadj v \tensor {\rightadj t}_{\rightcat{C^n}}  \\  && \Big\downarrow  \\  &&  \leftadj{ v \tensor {} } \leftcat 1 \rightadj{ {} \tensor t_{\rightcat{C^n}} }  \\  &&  \leftadj{     \llap{   B^m \tensor \eta  \rightadj{ {} \tensor [\leftadj{B^m}, \rightcat{C^n}] }   }   \Big\downarrow   }  &    \leftcat{  \searrow \rlap{ \leftadj v \tensor \zeta\inv }  }   \\    && \leftadj v \tensor ( \Sigma \rightadj{b^i} \tensor \leftadj{b_i} ) \tensor {\rightadj t}_{\rightcat{C^n}} &&    \\   & \rightadj{  \llap{ \epsilon_{\rightcat{k^1}} \tensor \leftadj{B^m} \tensor [\leftadj{B^m}, \rightcat{C^n}]  } \swarrow   } &&  \rightadj{  \searrow \rlap{ \leftadj v \tensor ( \black\Sigma b^i  \tensor \epsilon_{\rightcat{C^n}} ) }  } &   \\     \leftadj{   \big( \Sigma \rightadj{ \langle \leftadj v, b^i \rangle }  \tensor \leftadj{b_i} \big)  } \rightadj{ {} \tensor t_{\rightcat{ C^n}}  }   && \rightadj{  \epsilon_{\rightcat{k^1}} \tensor \epsilon_{ \rightcat{C^n} }  }     && \leftadj v \tensor \big( \Sigma \rightadj{b^i} \tensor  \rightadj { \langle \leftadj {b_i}, t_{\rightcat{C^n} }  \rangle } \big)   \\    \Vert & \rightadj{  \llap{ \rightcat{k^1} \tensor \epsilon_{\rightcat{C^n}}  } \searrow   }  && \rightadj{  \swarrow \rlap{ \epsilon_{\rightcat{k^1}} \tensor \rightcat{k^1} }  } &  \\   \leftadj{   \rightcat 1 \tensor \Sigma  \rightadj{ \langle \leftadj v, b^i \rangle } \leftadj{b_i}  } \rightadj{ {} \tensor t_{\rightcat{ C^n}}  }  && \Sigma \rightadj{ \langle \leftadj v, b^i \rangle } \tensor \rightadj{ \langle \leftadj b_i , t_{\rightcat{C^n}}  \rangle }   \\  \Vert  && \Big\Vert \rlap{   \leftadj{ \tensor \text{b.l.} } , \rightadj{  \langle,\rangle \text{ homog. and additive (thus b.l.)}  }   }  \\  \leftadj{   \rightcat 1 \tensor v  } \rightadj{ {} \tensor t_{\rightcat{ C^n}}  }   && \rightcat 1 \tensor \rightadj{ \big\langle \black{\displaystyle\Sigma} \langle \leftadj v, b^i \rangle  \leftadj b_i , t_{\rightcat{C^n}}  \big\rangle }   \\   &  \rightadj{  \llap{ \rightcat{k^1} \tensor \epsilon_{\rightcat{C^n}}  } \searrow   }   & \Big\Vert   \\ && \rightcat 1 \tensor \rightadj{ \big\langle \leftadj v, t_{\rightcat{C^n}}  \big\rangle  }   \\    \end{array} }   \]

Matrices

\[ \boxed{ \begin{array} {} 1 \\ & \leftcat\searrow &&& \leftcat\searrow \rlap{ \hom {\rightcat -} M {\leftcat i} } \\ && \leftcat{A_i} \rlap{   \leftcat{  \xrightarrow [\kern12em] { \textstyle \text{column vectors} \atop \textstyle \text{vectors} }  }   } &&&& \rightcat{ \displaystyle \mathop{\rightadj\prod}_{j=1} ^n B_j }  \\ & \leftcat{ \llap{x_i} \nearrow } && \leftadj{   \searrow \rlap{ \kern-2em \iota_{\rightcat i} = \widehat {e_{\leftcat i}}  }    }  && \searrow \rlap{ \hom {\rightcat j} M {\leftcat i} } && \rightadj{ \searrow \rlap{ \pi_{\rightcat j} } } \\ 1 \rlap{ \leftcat{ \xrightarrow[ \textstyle \text{either $x_ie_i$ or $X$} ] {\kern10em} } }  &&&& \leftcat{ {\displaystyle \mathop{\leftadj\sum}_{i=1} ^m} A_i } \rlap{ \rightcat{  \xrightarrow [ \textstyle \text{row vectors} \atop \textstyle \text{covectors} ] {\kern12em}  }   } &&&& \rightcat{B_j} \\ \\  \end{array} } \]