\section{Odds and Ends}

\subsection{Proofs of the Formulas in Aside~\ref{aside:SvsSS}}
\label{ssec:SvsSSProofs}

We can carry out the required computations in a faithful matrix
representation of $sl_2$ / $sl_2^0$; such representations automatically
extend to faithful representations of exponentials and products of
exponentials in $\hatcalU(sl_2)$ / $\hatcalU(sl_2^0)$. And as we have
computers, we may as well use them (sources in
\web{}). First, we enter the $sl_2$ matrices and verify
their commutation relations:

\dialoginclude{sl2matrices}

We then declare that {\tt$\bbE$[M]} means $\bbe^M$, when $M$ is a matrix, and
verify the $sl_2$ formulas in Aside~\ref{aside:SvsSS}:

\dialoginclude{Reordering_sl2}

\noindent(The truth, of course, is that we originally used a computer to {\tt
Solve} for $\eta_0$, $\alpha_0$, and $\xi_0$, but once the formulas are
found, we only need to check them).

In the case of $sl_2^0$, the matrix representation is a bit more
complicated, the formulas are a bit simpler, and the end result is the same
{\tt true}:

\dialoginclude{g0matrices}

\dialoginclude{Reordering_g0}
\qed