Finite-dimensional tensoring preserves Verma flags

For any $\mathfrak{b}$-module $V$, define $\mathrm{\Psi }:U(\mathfrak{g}){\otimes }_{U(\mathfrak{b})}(E\otimes V)\to E\otimes (U(\mathfrak{g}){\otimes }_{U(\mathfrak{b})}V)$ by $\mathrm{\Psi }(u\otimes (e\otimes v))=u\cdot (e\otimes (1\otimes v))$, using the diagonal action. For $x\in \mathfrak{b}$, the identity $x\cdot (e\otimes (1\otimes v))=xe\otimes (1\otimes v)+e\otimes (1\otimes xv)$ proves balancing, and the definition is $\mathfrak{g}$-linear. Under [F2]'s PBW identifications both sides are filtered by the degree in $U({\mathfrak{n}}^{-})$. Expanding the diagonal action of a negative-root monomial, its leading term acts entirely on the induced factor, so the associated graded map is the flip $u\otimes e\otimes v\mapsto e\otimes u\otimes v$. It is bijective. Induction on finite degree then proves that $\mathrm{\Psi }$ itself is bijective: lift a leading term and subtract to prove surjectivity; a nonzero highest-degree term cannot map to zero, proving injectivity.

Enumerate the weights of $E$ in nonincreasing $\mathrm{\ell }$-order and choose a basis in each weight space. The initial spans in $E\otimes {\mathbb{C}}_{\mu }$ are $\mathfrak{b}$-submodules: Cartan acts by scalars on each weight, and positive-root operators raise $\mathrm{\ell }$, landing in already included spaces. Their successive quotients are ${\mathbb{C}}_{\mu +\eta }$, once for each basis vector of $E_{\eta }$. Exact induction in [F2], followed by the tensor identity of step 1.1, gives a Verma flag of $E\otimes \mathrm{\Delta }(\mu )$ with factors $\mathrm{\Delta }(\mu +\eta )$ of multiplicity $\dim E_{\eta }$, in nonincreasing $\mathrm{\ell }$-order.

For a Verma-filtered $X$ induce on the flag length. For $X=0$ both sides vanish. For the top step $0\to K\to X\to \mathrm{\Delta }(\nu )\to 0$ of a flag, exactness of $E\otimes -$ by [F4] gives an exact sequence $0\to E\otimes K\to E\otimes X\to E\otimes \mathrm{\Delta }(\nu )\to 0$; by step 2.1 and the induction hypothesis $E\otimes K$ has a finite Verma flag with multiplicities $(E\otimes K:\mathrm{\Delta }(\mu ))={\sum }_{\eta }\dim E_{\eta }(K:\mathrm{\Delta }(\mu -\eta ))$, and adjoining the flag of $E\otimes \mathrm{\Delta }(\nu )$ with multiplicities $\dim E_{\eta }{\delta }_{\nu ,\mu -\eta }$ gives a finite Verma flag of $E\otimes X$. Since multiplicity is additive along the resulting top step and $(X:\mathrm{\Delta }(\mu -\eta ))=(K:\mathrm{\Delta }(\mu -\eta ))+{\delta }_{\nu ,\mu -\eta }$ by [F1], the formula $(E\otimes X:\mathrm{\Delta }(\mu ))={\sum }_{\eta }\dim E_{\eta }(X:\mathrm{\Delta }(\mu -\eta ))$ follows.

Steps 2.1 and 3.1 prove the single-Verma statement and the consequence for a general Verma-filtered $X$, completing the proof.