\begin{equation}\label{goodtodo}
\phi_n^\ell\big(v_n(x^r)\big) \delta_{n+1}^\ell\big( \bar
=  (-1)^{n(r+1)}
\delta_n^\ell\Big(\bar e^{(n)}\big((-1)^{n+r} t \big) \Big)
\phi_n^\ell\big(v_n\big((t-x)x^r\big)\Big)
\end{equation}
is satisfied in the superbimodule
for any $r \geq 0$.
Substituting the formulae from \cref{puky,events} into \cref{goodtodo} and
cancelling $(-1)^{\ell r+\ell (n+1)}$ from both sides,
this expands to the equation
\begin{multline*}
\Big(v_n(x^r) - (-1)^{\ell + r} \big(1-(-1)^r\big) \dot o^{(\ell)}v_n(x^{r-1})
\Big)
\Big(
\bar e^{(n+1)}\big((-1)^\ell t\big) -t^{-1} \dot o^{(\ell)} \bar e^{(n+1)}\big((-1)^\ell t\big)
+ t^{-1} \dot o^{(\ell)}\bar e^{(n+1)}\big((-1)^{\ell+1} t\big)
\Big)\\\quad=
\Big((-1)^{n(r+1)}\bar e^{(n)}\big((-1)^{\ell+n+r} t\big) -(-1)^{(n+1)r} t^{-1}\dot o^{(\ell)} \bar e^{(n)}\big((-1)^{\ell+n+r} t\big)+(-1)^{(n+1)r} t^{-1} \dot o^{(\ell)}\bar e^{(n)}\big((-1)^{\ell+n+r+1} t\big)
\Big)\\\times\:
\Big(v_n\big(\big((-1)^\ell t - x)x^r\big) - (-1)^{r}  \big(1-(-1)^r\big) t \dot o^{(\ell)}
- (-1)^{\ell+r} \big(1+(-1)^r\big) \dot o^{(\ell)} v_n(x^r)
\Big).
\end{multline*}
Now we expand both sides using that
$\big(\dot o^{(\ell)}\big)^2 = 0$. Commuting $\dot o^{(\ell)}$ then
$\bar e^{(n+1)}(\pm t)$ to the left with \cref{newrels1},
the left hand side contributes the sum of the following four terms:
\begin{align*}
v_n(x^r)\bar e^{(n+1)}\big((-1)^\ell t\big)&=(-1)^{n(r+1)}
\bar e^{(n)}\big((-1)^{\ell+n+r} t\big)v_n\big(\big((-1)^\ell t - x)x^r\big), \\
- (-1)^{\ell + r} \big(1-(-1)^r\big) \dot o^{(\ell)}
v_n(x^{r-1})\bar e^{(n+1)}\big((-1)^\ell t\big)&=
-(-1)^{(n+1)r+\ell} \big(1-(-1)^r\big) \dot o^{(\ell)}
\bar e^{(n)}\big((-1)^{\ell+n+r+1} t\big)\\&\hspace{50mm}\times v_n\big(\big((-1)^\ell t -
x\big) x^{r-1}\big),\\
-(-1)^{n+r} t^{-1}\dot o^{(\ell)} v_n(x^r) \bar e^{(n+1)}\big((-1)^\ell
%-(-1)^r t^{-1}\dot o^{(\ell)}v_n(x^r)  \bar
%          e^{(n+1)}\big((-1)^\ell t\big)=
-(-1)^{(n+1)r} t^{-1}\dot o^{(\ell)}         \bar e^{(n)}\big((-1)^{\ell+n+r}
t\big)v_n\big(((-1)^\ell t - x)x^r\big),
\\
(-1)^{n+r} t^{-1} \dot o^{(\ell)} v_n(x^r)  \bar e^{(n+1)}\big((-1)^{\ell+1} t\big)
%(-1)^{r} t^{-1} \dot o^{(\ell)}v_n(x^r)\bar e^{(n+1)}\big((-1)^{\ell+1} t\big)
= -(-1)^{(n+1)r} t^{-1} \dot o^{(\ell)} \bar
e^{(n)}\big((-1)^{\ell+n+r+1} t\big)
v_n\big(((-1)^\ell t + x) x^r\big).
\end{align*}
Commuting $\dot o^{(\ell)}$ to the left, the right hand side
contributes the sum of the following five terms:
\begin{align*}
\bar e^{(n)}\big((-1)^{\ell+n+r} t\big)v_n\big(\big((-1)^\ell t - x)x^r\big),&\\
-(-1)^{(n+1)r} t^{-1}\dot o^{(\ell)} \bar e^{(n)}\big((-1)^{\ell+n+r} t\big)
v_n\big(\big((-1)^\ell t - x)x^r\big),&\\
%-(-1)^{(n+1)r} t^{-1} \bar e^{(n)}\big((-1)^{\ell+n+r}
% t\big) \dot o^{(\ell)} v_n\big(\big((-1)^\ell t -
% x)x^r\big)&=
(-1)^{(n+1)r} t^{-1} \dot o^{(\ell)} \bar e^{(n)}\big((-1)^{\ell+n+r+1}
t\big) v_n\big(\big((-1)^\ell t - x)x^r\big),\\
-(-1)^{(n+1)r}  \big(1-(-1)^r\big) t \dot o^{(\ell)}\bar
e^{(n)}\big((-1)^{\ell+n+r+1} t\big)v_n(x^{r-1}),
%(-1)^{n(r+1)+\ell+r}\big(1+(-1)^r\big) \bar
%  e^{(n)}\big((-1)^{\ell+n+r} t\big) \dot o^{(\ell)} v_n(x^r)
-(-1)^{(n+1)r+\ell}\big(1+(-1)^r\big) \dot o^{(\ell)} \bar
e^{(n)}\big((-1)^{\ell+n+r+1} t\big) v_n(x^r).&
\end{align*}
From this, without making any  further commutations, it follows that the two sides are equal.
\end{proof}

\section{Rigidity \texorpdfstring{of $\OGBim_\ell$}{}}

In this section, we prove that the $2$-supercategory $\OGBim_\ell$
from \cref{shy} is
{\em rigid} in the sense that all of its 1-morphisms have
left and right duals.
Given a formal Laurent series $f(t)$, we use the notation $\big[f(t)\big]_{t^r}$
to denote its $t^r$-coefficient.
Similarly, we use $\big[f(t) \big]_{t^{\leq r}}$,
$\big[f(t) \big]_{t^{\geq r}}$, etc. for the
formal Laurent series obtained by keeping only the terms with the
specified powers of $t$.
Note also the following elementary identity:
we have that
\begin{align}\label{why}
f(x) &= \left[(t- x)^{-1} f(t) \right]_{t^{-1}}
\end{align}
for any polynomial $f(x) \in \k[x]$.
For the first lemma, recall the notation \cref{thisisnotbad1,thisisnotbad2}.

\begin{lemma}\label{simpson}
Suppose that $\ell=n+1+n'$
and $0 \leq r,s \leq n$.
\begin{enumerate}
\item
v_n\big((t-x)^{-1} x^r\big)
\sum_{p=r}^n v_n(x^p) \left[\bar\eps^{(n+1)}(t)\right]_{> t^p}
\bar\gamm^{(n+1)}(t) t^{r-p-1}
-\sum_{p=0}^{r-1} v_n(x^p) \left[\bar\eps^{(n+1)}(t)\right]_{\leq t^p}
\bar\gamm^{(n+1)}(t) t^{r-p-1}$.
\item
u_n\big((t-x)^{-1} x^s\big)
\sum_{q=s}^n \bar\gamm^{(n+1)}(t)  \left[\bar\eps^{(n+1)}(t)\right]_{> t^q}
-\sum_{q=0}^{s-1} \bar\gamm^{(n+1)}(t) \left[\bar\eps^{(n+1)}(t)\right]_{\leq t^q}
u_n(x^q) t^{s-q-1}$.
\end{enumerate}
\end{lemma}

\begin{proof}
Remembering \cref{thisisnotbad1} and the definition of the right action of $\EOH_{n+1}^\ell$ from \cref{lemma0}(1), the identity obtained by applying
$\gamma_{n+1}$ to \cref{neweasypeasy}(2) implies for any $m \geq 0$ that
-\sum_{p=0}^n v_n\big(x^p\big)
\sum_{s=0}^m (-1)^{m+n+1-p-s} \bar\eps_{m+n+1-p-s}^{(n+1)}
\bar\gamm_s^{(n+1)}.
We multiply this by $t^{r-m-n-2}$ and sum over $m \geq 0$ to obtain
\sum_{m \geq 0} v_n\big(x^{m+n+1}\big)
\left(
\sum_{m \geq 0}
\sum_{s=0}^m (-1)^{m+n+1-p-s} \bar\eps^{(n+1)}_{m+n+1-p-s} \bar\eta^{(n+1)}_s t^{p-m-n-1}
\right)
The expression in brackets is equal to $\left[\bar\eps^{(n+1)}(t)\right]_{\leq t^p} \bar\gamm^{(n+1)}(t)$,
as may be checked by comparing $t^{p-m-n-1}$-coefficients for all $m \in \Z$.
Using this and \cref{newigr}, we obtain
\begin{align*}
v_n\big((t-x)^{-1} x^r\big)
&= \sum_{p=r}^n v_n\big(x^p\big) t^{r-p-1}
+ \sum_{m \geq 0} v_n\big(x^{m+n+1}\big)t^{r-m-n-2}\\
\sum_{p=r}^n v_n\big(x^p\big) \bar\eps^{(n+1)}(t) \bar \gamm^{(n+1)}(t) t^{r-p-1}
v_n\big(x^p\big)\left[\bar\eps^{(n+1)}(t)\right]_{\leq t^p} \bar\gamma^{(n+1)}(t)
\end{align*}
It remains to write the first
$\left[\bar\eps^{(n+1)}(t)\right]_{> t^p}
+\left[\bar\eps^{(n+1)}(t)\right]_{\leq t^p}$
and make some obvious cancellations to obtain the desired formula.

\vspace{1mm}
\noindent
Remembering the sign in \cref{thisisnotbad2}
and the matching sign in the definition of the left action of $\EOH_{n+1}^\ell$ from \cref{lemma0}(2), the identity obtained by
applying $\operatorname{p}^{n'} \circ \sig_{n'} \circ \smiley_{n+1}$ to
\cref{neweasypeasy}(1)
\sum_{r=0}^m
\bar\gamm_r^{(n+1)}\bar\eps_{m+n+1-q-r}^{(n+1)}
for any $m \geq 0$.
We multiply this by $t^{s-m-n-2}$ and sum over $m \geq 0$ to obtain
\sum_{m \geq 0} u_n\big(x^{m+n+1}\big)
\left(
\sum_{m \geq 0}
\sum_{r=0}^m (-1)^{m+n+1-q-r} \bar\gamm^{(n+1)}_r \bar\eps^{(n+1)}_{m+n+1-q-r} t^{q-m-n-1}
\right)
The expression in brackets is equal to $\bar\gamma^{(n+1)}(t)\left[\bar\eps^{(n+1)}(t)\right]_{\leq t^q} $.
Now the proof is completed as in (1).
\end{proof}

\begin{lemma}\label{violins}
Suppose that $\ell=n+1+n'$.
The element
z :=
\sum_{\substack{r,s \geq 0 \\ r+s \leq n}} (-1)^{r+s}
v_n\big(x^{r}\big) \bar \eps^{(n+1)}_{n-r-s} \otimes u_n\big(x^{s}\big)
\in V_n^\ell\otimes_{\EOH_{n+1}^\ell} U_n^\ell
is central in the sense that $az = za$ for all $a \in \EOH_n^\ell$.
\end{lemma}

\begin{proof}
By \cref{lemma3}(b),
any element of $V_n^\ell \otimes_{\EOH_{n+1}^\ell} U_n^\ell$
can be written as $\sum_{p,q =0}^n v_n\big(x^p) f_{p,q} \otimes u_n\big(x^q\big)$ for unique $f_{p,q} \in \EOH_{n+1}^\ell$.
So there are unique
$L_{p,q}(t) = \sum_{k=0}^n L_{p,q;k} t^k,
R_{p,q}(t) =\sum_{k=0}^n R_{p,q;k} t^k
\in \EOH_{n+1}^\ell [t]$
such that
\begin{align*}
\bar\eps^{(n)}(t) z &=
\sum_{p,q =0}^n (-1)^{p+q} v_n\big(x^p) L_{p,q}(t) \otimes u_n\big(x^q\big),&
z \bar\eps^{(n)}(t)
\sum_{p,q =0}^n (-1)^{p+q} v_n\big(x^p) R_{p,q}(t) \otimes u_n\big(x^q\big).
\end{align*}
To prove the lemma,
it suffices to show that
$\bar\eps^{(n)}(t) z = z \bar\eps^{(n)}(t)$,
which we do by computing $L_{p,q}(t)$ and
$R_{p,q}(t)$ explicitly then checking that
$L_{p,q;k} = R_{p,q;k}$ for all $0 \leq p,q,k \leq n$.
For brevity, we adopt the convention that
$\eps^{(n+1)}_r = 0$ for $r < 0$; this allows the
restriction $r+s \leq n$ on the summation in the definition
of $z$ to be omitted.

To compute $L_{p,q}(t)$, we expand
$\bar\eps^{(n)}(t) z$ using \cref{newrelsfancy2}, \cref{simpson}(1) and \cref{newigr}:
\begin{align*}
\bar\eps^{(n)}(t) z &=
\sum_{r,q \geq 0} (-1)^{r+q}
\bar\eps^{(n)}(t) v_n\big(x^{r}\big) \bar \eps^{(n+1)}_{n-r-q} \otimes u_n\big(x^{q}\big)\\
\sum_{r,q \geq 0}(-1)^{r+q+n(r+1)} v_n\big(((-1)^{n+r}t- x)^{-1} x^r\big)\,
\bar \eps^{(n+1)}\big((-1)^{n+r}t\big)\bar \eps^{(n+1)}_{n-r-q} \otimes u_n\big(x^{q}\big)\\
\sum_{r,q \geq 0}\sum_{p=r}^n v_n(x^p)\left(
\left[\bar\eps^{(n+1)}\big((-1)^{n+r}t\big)\right]_{> t^p}
\bar \eps^{(n+1)}_{n-r-q}t^{r-p-1}\right) \otimes u_n\big(x^{q}\big)\\
\sum_{r,q \geq 0}
\sum_{p=0}^{r-1}
\left(
(-1)^{r+q+n(r+1)+(n+r)(r-p-1)} \left[\bar\eps^{(n+1)}\big((-1)^{n+r}t\big)\right]_{\leq t^p}
\bar \eps^{(n+1)}_{n-r-q}t^{r-p-1}\right) \otimes u_n\big(x^{q}\big).
\end{align*}
Hence, using $r+q+n(r+1)+(n+r)(r-p-1)+p+q\equiv
pr+pn+p+r\pmod{2}$ to simplify the sign,
we have that
\begin{multline}\label{adele}
\sum_{r=0}^{p}
\left[\bar\eps^{(n+1)}\big((-1)^{n+r}t\big)\right]_{> t^p}
\bar \eps^{(n+1)}_{n-r-q}t^{r-p-1}\\-
\sum_{r\geq p+1}
\left[\bar\eps^{(n+1)}\big((-1)^{n+r}t\big)\right]_{\leq t^p}
\bar \eps^{(n+1)}_{n-r-q}t^{r-p-1}
\end{multline}
for $0 \leq p,q \leq n$.
Similarly, we compute $R_{p,q}(t)$ using \cref{relsfancy3}, \cref{simpson}(2) and \cref{newigr}:
\begin{align*}
z\bar\eps^{(n)}(t) &=
\sum_{p,s \geq 0} (-1)^{p+s}
v_n\big(x^{p}\big) \bar \eps^{(n+1)}_{n-p-s} \otimes u_n\big(x^{s}\big)
\bar\eps^{(n)}(t) \\
\sum_{p,s \geq 0 } (-1)^{p+s+n(s+1)}
v_n\big(x^{p}\big) \bar \eps^{(n+1)}_{n-p-s}
\bar\eps^{(n+1)}\big((-1)^{s+1} t\big)\otimes
u_n\big(((-1)^{s+1}t-x)^{-1} x^s\big)\\
\sum_{p,s \geq 0} \sum_{q=s}^n v_n\big(x^{p}\big) \left((-1)^{p+s+n(s+1)+(s+1)(s-q-1)}
\bar \eps^{(n+1)}_{n-p-s}
\left[\bar\eps^{(n+1)}\big((-1)^{s+1}t\big)\right]_{> t^q}
t^{s-q-1}\right)\otimes  u_n(x^q)
\\
&\qquad-\sum_{p,s \geq 0} \sum_{q=0}^{s-1}
v_n\big(x^{p}\big) \left((-1)^{p+s+n(s+1)+(s+1)(s-q-1)} \bar \eps^{(n+1)}_{n-p-s}
\left[\bar\eps^{(n+1)}\big((-1)^{s+1}t\big)\right]_{\leq t^q}
t^{s-q-1}\right)\otimes u_n(x^q).
\end{align*}
From this, we get that
\begin{multline}\label{sinead}
R_{p,q}(t) =
\sum_{s=0}^{q}
\bar \eps^{(n+1)}_{n-p-s}
\left[\bar\eps^{(n+1)}\big((-1)^{s+1}t\big)\right]_{> t^q}
\sum_{s\geq q+1} (-1)^{ns+qs+n+1}
\bar \eps^{(n+1)}_{n-p-s}
\left[\bar\eps^{(n+1)}\big((-1)^{s+1}t\big)\right]_{\leq t^q}
\end{multline}
for $0 \leq p,q \leq n$.

Now we use \cref{adele,sinead} to compute the $t^k$-coefficients
and $R_{p,q;k}$ for $0 \leq k \leq n$:
\begin{align}\label{rumour}
L_{p,q;k} &=
\sum_{r=0}^k (-1)^{(n+k)(r+k)} \bar\eps^{(n+1)}_{n+r-p-k} \bar\eps^{(n+1)}_{n-r-q}
-\sum_{r\geq p+1} (-1)^{(n+k)(r+k)} \bar\eps^{(n+1)}_{n+r-p-k} \bar\eps^{(n+1)}_{n-r-q},\\
R_{p,q;k} &= \sum_{s=0}^k (-1)^{(n+k)s} \bar\eps^{(n+1)}_{n-p-s} \bar\eps^{(n+1)}_{n+s-q-k}-
\sum_{s\geq q+1} (-1)^{(n+k)s} \bar\eps^{(n+1)}_{n-p-s} \bar\eps^{(n+1)}_{n+s-q-k}.\label{hasit}
\end{align}
The details of these two computations are very similar, so we just elaborate
on the first one.
Note that
\bar\eps^{(n+1)}\big((-1)^{n+r}t\big)
\bar \eps^{(n+1)}_{n-r-q}t^{r-p-1}
\sum_{j\in\Z}
\bar\eps^{(n+1)}_{n+1-j}
\bar \eps^{(n+1)}_{n-r-q}t^{j+r-p-1}.
To get a contribution of $t^k$ from this,
we must have that $j = k+p-r+1$,
in which case
\bar\eps^{(n+1)}_{n+1-j}
\bar \eps^{(n+1)}_{n-r-q}=
\bar\eps^{(n+1)}_{n+r-p-k}
\bar \eps^{(n+1)}_{n-r-q}.
Using these observations, it follows
the $t^k$-coefficients from the
first summation in \cref{adele}
\bar\eps^{(n+1)}_{n+r-p-k}
\bar \eps^{(n+1)}_{n-r-q}$
summing over $r$ with $0 \leq r \leq p$
such that $j := k+p-r+1$ satisfies $j > p$,
i.e., $0 \leq r \leq \min(k,p)$.
Similarly, the $t^k$-coefficients from the second
summation in \cref{adele} contribute
\bar\eps^{(n+1)}_{n+r-p-k}
\bar \eps^{(n+1)}_{n-r-q}$
summing over $r$ with $r \geq p+1$
such that $j := k+p-r+1$ satisfies $j \leq p$,
i.e., $r \geq \max(k,p)+1$.
Thus, we have shown that
L_{p,q;k} =
\sum_{r=0}^{\min(k,p)} (-1)^{(n+k)(r+k)} \bar\eps^{(n+1)}_{n+r-p-k} \bar\eps^{(n+1)}_{n-r-q}
-\sum_{r\geq \max(k,p)+1}
(-1)^{(n+k)(r+k)} \bar\eps^{(n+1)}_{n+r-p-k} \bar\eps^{(n+1)}_{n-r-q}.
This is exactly as in \cref{rumour} when $k \leq p$.
To see that it is also
equal to \cref{rumour} when $k > p$, one just has to cancel
the overlapping terms
when $p+1 \leq r \leq k$
in the first and second summations from \cref{rumour}.

It remains to see that $L_{p,q;k} = R_{p,q;k}$ for every $0 \leq p,q,k \leq n$.
In fact, the first summation in \cref{rumour} is equal to the first summation in
\cref{hasit}. This is easily seen on making the substitution $s=k-r$ in one of them. To see that the second summation in \cref{rumour} is equal to the second summation in \cref{hasit}, we substitute $m=r-p$ in \cref{rumour} and $m=s-q$ in \cref{hasit}, and the problem reduces to showing that
\sum_{m \geq 1} (-1)^{(n+k)(m+p+k)} \bar\eps^{(n+1)}_{n-k+m} \bar\eps^{(n+1)}_{n-p-q-m}
=\sum_{m \geq 1} (-1)^{(n+k)(m+q)} \bar\eps^{(n+1)}_{n-p-q-m} \bar\eps^{(n+1)}_{n-k+m}
for all $0 \leq p,q,k \leq n$.
In fact this equality already holds in $\OSym_{n+1}$ thanks to
\cref{badday} or, rather, the identity obtained from that by applying the involution $\smiley_{n+1}$.
\end{proof}

\begin{theorem}\label{cupsandcaps}
Suppose that $\ell=n+1+n'$.
There are unique even degree 0 superbimodule homomorphisms
\begin{align}
\coev_n&:\EOH_n^\ell \rightarrow V_{n}^\ell \otimes_{\EOH_{n+1}^\ell}
1 &\mapsto
\sum_{\substack{r,s \geq 0 \\ r+s \leq n}} (-1)^{n-r-s}
v_n\big(x^{r}\big) \bar \eps^{(n+1)}_{n-r-s} \otimes u_n\big(x^{s}\big)\\\intertext{and}
\ev_n&:U_{n}^\ell \otimes_{\EOH_n^\ell}
V_{n}^\ell \rightarrow \EOH_{n+1}^\ell\notag
\\\label{reallynot}
u_n\big(x^{r}\big) \otimes v_n\big(x^{s}\big)
\left\{
\begin{array}{ll}
\bar \gamm^{(n+1)}_{r+s-n}&\text{if $r+s\geq n$}\\
\end{array}\right.
\end{align}
the latter being true for all $r,s \geq 0$.
Moreover, the following compositions are identities:
\begin{equation}\label{zigzag1}
\begin{tikzcd}
\arrow[r,"\operatorname{can}"]
U_n^\ell\otimes_{\EOH_n^\ell} \EOH_n^\ell
\arrow[r,"\id\otimes\coev_n"]&
U_n^\ell\otimes_{\EOH_n^\ell} V_n^\ell \otimes_{\EOH_{n+1}^\ell}
\arrow[r,"\ev_n\otimes\id"]
\EOH_{n+1}^\ell\otimes_{EOH_{n+1}^\ell}
U_n^\ell \arrow[r,"\operatorname{can}"]&
\end{tikzcd}
\end{equation}\begin{equation}\label{zigzag2}
\begin{tikzcd}
\arrow[r,"\operatorname{can}"]
\EOH_n^\ell\otimes_{\EOH_n^\ell} V_n^\ell
\arrow[r,"\coev_n\otimes\id"]&
V_n^\ell\otimes_{\EOH_{n+1}^\ell} U_n^\ell \otimes_{\EOH_{n}^\ell}
\arrow[r,"\id\otimes\ev_n"]
\EOH_{n+1}^\ell
\arrow[r,"\operatorname{can}"]&
\end{tikzcd}
\end{equation}
Hence, $\coev_n$ and $\ev_n$ are the unit and counit of an adjunction making $\left(U_{n}^\ell, V_{n}^\ell\right)$
into a dual pair
of 1-morphisms in $\OGBim_\ell$.
\end{theorem}

Before proving the theorem, we write down several equivalent formulations of the
definitions of $\coev_n$ and $\ev_n$, assuming that such superbimodule homomorphisms do indeed exist.
For the unit of adjunction, the element $\coev_n(1)$ in the statement of \cref{cupsandcaps}
is equal to $(-1)^n z$ where $z$ is the central tensor from \cref{violins}.
In terms of generating functions, we have that
\begin{equation}
\coev_n(1) =
\left[v_n((t-x)^{-1})  \bar \eps^{(n+1)}(t)
\otimes u_n\big((t- x)^{-1}\big)
\right]_{t^{-1}}.\label{sundoor1}
\end{equation}
This is easily checked by computing coefficients of $t$.
Using \cref{relsfancy3,newrelsfancy2}
with $r=0$, we have that
\begin{align}
&= \bar\eps^{(n)}\big((-1)^{n}t\big)v_n\big((-1)^{n}\big),\label{crap1}\\\label{crap2}
\bar\eps^{(n+1)}(t) u_{n}\big((t-x)^{-1}\big)
&= u_n\big((-1)^{n}\big) \bar\eps^{(n)}(-t).
\end{align}
Hence, we can rewrite the right hand side of \cref{sundoor1}
to obtain
\begin{align}\label{fridoor}
\coev_n(1) &=
\left[v_n((t-x)^{-1})\otimes u_n\big((-1)^n \big)\bar\eps^{(n)}(-t) \right]_{t^{-1}}=
\left[\bar \eps^{(n)}\big((-1)^{n}t\big)v_n\big((-1)^n \big)\otimes u_n\big((t- x)^{-1}\big)
\right]_{t^{-1}}.
\end{align}
Equating coefficients in \cref{fridoor} gives two more formulae:
\begin{align}\label{Jackdoor}
\coev_n(1) &
\sum_{r=0}^n v_n\big(x^{r}\big) \otimes u_n(1) \bar \eps^{(n)}_{n-r}
= \sum_{s=0}^n
\bar \eps^{(n)}_{n-s}
v_n(1)\otimes u_n\big(x^{s}\big).
\end{align}
For the counit $\ev_n$, we have the following two equivalent formulations:
\begin{align}\label{ev1}
\ev_n\left(u_n\big((t- x)^{-1}f(x)\big) \otimes
&= \left[\bar \gamm^{(n+1)}(t) f(t)g(t)\right]_{<t^{0}}\\
\ev_n\left(u_n\big(f(x)\big) \otimes v_n\big(g(x)(t- x)^{-1}\big)\right)
&= \left[\bar \gamm^{(n+1)}(t) f(t)g(t)\right]_{<t^{0}}\label{ev2}
\end{align}
for any $f(x),g(x)\in\k[x]$.
This can be checked by
assuming that $f(x)=x^r, g(x) = x^s$ then equating coefficients of $t$.

\begin{proof}[Proof of \cref{cupsandcaps}]
We split the proof up into six steps.

\vspace{1mm}
\noindent{\em Step one.}
We first construct the maps $\coev_n$ and $\ev_n$.
For $\coev_n$, we define
$\coev_n(a) := (-1)^n az$ for any $a \in \EOH_n^\ell$,
where $z$ is as in \cref{violins}.
This is an even degree 0 homomorphism of graded left $\EOH_n^\ell$-supermodules.
Since $(-1)^n az = (-1)^n za$ according to \cref{violins},
it is also a right $\EOH_n^\ell$-supermodule homomorphism, so it is a
superbimodule homomorphism.
Thus, we have defined the superbimodule homomorphism $\coev_n$, and
\cref{notsobad} holds.
For $\ev_n$,
$U_n^\ell \otimes_{\EOH_n^\ell} V_n^\ell$ is a free graded right $\EOH_{n+1}^\ell$-supermodule with basis
$u_n(x^r) \otimes v_n(x^s)\:(0 \leq r \leq n', 0 \leq s \leq n)$
by \cref{lemma3}(1b) and (2a).
So there is a unique even degree 0
graded right $\EOH_{n+1}^\ell$-supermodule homomorphism $\ev_n$ such that
\cref{reallynot} holds for $0 \leq r \leq n'$ and $0 \leq s \leq n$.
It is not yet clear that \cref{reallynot} holds for other values of $r$ and $s$,
or that $\ev_n$ is a graded left $\EOH_{n+1}^\ell$-supermodule homomorphism.

\vspace{1mm}
\noindent
{\em Step two.}
Next we use induction to show that
\cref{reallynot} also holds for $0 \leq r \leq n'$ and all
$s > n$.
Fix a choice of $r$ with $0 \leq r \leq n'$.
We know by our definition that \cref{reallynot} holds for $0 \leq s \leq n$.
For the induction step, we take some $s \geq n$, assume that \cref{reallynot}
holds for this and all smaller values of $s$, and show that it also holds
when $s$ is replaced by $s+1$.
The $m=0$ case of \cref{neweasypeasy}(2) shows that
$x_1^{n+1} = \sum_{p=0}^n (-1)^{n-p} x_1^p e^{(n+1)}_{n+1-p}$.
Multliplying on the left
by $x_1^{s-n}$ then applying $\smiley_{n+1}$, we deduce that
$x_{n+1}^{s+1} = \sum_{p=0}^n(-1)^{n-p} x_{n+1}^{p+s-n} \eps_{n+1-p}^{(n+1)}$.
u_n\big(x^r\big) \otimes v_n\big(x^{s+1}\big)
\sum_{p=0}^n (-1)^{n-p} u_n\big(x^r\big)\otimes v_n\big(x^{p+s-n}\big)
\bar\eps^{(n+1)}_{n+1-p}.
Now we apply the right supermodule homomorphism
$\ev_n$ using the induction hypothesis
to see that
\ev_n\Big(
u_n\big(x^r\big) \otimes v_n\big(x^{s+1}\big)\Big)
=  \sum_{p=\max(0,2n-r-s)}^n (-1)^{n-p} \bar \eta_{p+r+s-2n}^{(n+1)}
\bar\eps^{(n+1)}_{n+1-p}.
This is equal to $\bar \eta_{r+s+1-n}^{(n+1)}$ by \cref{newigr},
which is what we wanted.

\vspace{1mm}
\noindent
{\em Step three.}
Since $\ev_n$ is a right supermodule homomorphism by definition,
the composition of maps in \cref{zigzag1} makes sense
and is a right $\EOH_n^\ell$-supermodule homomorphism\footnote{
However, \cref{zigzag2} does not make sense at this point
since $\id \otimes \ev_n$ is not defined until we can shown that $\ev_n$
is a left supermodule homomorphism.}.
To show that the composition is equal to the identity map,
it suffices to show that it
takes $u_n(f(x))$ to $u_n(f(x))$ for any $f(x) \in \k[x]$ of degree $\leq n'$,
since these elements generate $U_n^\ell$ as a right $\EOH_n^\ell$-supermodule
by \cref{lemma3}(2a).
Using \cref{sundoor1}, we apply the even map
$\id \otimes \coev_n$ to $u_n(f(x))\otimes 1$
to obtain
\left[u_n\big(f(x)\big)\otimes v_n\big((t-x)^{-1}\big)
\otimes \bar \eps^{(n+1)}(t)
By step two, \cref{ev2} holds for $f(x)$ of degree $\leq n'$.
We use it to apply $\ev_n \otimes \id$, then multiply out the tensor,
to obtain
\left[\big[\bar \gamm^{(n+1)}(t) f(t)\big]_{<t^{0}}
\bar \eps^{(n+1)}(t) u_n\big(( t-x)^{-1}\big)\right]_{t^{-1}}.
Now, \cref{crap2} shows that $\bar \eps^{(n+1)}(t) u_n\big((t-x)^{-1}\big)$ is a polynomial in $t$, so we can omit the inside square brackets. Then
the $\gamm$ and $\eps$ cancel by \cref{newigr}, leaving us with
\left[f(t) u_n\big((t-x)^{-1}\big)\right]_{t^{-1}} =
where we applied \cref{why} for the final equality. Hence, the composition \cref{zigzag1}
is the identity.

\vspace{1mm}
\noindent
{\em Step four.}
We prove that $\ev_n$ is a left supermodule homomorphism.
Since $v_n(1)$ generates $V_n^\ell$ as a superbimodule (\cref{lemma3}(1c))
and $\ev_n$ is a right supermodule homomorphism, it suffices to show that
$a \ev_n(u \otimes v_n(1)) = \ev_n(au \otimes v_n(1))$ for all
$a \in \EOH_{n+1}^\ell$ and $u \in U_n^\ell$.
By step three, we have that
a \left((\ev_n \otimes \id) \circ (\id \otimes\coev_n)(u \otimes 1)\right) = a(1 \otimes u)
= (1 \otimes au) =
(\ev_n \otimes \id) \circ (\id \otimes\coev_n)(au \otimes 1)
in $\EOH_{n+1}^\ell\otimes_{\EOH_{n+1}^\ell} U_n^\ell$.
Using the formula for $\coev_n(1)$ from \cref{Jackdoor}, this shows that
\sum_{s=0}^n
a \ev_n\big(u \otimes \bar \eps^{(n)}_{n-s}
v_n(1)\big)\otimes u_n\big(x^{s}\big)
\sum_{s=0}^n
\ev_n\big(au \otimes \bar \eps^{(n)}_{n-s}
v_n(1)\big)\otimes u_n\big(x^{s}\big).
By \cref{lemma3}(2b), $U_n^\ell$ is a free left $\EOH_{n+1}^\ell$-supermodule
with basis $u_n(x^s)\:(0 \leq s \leq n)$, so we can project to
$-\otimes u_n(x^n)$-components in the identity just proved
to obtain the
desired equality $a \ev_n\big(u \otimes v_n(1)\big) = \ev_n\big(au \otimes v_n(1)\big)$.

\vspace{1mm}
\noindent
{\em Step five.}
We know already that \cref{reallynot} holds for $0 \leq r \leq n'$ and $s \geq 0$.
We now show that it holds for all remaining $r > n'$ and $s \geq 0$.
Take $r \geq n'$ and
assume by induction that \cref{reallynot} holds for this value of $r$ and
all $s \geq 0$.
Equating $t^n$-coefficients in \cref{rels1b} gives
that $u_n\big(x^{r+1}\big)
= \bar o^{(n+1)} u_n\big(x^r\big)
+ (-1)^r u_n\big(x^r\big) \bar o^{(n)}$.
Equating $t^n$-coefficients in \cref{newrels1}
(with $r$ replaced by $s$) gives that $v_n\big(x^{s+1}\big)= v_n\big(x^s\big) \bar o^{(n+1)}
- (-1)^{n+s} \bar o^{(n)} v_n\big(x^s\big)$.
Making these substitutions, it is then easy to check that
\begin{equation*}
u_n\big(x^{r+1}\big) \otimes v_n\big(x^s\big) = (-1)^{n+r+s+1} u_n\big(x^r\big) \otimes v_n(x^{s+1})
+ (-1)^{n+r+s} u_n\big(x^r\big) \otimes v_n\big(x^s\big) \bar o^{(n+1)}
+ \bar o^{(n+1)} u_n\big(x^r\big) \otimes v_n\big(x^s\big).
\end{equation*}
Now we compute $\ev_n\Big(u_n\big(x^{r+1}\big) \otimes v_n\big(x^s\big)\Big)$
by applying the superbimodule homomorphism $\ev_n$ to the right hand side of the equation just derived and using the induction hypothesis. If $r+s+1<n$ the right hand side evaluates to $0$
so $\ev_n\Big(u_n\big(x^{r+1}\big) \otimes v_n\big(x^s\big)\Big) = 0$ as required.
If $r+s+1=n$ the right hand side evaluates to $\bar \eta^{(n+1)}_{r+1+s-n}$
as required. If $r+s+1>n$ the right hand side evaluates to
(-1)^{n+r+s+1} \bar \eta^{(n+1)}_{r+1+s-n} + (-1)^{n+r+s}  \bar\eta^{(n+1)}_{r+s-n}
\bar o^{(n+1)} + \bar o^{(n+1)} \bar\eta^{(n+1)}_{r+s-n}.
If $n+r+s$ is odd then $\bar\eta^{(n+1)}_{r+s-n}$ and $\bar o^{(n+1)}$
commute by the image of the defining relation \cref{osym1b} under $\smiley$, so this simplifies to
the desired $\bar\eta^{(n+1)}_{r+1+s-n}$.
If $n+r+s$ is even then $\bar\eta^{(n+1)}_{r+s-n} \bar o^{(n+1)} + \bar o^{(n+1)} \bar\eta^{(n+1)}_{r+s-n} = 2 \bar\eta^{(n+1)}_{r+1+s-n}$ by the image of
the second relation from \cref{osym5}
under $\smiley$, so again the expression simplifies to

\vspace{1mm}
\noindent
{\em Step six.}
It remains to check that the composition
\cref{zigzag2}, which makes sense as $\ev_n$ is a left supermodule homomorphism, is the identity.
We do this by showing
that it takes $v_n(f(x))$ to $v_n(f(x))$ for any $f(x) \in \k[x]$.
The argument is similar to step three.
By \cref{sundoor1},
the map $\coev_n \otimes \id$ takes $1 \otimes v_n(f(x))$ to
\left[v_n\big((t-x)^{-1}\big)\bar\eps^{(n+1)}(t) \otimes u_n\big((t- x)^{-1}\big) \otimes v_n\big(f(x)\big)
\right]_{t^{-1}}.
Then we apply the even map $\id \otimes \ev_n$ using \cref{ev1} (whose validity relies on the conclusion of step five)
to get
$$\left[v_n\big((t-x)^{-1}\big)\bar \eps^{(n+1)}(t)
\big[\bar \gamm^{(n+1)}(t) f(t)\big]_{<t^{0}}\right]_{t^{-1}}.
Since $v_n\big((t-x)^{-1}\big)\bar \eps^{(n+1)}(t)$
is a polynomial in $t$ by \cref{crap1},
we can omit the inside square brackets. After doing that,
$\eps$ and $\gamm$ cancel using \cref{newigr}, so we obtain
\left[v_n\left((t-x)^{-1}\right)
f(t)\right]_{t^{-1}} = v_n\big(f(x)\big),
where we used \cref{why} for the final equality.
\end{proof}

\iffalse
% This is the old proof which was wrong...

\begin{proof}[Proof of \cref{cupsandcaps}]
We split the argument into several steps.

\vspace{1mm}
\noindent{\em Step one:
$\ev_n$ is a superbimodule homomorphism.}
To see this, we actually give a more transparent definition of this map.
We saw in the proof of \cref{lemma0} that
$V_{n}^\ell = (\Pi Q^{-2})^{n}\OSym_{(n,1,n')}\otimes_{\OSym_\ell} R_\ell$
is a free $R_\ell$-supermodule
generated by vectors of the form $b \otimes 1$
for $b \in \OSym_{(n,1)}$, and moreover the right action of
$\OSym_{n+1}$ defined for $f \in \OSym_{n+1}$
by $(b \otimes 1) \cdot f := bf \otimes 1$
is an action by $R_\ell$-supermodule endomorphisms.
Similarly $U_{n}^\ell = R_\ell \otimes_{\OSym_\ell} \OSym_{(n',1,n)}$
is a free $R_\ell$-supermodule generated
by vectors of the form $1 \otimes \sig_{n'}(a)$
for $a \in \OSym_{(1,n)}$, and the left action of $\OSym_{n+1}$
for $f \in \OSym_{n+1}$
by $f \cdot (1 \otimes \sig_{n'}(a)) := (-1)^{n'\parity(f)}
1 \otimes \sig_{n'}(f a)$ is an action by $R_\ell$-supermodule endomorphisms.
Consider the $R_\ell$-supermodule homomorphism
\begin{align}\label{thehardformula}
\theta:
U_{n}^\ell \otimes_{R_\ell} V_{n}^\ell
&\rightarrow \OSym_{(n+1,n')}\otimes_{\OSym_\ell} R_\ell,\\\notag
\left(1 \otimes \sig_{n'}(a)\right) \otimes \left(
b \otimes 1\right) &\mapsto
\tau_1 \cdots \tau_n \cdot \big({^{s_n \cdots s_1} a}\big) b \otimes 1
\end{align}
for $a \in \OSym_{(1,n)}$ and $b \in \OSym_{(n,1)}$.
Note that $\theta$ is even of degree 0. We claim that it
is $\OSym_n$-balanced for the
natural left action of $\OSym_n$ on $V_{n}^\ell$
and the
right action
on $U_{n}^\ell$ defined by restriction along $\sig_{n'+1}\circ\operatorname{p}^{n'+1}:
\OSym_n \rightarrow \OSym_{(n',1,n)}$, i.e., acting with
$f \in \OSym_n$ takes $1\otimes\sig_{n'}(a)$ to $(-1)^{(n'+1)\parity(f)}
1 \otimes \sig_{n'}(a\sig_1(f))$.
To see this, we have to show that
(-1)^{n+(n'+1)\parity(f)}\theta\left(1 \otimes \sig_{n'}(a\sig_1(f))  \otimes (b \otimes 1)\right)=
(-1)^{n+n\parity(f)}\theta\left((1 \otimes \sig_{n'}(a) \otimes (f b \otimes 1)\right)
for $a \in \OSym_{(1,n)}, b \in \OSym_{(n,1)}$ and $f \in \OSym_n$.
This follows because
${^{s_n \cdots s_1}}\sig_1(f) = (-1)^{(n-1)\parity(f)} f$,
as is easily checked by contemplating ${^{s_n\cdots s_1}}x_i\:(i=2,\dots,n+1)$,
\begin{align*}
\theta\left(1 \otimes \sig_{n'}(a \sig_1(f)) \otimes (b \otimes 1)\right)&=
(-1)^{n+n'\parity(a)+n\parity(f)} \tau_1 \cdots \tau_n \cdot \big({^{s_n \cdots s_1}a}\big) f b\otimes 1\\
&=(-1)^{n+n\parity(f)}\theta\left((1 \otimes \sig_{n'}(a) \otimes (f b \otimes 1)\right).
\end{align*}
Now the first claim is checked, and it implies that $\theta$
induces an $R_\ell$-supermodule homomorphism
\bar \theta:
U_{n}^\ell \otimes_{\EOH_n^\ell} V_{n}^\ell
\rightarrow  \OSym_{(n+1,n')}\otimes_{\OSym_\ell} R_\ell.
We next claim that $\bar \theta$ is an $(\OSym_{n+1},\OSym_{n+1})$-superbimodule
homomorphism. This is obvious for the right actions.
To see it for the left actions, we must show that
\tau_1 \cdots \tau_n \cdot \left({^{s_n\cdots s_1}} (fa)\right)\otimes 1
= f \tau_1 \cdots \tau_n \cdot \left({^{s_n \cdots s_1}}a\right)\otimes 1
for all $a \in \OSym_{(1,n)}$ and $f \in \OSym_{n+1}$.
Using the definition \cref{betteract},
the proof of this reduces to showing for each $i=n,\dots,1$
that $\tau_i \cdot \left({^{s_i \cdots s_1}} f\right)=0$
for $f \in \OSym_{n+1}$. It suffices to check this for
$f = (t+x_1)\cdots(t+x_{n+1})$, when it is clear
as ${^{s_i\cdots s_1}} f =
(t-x_1)\cdots (t-x_{i-1})(t+x_{i+1})(t+x_i)$
which is annihilated by $\partial_i$.
The second claim is now proved.
Then we post-compose $\bar \theta$ with
the inverse of the isomorphism
$\EOH_{n+1}^\ell \stackrel{\sim}{\rightarrow}
\OSym_{(n+1,n')}\otimes_{\OSym_\ell} R_\ell
$ from \cref{EOH}(1).
The second claim implies that this is produces an $\big(\EOH_{n+1}^\ell,\EOH_{n+1}^\ell\big)$-superbimodule
$U_{n}^\ell\otimes_{\EOH_n^\ell} V_{n}\rightarrow \EOH_{n+1}^\ell$.
Finally, we observe that this is the map
$\ev_n$ from the statement of the theorem because
it takes $u_n(x^r) \otimes v_n(x^s)$
(-1)^n \tau_1\cdots \tau_n\cdot \left({^{s_n\cdots s_1}} x_{1}^r\right)
x_{n+1}^s \hatotimes 1=
(-1)^n \tau_1\cdots \tau_n\cdot
x_{n+1}^{r+s} \hatotimes 1=
\bar \gamm_{r+s-n}^{(n+1)},
where the final equality follows from
the identity obtained by applying $\smiley_{n}$
to \cref{yesIneedit}.
This completes the proof that $\ev_n$ is a superbimodule homomorphism.

\vspace{1mm}
\noindent
{\em Step two: the zig-zag identities hold.}
For $\coev_n$, we
define it to be the unique even degree 0 homomorphism of
graded {\em right} $\EOH_n^\ell$-supermodules
taking the identity element $1 \in \EOH_n^\ell$ to the expression
in the statement of the theorem.
It is not yet clear that it is a {\em left} $\EOH_{n+1}^\ell$-supermodule homomorphism.
We will deduce this in step three after we have checked the zig-zag identities.
To check the zig-zag identities,
we take a polynomial $f(x) \in \k[x]$. We first show that
$\big((\id \otimes \ev_n) \circ (\coev_n \otimes \id)\big)\Big(v_n\big(f(x)\big)\Big) = v_n\big(f(x)\big)$.
By \cref{sundoor1}, the map $\coev_n \otimes\id$ takes $v_n\big(f(x)\big)$ to
(-1)^{n+1}\left[v_n\big((t-x)^{-1}\big)\bar\eps^{(n+1)}(-t) \otimes u_n\big((t- x)^{-1}\big) \otimes v_n\big(f(x)\big)
\right]_{t^{-1}}.
Then we apply the second (even) map using \cref{ev1}
to get
$$(-1)^{n+1} \left[v_n\big((t-x)^{-1}\big)\bar \eps^{(n+1)}(-t)
\big[\bar \gamm^{(n+1)}(t) f(t)\big]_{<t^{0}}\right]_{t^{-1}}.
Since $v_n\big((t-x)^{-1}\big)\bar \eps^{(n+1)}(-t)
= -\bar \eps^{(n)}\big((-1)^{n+1}t\big)v_n(1)$ and, crucially, this is a polynomial in $t$,
we can omit the inside square brackets. After doing that,
$\eps$ and $\gamm$ cancel using \cref{newigr}, so we obtain
\left[v_n\left((t-x)^{-1}\right)
f(t)\right]_{t^{-1}} = v_n\big(f(x)\big),
where we used \cref{why} for the final equality.
The check of the second zig-zag identity, namely, that
$((\ev_n \otimes \id) \circ (\id \otimes \coev_n))\Big( u_n\big(f(x)\big)\Big) = u_n\big(f(x)\big)$ is similar:
applying the unit gives us
(-1)^{n+1}\left[u_n\big(f(x)\big)\otimes v_n\big((t-x)^{-1}\big)
\otimes \bar \eps^{(n+1)}(-t)
Then we use \cref{ev2} to get
(-1)^{n+1} \left[\big[\bar \gamm^{(n+1)}(t) f(t)\big]_{<t^{0}}
\bar \eps^{(n+1)}(-t)u_n\big(( t-x)^{-1}\big)\right]_{t^{-1}}.
Again we use that $\bar \eps^{(n+1)}(-t) u_n\big((t-x)^{-1}\big)$ is a polynomial in $t$ to see that we can omit the inside square brackets. Then
the $\gamm$ and $\eps$ cancel by the infinite Grassmannian relation, leaving us with
\left[f(t) u_n\big((t-x)^{-1}\big)\right]_{t^{-1}} =
Both zig-zag identities are now proved.

\vspace{1mm}
\noindent{\em Step three: $\coev_n$ is a superbimodule homomorphism.}
It remains to show that $\coev_n$, which we have defined so that it is
a right $\EOH_n^\ell$-supermodule homomorphism, is also a left $\EOH_{n}^\ell$-supermodule homomorphism.
It suffices to show that
$\bar \eps^{(n)}_r \coev_n(1) = \coev_n(1) \bar \eps^{(n)}_r$
for all $r \geq 1$. We show
that $\bar \eps^{(n)}\big((-1)^n t\big) \coev_n(1) = \coev_n(1)
\bar\eps^{(n)}\big((-1)^n t\big)$.
By \cref{lemma3}(1a),
this follows if we can show that
$\bar \eps^{(n)}\big((-1)^n t\big) \coev_n(1) \otimes
v_n(1) = \coev_n(1)
\bar\eps^{(n)}\big((-1)^n t\big ) \otimes v_n(1)$
in $V_{n}^\ell \otimes_{\EOH_{n+1}^\ell}
U_{n}^\ell \otimes_{\EOH_n^\ell}
The zig-zag identities imply that
$\id \otimes \ev_n$ is injective, so we can apply it to
this equation to reduce the problem one more time
to that of showing
\Big(\id \otimes \ev_n\Big) \Big(
\bar \eps^{(n)}\big((-1)^n t\big) \coev_n(1) \otimes v_n(1)\Big) =
\Big(\id \otimes \ev_n\Big)\Big(
\coev_n(1)
\bar\eps^{(n)}\big((-1)^n t\big ) \otimes v_n(1)\Big).
By the zig-zag identities again, the left hand side is simply equal to
$\bar\eps^{(n)}\big((-1)^n t\big) v_n(1)
=  v_n(t+x) \bar\eps^{(n+1)}(t)$.
To see that the right hand side is equal to this, we
commute $\bar\eps^{(n)}\big ((-1)^nt\big )$
to the right to
\Big(\id
\otimes \ev_n\Big)\Big(
\coev_n(1)
\otimes
\bar\eps^{(n)}\big((-1)^n t\big)
\Big(\id
\otimes \ev_n\Big)\Big(
\coev_n(1)
\otimes
\Big).
We {\em do} know that $\ev_n$ is a right $\EOH_{n+1}^\ell$-supermodule
homomorphism, so we can now compute this using the zig-zag identity a final time to see that it equals
$v_n\big((t+x)^{-1}\big)\bar \eps^{(n+1)}(t)$.
This completes the proof.
\end{proof}
\fi

For the following corollary, recall from \cref{buckley} that
$\EONH_n^\ell$ is a subalgebra of $\EONH_{n+1}^\ell$ in a natural way
for $0 \leq n < \ell$.

\begin{corollary}\label{indresrel}
For $0 \leq n < \ell$, the following diagrams of graded superfunctors commute up to even degree 0 isomorphisms:
\begin{tikzcd}
\arrow[d,"(\overline{\omega\chi})_{n+1}-" left]
\EONH_{n+1}^\ell\sMod
\arrow[rr,"\!\!{(\Pi Q^{-2})^n \res_{\EONH_n^\ell}^{\EONH_{n+1}^\ell}}" above]&&
\EONH_{n}^\ell\sMod\arrow[d,"(\overline{\omega\chi})_n-" right]\\
\EOH_{n+1}^\ell\sMod\arrow[rr,"{V_{n}^\ell \otimes_{\EOH_{n+1}^\ell}\!\!\!\!\!-}" below]&&\EOH_{n}^\ell\sMod
\end{tikzcd}\qquad
\begin{tikzcd}
\arrow[rr,"(\Pi Q^{2})^n \ind_{\EONH_n^\ell}^{\EONH_{n+1}^\ell}" above]
\arrow[d,"(\overline{\omega\chi})_n-" left]
\EONH_{n}^\ell\sMod
&&\arrow[d,"(\overline{\omega\chi})_{n+1}-" right]\EONH_{n+1}^\ell\sMod
\\
\arrow[rr,"U_{n}^\ell \otimes_{\EOH_{n}^\ell}-\!\!" below]\EOH_{n}^\ell\sMod
\end{tikzcd}
(The vertical arrows are the equivalences
of graded supercategories from \cref{veryslow}.)
\end{corollary}

\begin{proof}
Note that
$(\Pi Q^2)^n \ind_{\EONH_n^\ell}^{\EONH_{n+1}^\ell}$
is left adjoint to $(\Pi Q^{-2})^n \res_{\EONH_n^\ell}^{\EONH_{n+1}^\ell}$.
Also $U_n^\ell\otimes_{\EOH_n^\ell}-$ is left adjoint to
$V_n^\ell\otimes_{\EOH_{n+1}^\ell}-$ by \cref{cupsandcaps}.
Hence, using the uniqueness of left adjoints,
it suffices to prove that the first square commutes.
We show equivalently that the following commutes up to even degree 0 isomorphism:
\begin{tikzcd}
\EONH_{n+1}^\ell\sMod
\arrow[rr,"{\res_{\EONH_n^\ell}^{\EONH_{n+1}^\ell}}" above]&&
\EONH_{n}^\ell\sMod\arrow[d,"(\overline{\omega\chi})_n-" right]\\
\arrow[u,"\OPol_{n+1} \otimes_{\OSym_{n+1}}\EOH_{n+1}^\ell\otimes_{\EOH_{n+1}^\ell}-" left]
\EOH_{n+1}^\ell\sMod\arrow[rr,"{\tV_{n}^\ell \otimes_{\EOH_{n+1}^\ell}\!\!\!\!\!-}" below]&&\EOH_{n}^\ell\sMod
\end{tikzcd}
Here, we have removed the degree and parity shifts on the horizontal arrows
and we have replaced the equivalence
$(\overline{\omega\chi})_{n+1}- \simeq
\Hom_{\ONH_{n+1}^\ell}\big(\ONH_{n+1}^\ell (\overline{\omega\chi})_{n+1},-\big)$
on the left hand vertical arrow with the
quasi-inverse equivalence
$\ONH_{n+1}^\ell (\overline{\omega\chi})_{n+1}
\otimes_{\EOH_{n+1}^\ell}-
\simeq \OPol_{n+1}\otimes_{\OSym_{n+1}}\EOH_{n+1}^\ell
\otimes_{\EOH_{n+1}^\ell}-$.
To prove this new diagram commutes, it suffices to show that
(\omega\chi)_n \OPol_{n+1} \otimes_{\OSym_{n+1}} \EOH_{n+1}^\ell
\simeq
\tV_{n}^\ell
as $(\EOH_n^\ell,\EOH_{n+1}^\ell)$-superbimodules.
As the proof of \cref{lemma0}(1) in the case $d=0$ shows, the isomorphism
$\EOH_{n+1}^\ell \stackrel{\sim}{\rightarrow}
\OSym_{(n+1,n')} \otimes_{\OSym_\ell} R_\ell$
of \cref{EOH}(1) is an isomorphism of
graded $(\EOH_{n+1}^\ell,\EOH_{n+1}^\ell)$-superbimodules.
$(\omega\chi)_n \OPol_{n+1} \otimes_{\OSym_{n+1}} \EOH_{n+1}^\ell
\simeq
(\omega\chi)_{n} \OPol_{n+1} \otimes_{\OSym_{n+1}}
\OSym_{(n+1,n')} \otimes_{\OSym_\ell} R_\ell$.
By \cref{newsnow},
we have that $(\omega\chi)_n \OPol_{n+1} \simeq
\OSym_{(n,1)}$, so
this is
$\simeq \OSym_{(n,1,n')}\otimes_{\OSym_\ell} R_\ell$,
which is exactly the definition of $\tV_{n}^\ell$.
\end{proof}

The next theorem, which we prove by twisting \cref{cupsandcaps} with
some automorphisms,
gives the second adjunction. The explicit formulae for
this are not as nice as for the first adjunction.

\begin{theorem}\label{secondadjunction}
Suppose that $\ell=n+1+n'$.
There are unique even degree 0 superbimodule homomorphisms
\begin{align*}\tcoev_n&:
\EOH_{n+1}^\ell
\rightarrow \tU_{n}^\ell \otimes_{\EOH_{n}^\ell}
\tV_{n}^\ell\\
1 &\mapsto
%(-1)^{(n+1)r+\binom{r}{2}} \Big[\tu_n(x^r) -
%  (-1)^{n'}  \big(1-(-1)^r\big)\dot o^{(\ell)} \tu_n(x^{r-1})\Big] \otimes \tv_n(1) \Big[\big(\psi_{n+1}^\ell\big)^{-1}\Big(\bar\eps_{n'-r}^{(n')}\Big)\Big]\\&\qquad\qquad=
\sum_{s=0}^{n'}
(-1)^{\ell s+\binom{s}{2}}
\big(\psi_{n+1}^\ell\big)^{-1}\Big(\bar\eps_{n'-s}^{(n')}\Big)
\tu_n(1) \otimes \tv_n(x^s)\\\intertext{and}\tev_n&:
\tV_{n}^\ell \otimes_{\EOH_{n+1}^\ell}
\tU_{n}^\ell \rightarrow \EOH_{n}^\ell\\
\!\!\!\tv_n(x^r)\otimes \tu_n(x^s)&\mapsto
\left\{
\begin{array}{ll}
\!\!(-1)^{n(r+s)+\binom{r}{2}+\binom{s+1}{2}}
\Big[\big(\psi_{n}^\ell\big)^{-1} \Big(
\bar\gamm_{r+s-n'}^{(n'+1)}
+(-1)^{n+1}\big(1-(-1)^s\big) \bar\eta_{r+s-n'-1}^{(n'+1)} \dot o^{(\ell)}
\Big)\Big]
&\text{if $r+s> n'$}\\
\!\!(-1)^{n(r+s)+\binom{r}{2}+\binom{s+1}{2}}
&\text{if $r+s=n'$}\\
\end{array}\right.
\end{align*}
giving the unit and counit of an adjunction making
$\left(\tV_{n}^\ell, \tU_{n}^\ell\right)$
into another dual pair of 1-morphisms in $\OGBim_\ell$.
\end{theorem}

\begin{proof}
Let $\dagger := \phi_{n'}^\ell \circ *:\tU_n^\ell
\rightarrow V_{n'}^\ell$, where $\phi_{n'}^\ell$ is the map
from \cref{crazycrazy}.
Since $\psi_{n+1}^\ell = \delta_{n'}^\ell \circ
\big(\psi_{n'}^\ell\big)^{-1}$
and $\psi_n^\ell = \delta_{n'+1}^\ell \circ
\big(\psi_{n'+1}^\ell\big)^{-1}$
according to the definition \cref{deltadef},
\cref{crazycrazy} and \cref{lemma0b}(2) imply that
\begin{equation}\label{lemma0bchanged}
\left(\bar b_1 u \bar b_2\right)^{\dagger} = \psi_{n+1}^\ell(\bar b_1) u^{\dagger} \psi_{n}^\ell(\bar b_2)
\end{equation}
for $u \in \tU_n^\ell$, $b_1 \in \OSym_{n+1}$ and $b_2
\in \OSym_n$.
Now we define even degree 0 graded $R_\ell$-supermodule homomorphisms
$\tcoev_n$ and $\tev_n$
so that the following diagrams commute:
\begin{equation*}
\arrow[d,"\psi^\ell_{n+1}" left]
\EOH_{n+1}^\ell\arrow[r,"\tcoev_n" above]&
\tU_{n}^\ell \otimes_{\EOH_{n}^\ell}
\tV_{n}^\ell\arrow[d,"\dagger \otimes *" right]\\
\EOH_{n'}^\ell
\arrow[r,"\coev_{n'}" below] &V^\ell_{n'}\otimes_{\EOH_{n'+1}^\ell} U^\ell_{n'}
\end{tikzcd}}
\qquad\qquad
\tV_n^\ell\otimes_{\EOH_{n+1}^\ell} \tU_n^\ell
\arrow[r,"\tev_n" above]\arrow[d,"*\otimes \dagger" left]&
\EOH_n^\ell\arrow[d,"\psi_n^\ell" right]\\
U_{n'}^\ell\otimes_{\EOH_{n'}^\ell} V_{n'}^\ell
\arrow[r,"\ev_{n'}" below]
\end{tikzcd}}
\end{equation*}
To see that the vertical maps $\dagger\otimes *$ and $* \otimes \dagger$ in these diagrams make sense, one needs to check that they are balanced,
which follows using
\cref{lemma0b}(1) and \cref{lemma0bchanged}.
In fact, $\tcoev_n$ and $\tev_n$ defined
in this way are superbimodule homomorphisms.
This again follows using
\cref{lemma0b}(1) and \cref{lemma0bchanged}
since $\coev_{n'}$ and $\ev_{n'}$ are superbimodule homomorphisms.

The zig-zag identities
for $\tcoev_n$ and $\tev_n$
follow from their definitions using the zig-zag identities
\cref{zigzag1,zigzag2}
for $\coev_{n'}$ and $\ev_{n'}$.
Hence they give the unit and counit of an adjunction.

It just remains to compute the explicit formulae for the maps given in
the statement of the corollary.
To see that $\tcoev_n(1) = \sum_{s=0}^{n'}
(-1)^{\ell s + \binom{s}{2}}
\Big[   \big(\psi_{n+1}^\ell\big)^{-1}\Big]\big(\bar\eps_{n'-s}^{(n')}\big)
\tu_n(1) \otimes \tv_n(x^s)$, the image of $1$ under the
southwest pair of maps in the diagram defining $\tcoev_n$
is $\sum_{s=0}^{n'} (-1)^{(n'+1)s} \bar\eps_{n'-s}^{(n')}
v_{n'}(1)\otimes u_{n'}(x^s)$ thanks to \cref{Jackdoor}.
This is also the image of
(-1)^{\ell s+\binom{s}{2}}
\Big[    \big(\psi_{n+1}^\ell\big)^{-1}\big(\bar\eps_{n'-s}^{(n')}\big)\Big]
\tu_n(1) \otimes \tv_n(x^s)$
under the right hand map $\dagger \otimes *$ by
\cref{reallystarry1,reallystarry2,lemma0bchanged,events}.
%The other formula for $\tcoev_n(1)$ (which we actually never use) is proved similarly
%using the other case of \cref{Jackdoor}.

To compute $\tev_n\big(\tv_n(x^r)\otimes \tu_n(x^s)\big)$, we use the diagram defining $\tev_n$.
From \cref{reallystarry1,reallystarry2,events},
one sees that
(* \otimes \dagger)\big(\tv_n(x^r)\otimes \tu_n(x^s)\big) = (-1)^{\binom{r}{2}+\binom{s+1}{2}+n(r+s)} u_{n'}(x^r)
\otimes
\left[
v_{n'}(x^s)+(-1)^{n+1} \big(1-(-1)^s\big) v_{n'}(x^{s-1}) \dot o^{(\ell)}\right].
Using \cref{reallynot}, the image of this under the homomorphism
$\big(\psi_n^\ell\big)^{-1} \circ \ev_{n'}$ is easily seen to be equal
to the formula for $\tev_n\big(\tv_n(x^r)\otimes \tu_n(x^s)\big)$ given in the statement of the lemma.
\end{proof}

\begin{corollary}\label{indresrel2}
For $0 \leq n < \ell$, the following diagrams of graded superfunctors commute up to even degree 0 isomorphisms:
\begin{tikzcd}
\arrow[d,"(\overline{\omega\chi})_{n+1}-" left]
\EONH_{n+1}^\ell\sMod \arrow[rr,"\res_{\EONH_n^\ell}^{\EONH_{n+1}^\ell}" above]&&
\EONH_{n}^\ell\sMod\arrow[d,"(\overline{\omega\chi})_n-" right]\\
\EOH_{n+1}^\ell\sMod\arrow[rr,"\tV_n^\ell \otimes_{\EOH_{n+1}^\ell}\!\!\!\!\!-" below]&&\EOH_{n}^\ell\sMod
\end{tikzcd}\qquad
\begin{tikzcd}
\arrow[rr,"\coind_{\EONH_n^\ell}^{\EONH_{n+1}^\ell}" above]
\arrow[d,"(\overline{\omega\chi})_n-" left]
\EONH_{n}^\ell\sMod
&&\arrow[d,"(\overline{\omega\chi})_{n+1}-" right]\EONH_{n+1}^\ell\sMod
\\
\arrow[rr,"\tU_{n}^\ell \otimes_{\EOH_{n}^\ell}-\!\!" below]\EOH_{n}^\ell\sMod
\end{tikzcd}
(The vertical arrows are the equivalences
of graded supercategories from \cref{veryslow}.)
\end{corollary}

\begin{proof}
The commutativity of the first diagram follows from \cref{indresrel}, then the
second follows using \cref{secondadjunction} and the uniqueness of right adjoints.
\end{proof}

The following generalizes \cref{forconsistency}.

\begin{corollary}
For $0 \leq n < \ell$, we have that
\ind_{\EONH_n^\ell}^{\EONH_{n+1}^\ell}
\simeq
(\Pi Q^{2})^{\ell-2n-1} \coind_{\EONH_n^\ell}^{\EONH_{n+1}^\ell}.
Hence, $\EONH_{n+1}^\ell$ is a graded Frobenius extension of
of degree $2(\ell-2n-1)$ and parity $\ell-2n-1\pmod{2}$.
\end{corollary}

\begin{proof}
The second statement follows from the first statement by the general
theory of Frobenius extensions explained after \cref{generaltheory}.
To prove the first statement,
\cref{indresrel,indresrel2}
show that under the Morita equivalence $\ind_{\EONH_n^\ell}^{\EONH_{n+1}^\ell}$
corresponds to $(\Pi Q^2)^{-n} U_n \otimes_{\EOH_n^\ell}-$
and $\coind_{\EONH_n^\ell}^{\EONH_{n+1}^\ell}$ corresponds
to $\tU_n\otimes_{\EOH_n^\ell}-$.
Now the result follows because
$(\Pi Q^2)^{-n} U_n \simeq (\Pi Q^2)^{\ell-2n-1} \tU_n$ according to \cref{evil}.
\end{proof}

The final task in this section is to compute various mates of the
endomorphisms of $U_{(1^d);n}^\ell$ defined by the
action of $\ONH_d$ from \cref{lemma2}(2). Specifically,
we need to work out the endomorphisms in $\OGBim_\ell$
that correspond to the diagrams \cref{sigrel,phew} in the graphical calculus to be introduced later in the article.
Suppose that $\ell=n+d+n'$ for $d \geq 0$.
We define graded superalgebra homomorphisms
\begin{align}
\rho_{(1^d);n}:\ONH_d &\rightarrow
\End_{\EOH_{n+d}^\ell\dash \EOH_n^\ell}
\big(U_{n+d-1}^\ell\otimes_{\EOH_{n+d-1}^\ell}
\cdots\otimes_{\EOH_{n+1}^\ell} U_{n}^\ell\big)^{\sop}\label{cam}\\\label{smith}
\lambda_{n;(1^d)}:\ONH_d&\rightarrow
\End_{\EOH_n^\ell\dash \EOH_{n+d}^\ell}
\big(V_n^\ell \otimes_{\EOH_{n+1}^\ell} \cdots\otimes_{\EOH_{n+d-1}^\ell}(V_{n+d-1}^\ell)\big)
\end{align}
as follows.
For $a \in \ONH_d$, $\rho_{(1^d);n}(a)$ is defined
to be the top map the following diagram commute:
\begin{equation}\label{out}
\begin{tikzcd}
\arrow[d,"\big(b_{(1)^d}\big)^{-1}" left]
U_{n+d-1}^\ell \otimes_{\EOH_{n+d-1}^\ell}
\cdots\otimes_{\EOH_{n+1}^\ell}
\arrow[rr,"\rho_{(1^d);n}(a)" above]
U_{n+d-1}^\ell \otimes_{\EOH_{n+d-1}^\ell}
\cdots\otimes_{\EOH_{n+1}^\ell}
\arrow[rr,"u_{(1^d);n}(f) \mapsto (-1)^{\parity(a)\parity(f)} u_{(1^d);n}(f) \cdot a" below]&&
U_{(1^d);n}^\ell\arrow[u,"b_{(1)^d}" right]
\end{tikzcd}
\end{equation}
Also $\lambda_{n;(1^d)}(a)$ is the top map making
the following commute:
\begin{equation}\label{in}
\begin{tikzcd}
\arrow[d,"\big(c_{(1)^d}\big)^{-1}" left]
V_{n}^\ell \otimes_{\EOH_{n+1}^\ell}
\cdots\otimes_{\EOH_{n+d-1}^\ell}
\arrow[rr,"\lambda_{n;(1^d)}(a)" above]
V_{n}^\ell \otimes_{\EOH_{n+1}^\ell}
\cdots\otimes_{\EOH_{n+d-1}^\ell}
\\
\arrow[rr,"v_{n;(1^d)}(f) \mapsto
a\cdot v_{n;(1^d)}(f)" below]&&
V_{n;(1^d)}^\ell\arrow[u,"c_{(1)^d}" right]
\end{tikzcd}
\end{equation}
The vertical maps in \cref{out,in} come from \cref{ukraine2,ukraine3}.
We also remind the reader that
$u_{(1^d);n}(f) \cdot a = (-1)^{(d-1)\parity(a)} u_{(1^d);n}(f\cdot a)$
and $a\cdot v_{n;(1^d)}(f) = (-1)^{(n\# (d-1))\parity(a)} v_{n;(1^d)}(a \cdot f)$.

\begin{lemma}\label{mate1}
For $0 \leq n < \ell$, the mate
of the $\big(\EOH_{n+1}^\ell,\EOH_{n}^\ell\big)$-superbimodule endomorphism
under the adjunction from \cref{cupsandcaps},
that is, the composition
\begin{tikzcd}
\EOH_n^\ell\otimes_{\EOH_n^\ell} V_n^\ell\arrow[rr,"\coev_n\otimes\id"]&&
V_n^\ell \otimes_{\EOH_{n+1}^\ell} U_n^\ell\otimes_{\EOH_n^\ell} V_n^\ell\arrow[rrr,"{\id\otimes\rho_{(1);n}(x_1)\otimes\id}"]&&&
\phantom{x}
\end{tikzcd}\qquad\qquad\qquad
\qquad\qquad\qquad\qquad\qquad\begin{tikzcd}
V_n^\ell \otimes_{\EOH_{n+1}^\ell}
U_n^\ell\otimes_{\EOH_n^\ell} V_n^\ell\arrow[rr,"\id\otimes\ev_n"]&&
V_n^\ell\otimes_{\EOH_{n+1}^\ell} \EOH_{n+1}^\ell\arrow[r,"\operatorname{can}"]&
\end{tikzcd}
is equal to $\lambda_{n;(1)}(x_1)$.
\end{lemma}

\begin{proof}
Since $V_{n}^\ell$ is generated as a superbimodule
by $v_n(1)$ by \cref{lemma3}(1c), it suffices to show that
(\id \otimes \ev_n)\circ
(\id \otimes \rho_{(1);n}(x_1) \otimes \id)
\circ (\coev_n \otimes\id)\big(1 \otimes v_n(1)\big)
\lambda_{n;(1)}(x_1)\big(v_n(1)\big) \otimes 1.
This is a calculation from the definitions.
The right hand side is
$v_n(x) \otimes 1$ by the definition \cref{in}.
For the left hand side, we first apply
$\coev_n \otimes\id$ using \cref{fridoor}
to get
\Big[
\bar\eps^{(n)}\big((-1)^{n} t \big)
v_n\big((-1)^n\big) \otimes u_n\big((t-x)^{-1}\big) \otimes v_n(1)
\Big]_{t^{-1}}.
Then we apply the odd endomorphism
$\id \otimes \rho_{(1);n}(x_1) \otimes \id$
defined by \cref{out} to get
\Big[
\bar\eps^{(n)}\big((-1)^{n+1} t \big)
v_n\big((-1)^n\big) \otimes u_n\big((t+x)^{-1}x\big) \otimes v_n(1)
\Big]_{t^{-1}}.
Finally we apply
$\id \otimes \ev_n$ using \cref{ev1} with $t$ replaced by $-t$ to get
\Big[
\bar\eps^{(n)}\big((-1)^{n+1} t \big)
v_n\big((-1)^n\big) \big[
\bar\gamm^{(n+1)}(-t)t
\big]_{<t^{0}}\Big]_{t^{-1}} \otimes 1.
Computing the coefficients explicitly,
this is equal to
$v_n(1)\bar\gamm^{(n+1)}_1-(-1)^n\bar\eps_1^{(n)} v_n(1)$.
Since $\gamm_1^{(n+1)} = x_1+\cdots+x_{n+1}$
and $\eps_1^{(n)} = x_1+\cdots+x_n$ (and $(-1)^n$ cancels
when $\eps_1^{(n)}$ acts on $v_n(1)$ due to the parity shift) this is $v_n(x)\otimes 1$.
\end{proof}

\begin{lemma}\label{mate2}
For $0 < n < \ell$, the $\big(\EOH_n^\ell,\EOH_n^\ell\big)$-superbimodule
endomorphism $\sigma_n$ that is defined by the composition
\begin{tikzcd}
U_{n-1}^\ell\otimes_{\EOH_{n-1}^\ell} V_{n-1}^\ell
\arrow[r,"\operatorname{can}"]&
\EOH_n^\ell\otimes_{\EOH_n^\ell} U_{n-1}^\ell\otimes_{\EOH_{n-1}^\ell} V_{n-1}^\ell\arrow[rrr,"\coev_n \otimes \id\otimes\id"]&&&\phantom{x}
\end{tikzcd}\qquad\qquad\qquad\qquad\qquad$$$$\begin{tikzcd}
V_n^\ell\otimes_{\EOH_{n+1}^\ell} U_n^\ell \otimes_{\EOH_n^\ell}
U_{n-1}^\ell\otimes_{\EOH_{n-1}^\ell} V_{n-1}^\ell\arrow[rrr,"\id \otimes \rho_{(1^2);n-1}(\tau_1) \otimes \id"]&&&
V_n^\ell\otimes_{\EOH_{n+1}^\ell} U_n^\ell \otimes_{\EOH_n^\ell}
U_{n-1}^\ell\otimes_{\EOH_{n-1}^\ell} V_{n-1}^\ell
\end{tikzcd}$$$$\qquad\qquad\qquad\qquad\qquad\qquad\quad\begin{tikzcd}
\phantom{x}\arrow[rrr,"\id\otimes\id\otimes\ev_{n-1}"]&&&
V_n^\ell\otimes_{\EOH_{n+1}^\ell} U_n^\ell \otimes_{\EOH_n^\ell}
\EOH_n^\ell\arrow[r,"\operatorname{can}"]&
V_n^\ell\otimes_{\EOH_{n+1}^\ell} U_n^\ell
\end{tikzcd}
$u_{n-1}\big(x^r\big) \otimes v_{n-1}\big(x^s\big)$
to \begin{equation}\label{Ian}
(-1)^{nr+rs+r+s+n+1} v_n\big(x^s\big) \otimes u_n\big(x^r\big)
\sum_{p=0}^n \sum_{q=0}^{r+s-n}
v_n\big(x^p\big) \otimes u_n\big(x^{q}\big)
\bar\eps^{(n)}_{n-p} \bar \gamm^{(n)}_{r+s-n-q}
\end{equation}
for any $r \geq 0$ and $0 \leq s \leq n-1$.
\end{lemma}

\begin{proof}
First, we show that
\Big(u_n\big((t- x)^{-1}\big)
\otimes u_{n-1}\big(x^r\big)\Big)$
\begin{equation}\label{signtrouble}
-u_{n}\big((t+x)^{-1} x^r\big) \otimes u_{n-1}\Big(\big(t-(-1)^r x\big)^{-1}\Big)
+ \sum_{q=0}^{r-1} (-1)^{q+r+rq}
u_{n}\big((t+x)^{-1}x^{q}\big)\otimes u_{n-1}\big(x^{r-q-1}\big).
\end{equation}
To do this, according to the definition \cref{out},
we first use the inverse of the map $b_{(1)^2}$ from \cref{ukraine2} to pass to
This maps
$u_n\big((t- x)^{-1}\big)\otimes
$(-1)^r u_{(1^2);n-1}\big((t-x_2)^{-1} x_1^r\big)$.
The application of $\rho_{(1^2);n-1}(\tau_1)$
takes this to
$-u_{(1^2);n-1}\big((t+x_2)^{-1} x_1^r \cdot \tau_1\big)$.
This we can compute with \cref{trulycrazy}
to get
-u_{(1^2);n-1}\Big((t+x_2)^{-1} x_2^r \big(t+(-1)^r x_1\big)^{-1}\Big)
- \sum_{q=0}^{r-1} (-1)^{rq}
After that we apply $b_{(1)^2}$ to
obtain the vector
in $U_{n}^\ell\otimes_{\EOH_n^\ell} U_{n-1}^\ell$
displayed in \cref{signtrouble}.

Now to prove the lemma, we again calculate
with generating functions.
Start with the vector $u_{n-1}\big(x^r\big) \otimes v_{n-1}\big(x^s\big)$ for $0 \leq s \leq n-1$ (this assumption on $s$ will be crucial shortly).
By \cref{sundoor1}, the map
$\coev_n \otimes \id \otimes \id$ takes it to
\begin{equation}\label{crv}
\Big[ v_n((t-x)^{-1}) \bar \eps^{(n+1)}(t) \otimes
u_n\big((t- x)^{-1}\big)\otimes
u_{n-1}\big(x^r\big) \otimes v_{n-1}\big(x^s\big)
\Big]_{t^{-1}}.
\end{equation}
Then we apply the odd homomorphism
$\id \otimes \rho_{(1^2);n-1}(\tau_1) \otimes \id$
using \cref{signtrouble} to obtain
\begin{multline}\label{tricky}
\Big[ v_n((t+x)^{-1}) \bar \eps^{(n+1)}(-t) \otimes
u_{n}\big((t+x)^{-1} x^r\big) \otimes u_{n-1}\Big(\big(t-(-1)^r x\big)^{-1}\Big)
\otimes v_{n-1}\big(x^s\big)
\Big]_{t^{-1}}\\
\sum_{q=0}^{r-1} (-1)^{q+r+rq+1}
\Big[ v_n((t+x)^{-1}) \bar \eps^{(n+1)}(-t) \otimes
u_{n}\big((t+x)^{-1}x^{q}\big)\otimes u_{n-1}\big(x^{r-q-1}\big)
\otimes v_{n-1}\big(x^s\big)
\Big]_{t^{-1}}.
\end{multline}
It just remains to apply $\id\otimes\id\otimes \ev_{n-1}$.
We treat the two terms in \cref{tricky}
separately. For the first term, we have
$\ev_{n-1}\Big(u_{n-1}\Big(\big(t- (-1)^r x\big)^{-1}\Big)
\otimes v_{n-1}\big(x^s\big)\Big)
=(-1)^{rs+r} \left[\bar \gamm^{(n)}\big((-1)^r t\big) t^s\right]_{<t^{0}}$
by \cref{ev1} (with $t$ replaced by $(-1)^{r}t$).
The assumption that $s \leq n-1$
means that we can omit the truncation to $<t^{0}$ here.
So the first term contributes
\Big[ v_n((t+x)^{-1}) \otimes \bar \eps^{(n+1)}(-t) u_{n}\big((t+x)^{-1} x^r\big)\otimes
\bar \gamm^{(n)}\big((-1)^r t\big) t^s
\Big]_{t^{-1}}.
Now we use \cref{relsfancy3} to rewrite this as
\Big[ v_n((t+x)^{-1}) \otimes
u_n\big(x^r\big) \bar\eps^{(n)}\big((-1)^{r} t\big)
\bar \gamm^{(n)}\big((-1)^r t\big) t^s \otimes 1
\Big]_{t^{-1}}.
The $\eps$ and $\gamm$ cancel by the infinite Grassmannian relation
to leave
\Big[ v_n((t+x)^{-1}t^s) \otimes
u_n\big(x^r\big) \otimes 1
\Big]_{t^{-1}}
\stackrel{\cref{why}}{=}
v_n\big(x^s\big) \otimes u_n\big(x^r\big)\otimes 1.
It remains to consider the term obtained by applying
$\id\otimes\id\otimes \ev_{n-1}$
to the second term from \cref{tricky}. Using \cref{reallynot,relsfancy3}, this contributes
\begin{multline*}
\sum_{q=0}^{r+s-n} (-1)^{q+r+rq+1}
\Big[ v_n((t+x)^{-1}) \otimes
\bar \eps^{(n+1)}(-t) u_{n}\big((t+x)^{-1}x^{q}\big)
\otimes \bar \gamm^{(n)}_{r+s-q-n}
\Big]_{t^{-1}}=\\
\sum_{q=0}^{r+s-n} (-1)^{q+r+rq+nq+n}
\Big[ v_n\big((t+x)^{-1}\big)\otimes u_n\big(x^q\big)\bar \eps^{(n)}\big((-1)^{q}t\big)\bar\gamm^{(n)}_{r+s-q-n}\otimes 1\Big]_{t^{-1}}.
\end{multline*}
It remains to work out the $t^{-1}$-coefficient explicitly to complete the proof.
\end{proof}

\begin{lemma}\label{mate3}
For $0 < n < \ell$, the mate of $\rho_{(1^2);n-1}(\tau_1)$
under the adjunction from \cref{cupsandcaps}, that is, the composition
\begin{tikzcd}
V_{n-1}^\ell\otimes_{\EOH_{n}^\ell} V_{n}^\ell\arrow[r,"\operatorname{can}"]&
\EOH_{n-1}^\ell\otimes_{\EOH_{n-1}^\ell}V_{n-1}^\ell\otimes_{\EOH_{n}^\ell} V_{n}^\ell
\arrow[rrr,"\coev_{n-1}\otimes\id\otimes \id"]&&&\phantom{x}
\end{tikzcd}\qquad\qquad\qquad\qquad\qquad
\begin{tikzcd}
V_{n-1}^\ell\otimes_{\EOH_n^\ell} U_{n-1}^\ell
\otimes_{\EOH_{n-1}^\ell}V_{n-1}^\ell\otimes_{\EOH_{n}^\ell} V_{n}^\ell
\arrow[rr,"\id\otimes\sigma_n\otimes \id"]&&
V_{n-1}^\ell\otimes_{\EOH_n^\ell} V_{n}^\ell
\otimes_{\EOH_{n+1}^\ell}U_{n}^\ell\otimes_{\EOH_{n}^\ell} V_{n}^\ell
\end{tikzcd}
\qquad\qquad\qquad\qquad\qquad
\begin{tikzcd}
\phantom{x}\arrow[rrr,"\id\otimes\id \otimes \ev_{n}"]&&&
V_{n-1}^\ell\otimes_{\EOH_n^\ell} V_{n}^\ell
\otimes_{\EOH_{n+1}^\ell} \EOH_{n+1}^\ell\arrow[r,"\operatorname{can}"]&
V_{n-1}^\ell\otimes_{\EOH_n^\ell} V_{n}^\ell
\end{tikzcd}
$$ where $\sigma_n$ is the superbimodule homomorphism\footnote{Diagrammatically, we have rotated through $180^\circ$ by rotating by $90^\circ$ twice, see \cref{sigrel,phew}.}
defined in \cref{mate2},
is equal to $\lambda_{n-1;(1^2)}(\tau_1)$.
\end{lemma}

\begin{proof}
By \cref{lemma3}(1b)--(1c),
V_{n}^\ell$ is generated as an
by the vectors $v_{n-1}(1)\otimes v_n(x^s)\:\:(0 \leq s \leq n)$.
Therefore it suffices to show that
(\id\otimes\id \otimes \ev_{n})
\circ (\id \otimes \sigma_n \otimes \id) \circ (\coev_{n-1}
\otimes \id \otimes \id)
\big(1 \otimes v_{n-1}(1)\otimes v_n(x^s)\big) =
\lambda_{n-1;(1^2)}(\tau_1) \big( v_{n-1}(1)\otimes v_n(x^s)\big) \otimes 1
for $0 \leq s \leq n$.
The right hand side may be computed directly
from \cref{in,ukraine3}.
It equals
(-1)^{n} c_{(1)^2}\Big(v_{n-1;(1^2)}\big(\tau_1 \cdot x_2^s\big)\Big) \otimes 1
\stackrel{\cref{rank22}}{=}  (-1)^{n+1} c_{(1)^2}\Big( v_{n-1;(1^2)}\big(\gamm^{(2)}_{s-1}\big)\Big) \otimes 1.
So to complete the proof we must show that
\begin{multline}\label{todo}
\!\!\left(c_{(1)^2}\otimes\id\right)^{\!-1}\!\!
\Big( (\id\otimes\id \otimes \ev_{n})\
\!\circ (\id \otimes \sigma_n \otimes \id) \circ (\coev_{n-1}
\otimes \id \otimes \id)
\big(1 \otimes v_{n-1}(1)\otimes v_n(x^s)\big)\Big)\\ =
(-1)^{n+1} v_{n-1;(1^2)}\big(\gamm^{(2)}_{s-1}\big)\otimes 1.
\end{multline}
To compute the left hand side, we first use \cref{Jackdoor}
to get
\otimes \id \otimes \id)
\big(1\otimes v_{n-1}(1)\otimes v_n(x^s)\big)
\sum_{r=0}^{n-1}(-1)^{nr} \bar \eps_{n-1-r}^{(n-1)}
v_{n-1}(1) \otimes
u_{n-1}\big(x^r\big) \otimes v_{n-1}(1)
\otimes v_n(x^s).
Then we apply $\id \otimes \sigma_n \otimes \id$
using \cref{Ian}, noting also that $\sigma_n$ is {\em odd}.
Since $r \leq n-1$ in this expression,
the summation over $q$ on the right hand side of \cref{Ian} is actually
an empty sum, so zero, and we get simply
(-1)^{n+1} \sum_{r=0}^{n-1}
\bar \eps_{n-1-r}^{(n-1)}
v_{n-1}(1) \otimes
v_n(1) \otimes u_n\big(x^r\big)
\otimes v_n\big (x^s\big ).
Next we apply $\id\otimes\id\otimes\ev_n$.
We must have that $r+s \geq n$ so $r \geq n-s$, and the final expression is
(-1)^{n+1} \sum_{r=n-s}^{n-1}
\bar \eps_{n-1-r}^{(n-1)}
v_{n-1}(1) \otimes
\bar\gamm^{(n+1)}_{r+s-n}
= (-1)^{n+1}\sum_{r=0}^{s-1} \bar\eps_r^{(n-1)}
v_{n-1}(1) \otimes
\bar\gamm^{(n+1)}_{s-1-r}.
Applying $\big(c_{(1)^2}\otimes\id\big)^{-1}$ as is required for \cref{todo}, we get
(-1)^{n+1} \sum_{r=0}^{s-1} \bar\eps_r^{(n-1)}
\bar\gamm^{(n+1)}_{s-1-r}.
There is a sign change of $(-1)^r$
due to the parity shift $(n-1)\# 2 \equiv 1 \pmod{2}$. Also
we have that $\sum_{r=0}^{s-1} (-1)^r \eps_r^{(n-1)} \gamm^{(n+1)}_{s-1-r}
= \sig_{n-1}\big(\gamm^{(2)}_{s-1}\big)$ by a similar argument to the proof of \cref{notsoeasypeasy}.
So this is $(-1)^{n+1} v_{n-1;(1^2)}\big(\gamm^{(2)}_{s-1}\big)$
exactly as in \cref{todo}.
\end{proof}

\section{Singular Rouquier complex}\label{derby}

Throughout the section, we fix $\ell \in \N$.
The graded $(Q,\Pi)$-2-supercategory
categorifies the locally unital $\Z[q,q^{-1}]^\pi$-algebra that is
the image of $\mathbf{U}_{q,\pi}(\sl_2)$
in its representation on
$\mathbf{V}(-\ell)$, notation as at the end of \cref{leavingdepoe}.
To make this statement precise, let
$K_0(\EOH_n^\ell)$ be the Grothendieck group of
$\EOH_n^\ell$, which we identify with
Since $\EOH_n^\ell$ is positively graded with
degree 0 component that is the ground field $\k$,
this is nothing more than the free $\Z[q,q^{-1}]^\pi$-module
generated by the isomorphism class $[\EOH_n^\ell]$
of the regular module, with the actions of $\pi$ and $q$
induced by the parity and degree shift functors $\Pi$ and $Q$, respectively.
So we can identify
\begin{align}
\mathbf{V}(-\ell)
\bigoplus_{n=0}^\ell
b_n^\ell &\equiv [\EOH_n^\ell].\label{theid}
\end{align}
The following matches up the action of generators of
on $\mathbf{V}(-\ell)$ with
endomorphisms of the Grothendieck group
induced by tensoring with odd Grassmannian bimodules.

\begin{theorem}\label{K0}
Under the identification \cref{theid} of
$\Z[q,q^{-1}]^\pi$-module endomorphisms induced by
tensoring with odd Grassmannian bimodules
to endomorphisms defined
by actions of elements of $\mathbf{U}_{q,\pi}(\sl_2)$ according to the following dictionary:
\begin{enumerate}
\item
$\big[U_n^\ell\otimes_{\EOH_n^\ell}-\big]\equiv q^n E 1_{2n-\ell}$
and, more generally, $\big[U_{(d);n}^\ell\otimes_{\EOH_n^\ell}-\big]
\equiv q^{nd} E^{(d)}1_{2n-\ell}$;
\item $\big[V_n^\ell\otimes_{\EOH_{n+1}^\ell}-\big]
\equiv q^{\ell-3n-1} 1_{2n-\ell} F$
and $\big[V_{n;(d)}^\ell\otimes_{\EOH_{n+d}^\ell}-\big]\equiv
q^{d(\ell-3n-2d+1)} 1_{2n-\ell} F^{(d)}$.
\end{enumerate}
Also, for $-\ell \leq k \leq \ell$
with $k \equiv \ell\pmod{2}$,
the map $T:1_{-k} \mathbf{V}(-\ell)
\rightarrow 1_k \mathbf{V}(-\ell)$
from \cref{oddreflection}
corresponds to the $\Z[q,q^{-1}]^\pi$-module
\begin{align}\label{fromR}
T:K_0(\EOH_n^\ell) &\rightarrow K_0(\EOH_{n'}^\ell),&
\big[\EOH_n^\ell\big]&\mapsto
(-1)^n (\pi q^2)^{\binom{n+1}{2}+nk} q^{-nk}
\big[\EOH_{n'}^\ell\big]
\end{align}
where $n:=\frac{\ell-k}{2}$ and $n':=\frac{\ell+k}{2}$.
\end{theorem}

\begin{proof}
Note here we are assuming implicitly that $0 \leq n \leq \ell-1$
$0 \leq n \leq \ell-d$, respectively
so that $U_n^\ell$ and $U_{(d);n}^\ell$
are defined.
By \cref{lemma3}(2b), we have that
$\big[U_n^\ell \otimes_{\EOH_n^\ell} \EOH_n^\ell\big]
q^n [n+1]_{q,\pi} \big[\EOH_{n+1}^\ell\big].$
Also $E b_n^\ell =
[n+1]_{q,\pi} b_n^\ell$.
It follows that
$\big[U_n^\ell\otimes_{\EOH_n^\ell}-\big]$ and
$q^n E 1_{2n-\ell}$
define the same endomorphisms of $\mathbf{V}(-\ell)$.
For the more general assertion, take $d \geq 1$.
By \cref{lemma2}(2) and \cref{poincare}, we have that
= q^{\binom{d}{2}} [d]^!_{q,\pi}
\big[U_{(d);n}^\ell\otimes_{\EOH_n^\ell}-\big]$.
Also $U_{(1^d);n}^\ell
\simeq U^\ell_{n+d-1}\otimes_{\EOH_{n+d-1}^\ell}
\cdots\otimes_{\EOH_{n+1}^\ell} U_n^\ell$
by \cref{ukraine2},
so we deduce using the special case already treated that
\begin{align*}
q^{\binom{d}{2}} [d]^!_{q,\pi}
\big[U_{(d);n}^\ell\otimes_{\EOH_n^\ell}-\big]
q^{nd+\binom{d}{2}} E^d 1_{2n-\ell}
q^{nd+\binom{d}{2}} [d]^!_{q,\pi}
E^{(d)} 1_{2n-\ell}.
\end{align*}
Cancelling $q^{\binom{d}{2}} [d]^!_{q,\pi}$
gives the required conclusion.

\vspace{1mm}
\noindent
(2) Again we are assuming that
$0 \leq n \leq \ell-1$ and $0 \leq n \leq \ell-d$, respectively.
The first step is to show that
= q^{\ell-n-1}\pi^{n} 1_{2n-\ell} F$,
which follows from \cref{lemma3}(1a) like in the proof of (1).
Hence, since $V_n^\ell
= (\Pi Q^{-2})^n \tV_n^\ell$,
we get that
= q^{\ell-3n-1} 1_{2n-\ell} F$.
The passage from this to
the more general
result about $V_{n;(d)}^\ell$
follows in a similar way to the argument given in (1).

\vspace{1mm}
\noindent
Now consider the final statement about $T$.
Take $k$ and $n=\frac{\ell-k}{2}, n'=\frac{\ell+k}{2}$
as in the statement of the theorem.
We saw in \cref{rain2} that $T(b_n^\ell) =
(-1)^n \pi^{\binom{n}{2}+nn'} q^{n+n n'} b_{n'}^\ell$.
Using the identification \cref{theid},
it follows that
(-1)^n \pi^{\binom{n}{2}+nn'} q^{n+n n'}
\big[\EOH_{n'}^\ell\big].$
On replacing $n'$ by $k+n$,
this becomes the formula in the statement of the theorem.
\end{proof}

The goal in the remainder section is to
categorify $T:1_{-k} \mathbf{V}(-\ell)
\rightarrow 1_k \mathbf{V}(-\ell)$
for all $-\ell \leq k \leq \ell$ with $k \equiv \ell\pmod{2}$.
Throughout, we let $n := \frac{\ell-k}{2}$ and $n' := \frac{\ell+k}{2}=n+k$
so that $2n-\ell=-k$ and $2n'-\ell=k$.
Since $n+n'=\ell$, \cref{EOH}(4) shows that
the graded superalgebras
$\EOH_n^\ell$ and $\EOH_{n'}^\ell$ are isomorphic.

\begin{definition}\label{weekend}
For $0 \leq d \leq n$, let
\begin{align}
C_{d} &:=
\left\{
\begin{array}{ll}
U^\ell_{(k+d);n-d} \otimes_{\EOH_{n-d}^\ell}
&\text{if $d \geq -k$,}\\
\end{array}
\right.
\end{align}
The {\em singular Rouquier complex} for odd Grassmannian bimodules
the following sequence of graded
and even degree 0 superbimodule homomorphisms
in $\OGBim_\ell$:
\begin{equation}\label{src}
0 \stackrel{\partial_{n+1}}{\longrightarrow} C_n
\stackrel{\partial_n}{\longrightarrow} \cdots
\stackrel{\partial_{d+1}}{\longrightarrow} C_d \stackrel{\partial_d}{\longrightarrow} C_{d-1}\stackrel{\partial_{d-1}}{\longrightarrow}\cdots\stackrel{\partial_2}{\longrightarrow} C_1
\stackrel{\partial_1}{\longrightarrow} C_0 \stackrel{\partial_0}{\longrightarrow} 0
\end{equation}
where $\partial_d = 0$ unless $\max(0,-k) < d \leq n$, in which case
$\partial_d:C_d \rightarrow C_{d-1}$ is the even degree 0
superbimodule homomorphism defined by the composition
\!\begin{tikzcd}
U^\ell_{(k+d);n-d} \otimes_{\EOH_{n-d}^\ell} V_{n-d;(d)}^\ell
\arrow[r,"\operatorname{inc}" above]
U^\ell_{(k+d-1,1);n-d} \otimes_{\EOH_{n-d}^\ell}
\arrow[rrr,"{c_{(k+d-1),(1)}' \otimes\; c_{(1),(d-1)}}" above]&&&\phantom{psi[mgjokurhx}
\end{tikzcd}\!

\vspace{-4mm}

\!\begin{tikzcd}
U^\ell_{n-d}\otimes_{\EOH_{n-d}^\ell} V_{n-d}^\ell \otimes_{\EOH_{n-d+1}^\ell} V_{n-d+1;(d-1)}^\ell
\arrow[rr,"\id \otimes \ev_{n-d} \otimes \id" above]&&\phantom{x;oiagrhjqnrdgore'pj}
\end{tikzcd}\!

\vspace{-4mm}

\!\begin{tikzcd}
\arrow[r,"\operatorname{can}" above]&
\end{tikzcd}\!
\end{definition}

\begin{theorem}\label{SRC}
The singular Rouquier complex \cref{src} is a chain complex
with homology that is zero in all except for the top ($n$th) homological degree.
as a graded
the top homology is $\simeq(\Pi Q^2)^{\binom{n+1}{2}+nk}\EOH_{n'}^\ell$
viewed as a graded left $\EOH_{n'}^\ell$-supermodule by the natural action
and as a graded right $\EOH_{n}^\ell$-supermodule
by restricting the natural right action of $\EOH_{n'}^\ell$ along
some graded superalgebra isomorphism
\EOH_{n'}^\ell$.
\end{theorem}

The following corollary follows immediately. To formulate it, let
$K^b(\EOH_n^\ell\psmod)$ be the bounded homotopy supercategory
of the graded supercategory finitely generated projective
graded left $\EOH_n^\ell$-supermodules;
in the definition of this
we require that differentials and homotopies are even of degree 0 but
chain maps between cochain complexes can be constructed using
arbitrary morphisms in $\EOH_n^\ell\psmod$.
By Euler characteristic,
the Grothendieck group of the underlying ordinary category
is identified with $K_0(\EOH_n^\ell)$, hence,
via \cref{theid}, with $1_{-k} \mathbf{V}(-\ell)$.

\begin{corollary}\label{weirdshift}
Tensoring with the singular Rouquier complex
\cref{src} (viewed now as a cochain complex rather than a chain complex
as usual when working with homotopy categories)
then taking the total complex
defines a graded superequivalence
$K^b(\EOH_n^\ell\psmod) \rightarrow K^b(\EOH_{n'}^\ell\psmod)$.
The induced  $\Z[q,q^{-1}]^\pi$-module isomorphism
$1_{-k} \mathbf{V}(-\ell)\stackrel{\sim}{\rightarrow}
1_k \mathbf{V}(-\ell)$
at the level of Grothendieck groups
is equal to $q^{nk} T$ for $T$ as in \cref{fromR}.
\end{corollary}

The remainder of the section is devoted to the proof of \cref{SRC}, which will be carried out with a series of lemmas.
We assume for simplicity of notation that $k \geq 0$, although with obvious modifications the arguments work for negative $k$ too.

\begin{lemma}\label{isdifferential}
We have that $\partial_{d-1} \circ \partial_d = 0$ for $d=1,\dots,n+1$,
hence, \cref{src} is a chain complex.
\end{lemma}

\begin{proof}
By the super interchange law, $\partial_{d-1} \circ \partial_d$
factorizes as the composition first of the embedding
\begin{tikzcd}
C_d = U_{(k+d);n-d}^\ell \otimes_{\EOH_{n-d}^\ell}
\arrow[r,"\operatorname{inc}" above]
&U_{(k+d-2,2);n-d}^\ell \otimes_{\EOH_{n-d}^\ell}
\arrow[rrr,"b_{(k+d-2),(2)}\otimes\;c_{(2),(d-2)}" above]
\end{tikzcd}

\vspace{-4mm}

\begin{tikzcd}
\qquad\qquad\qquad U_{(k+d-2);n-d+2}^\ell\otimes_{\EOH_{n-d+2}^\ell}
U_{(2);n-d}^\ell \otimes_{\EOH_{n-d}^\ell}
\end{tikzcd}
then the map $\id\otimes(\partial\circ\iota)\otimes\id$
from there to
\begin{tikzcd}
\iota:U_{(2);n-d}^\ell \otimes_{\EOH_{n-d}^\ell}
V_{n-d;(2)}^\ell\arrow[r,"\operatorname{inc}" above]&
\arrow[rr,"b_{(1),(1)}\otimes\;c_{(1),(1)}" above]&&\phantom{xwoiprgeqjrgpqjj}
\end{tikzcd}

\vspace{-4mm}

\phantom{oiergnoweirjgf}U_{n-d+1}^\ell\otimes_{\EOH_{n-d+1}^\ell}
\otimes_{\EOH_{n-d+1}^\ell}

\begin{tikzcd}
\partial:\!U_{n-d+1}^\ell\!\otimes_{\EOH_{n-d+1}^\ell}\!\!\!\!
\!\otimes_{\EOH_{n-d+1}^\ell}\!\!\!
\arrow[rr,"\id\otimes\ev_{n-d}\otimes\id" above]&&
\!\otimes_{\EOH_{n-d+1}^\ell}\!\!\!\!
\EOH_{n-d+1}^\ell\!\otimes_{\EOH_{n-d+1}^\ell}\!\!\!
\end{tikzcd}

\vspace{-4mm}

\begin{tikzcd}
\phantom{aoeikrerfefg;rgja;porgi}
\otimes_{\EOH_{n-d+1}^\ell}
\arrow[rr,"\ev_{n-d+1}" above]&&
\EOH_{n-d+2}^\ell.\phantom{rgwtwrthtgrw}
\end{tikzcd}
Thus, we are reduced to proving that $\partial$ takes vectors in the image
of $\iota$ to zero.
By \cref{lemma2}, the image of $\iota$
is equal to the image of the projection
\otimes \lambda_{n-d;(1^2)}\big((\omega\chi)_2\big)$.
This projection equals
\rho_{(1^2);n-d}(x_1 \tau_1)
\otimes \lambda_{n-d;(1^2)}(\tau_1 x_1)
\rho_{(1^2);n-d}(\tau_1) \otimes
\lambda_{n-d;(1^2)}(\tau_1)\big)
\circ\big(
\rho_{(1^2);n-d}(x_1)
\otimes \lambda_{n-d;(1^2)}(x_1)\big).
Finally, to complete the proof,
we observe that
$\partial \circ \big(\rho_{(1^2);n-d}(\tau_1) \otimes \lambda_{n-d;(1^2)}(\tau_1)\big) = 0$
\partial \circ \big(\rho_{(1^2);n-d}(\tau_1) \otimes \id\otimes \id\big)
\partial \circ  \big(\id \otimes \id \otimes \lambda_{n-d;(1^2)}(\tau_1)\big)
thanks to \cref{mate3},
$\lambda_{n-d;(1^2)}(\tau_1) \circ \lambda_{n-d;(1^2)}(\tau_1)
= \lambda_{n-d;(1^2)}\big(\tau_1^2\big) = 0$.
\end{proof}

Now we need to understand the ``numerology" of \cref{src}.
In fact, the combinatorial \cref{numerology} derived long ago
is just what we need for this. Recall the definitions
of $b_{m,n}(r), c_{m,n}(r) \in \Z[q,q^{-1}]^\pi$
made in the statement of that lemma.
The following shows that $c_{n+k,n}(d)$ is
the graded superrank of $C_d$ either as a
free graded
right $\EOH_n^d$-supermodule or a free graded left $\EOH_{n'}^d$-supermodule.
We will also see in a bit that $b_{n+k,n}(d)$ is the graded rank of
$\im \partial_{d}$ for $d=0,1,\dots,n$.

% NOTE IN ALL OF THE BELOW I CHANGED NOTATION SO THAT
% s_\lambda^* = (-1)^{dN(\lambda)+dE(\lambda)} \sigma_\lambda

\begin{lemma}\label{depoebay}
The vectors
\begin{equation}\label{thebasis}
\bigg\{
u_{(k+d);n-d}\big(\bar \sigma^{(k+d)}_\lambda\big)
\otimes v_{n-d;(d)}\big(\bar \sigma^{(d)}_\mu\big)
\:\bigg|\:
(\lambda,\mu) \in \GPar{(k+d)}{n}\times \GPar{d}{(n-d)}
\bigg\}
\end{equation}
give a basis for $C_d$ as a free right $\EOH_n^\ell$-supermodule.
as a graded right $\EOH_n^\ell$-supermodule,
$C_d$ is free
of graded superrank $c_{n+k,n}^{(d)}$.
It is also free as a graded left $\EOH_{n'}^\ell$-superbimodule
with the same graded superrank.
\end{lemma}

\begin{proof}
\cref{lemma01} implies that it is free as a graded right $\EOH_n^\ell$-supermodule with basis
\cref{thebasis}.
The formula for its graded superrank then follows using
\cref{qbinomialformula}. It is also free as a graded left $\EOH_{n'}^\ell$-supermodule
thanks to \cref{lemma01} again. Since $\EOH_{n'}^\ell
\cong \EOH_n^\ell$, its graded superrank for $\EOH_{n'}^\ell$
is the same as for $\EOH_n^\ell$.
\end{proof}

Recall that $\EOH_n^\ell$ is positively graded
with degree 0 component isomorphic
the ground field $\k$.
We apply the functor
$-\otimes_{\EOH_n^\ell} \k$ to \cref{src} to obtain the chain complex
\begin{equation}\label{src2}
0 \stackrel{\overline{\partial}_{n+1}}{\longrightarrow} \overline{C}_n
\stackrel{\overline{\partial}_n}{\longrightarrow} \cdots
\stackrel{\overline{\partial}_{d+1}}{\longrightarrow} \overline{C}_d \stackrel{\overline{\partial}_d}{\longrightarrow} \overline{C}_{d-1}\stackrel{\overline{\partial}_{d-1}}{\longrightarrow}\cdots\stackrel{\overline{\partial}_2}{\longrightarrow} \overline{C}_1
\stackrel{\overline{\partial}_1}{\longrightarrow} \overline{C}_0 \stackrel{\overline{\partial}_0}{\longrightarrow} 0
\end{equation}
of graded left $\ROH_{n'}^\ell$-supermodules.
\cref{depoebay} implies that
$\overline{C}_d$ is of graded superdimension $c_{n+k,n}(d)$.

\begin{lemma}\label{mainstep}
Suppose we are given that $\dim \im \bar\partial_d \geq |b_{n+k,n}(d)|$
for $d=1,\dots,n$,
where $|b_{n+k,n}(d)|$ denotes the natural number obtained by
applying the evaluation
map $\Z[q,q^{-1}]^\pi \rightarrow \Z, q \mapsto 1, \pi \mapsto 1$
to $b_{n+k,n}(d)$.
Then \cref{SRC} is true.
\end{lemma}

\begin{proof}
We first consider the specialized complex \cref{src2},
showing that $\im \overline{\partial}_d = \ker \overline{\partial}_{d-1}$
and that it is of graded superdimension $b_{n+k,n}(d)$
for each $d=1,\dots,n$. This follows by induction
on $d$, defining $\overline{\partial}_{-1}$ to be the zero map
so that we can start the induction at $d=0$. The induction base
holds because $b_{n+k,n}(0) = 0$.
For the induction step, take $0 \leq d < n$ and assume
that $\im\overline{\partial}_d = \ker \overline{\partial}_{d-1}$
is of graded superdimension $b_{n+k,n}(d)$.
We have that
\overline{C}_d = \overline{B}'_d \oplus \overline{Z}_d
where $\overline{Z}_d := \ker \overline{\partial}_d$
and $\overline{B}'_d \simeq \im \overline{\partial}_d$ is a complementary graded superspace.
By induction, $\gsdim \overline{B}'_d = b_{n+k,n}(d)$.
We have that
$\dim \overline{C}_d = \dim \im \overline{\partial}_d+\dim \ker \overline{\partial}_d$ so, using \cref{numerology} for the final equality, get that
\begin{align*}
|c_{n+k,n}(d)| = |b_{n+k,n}(d)| \!+\! \dim \ker \overline{\partial}_d
\geq |b_{n+k,n}(d)|\!+\! \dim \im \overline{\partial}_{d+1}
\geq |b_{n+k,n}(d)|\!+\!|b_{n+k,n}(d+1)| = |c_{n+k,n}(d)|.
\end{align*}
This means that equality holds throughout, thereby proving
that $\im \overline{\partial}_{d+1} = \ker \overline{\partial}_d$.
The same sequence of equalities without evaluating
at $q=\pi = 1$ now gives that
$\gsdim \im \overline{\partial}_{d+1} = b_{n+k,k}(d+1)$,
and the argument is complete.

Next we show that
$\im \partial_d = \ker \partial_{d-1}$
and that it is free as a graded right $\EOH_n^\ell$-supermodule
of graded superrank $b_{n+k,n}(d)$
for each $d=1,\dots,n$. This is a similar induction to the one in the previous paragraph.
For the induction step, we take $0 \leq d < n$
and assume that we have shown already that
$\im \partial_d$ is free of
graded superrank $b_{n+k,n}(d)$. Consider the short exact sequence
0 \longrightarrow Z_d \longrightarrow C_d \longrightarrow \im \partial_d \longrightarrow 0
where $Z_d := \ker \partial_d$.
Since $\im \partial_d$ is free, this short exact sequence splits,
so we have that
C_d = B_d' \oplus Z_d
where $B'_d \simeq \im \partial_d$ is a complement to $Z_d$ in $C_d$
as a graded right $\EOH_n^\ell$-supermodule.
Moreover, $\overline{Z}_d$ from the previous paragraph
is $Z_d \otimes 1$. As it is a summand of $C_d$, which is free,
we deduce that $Z_d$ is a free graded right $\EOH_n^\ell$-supermodule
with $\gsrank Z_d = \gsdim \overline{Z}_d = b_{n+k,k}(d+1)$.
The map $\partial_{d+1}:C_{d+1}\rightarrow Z_d$
is surjective because $\id\otimes\partial_{d+1}:\overline{C}_{d+1}
\rightarrow \overline{Z}_d$ is surjective according to the previous paragraph.
We deduce that $\im \partial_{d+1} = \ker \partial_d$
is free of graded superrank $b_{n+k,k}(d+1)$, and the argument
is complete.

So now we have shown that $\im \partial_d = \ker \partial_{d-1}$
is free as a graded right $\EOH_n^\ell$-supermodule
of graded superrank $b_{n+k,n}(d)$ for $d=1,\dots,n$.
The same is true as a graded left $\EOH_{n'}^\ell$-supermodule
since $\EOH_{n'}^\ell \cong \EOH_n^\ell$ and all of the numerology is the same.

To complete the proof of \cref{SRC}, it just remains
to prove the assertion about the top degree homology.
As $\EOH_{n'}^\ell \cong \EOH_n^\ell$, it suffices to show that it is
of graded superrank
$(\pi q^2)^{\binom{n+1}{2}+nk}$ both as a graded right $\EOH_n^\ell$- and as a graded left $\EOH_{n'}^\ell$-supermodule.
We have already shown that the image of $\partial_n$ is free
of graded superrank $b_{n+k,k}(n)$. Hence, since $C_n$ is free of
graded superrank $c_{n+k,n}(n)$ by \cref{depoebay},
we deduce that $\ker \partial_n$
is free of graded superrank $c_{n+k,n}(n)-b_{n+k,k}(n)$.
Thus, we are reduced to showing that
$c_{n+k,n}(n)-b_{n+k,k}(n) = (\pi q^2)^{\binom{n+1}{2}+nk}.$
This follows from the following calculation:
\begin{align*}
c_{n+k,n}(n) - b_{n+k,k}(n) &=
(\pi q^{-2})^{\binom{n}{2}}
(\pi q^{-2})^{\binom{n}{2}}
\sum_{s=0}^{n-1} (\pi q^{2})^{(n+k)(n-s-1)}
\sqbinom{n+k+s}{s+1}_{q,\pi}\\
(\pi q^{-2})^{\binom{n}{2}}
\sum_{s=0}^{n} (\pi q^{2})^{(n+k)(n-s)}
\sqbinom{n+k+s-1}{s}_{q,\pi}\\&\qquad\qquad-
(\pi q^{-2})^{\binom{n}{2}}
\sum_{s=1}^{n} (\pi q^{2})^{(n+k)(n-s)}
\sqbinom{n+k+s-1}{s}_{q,\pi}\\
(\pi q^{2})^{(n+k)n-\binom{n}{2}}
= (\pi q^2)^{\binom{n+1}{2}+nk}.
\end{align*}
Here, we have used the definitions in \cref{numerology} for the first equality and \cref{numerologyc} for the second.
\end{proof}

\begin{remark}
From \cref{K0}(1)--(2),
tensoring with the $d$th term
$U^\ell_{(k+d);n-d} \otimes_{\EOH_{n-d}^\ell} V_{n-d;(d)}^\ell$
in the singular Rouquier complex
corresponds at the level of Grothendieck groups to the
$\Z[q,q^{-1}]^\pi$-module homomorphism
\rightarrow 1_k\mathbf{V}(-\ell)$
defined by the action of
= q^{nk}
\left(q^d E^{(k+d)}F^{(d)}
From the original definition of the map $T$ in
\cref{oddreflection},
it follows that  multiplication by the
Euler characteristic of \cref{src}
corresponds to
$q^{nk}T: 1_{-k} \mathbf{V}(-\ell)
\rightarrow 1_k \mathbf{V}(-\ell)$.
Given that the homology of the complex
vanishes in all but the top degree,
it then follows by \cref{fromR} that the
top homology is
$(\pi q^2)^{\binom{n+1}{2}+nk}\left[\EOH_{n'}^\ell\right]$
which, reassuringly, agrees with the final assertion of \cref{SRC}.
\end{remark}

\begin{proof}[Proof of \cref{SRC}]
Fix $d$ with $1 \leq d \leq n$.
Define an {\em initial pair} to be
$(\lambda,\mu) \in \GPar{(k+d)}{n}\times\GPar{d}{(n-d)}$
such that
$\lambda_{k+d} = d-1-s$ and $\mu_{d-s} = n-d$
for some $0 \leq s \leq d-1$. This condition is illustrated by the following picture:
\begin{align*}
\lambda &=
\begin{tikzpicture}[anchorbase,scale=1.3]
\draw[-] (1,0) to (1,1.8);
\draw[-] (1,.2) to (2,.2);
\fill [lightgray] (-.2,1.8) rectangle (2,1.4);
\fill [lightgray] (-.2,1.4) rectangle (1.8,1);
\fill [lightgray] (-.2,1) rectangle (1.2,.6);
\fill [gray] (-.2,0) rectangle (1,1.8);
\draw [-] (1,0) to (1,1.8);
\draw[-] (-.2,0) to (1,0) to (1,.6) to (1.2,.6) to (1.2,1) to (1.8,1) to (1.8,1.4) to (2,1.4);
\draw[-] (-.2,0) to (2,0) to (2,1.8) to (-.2,1.8) to (-.2,0);
\draw[-] (-.2,.2) to (1,.2);
\draw [decorate, decoration = {calligraphic brace}] (-.2,1.9) --  (2,1.9);
\node at (.9,2.1) {$\scriptstyle n$};
\draw [decorate, decoration = {calligraphic brace}] (-.3,0) --  (-.3,1.8);
\node at (-.6,.9) {$\scriptstyle k+d$};
\draw [decorate, decoration = {calligraphic brace,mirror}] (-.2,-.1) --  (1,-.1);
\node at (0.4,-.3) {$\scriptstyle d-s-1$};
\node at (1.4,1.45) {?};
\draw [decorate, decoration = {calligraphic brace,mirror}] (2.1,.2) --  (2.1,1.8);
\node at (2.5,1) {$\scriptstyle k+d-1$};
\draw[-] (1,0) to (2,.2);
\draw[-] (1,0.2) to (2,0);
\end{tikzpicture}
\mu &=
\begin{tikzpicture}[anchorbase,scale=1.3]
\fill [lightgray] (0,0) rectangle (.2,.4);
\fill [lightgray] (.2,.2) rectangle (.8,.4);
\fill [gray] (0,.4) rectangle (.8,1.6);
\draw[-] (0,1.4) to (.8,1.4);
\draw[-] (0,0) to (.8,0) to (.8,1.6) to (0,1.6) to (0,0);
\draw [-] (0,.4) to (.8,.4);
\draw[-] (0,0) to (.2,0) to (.2,.2) to (.8,.2);
\node at (.1,.2) {?};
\draw [decorate, decoration = {calligraphic brace}] (0,1.7) --  (.8,1.7);
\node at (0.4,1.9) {$\scriptstyle n-d$};
\draw [decorate, decoration = {calligraphic brace,mirror}] (0,-.1) --  (.8,-.1);
\node at (.4,-.3) {$\scriptstyle n-d$};
\draw [decorate, decoration = {calligraphic brace}] (-.1,0) --  (-.1,1.6);
\node at (-0.3,.8) {$\scriptstyle d$};
\draw [decorate, decoration = {calligraphic brace,mirror}] (.9,.4) --  (.9,1.6);
\node at (1.2,1) {$\scriptstyle d-s$};
\end{tikzpicture}
\end{align*}
Let $I$ be the set of all initial pairs. Note that
\begin{equation}\label{siz}
|I| = |b_{n+k,n}(d)|.
\end{equation}
To see this, the number of $(\lambda,\mu)\in I$
with $\lambda_{k+d} = d-1-s$ and $\mu_{d-s} = n-d$
is $|\GPar{(k+d-1)}{(n-d+s+1)} \times \GPar{s}{(n-d)}|$, which is
Summing\footnote{This is all we need here, but with a little more care using also \cref{qbinomialformula},
this argument can be used to show that
the coefficient of $q^{2r} \pi^r $ in $b_{n+k,n}(d)$
is equal to
the number of $(\lambda,\mu) \in I$ with $|\lambda|+|\mu| = 2r$, explaining the
definition of $b_{n+k,n}(d)$ itself rather than merely
its evaluation at $q=\pi=1$.} over $s=0,1,\dots,d-1$
gives $|b_{n+k,n}(d)|$ by the original definition of this natural number.

Also define a {\em terminal pair}
to be
$(\kappa,\nu) \in \GPar{(k+d-1)}{n}\times\GPar{(d-1)}{(n-d+1)}$
such that
$\kappa_{k+d-1} \geq d-1-s$ and $\nu_{d-s} <\nu_{d-s-1}= n-d+1$
for some $0 \leq s \leq d-1$:
\begin{align*}
\kappa &=
\begin{tikzpicture}[anchorbase,scale=1.3]
\draw[-] (1,.2) to (1,1.8);
\fill [lightgray] (-.2,1.8) rectangle (2,1.4);
\fill [lightgray] (-.2,1.4) rectangle (1.8,1);
\fill [lightgray] (-.2,1) rectangle (1.2,.6);
\fill [gray] (-.2,.2) rectangle (1,1.8);
\draw [-] (1,.2) to (1,1.8);
\draw[-] (-.2,.2) to (1,.2) to (1,.6) to (1.2,.6) to (1.2,1) to (1.8,1) to (1.8,1.4) to (2,1.4);
\draw[-] (-.2,.2) to (2,.2) to (2,1.8) to (-.2,1.8) to (-.2,.2);
\draw [decorate, decoration = {calligraphic brace}] (-.2,1.9) --  (2,1.9);
\node at (.9,2.1) {$\scriptstyle n$};
\draw [decorate, decoration = {calligraphic brace}] (-.3,.2) --  (-.3,1.8);
\node at (-.7,1) {$\scriptstyle k+d-1$};
\draw [decorate, decoration = {calligraphic brace,mirror}] (-.2,.1) --  (1,.1);
\node at (0.4,-.1) {$\scriptstyle d-s-1$};
\node at (1.4,1.45) {?};
\draw [decorate, decoration = {calligraphic brace,mirror}] (2.1,.2) --  (2.1,1.8);
\node at (2.5,1) {$\scriptstyle k+d-1$};
\end{tikzpicture}
\nu &=
\begin{tikzpicture}[anchorbase,scale=1.3]
\fill [lightgray] (0,0) rectangle (.2,.4);
\fill [lightgray] (.2,.2) rectangle (.8,.4);
\fill [gray] (0,.4) rectangle (1,1.4);
\draw[-] (0,0) to (1,0) to (1,1.4) to (0,1.4) to (0,0);
\draw[-] (.8,0) to (.8,1.4);
\draw [-] (0,.4) to (1,.4);
\draw[-] (0,0) to (.2,0) to (.2,.2) to (.8,.2);
\node at (.1,.2) {?};
\draw [decorate, decoration = {calligraphic brace}] (0,1.5) --  (1,1.5);
\node at (0.4,1.7) {$\scriptstyle n-d+1$};
\draw [decorate, decoration = {calligraphic brace,mirror}] (0,-.1) --  (.8,-.1);
\node at (.4,-.3) {$\scriptstyle n-d$};
\draw [decorate, decoration = {calligraphic brace}] (-.1,0) --  (-.1,1.4);
\node at (-0.5,.7) {$\scriptstyle d-1$};
\draw [decorate, decoration = {calligraphic brace,mirror}] (1.1,.4) --  (1.1,1.4);
\node at (1.6,1) {$\scriptstyle d-s-1$};
\draw[-] (.8,0) to (.8,.4);
\draw[-] (.8,0) to (1,.4);
\draw[-] (1,0) to (.8,.4);
\end{tikzpicture}
\end{align*}
Let $T$ be the set of all terminal pairs.
Our final combinatorial observation
is that there is a bijection \begin{equation}\label{fd}
f:I \stackrel{\sim}{\rightarrow} T
\end{equation}
$(\lambda,\mu) \in I$ to $(\lambda^-,\mu^+) \in T$
where $\lambda^-$ is obtained from $\lambda$ by removing the
bottom row of its Young diagram, and
$\mu^+$ is obtained from $\mu$ by
adding one box to the end of the first $(d-s)$ rows
then removing completely the top row.

Now we are going to make an explicit computation of
the differential
$\bar\partial_d$ in terms of the basis
for $\overline{C}_d = C_d \otimes_{\EOH_n^\ell} \k$
consisting of the vectors
% NOTE w(\lambda,\mu) = (-1)^{dN(\lambda)+dE(\lambda)+dE(\mu)+dE(\mu)} w_old(\lambda,\mu)
\begin{equation}
w(\lambda,\mu) :=
u_{n-d;(k+d)}\big(\bar \sigma^{(k+d)}_\lambda\big)
\otimes v_{n-d;(d)}\big(\bar \sigma^{(d)}_\mu\big)
\otimes 1 \in
V_{n-d;(d)}^\ell \otimes_{\EOH_n^\ell} \k
\end{equation}
for $(\lambda,\mu) \in
\GPar{(k+d)}{n}\times \GPar{d}{(n-d)}$; cf. \cref{depoebay}.
Order pairs $(\kappa,\nu) \in \GPar{(k+d-1)}{n} \times \GPar{(d-1)}{(n-d+1)}$
so that $(\kappa',\nu') < (\kappa,\nu)$
if either $|\kappa'| < |\kappa|$,
or $|\kappa'| = |\kappa|$ and $\nu' <_{\lex} \nu$.
We claim for $(\lambda,\mu) \in I$ that
\begin{equation}\label{triangularplace}
\overline{\partial}_d(w(\lambda,\mu))
= \pm w(\lambda^-,\mu^+) + \text{
(a linear combination of $w(\kappa,\nu)$ for $(\kappa,\nu) < (\lambda^-,\mu^+)$)}.
\end{equation}
Given the claim, it follows by
\cref{siz,fd} that
$|\im \overline{\partial}_d| \geq |b_{n+k,n}(d)|$, so that the theorem
follows by \cref{mainstep}.

It remains to prove \cref{triangularplace}.
Take $(\lambda,\mu) \in
\GPar{(k+d)}{n}\times \GPar{d}{(n-d)}$
and consider $\overline{\partial}_d(w(\lambda,\mu))$.
According to
the definition of $\overline{\partial}_d$, we have to apply three
different maps to $w(\lambda,\mu)$ arising from $b_{(d+k-1),(1)}$,
$c_{(1),(d-1)}$ and $\ev_{n-d}$. We apply these maps one by one.
\begin{itemize}
\item
First, the map $b_{(d+k-1),(1)}$ comes from the embedding
\OSym_{k+d} \hookrightarrow \OSym_{(k+d-1,1)}
\stackrel{\sim}{\rightarrow}
\OSym_{k+d-1} \otimes \k[x].
\cref{thepierineededlater} shows that this embedding takes
to $\sum_{\kappa} \pm s_{\kappa}^{(k+d-1)}
\otimes x^{|\lambda|-|\kappa|}$
summing over all
$\kappa \in \GPar{(k+d-1)}{n}$ whose Young diagram is
obtained by removing boxes from the bottoms of different columns of
the Young diagram of $\lambda$,
necessarily including all
boxes on its $(k+d)$th row.
We say simply ``$\kappa$ obtained by removing a row strip from $\lambda$''
for this from now on.
\item
Next, we apply the map $c_{(1),(d-1)}$, which comes from the embedding
\OSym_d \hookrightarrow \OSym_{(1,d-1)}
\stackrel{\sim}{\rightarrow} \k[x] \otimes \OSym_{d-1},
plus some extra signs due to the parity shift.
The version of Pieri obtained by applying $\gamma_d$
to \cref{thepierineededlater} (using also \cref{littlebears})
shows that this
takes $\sigma_\mu^{(d)}$
to $\sum_{\delta} \pm x^{|\mu|-|\delta|} \otimes
\sigma_{\delta}^{(d-1)}$
summing over
$\delta\in \GPar{(d-1)}{(n-d)}$ whose Young diagram is obtained by removing
boxes from the bottoms of different columns of the Young diagram
of $\mu$, necessarily including all $\mu_d$ boxes on its $d$th row,
to obtain the Young diagram of partition $\delta$.
We say simply ``$\delta$ obtained by removing a row strip from $\mu$'' for this from now on.
\item
So far, remembering \cref{fancynotation2},
we have shown that
$\big(b_{(k+d-1),(1)}\otimes\; c_{(1),(d-1)}\otimes \id \big)\circ (\operatorname{inc} \otimes \id)$
takes $w(\lambda,\mu)$
\sum_{(\kappa,\delta)} \pm u_{(k+d-1);n-d+1}\big(\sigma_\kappa^{(k+d-1)}\big)
\otimes u_{n-d}\big(x^{|\lambda|-|\kappa|}\big) \otimes v_{n-d}\big(x^{|\mu|-|\delta|}\big)
\otimes v_{n-d+1;(d-1)}\big(\sigma_\delta^{(d-1)}\big)\otimes 1
summing over $(\kappa,\delta) \in \GPar{(k+d-1)}{n}\times\GPar{(d-1)}{(n-d)}$
such that $\kappa$ is obtained by removing a row strip from
$\lambda$ and $\delta$ is obtained by removing a row strip from $\mu$.
Then we use the definition in
\cref{cupsandcaps} to
apply $(\operatorname{can}\otimes \id) \circ (\id \otimes \ev_{n-d}\otimes \id \otimes \id)$, giving
\overline{\partial}_d(w(\lambda,\mu))
\sum_{(\kappa,\delta)} \pm u_{(k+d-1);n-d+1}\big(\sigma_\kappa^{(k+d-1)}\big)
\otimes \bar\gamm^{(n-d+1)}_{(|\lambda|-|\kappa|)+(|\mu|-|\delta|)-
v_{n-d+1;(d-1)}\big(\sigma_\delta^{(d-1)}\big)\otimes 1.
summing over all $(\kappa,\delta) \in \GPar{(k+d-1)}{n}\times
\GPar{(d-1)}{(n-d)}$
obtained by removing a row strip from $(\lambda,\mu)
\in \GPar{(k+d)}{n}\times\GPar{d}{(n-d)}$.
\end{itemize}
It remains to commute the
elements $\bar\gamm^{(n-d+1)}_{(|\lambda|-|\kappa|)+(|\mu|-|\delta|)-
(n-d)}$ to the right hand side in this expression.
In view of \cref{lemma01}(1)
and degree considerations, this will produce
some linear combination of basis vectors of the form $w(\kappa,\nu)$
for $\nu\in\GPar{(d-1)}{(n-d+1)}$ with $|\nu| =
We just need to show that $w(\lambda^-,\mu^+)$ appears with
coefficient $\pm 1$ and all other $w(\kappa,\nu)$
that arise satisfy $(\kappa,\nu) < (\lambda^-,\mu^+)$.
This is clearly the case if $|\kappa| < |\lambda^-|$,
so we may assume from now on that $\kappa$, like $\lambda^-$,
is obtained from $\lambda$
by removing the minimal number of boxes, i.e., just
its bottom row. So we have that $\kappa = \lambda^-$
and $|\lambda|-|\kappa| = \lambda_{k+d}$, which equals $d-s-1$ for
a unique $0 \leq s < d$.
Also let $p := (d-s+1)+(|\mu|-|\delta|)
- (n-d)$ for short and consider
\bar\gamm^{(n-d+1)}_{p}
v_{n-d+1;(d-1)}\big(\sigma_\delta^{(d-1)}\big)\otimes 1.
By \cref{alreadybasis}, we have that
$\gamm^{(n-d+1)}_p = s^{(n-d+1)}_{(p)}$
plus a linear combination of other $s^{(n-d+1)}_\tau$
for partitions $\tau$ with $|\tau|=p$ and $\h(\tau) > 1$.
Also $\sigma_{(1^p)}^{(d-1)} = \eps_p^{(d-1)}$.
Using \cref{trains}, we deduce that
\begin{equation}\label{dishy}
\bar\gamm^{(n-d+1)}_{p}
v_{n-d+1;(d-1)}\big(\sigma_\delta^{(d-1)}\big)\otimes 1
\pm v_{n-d+1;(d-1)}\big(\sigma_{\delta}^{(d-1)} \eps_p^{(d-1)}\big) \otimes 1
+ (*)
\end{equation}
where $(*)$
is a linear combination of
terms of the form
$v_{n-d+1;(d-1)}\big(\sigma_\delta^{(d-1)} \sigma^{(d-1)}_\tau\big)\otimes 1$
for partitions $\tau$ with $|\tau|=p$ and $\tau_1 > 1$.
We can compute all of these products of dual Schur polynomials
by conjugating with $\smiley_{d-1}$ and
using the odd Littlewood-Richardson rule; see \cref{discussionhere}.
Remembering also that
$v_{n-d+1;(d-1)}\big(\sigma_\nu^{(d-1)}\big)\otimes 1 = 0$
unless $\nu \in \GPar{(d-1)}{(n-d+1)}$ by \cref{lemma01}(1) again,
we obtain a linear combination of
basis vectors
$v_{n-d+1;(d-1)}\big(\sigma_{\nu}^{(d-1)}\big)\otimes 1$
for $\nu\in \GPar{(d-1)}{(n-d+1)}$ obtained from $\delta$
by adding $p$ boxes in particular ways.
If $p < d-s-1$ then we cannot have $\nu = \mu^+$
since that has $d-s+1$ boxes in the rightmost column,
whereas that column is empty in $\delta$.
Now suppose that $p = d-s-1$; then $\delta$ is $\mu$ with
all $(n-d)$ boxes in its first row removed.
In this case,
the leading term
$\pm v_{n-d+1;(d-1)}\Big(\sigma_{\delta}^{(d-1)}\eps_p^{(d-1)} \big) \otimes 1$ computed via the odd Littlewood-Richardson rule
does produce $\pm v_{n-d+1;(d-1)}\big(\sigma_{\mu^+}^{(d-1)}\big)\otimes 1$
when a column strip of $p$ boxes is added at the top right of the Young diagram of $\delta$. All other basis vectors coming from this leading term
are of the form
$v_{n-d+1;(d-1)}\big(\sigma_{\nu}^{(d-1)}\big)\otimes 1$
for $\nu <_{\lex} \mu^+$.
The basis vectors coming from the lower terms
$v_{n-d+1;(d-1)}\big(\sigma_\delta^{(d-1)}\sigma^{(d-1)}_\tau \big)\otimes 1$
for $\tau$ with $|\tau|=p$ and $\tau_1 > 1$
must also all be of the form
$v_{n-d+1;(d-1)}\big(s_{\nu}^{(d-1)}\big)\otimes 1$
for $\nu <_{\lex} \mu^+$ since when $\tau_1 > 1$ the odd Littlewood-Richardson rule
does not allow all $p$ boxes to be added to the same column of the
Young diagram of $\delta$.
\end{proof}

\section{Non-degeneracy of the odd 2-category
\texorpdfstring{$\UU(\sl_2)$}{U(sl(2))}}\label{catsec}

In this section, we will use the
string calculus for strict graded monoidal supercategories and 2-supercategories
adopting all of the conventions from [2]. In particular,
$f \circ g$ is vertical composition ($f$ on top of $g$) and $f \otimes g$ or simply $fg$ is horizontal composition
($f$ to the left of $g$).
The following definition originated in [18] and was reformulated in the present terms in [3].

\begin{definition}\label{km2cat}
The {\em odd $\mathfrak{sl}_2$ 2-category}
is the strict graded $2$-supercategory
$\UU(\sl_2)$ with object set $\Z$,
generating 1-morphisms
$E 1_k =1_{k+2} E:k \rightarrow k\!+\!2$ and
$1_k F = F 1_{k+2}:k\!+\!2 \rightarrow k$ for each $k \in \Z$
whose identity 2-morphisms are represented graphically
by $\Big\uparrow \:{\red\scriptstyle k}={\red \scriptstyle k+2}\:\Big\uparrow$ and
${\red\scriptstyle k} \:\Big\downarrow=\Big\downarrow \:{\red \scriptstyle k+2}$, respectively,
and generating 2-morphisms
\begin{align}\label{solid1}
\begin{tikzpicture}[anchorbase]
\draw[->] (0.08,-.3) to (0.08,.4);
\opendot{0.08,0.05};
\node at (.3,.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
:E 1_k \Rightarrow E 1_k
\begin{tikzpicture}[anchorbase]
\draw[->] (0.2,-.3) to (-0.2,.4);
\draw[->] (-0.2,-.3) to (0.2,.4);
\node at (.35,.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}:E^2 1_k \Rightarrow E^2 1_k
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.4,0.3) to[out=-90, in=0] (0.1,-0.2);
\draw[-] (0.1,-0.2) to[out = 180, in = -90] (-0.2,0.3);
\node at (0.55,-0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
:FE 1_k\Rightarrow 1_k
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.4,-0.2) to[out=90, in=0] (0.1,0.3);
\draw[-] (0.1,0.3) to[out = 180, in = 90] (-0.2,-0.2);
\node at (0.55,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
:1_{k} \Rightarrow EF 1_{k}
\end{align}
which are odd of degree 2, odd of degee $-2$,
even of degree $k+1$, and even of degree $1-k$, respectively.
Then there are three families of relations.
First we have the odd nil-Hecke relations (in the standard formulation
rather than the modified version from \cref{ONH1,ONH3,ONH5,ONH2,ONH4,ONH6}):
\begin{align}
\begin{tikzpicture}[anchorbase,scale=.85]
\draw[->] (0.28,.4) to[out=90,in=-90] (-0.28,1.1);
\draw[->] (-0.28,.4) to[out=90,in=-90] (0.28,1.1);
\draw[-] (0.28,-.3) to[out=90,in=-90] (-0.28,.4);
\draw[-] (-0.28,-.3) to[out=90,in=-90] (0.28,.4);
\node at (0.5,0.4) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.45,.8) to (-0.45,-.4);
\draw[->] (0.45,-.4) to (-0.45,.8);
\draw[-] (0,-.4) to[out=90,in=-90] (-.45,0.2);
\draw[->] (-0.45,0.2) to[out=90,in=-90] (0,0.8);
\node at (.4,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.45,.8) to (-0.45,-.4);
\draw[->] (0.45,-.4) to (-0.45,.8);
\draw[-] (0,-.4) to[out=90,in=-90] (.45,0.2);
\draw[->] (0.45,0.2) to[out=90,in=-90] (0,0.8);
\node at (0.7,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}&
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.25,.6) to (-0.25,-.2);
\draw[->] (0.25,-.2) to (-0.25,.6);
\opendot{0.15,0.42};
\node at (0.4,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}+
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.25,.6) to (-0.25,-.2);
\draw[->] (0.25,-.2) to (-0.25,.6);
\opendot{-0.13,-0.02};
\node at (0.4,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.25,.6) to (-0.25,-.2);
\draw[->] (0.25,-.2) to (-0.25,.6);
\opendot{0.15,-0.02};
\node at (.3,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.25,.6) to (-0.25,-.2);
\draw[->] (0.25,-.2) to (-0.25,.6);
\opendot{-0.13,0.42};
\node at (.3,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[->] (0.08,-.2) to (0.08,.6);
\draw[->] (-0.2,-.2) to (-0.2,.6);
\node at (0.3,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\label{nearlydone}\end{align}
Next we have the {\em right adjunction relations}
asserting that $Q^{-k-1} 1_{k}F $ is
right dual to $E 1_k$ in the $(Q,\Pi)$-envelope of $\UU(\sl_2)$
(cf. \cref{oddadjunction}(1)):
\begin{align}\label{rightadj}
\begin{tikzpicture}[anchorbase]
\draw[->] (0.3,0) to (0.3,.4);
\draw[-] (0.3,0) to[out=-90, in=0] (0.1,-0.3);
\draw[-] (0.1,-0.3) to[out = 180, in = -90] (-0.1,0);
\draw[-] (-0.1,0) to[out=90, in=0] (-0.3,0.3);
\draw[-] (-0.3,0.3) to[out = 180, in =90] (-0.5,0);
\draw[-] (-0.5,0) to (-0.5,-.4);
\node at (0.5,.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[->] (0,-0.4) to (0,.4);
\node at (0.2,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}&
\begin{tikzpicture}[anchorbase]
\draw[->] (0.3,0) to (0.3,-.4);
\draw[-] (0.3,0) to[out=90, in=0] (0.1,0.3);
\draw[-] (0.1,0.3) to[out = 180, in = 90] (-0.1,0);
\draw[-] (-0.1,0) to[out=-90, in=0] (-0.3,-0.3);
\draw[-] (-0.3,-0.3) to[out = 180, in =-90] (-0.5,0);
\draw[-] (-0.5,0) to (-0.5,.4);
\node at (-0.7,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0,-0.4) to (0,.4);
\node at (-0.2,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\end{align}
Finally there are some {\em inversion relations}.
To formulate these, we first
introduce new 2-morphisms
\begin{align}\label{sigrel}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.3,-.3) to (-0.3,.4);
\draw[->] (-0.3,-.3) to (0.3,.4);
\node at (.4,.05) {$\red\scriptstyle k$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[->] (0.3,-.5) to (-0.3,.5);
\draw[->] (-0.7,.4) to[out=-90,in=180] (-.35,-.4) to[out=0,in=180] (.35,.4) to[out=0,in=90] (.7,-.5);
\node at (.9,.05) {$\red\scriptstyle k$};
\end{tikzpicture}
:E F 1_k \rightarrow F E 1_k.
\end{align}
Then, denoting powers of the dot generator by labelling it with a natural number,  we require that the following (not necessarily homogeneous) 2-morphisms are isomorphisms:
\begin{align}\label{inv1}
\left(\:
\displaystyle\begin{tikzpicture}[baseline = 0]
\draw[<-] (0.3,-.3) to (-0.3,.4);
\draw[->] (-0.3,-.3) to (0.3,.4);
\node at (.4,.05) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\qquad
\begin{tikzpicture}[baseline = 0]
\draw[<-] (0.4,-.1) to[out=90, in=0] (0.1,0.4);
\draw[-] (0.1,0.4) to[out = 180, in = 90] (-0.2,-.1);
\node at (0.6,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\qquad
\begin{tikzpicture}[baseline = 0]
\draw[<-] (0.4,-.1) to[out=90, in=0] (0.1,0.4);
\draw[-] (0.1,0.4) to[out = 180, in = 90] (-0.2,-.1);
\node at (0.6,0.2) {$\red\scriptstyle{k}$};
\opendot{-0.15,0.2};
\end{tikzpicture}\qquad
\cdots\qquad
\begin{tikzpicture}[baseline = 0]
\draw[<-] (0.5,-.1) to[out=90, in=0] (0.15,0.4);
\draw[-] (0.15,0.4) to[out = 180, in = 90] (-0.2,-.1);
\node at (0.7,0.2) {$\red\scriptstyle{k}$};
\node at (0.15,0.2) {$\scriptstyle{k-1}$};
\opendot{-0.15,0.2};
\end{tikzpicture}
\right)^T&:
E F 1_k\stackrel{\sim}{\rightarrow}
F E 1_k \oplus 1_k^{\oplus k}&&
\text{for $k \geq 0$}\\
\left(\:
\displaystyle\begin{tikzpicture}[baseline = 0]
\draw[<-] (0.3,-.3) to (-0.3,.4);
\draw[->] (-0.3,-.3) to (0.3,.4);
\node at (.4,-.05) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\qquad
\begin{tikzpicture}[baseline = 0]
\draw[<-] (0.4,0.2) to[out=-90, in=0] (0.1,-.3);
\draw[-] (0.1,-.3) to[out = 180, in = -90] (-0.2,0.2);
\node at (0.6,-0.25) {$\red\scriptstyle{k}$};
\end{tikzpicture}\qquad
\begin{tikzpicture}[baseline = 0]
\draw[<-] (0.4,0.2) to[out=-90, in=0] (0.1,-.3);
\draw[-] (0.1,-.3) to[out = 180, in = -90] (-0.2,0.2);
\opendot{.38,0};
\node at (0.6,-0.25) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\qquad\cdots\qquad
\begin{tikzpicture}[baseline = 0]
\draw[<-] (0.5,0.2) to[out=-90, in=0] (0.1,-.3);
\draw[-] (0.1,-.3) to[out = 180, in = -90] (-0.3,0.2);
\node at (0.65,-0.25) {$\red\scriptstyle{k}$};
\node at (0.1,0) {$\scriptstyle{-k-1}$};
\opendot{.47,0};
\end{tikzpicture}\right)
&:E F 1_k \oplus  1_k^{\oplus (-k)}
\stackrel{\sim}{\rightarrow}
F E 1_k&&\text{for $k \leq 0$.}\label{inv2}
\end{align}
The morphisms depicted in \cref{inv1,inv2}
represent a $(k+1)\times 1$ matrix
and a $1\times (1-k)$ matrix of 2-morphisms
in $\UU(\sl_2)$, respectively, i.e., they are 2-morphisms in the additive envelope of $\UU(\sl_2)$. Saying that they are isomorphisms means that
there are some
further generating $2$-morphisms in $\UU(\sl_2)$ which provide
the matrix entries of two-sided inverses to these morphisms.
\end{definition}

The defining relations \cref{solid1,nearlydone,rightadj,inv1,inv2} look quite innocent but they imply many further relations.
In order to record some of these, we first
need to introduce some further shorthand for
generating $2$-morphisms whose existence is provided by the inversion relation. First, we have the leftward crossing and the leftward cups and caps \begin{align}\label{solid2}
\begin{tikzpicture}[baseline = 0]
\draw[->] (0.3,-.3) to (-0.3,.4);
\draw[<-] (-0.3,-.3) to (0.3,.4);
\node at (.45,.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}:F E 1_k \Rightarrow E F 1_k
\begin{tikzpicture}[baseline = 0]
\draw[-] (0.4,0.3) to[out=-90, in=0] (0.1,-0.2);
\draw[->] (0.1,-0.2) to[out = 180, in = -90] (-0.2,0.3);
\node at (0.55,-0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
:1_{k} EF\Rightarrow 1_{k}
\begin{tikzpicture}[baseline = 0]
\draw[-] (0.4,-0.2) to[out=90, in=0] (0.1,0.3);
\draw[->] (0.1,0.3) to[out = 180, in = 90] (-0.2,-0.2);
\node at (0.55,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
:1_{k} \Rightarrow FE 1_{k}
\end{align}
which are defined as follows.
\begin{itemize}
\item
We let
$\begin{tikzpicture}[baseline = 0,scale=.8]
\draw[->] (0.3,-.3) to (-0.3,.4);
\draw[<-] (-0.3,-.3) to (0.3,.4);
\node at (.45,.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}:F E 1_k \Rightarrow E F 1_k
be the {\em negation} of the leftmost entry of the $1 \times (k+1)$ matrix that is the two-sided inverse of \cref{inv1}
if $k \geq 0$,
or the {\em negation} of the top entry of the $(1-k)\times 1$ matrix that is the two-sided inverse of \cref{inv2} if $k \leq 0$; cf. \cite[(2.8)--(2.9)]{BE2}.
\item
We let
$\begin{tikzpicture}[baseline = 0,scale=.8]
\draw[-] (0.4,0.3) to[out=-90, in=0] (0.1,-0.2);
\draw[->] (0.1,-0.2) to[out = 180, in = -90] (-0.2,0.3);
\node at (0.5,-0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
be the rightmost entry of the $1\times (k+1)$ matrix that is the
two-sided inverse of \cref{inv1} if $k > 0$,
or $(-1)^{k+1}
\begin{tikzpicture}[anchorbase,scale=.75]
\draw[-] (0.28,.6) to[out=240,in=90] (-0.28,-.1);
\draw[<-] (-0.28,.6) to[out=300,in=90] (0.28,-0.1);
\node at (-.05,-.1) {$\scriptstyle{-k}$};
\draw[-] (0.28,-0.1) to[out=-90, in=0] (0,-0.4);
\draw[-] (0,-0.4) to[out = 180, in = -90] (-0.28,-0.1);
\node at (.7,0.1) {$\red\scriptstyle{k}$};
\opendot{0.28,-0.1};
\end{tikzpicture}$ if $k \leq 0$; cf. \cite[(2.10)]{BE2}.
\item We let
\begin{tikzpicture}[baseline = 0,scale=.8]
\draw[-] (0.4,-0.2) to[out=90, in=0] (0.1,0.3);
\draw[->] (0.1,0.3) to[out = 180, in = 90] (-0.2,-0.2);
\node at (0.55,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
be the bottom entry of the $(1-k) \times 1$ matrix that is the two-sided inverse of \cref{inv2}
if $k < 0$, or
\begin{tikzpicture}[anchorbase,scale=.75]
\draw[-] (0.28,-.6) to[out=120,in=-90] (-0.28,.1);
\draw[<-] (-0.28,-.6) to[out=60,in=-90] (0.28,.1);
\node at (.5,-.1) {$\red\scriptstyle{k}$};
\draw[-] (0.28,0.1) to[out=90, in=0] (0,0.4);
\draw[-] (0,0.4) to[out = 180, in = 90] (-0.28,0.1);
\node at (-0.05,0.1) {$\scriptstyle{k}$};
\opendot{-.25,0.1};
\end{tikzpicture}$ if $k \geq 0$; cf. \cite[(2.11)]{BE2}
\end{itemize}
Finally, we have the downward dot and the downward crossing, which are
the right mates of the upward dot and the upward crossing:
\begin{align}\label{phew}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.08,-.4) to (0.08,.4);
\opendot{0.08,0};
\node at (-.21,.15) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[->] (0.3,0) to (0.3,-.4);
\draw[-] (0.3,0) to[out=90, in=0] (0.1,0.3);
\draw[-] (0.1,0.3) to[out = 180, in = 90] (-0.1,0);
\draw[-] (-0.1,0) to[out=-90, in=0] (-0.3,-0.3);
\draw[-] (-0.3,-0.3) to[out = 180, in =-90] (-0.5,0);
\draw[-] (-0.5,0) to (-0.5,.4);
\opendot{-0.1,0};
\node at (-0.67,0) {$\red\scriptstyle{k}$};
\end{tikzpicture}
:1_k F \Rightarrow 1_k F&
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.3,-.4) to (-0.3,.4);
\draw[<-] (-0.3,-.4) to (0.3,.4);
\node at (-.35,.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[->] (1.3,.4) to (1.3,-1.2);
\draw[-] (-1.3,-.4) to (-1.3,1.2);
\draw[-] (.5,1.1) to [out=0,in=90] (1.3,.4);
\draw[-] (-.35,.4) to [out=90,in=180] (.5,1.1);
\draw[-] (-.5,-1.1) to [out=180,in=-90] (-1.3,-.4);
\draw[-] (.35,-.4) to [out=-90,in=0] (-.5,-1.1);
\draw[-] (.35,-.4) to [out=90,in=-90] (-.35,.4);
\draw[-] (-0.35,-.5) to[out=0,in=180] (0.35,.5);
\draw[->] (0.35,.5) to[out=0,in=90] (0.8,-1.2);
\draw[-] (-0.35,-.5) to[out=180,in=-90] (-0.8,1.2);
\node at (-1.5,0) {$\red\scriptstyle{k}$};
\end{tikzpicture}
:1_k F^2 \Rightarrow 1_k F^2.
\end{align}
The following table summarizes the parity and degree information about all of the 2-morphisms defined thus far.
\begin{equation}\label{table}
\begin{array}{|c|c|c||c|c|c|}
\hline
\text{Generator}&\text{Degree}&\text{Parity}&\text{Generator}&\text{Degree}&\text{Parity}\\\hline
\begin{tikzpicture}[baseline = 0,scale=.8]
\draw[->] (0.08,-.3) to (0.08,.3);
\opendot{.08,0};
\end{tikzpicture}
{\red\scriptstyle k}
&2&\bar 1&
\begin{tikzpicture}[baseline = 0,scale=.8]
\draw[<-] (0.08,-.3) to (0.08,.3);
\opendot{0.08,0.05};
\end{tikzpicture}
{\red\scriptstyle k}
&2&\bar 1\\
\begin{tikzpicture}[baseline = 0,scale=.8]
\draw[->] (0.3,-.3) to (-0.3,.3);
\draw[->] (-0.3,-.3) to (0.3,.3);
\node at (.4,.05) {$\red\scriptstyle{k}$};
\end{tikzpicture}
&-2&\bar 1&
\begin{tikzpicture}[baseline = 0,scale=.8]
\draw[<-] (0.3,-.3) to (-0.3,.3);
\draw[->] (-0.3,-.3) to (0.3,.3);
\node at (.4,.05) {$\red\scriptstyle{k}$};
\end{tikzpicture}&0&\bar 1\\
\begin{tikzpicture}[baseline = 0,scale=.8]
\draw[<-] (0.3,-.3) to (-0.3,.3);
\draw[<-] (-0.3,-.3) to (0.3,.3);
\node at (.4,.05) {$\red\scriptstyle{k}$};
\end{tikzpicture}
&-2&\bar 1&
\begin{tikzpicture}[baseline = 0,scale=.8]
\draw[->] (0.3,-.3) to (-0.3,.3);
\draw[<-] (-0.3,-.3) to (0.3,.3);
\node at (.4,.05) {$\red\scriptstyle{k}$};
\end{tikzpicture}
&0&\bar 1\\
\begin{tikzpicture}[baseline = 0,scale=.8]
\draw[<-] (0.4,0.4) to[out=-90, in=0] (0.1,-0.1);
\draw[-] (0.1,-0.1) to[out = 180, in = -90] (-0.2,0.4);
\node at (0.65,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[baseline = 0,scale=.8]
\draw[-] (0.4,0.4) to[out=-90, in=0] (0.1,-0.1);
\draw[->] (0.1,-0.1) to[out = 180, in = -90] (-0.2,0.4);
\node at (0.65,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
&1-k&\bar k+\1\\
\begin{tikzpicture}[baseline = 0,scale=.8]
\draw[<-] (0.4,-0.1) to[out=90, in=0] (0.1,0.4);
\draw[-] (0.1,0.4) to[out = 180, in = 90] (-0.2,-0.1);
\node at (0.65,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[baseline = 0,scale=.8]
\draw[-] (0.4,-0.1) to[out=90, in=0] (0.1,0.4);
\draw[->] (0.1,0.4) to[out = 180, in = 90] (-0.2,-0.1);
\node at (0.65,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
&k+1&\bar k+\1\\
\hline
\end{array}
\end{equation}
The following relations
are derived from the defining relations
in [3].
\begin{itemize}
\item {\em Downward odd nil-Hecke relations}; cf. \cite[(3.7),(3.9),(3.5)--(3.6)]{BE2}.
\begin{align}
\begin{tikzpicture}[anchorbase,scale=.85]
\draw[-] (0.28,.4) to[out=90,in=-90] (-0.28,1.1);
\draw[-] (-0.28,.4) to[out=90,in=-90] (0.28,1.1);
\draw[<-] (0.28,-.3) to[out=90,in=-90] (-0.28,.4);
\draw[<-] (-0.28,-.3) to[out=90,in=-90] (0.28,.4);
\node at (-0.5,0.4) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[->] (0.45,.8) to (-0.45,-.4);
\draw[<-] (0.45,-.4) to (-0.45,.8);
\draw[<-] (0,-.4) to[out=90,in=-90] (-.45,0.2);
\draw[-] (-0.45,0.2) to[out=90,in=-90] (0,0.8);
\node at (-.7,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[->] (0.45,.8) to (-0.45,-.4);
\draw[<-] (0.45,-.4) to (-0.45,.8);
\draw[<-] (0,-.4) to[out=90,in=-90] (.45,0.2);
\draw[-] (0.45,0.2) to[out=90,in=-90] (0,0.8);
\node at (-0.5,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}&
\begin{tikzpicture}[anchorbase]
\draw[->] (0.25,.6) to (-0.25,-.2);
\draw[<-] (0.25,-.2) to (-0.25,.6);
\opendot{0.15,0.42};
\node at (-0.4,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}+
\begin{tikzpicture}[anchorbase]
\draw[->] (0.25,.6) to (-0.25,-.2);
\draw[<-] (0.25,-.2) to (-0.25,.6);
\opendot{-0.13,-0.02};
\node at (-0.4,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\draw[->] (0.25,.6) to (-0.25,-.2);
\draw[<-] (0.25,-.2) to (-0.25,.6);
\opendot{0.15,-0.02};
\node at (-.3,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[->] (0.25,.6) to (-0.25,-.2);
\draw[<-] (0.25,-.2) to (-0.25,.6);
\opendot{-0.13,0.42};
\node at (-.3,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
-   \begin{tikzpicture}[anchorbase]
\draw[<-] (0.08,-.2) to (0.08,.6);
\draw[<-] (-0.2,-.2) to (-0.2,.6);
\node at (-0.35,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\label{nearlydone2}\end{align}
\item {\em Left adjunction relations}; cf. \cite[(6.6)]{BE2}.
\begin{align}\label{leftadj}
\begin{tikzpicture}[anchorbase]
\draw[-] (0.3,0) to (0.3,.4);
\draw[-] (0.3,0) to[out=-90, in=0] (0.1,-0.3);
\draw[-] (0.1,-0.3) to[out = 180, in = -90] (-0.1,0);
\draw[-] (-0.1,0) to[out=90, in=0] (-0.3,0.3);
\draw[-] (-0.3,0.3) to[out = 180, in =90] (-0.5,0);
\draw[->] (-0.5,0) to (-0.5,-.4);
\node at (-0.7,.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0,-0.4) to (0,.4);
\node at (-0.2,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}&
\begin{tikzpicture}[anchorbase]
\draw[-] (0.3,0) to (0.3,-.4);
\draw[-] (0.3,0) to[out=90, in=0] (0.1,0.3);
\draw[-] (0.1,0.3) to[out = 180, in = 90] (-0.1,0);
\draw[-] (-0.1,0) to[out=-90, in=0] (-0.3,-0.3);
\draw[-] (-0.3,-0.3) to[out = 180, in =-90] (-0.5,0);
\draw[->] (-0.5,0) to (-0.5,.4);
\node at (0.5,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
(-1)^{k+1} \begin{tikzpicture}[anchorbase]
\draw[->] (0,-0.4) to (0,.4);
\node at (0.2,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\end{align}
Recalling \cref{oddadjunction}(1), these imply that
$Q^{k+1} \Pi^{k+1}E 1_k$ is right dual to $1_k F$ in the $(Q,\Pi)$-envelope
of $\UU(\sl_2)$.
\item {\em Infinite Grassmannian relation}; cf. \cite[(5.3)--(5.7)]{BE2}.
Recall that $R$ is the largest supercommutative quotient of
$\OSym$ described explicitly in \cref{dumbc1}.
For each $k \in \Z$, there is a graded
superalgebra homomorphism\footnote{There is some freedom in defining
$\beta_k$---it is unique only up to an automorphism of $R$.
The specific choice here has been made to facilitate \cref{counterclockwisebubbles}.}
\begin{align}\label{hatbeta}
\beta_k:R &\rightarrow \End_{\UU(\sl_2)}(1_k),\\\notag
\dot \eps_r
\draw[<-] (0,0.4) to[out=180,in=90] (-.2,0.2);
\draw[-] (0.2,0.2) to[out=90,in=0] (0,.4);
\draw[-] (-.2,0.2) to[out=-90,in=180] (0,0);
\draw[-] (0,0) to[out=0,in=-90] (0.2,0.2);
\node at (0.4,0.2) {$\red\scriptstyle{k}$};
\opendot{-0.2,0.2};
\node at (-0.7,0.2) {$\scriptstyle{r+k-1}$};
\end{tikzpicture}
\text{ if $r \geq 1-k$,}\\\notag
\dot \eta_r
(-1)^{(k+1)r}\!\!\! \begin{tikzpicture}[anchorbase]
\draw[->] (0.2,0.2) to[out=90,in=0] (0,.4);
\draw[-] (0,0.4) to[out=180,in=90] (-.2,0.2);
\draw[-] (-.2,0.2) to[out=-90,in=180] (0,0);
\draw[-] (0,0) to[out=0,in=-90] (0.2,0.2);
\node at (-0.35,0.2) {$\red\scriptstyle{k}$};
\opendot{0.2,0.2};
\node at (0.7,0.2) {$\scriptstyle{r-k-1}$};
\end{tikzpicture}
\text{ if $r\geq k+1$.}
\end{align}
Following Lauda's convention from [30, 31],
we introduce new shorthands for
endomorphisms of $1_k$ called ``fake bubbles":
we have clockwise bubbles
decorated by $r+k-1$ dots on their left boundary for all $r \leq -k$
which denote $(-1)^{(k+1)r}\beta_k(\dot \eps_r)$ if $r \geq 0$ or $0$ if $r < 0$,
and we have counterclockwise bubbles decorated by $r-k-1$
dots on their right boundary for all $r \leq k$ which denote
$(-1)^{(k+1)r}\beta_k(\dot \eta_r)$ if $r \geq 0$ or $0$ if $r < 0$.
\item {\em Centrality of the odd bubble}; cf. \cite[(7.15)]{BE2}.
The ``odd bubble"
\draw[-] (0,0.3) to[out=180,in=90] (-.2,0.1);
\draw[-] (0.2,0.1) to[out=90,in=0] (0,.3);
\draw[-] (-.2,0.1) to[out=-90,in=180] (0,-0.1);
\draw[-] (0,-0.1) to[out=0,in=-90] (0.2,0.1);
\draw[-] (0.14,-0.05) to (-0.14,0.23);
\draw[-] (0.14,0.23) to (-0.14,-0.05);
\node at (0.4,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}$ is shorthand for
\draw[<-] (0,0.3) to[out=180,in=90] (-.2,0.1);
\draw[-] (0.2,0.1) to[out=90,in=0] (0,.3);
\draw[-] (-.2,0.1) to[out=-90,in=180] (0,-0.1);
\draw[-] (0,-0.1) to[out=0,in=-90] (0.2,0.1);
\opendot{-0.2,0.1};
\node at (-.03,0.1) {$\scriptstyle{k}$};
\node at (0.4,.13) {$\red\scriptstyle{k}$};
\end{tikzpicture}
if $k \geq 0$ or
\node at (0.4,0.13) {$\red\scriptstyle{k}$};
\draw[->] (0.2,0.1) to[out=90,in=0] (0,.3);
\draw[-] (0,0.3) to[out=180,in=90] (-.2,0.1);
\draw[-] (-.2,0.1) to[out=-90,in=180] (0,-0.1);
\draw[-] (0,-0.1) to[out=0,in=-90] (0.2,0.1);
\opendot{0.2,0.1};
\node at (-.06,0.13) {$\scriptstyle{-k}$};
\end{tikzpicture}$
if $k \leq 0$.
So it is
$(-1)^{k+1} \beta_k(\dot o) \in \End_{\UU(\sl_2)}(1_k)$.
These are odd 2-morphisms whose square is zero.
Moreover, they are strictly central:
\begin{align}\label{centrality}
\begin{tikzpicture}[anchorbase]
\draw[-] (0,0.2) to[out=180,in=90] (-.2,0);
\draw[-] (0.2,0) to[out=90,in=0] (0,.2);
\draw[-] (-.2,0) to[out=-90,in=180] (0,-0.2);
\draw[-] (0,-0.2) to[out=0,in=-90] (0.2,0);
\draw[-] (0.14,-0.15) to (-0.14,0.13);
\draw[-] (0.14,0.13) to (-0.14,-0.15);
\node at (.7,0) {$\red\scriptstyle{k}$};
\draw[->] (.5,-.4) to (.5,.4);
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[-] (0,0.2) to[out=180,in=90] (-.2,0);
\draw[-] (0.2,0) to[out=90,in=0] (0,.2);
\draw[-] (-.2,0) to[out=-90,in=180] (0,-0.2);
\draw[-] (0,-0.2) to[out=0,in=-90] (0.2,0);
\draw[-] (0.14,-0.15) to (-0.14,0.13);
\draw[-] (0.14,0.13) to (-0.14,-0.15);
\node at (.4,0) {$\red\scriptstyle{k}$};
\draw[->] (-.5,-.4) to (-.5,.4);
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[-] (0,0.2) to[out=180,in=90] (-.2,0);
\draw[-] (0.2,0) to[out=90,in=0] (0,.2);
\draw[-] (-.2,0) to[out=-90,in=180] (0,-0.2);
\draw[-] (0,-0.2) to[out=0,in=-90] (0.2,0);
\draw[-] (0.14,-0.15) to (-0.14,0.13);
\draw[-] (0.14,0.13) to (-0.14,-0.15);
\node at (.7,0) {$\red\scriptstyle{k}$};
\draw[<-] (.5,-.4) to (.5,.4);
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[-] (0,0.2) to[out=180,in=90] (-.2,0);
\draw[-] (0.2,0) to[out=90,in=0] (0,.2);
\draw[-] (-.2,0) to[out=-90,in=180] (0,-0.2);
\draw[-] (0,-0.2) to[out=0,in=-90] (0.2,0);
\draw[-] (0.14,-0.15) to (-0.14,0.13);
\draw[-] (0.14,0.13) to (-0.14,-0.15);
\node at (.4,0) {$\red\scriptstyle{k}$};
\draw[<-] (-.5,-.4) to (-.5,.4);
\end{tikzpicture}
\end{align}
\item {\em Pitchfork relations}; cf. \cite[(2.4)--(2.5), (7.5)--(7.6)]{BE2}.
\begin{align}
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[<-](.6,.3) to (.1,-.3);
\draw[<-] (0.6,-0.3) to[out=140, in=0] (0.1,0.2);
\draw[-] (0.1,0.2) to[out = -180, in = 90] (-0.2,-0.3);
\node at (0.7,0) {$\red\scriptstyle{k}$};
\end{tikzpicture}&=
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[<-](-.5,.3) to (0,-.3);
\draw[<-] (0.3,-0.3) to[out=90, in=0] (0,0.2);
\draw[-] (0,0.2) to[out = -180, in = 40] (-0.5,-0.3);
\node at (0.5,0) {$\red\scriptstyle{k}$};
\end{tikzpicture}&
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[->](-.5,-.2) to (0,.4);
\draw[<-] (0.3,0.4) to[out=-90, in=0] (0,-0.1);
\draw[-] (0,-0.1) to[out = 180, in = -40] (-0.5,0.4);
\node at (0.5,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}&=
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[->](.6,-.2) to (.1,.4);
\draw[<-] (0.6,0.4) to[out=-140, in=0] (0.1,-0.1);
\draw[-] (0.1,-0.1) to[out = 180, in = -90] (-0.2,0.4);
\node at (0.7,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\draw[->](.6,.3) to (.1,-.3);
\draw[<-] (0.6,-0.3) to[out=140, in=0] (0.1,0.2);
\draw[-] (0.1,0.2) to[out = -180, in = 90] (-0.2,-0.3);
\node at (0.7,0) {$\red\scriptstyle{k}$};
\end{tikzpicture}&=
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[->](-.5,.3) to (0,-.3);
\draw[<-] (0.3,-0.3) to[out=90, in=0] (0,0.2);
\draw[-] (0,0.2) to[out = -180, in = 40] (-0.5,-0.3);
\node at (0.5,0) {$\red\scriptstyle{k}$};
\end{tikzpicture}&
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[<-](-.5,-.2) to (0,.4);
\draw[<-] (0.3,0.4) to[out=-90, in=0] (0,-0.1);
\draw[-] (0,-0.1) to[out = 180, in = -40] (-0.5,0.4);
\node at (0.5,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}&=
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[<-](.6,-.2) to (.1,.4);
\draw[<-] (0.6,0.4) to[out=-140, in=0] (0.1,-0.1);
\draw[-] (0.1,-0.1) to[out = 180, in = -90] (-0.2,0.4);
\node at (0.7,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}\\
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[<-](.6,.3) to (.1,-.3);
\draw[-] (0.6,-0.3) to[out=140, in=0] (0.1,0.2);
\draw[->] (0.1,0.2) to[out = -180, in = 90] (-0.2,-0.3);
\node at (0.7,0) {$\red\scriptstyle{k}$};
\end{tikzpicture}&=
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[<-](-.5,.3) to (0,-.3);
\draw[-] (0.3,-0.3) to[out=90, in=0] (0,0.2);
\draw[->] (0,0.2) to[out = -180, in = 40] (-0.5,-0.3);
\node at (0.5,0) {$\red\scriptstyle{k}$};
\end{tikzpicture}&
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[->](-.5,-.2) to (0,.4);
\draw[-] (0.3,0.4) to[out=-90, in=0] (0,-0.1);
\draw[->] (0,-0.1) to[out = 180, in = -40] (-0.5,0.4);
\node at (0.5,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}&=
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[->](.6,-.2) to (.1,.4);
\draw[-] (0.6,0.4) to[out=-140, in=0] (0.1,-0.1);
\draw[->] (0.1,-0.1) to[out = 180, in = -90] (-0.2,0.4);
\node at (0.7,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}&
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[->](.6,.3) to (.1,-.3);
\draw[-] (0.6,-0.3) to[out=140, in=0] (0.1,0.2);
\draw[->] (0.1,0.2) to[out = -180, in = 90] (-0.2,-0.3);
\node at (0.7,0) {$\red\scriptstyle{k}$};
\end{tikzpicture}&=
\draw[->](-.5,.3) to (0,-.3);
\draw[-] (0.3,-0.3) to[out=90, in=0] (0,0.2);
\draw[->] (0,0.2) to[out = -180, in = 40] (-0.5,-0.3);
\node at (0.5,0) {$\red\scriptstyle{k}$};
\end{tikzpicture}&
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[<-](-.5,-.2) to (0,.4);
\draw[-] (0.3,0.4) to[out=-90, in=0] (0,-0.1);
\draw[->] (0,-0.1) to[out = 180, in = -40] (-0.5,0.4);
\node at (0.5,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}&=
\draw[<-](.6,-.2) to (.1,.4);
\draw[-] (0.6,0.4) to[out=-140, in=0] (0.1,-0.1);
\draw[->] (0.1,-0.1) to[out = 180, in = -90] (-0.2,0.4);
\node at (0.7,0.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\end{align}
\item {\em Dot slides}; cf. \cite[(2.3),(4.3)--(4.4)]{BE2}.
\begin{align}\label{ds}
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[<-] (0.4,0) to[out=90, in=0] (0.1,0.5);
\draw[-] (0.1,0.5) to[out = 180, in = 90] (-0.2,0);
\opendot{-0.17,0.25};
\node at (0.6,0.35) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[<-] (0.4,0) to[out=90, in=0] (0.1,0.5);
\draw[-] (0.1,0.5) to[out = 180, in = 90] (-0.2,0);
\node at (-0.4,0.35) {$\red\scriptstyle{k}$};
\opendot{0.35,0.3};
\end{tikzpicture}
\draw[<-] (0.4,0.5) to[out=-90, in=0] (0.1,0);
\draw[-] (0.1,0) to[out = 180, in = -90] (-0.2,0.5);
\opendot{-0.16,0.2};
\node at (0.55,0.15) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[<-] (0.4,0.5) to[out=-90, in=0] (0.1,0);
\draw[-] (0.1,0) to[out = 180, in = -90] (-0.2,0.5);
\node at (-0.35,0.15) {$\red\scriptstyle{k}$};
\opendot{.36,.2};
\end{tikzpicture}\\
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[-] (0.4,0) to[out=90, in=0] (0.1,0.5);
\draw[->] (0.1,0.5) to[out = 180, in = 90] (-0.2,0);
\node at (-0.4,0.4) {$\red\scriptstyle{k}$};
\opendot{0.35,0.3};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[-] (0.4,0) to[out=90, in=0] (0.1,0.5);
\draw[->] (0.1,0.5) to[out = 180, in = 90] (-0.2,0);
\opendot{-0.15,0.25};
\node at (0.6,0.35) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[-] (.44,0.65) to (0.16,0.37);
\draw[-] (0.44,.37) to (0.16,0.65);
\draw[-] (0.3,0.3) to[out=180,in=-90] (0.1,0.5);
\draw[-] (0.5,0.5) to[out=-90,in=0] (0.3,0.3);
\draw[-] (0.1,0.5) to[out=90,in=180] (0.3,0.7);
\draw[-] (0.3,0.7) to[out=0,in=90] (0.5,0.5);
\draw[-] (0.6,-0.3) to[out=90, in=0] (0.3,0.2);
\draw[->] (0.3,0.2) to[out = 180, in = 90] (0,-0.3);
\node at (-0.1,0.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[-] (0.4,0.5) to[out=-90, in=0] (0.1,0);
\draw[->] (0.1,0) to[out = 180, in = -90] (-0.2,0.5);
\node at (0.55,0.15) {$\red\scriptstyle{k}$};
\opendot{-.16,.2};
\end{tikzpicture}
\draw[-] (0.4,0.5) to[out=-90, in=0] (0.1,0);
\draw[->] (0.1,0) to[out = 180, in = -90] (-0.2,0.5);
\opendot{0.36,0.2};
\node at (-0.4,0.15) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[-] (.45,-0.35) to (0.17,-0.63);
\draw[-] (0.45,-.63) to (0.17,-0.35);
\draw[-] (0.31,-0.7) to[out=180,in=-90] (.11,-.5);
\draw[-] (0.11,-.5) to[out=90,in=180] (0.31,-0.3);
\draw[-] (.31,-.3) to[out=0,in=90] (0.51,-0.5);
\draw[-] (.51,-0.5) to[out=-90,in=0] (0.31,-.7);
\draw[-] (0.6,0.3) to[out=-90, in=0] (0.3,-0.2);
\draw[->] (0.3,-0.2) to[out = 180, in = -90] (0,0.3);
\node at (-0.15,-0.15) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\end{align}
\item {\em Almost pivotal structure\footnote{Here, we have corrected
a sign error in \cite[(1.28)]{BE2}, and another one is corrected
in \cref{notasbroad} below. These mistakes were uncovered in [13].}}; cf. \cite[(1.27)--(1.28)]{BE2}.
\begin{align}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.08,-.4) to (0.08,.4);
\opendot{0.08,0};
\node at (-.25,.15) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\draw[-] (0,0.3) to[out=180,in=90] (-.2,0.1);
\draw[-] (0.2,0.1) to[out=90,in=0] (0,.3);
\draw[-] (-.2,0.1) to[out=-90,in=180] (0,-0.1);
\draw[-] (0,-0.1) to[out=0,in=-90] (0.2,0.1);
\draw[-] (0.14,-0.05) to (-0.14,0.23);
\draw[-] (0.14,0.23) to (-0.14,-0.05);
\node at (-.4,.1) {$\red\scriptstyle k$};
\draw[<-] (0.38,-.4) to (0.38,.4);
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[-] (0.3,0) to (0.3,.4);
\draw[-] (0.3,0) to[out=-90, in=0] (0.1,-0.3);
\draw[-] (0.1,-0.3) to[out = 180, in = -90] (-0.1,0);
\draw[-] (-0.1,0) to[out=90, in=0] (-0.3,0.3);
\draw[-] (-0.3,0.3) to[out = 180, in =90] (-0.5,0);
\draw[->] (-0.5,0) to (-0.5,-.4);
\node at (-.65,0) {$\red\scriptstyle{k}$};
\opendot{-0.1,0};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.3,-.4) to (-0.3,.4);
\draw[<-] (-0.3,-.4) to (0.3,.4);
\node at (-.35,.1) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\draw[->] (-1.3,.4) to (-1.3,-1.2);
\draw[-] (1.3,-.4) to (1.3,1.2);
\draw[-] (-.5,1.1) to [out=180,in=90] (-1.3,.4);
\draw[-] (.35,.4) to [out=90,in=0] (-.5,1.1);
\draw[-] (.5,-1.1) to [out=0,in=-90] (1.3,-.4);
\draw[-] (-.35,-.4) to [out=-90,in=180] (.5,-1.1);
\draw[-] (-.35,-.4) to [out=90,in=-90] (.35,.4);
\draw[-] (0.35,-.5) to[out=180,in=0] (-0.35,.5);
\draw[->] (-0.35,.5) to[out=180,in=90] (-0.8,-1.2);
\draw[-] (0.35,-.5) to[out=0,in=-90] (0.8,1.2);
\node at (-1.55,0) {$\red\scriptstyle{k}$};
\end{tikzpicture}\label{crossingcyclicity}
\end{align}
\item {\em Bubble slides}; cf. \cite[(7.10)]{BE2}.
\begin{align}
\begin{tikzpicture}[anchorbase]
\draw[<-] (-.1,0.2) to[out=180,in=90] (-.3,0);
\draw[-] (0.1,0) to[out=90,in=0] (-0.1,.2);
\draw[-] (-.3,0) to[out=-90,in=180] (-0.1,-0.2);
\draw[-] (-.1,-0.2) to[out=0,in=-90] (0.1,0);
\node at (-.85,0) {$\scriptstyle{r+k+1}$};
\opendot{-0.3,0};
\end{tikzpicture}\:\:\:
\begin{tikzpicture}[anchorbase]
\draw[->] (0.08,-.4) to (0.08,.4);
\node at (0.33,0) {${\red\scriptstyle k}$};
\end{tikzpicture}
\sum_{s \geq 0}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0,0.2) to[out=180,in=90] (-.2,0);
\draw[-] (0.2,0) to[out=90,in=0] (0,.2);
\draw[-] (-.2,0) to[out=-90,in=180] (0,-.2);
\draw[-] (0,-0.2) to[out=0,in=-90] (0.2,0);
\node at (-.9,0) {$\scriptstyle{r+k-2s-1}$};
\opendot{-0.2,0};
\draw[->] (-1.68,-.2) to (-1.68,.6);
\node at (-1.95,0.3) {$\scriptstyle{2s}$};
\opendot{-1.68,.3};
\node at (-.8,.4) {${\red\scriptstyle k}$};
\end{tikzpicture}
\end{align}
\item {\em Curl relations}; cf. \cite[(5.21)]{BE2}.
\begin{align}\label{curlrel}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0,0.5) to (0,0.3);
\draw[-] (0,0.3) to [out=-90,in=180] (.3,-0.2);
\draw[-] (0.3,-0.2) to [out=0,in=-90](.5,0);
\draw[-] (0.5,0) to [out=90,in=0](.3,0.2);
\draw[-] (0.3,.2) to [out=180,in=90](0,-0.3);
\draw[-] (0,-0.3) to (0,-0.5);
\node at (0.3,-0.02) {$\scriptstyle{r}$};
\opendot{.2,-.18};
\node at (.3,0.4) {$\red\scriptstyle{k}$};
\end{tikzpicture}&=
\sum_{s\geq 0} (-1)^{s}
\begin{tikzpicture}[anchorbase]
\draw[->] (-0.3,-.5) to (-0.3,.5);
\node at (-0.54,0.2) {$\scriptstyle{s}$};
\opendot{-.3,0.2};
\draw[<-] (1,0) to[out=180,in=90] (.8,-0.2);
\draw[-] (1.2,-0.2) to[out=90,in=0] (1,0);
\draw[-] (.8,-0.2) to[out=-90,in=180] (1,-.4);
\draw[-] (1,-.4) to[out=0,in=-90] (1.2,-0.2);
\node at (.3,-0.2) {$\scriptstyle{r-s-1}$};
\opendot{.8,-0.2};
\node at (.4,.2) {$\red\scriptstyle k$};
\end{tikzpicture}
\end{align}
\item {\em Alternating braid relation}; cf. \cite[(7.20)]{BE2}.
\begin{align}
\label{notasbroad}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.45,.8) to (-0.45,-.4);
\draw[->] (0.45,-.4) to (-0.45,.8);
\draw[<-] (0,-.4) to[out=90,in=-90] (-.45,0.2);
\draw[-] (-0.45,0.2) to[out=90,in=-90] (0,0.8);
\node at (.5,.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.45,.8) to (-0.45,-.4);
\draw[->] (0.45,-.4) to (-0.45,.8);
\draw[<-] (0,-.4) to[out=90,in=-90] (.45,0.2);
\draw[-] (0.45,0.2) to[out=90,in=-90] (0,0.8);
\node at (.6,.2) {$\red\scriptstyle{k}$};
\end{tikzpicture}
\displaystyle\sum_{q,r,s \geq 0}
\begin{tikzpicture}[anchorbase]
\draw[<-] (0.3,0.7) to[out=-90, in=0] (0,0.3);
\draw[-] (0,0.3) to[out = 180, in = -90] (-0.3,0.7);
\node at (.6,0) {$\red\scriptstyle{k}$};
\draw[-] (0.2,0) to[out=90,in=0] (0,0.2);
\draw[<-] (0,0.2) to[out=180,in=90] (-.2,0);
\draw[-] (-.2,0) to[out=-90,in=180] (0,-0.2);
\draw[-] (0,-0.2) to[out=0,in=-90] (0.2,0);
\opendot{-0.2,0};
\node at (-1,0) {$\scriptstyle{-q-r-s-3}$};
\opendot{0.23,0.43};
\node at (0.43,0.43) {$\scriptstyle{r}$};
\draw[-] (0.3,-.7) to[out=90, in=0] (0,-0.3);
\draw[->] (0,-0.3) to[out = 180, in = 90] (-0.3,-.7);
\opendot{0.25,-0.5};
\node at (.4,-.5) {$\scriptstyle{s}$};
\draw[->] (-.98,-0.7) to (-.98,0.7);
\opendot{-0.98,0.5};
\node at (-1.15,0.5) {$\scriptstyle{q}$};
\end{tikzpicture}
\displaystyle\sum_{q,r,s \geq 0}
\begin{tikzpicture}[anchorbase]
\draw[-] (0.3,0.7) to[out=-90, in=0] (0,0.3);
\draw[->] (0,0.3) to[out = 180, in = -90] (-0.3,0.7);
\node at (1.4,-0.32) {$\red\scriptstyle{k}$};
\draw[->] (0.2,0) to[out=90,in=0] (0,0.2);
\draw[-] (0,0.2) to[out=180,in=90] (-.2,0);
\draw[-] (-.2,0) to[out=-90,in=180] (0,-0.2);
\draw[-] (0,-0.2) to[out=0,in=-90] (0.2,0);
\opendot{0.2,0};
\node at (.96,0) {$\scriptstyle{-q-r-s-3}$};
\opendot{-0.23,0.43};
\node at (-0.43,0.43) {$\scriptstyle{r}$};
\draw[<-] (0.3,-.7) to[out=90, in=0] (0,-0.3);
\draw[-] (0,-0.3) to[out = 180, in = 90] (-0.3,-.7);
\opendot{-0.25,-0.5};
\node at (-.4,-.5) {$\scriptstyle{s}$};
\draw[->] (.98,-0.7) to (.98,0.7);
\opendot{0.98,0.5};
\node at (1.15,0.5) {$\scriptstyle{q}$};
\end{tikzpicture}
\end{align}
\end{itemize}

The following theorem is an odd analog of \cite[Th.~4.12]{Lauda2}.
Our proof is shorter since we are using the more efficient
presentation of \cref{km2cat} (although afterwards there is still work to do to determine the
images of the leftward cups and caps).

\begin{theorem}\label{actiontheorem}
Fix $\ell \geq 0$.
There is a graded 2-superfunctor
$\Psi_\ell:\UU(\sl_2) \rightarrow \OGBim_\ell$
with the following properties.
\begin{enumerate}
\item
On objects,
$\Psi_\ell$ takes
to the graded superalgebra
$\EOH_n^\ell$ for $0 \leq n \leq \ell$.
All other objects of $\UU(\sl_2)$ go to the trivial graded superalgebra.
\item
On generating 1-morphisms,
$\Psi_\ell$ takes
$E 1_{2n-\ell}$ to
the graded superbimodule
$Q^{-n} U_{n}^\ell$
and $1_{2n-\ell} F$ to
the graded superbimodule $Q^{3n-\ell+1} V_{n}^\ell$, respectively,
both for $0 \leq n < \ell$.
All other generating 1-morphisms necessarily go to trivial graded superbimodules.
\item
On generating 2-morphisms,
$\Psi_\ell$ takes
\begin{align*}
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[->] (0.08,-.3) to (0.08,.4);
\opendot{0.08,0.05};
\node at (.65,.1) {$\red\scriptstyle{2n-\ell}$};
\end{tikzpicture}&\mapsto\Big(\rho_{(1);n}(x_1):Q^{-n}U_n^\ell \rightarrow
Q^{-n}U_n^\ell\Big)&&(0 \leq n \leq \ell-1)\\
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[->] (0.2,-.3) to (-0.2,.4);
\draw[->] (-0.2,-.3) to (0.2,.4);
\node at (.65,.1) {$\red\scriptstyle{2n-\ell}$};
\end{tikzpicture}&\mapsto
\Big(-\rho_{(1^2);n}(\tau_1):Q^{-2n-1} U_{n+1}^\ell\otimes_{\EOH_{n+1}^\ell} U_n^\ell
\rightarrow Q^{-2n-1}U_{n+1}^\ell \otimes_{\EOH_{n+1}^\ell} U_n^\ell
\Big)&&(0 \leq n \leq \ell-2)\\
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[<-] (0.4,0.3) to[out=-90, in=0] (0.1,-0.2);
\draw[-] (0.1,-0.2) to[out = 180, in = -90] (-0.2,0.3);
\node at (0.8,-0.1) {$\red\scriptstyle{2n-\ell}$};
\end{tikzpicture}
&\mapsto \Big(\coev_n
: \EOH_n^\ell\rightarrow
Q^{2n-\ell + 1} V_{n}^\ell \otimes_{\EOH_{n+1}^\ell} U_{n}^\ell\Big)&&(0\leq n\leq\ell-1)\\
\begin{tikzpicture}[anchorbase,scale=.8]
\draw[<-] (0.4,-0.2) to[out=90, in=0] (0.1,0.3);
\draw[-] (0.1,0.3) to[out = 180, in = 90] (-0.2,-0.2);
\node at (.99,0.2) {$\red\scriptstyle{2n-\ell+2}$};
\end{tikzpicture}
\Big(\ev_{n}: Q^{2n-\ell+1} U_{n}^\ell \otimes_{\EOH_{n}^\ell}
V_{n}^\ell \rightarrow \EOH_{n+1}^\ell\Big)
&&(0 \leq n \leq \ell-1)
\end{align*}
Here, $\rho_{(1^d);n}(a)$ is the superbimodule endomorphism
from \cref{out},
and $\ev_n$ and $\coev_n$ are as in \cref{cupsandcaps}\footnote{We
mean the same underlying linear maps---in some places we have
applied some degree shifts (but no parity shifts) so that they are
not now being viewed as homomorphisms between exactly the same {\em graded} superbimodules as before.}.
All other generating 2-morphisms are taken to zero.
\end{enumerate}
\end{theorem}

\begin{proof}
Note to start with that the assignments in (3) are superbimodule
homomorphisms of the correct degrees and parities; cf. \cref{table}.
Viewing $\OGBim_\ell$ as a strict graded 2-supercategory
as explained in \cref{howstrict}, we will simply construct
$\Psi_\ell$ as a strict
graded 2-superfunctor by checking that the defining relations from
\cref{km2cat} are all satisfied.
There are three sets of relations,
\cref{nearlydone}, \cref{rightadj} and \cref{inv1}--\cref{inv2}.

The right adjunction relations \cref{rightadj} follow immediately from \cref{cupsandcaps}.

Let us check the odd nil-Hecke relations
from \cref{nearlydone}. The
formulation of these relations in \cref{nearlydone}