Verma-filtered objects are acyclic for n-minus coinvariants

For $j>0$ one has ${\mathrm{Tor}}_j^{U({\mathfrak{n}}^{-})}(\mathbb{C},M(\psi ))=0$: by [F1] the module $M(\psi )$ is free, hence projective, and [F2] applies to a projective resolution of $M(\psi )$.

Induction on the filtration length $n$. For $n=0$ we have $M=0$ and all Tors vanish. For $n\ge 1$ use the short exact sequence $0\to M_{n-1}\to M_n\to M({\psi }_n)\to 0$ and its long exact Tor sequence [F3]. Its piece ${\mathrm{Tor}}_j(\mathbb{C},M_{n-1})\to {\mathrm{Tor}}_j(\mathbb{C},M_n)\to {\mathrm{Tor}}_j(\mathbb{C},M({\psi }_n))$ has vanishing outer terms for $j>0$: the first by induction and the second by step 1.1. Exactness in the middle gives ${\mathrm{Tor}}_j^{U({\mathfrak{n}}^{-})}(\mathbb{C},M)=0$ for all $j>0$.

For exactness of the coinvariant functor, let $0\to A\to B\to C\to 0$ be a short exact sequence of Verma-filtered objects. Its long exact Tor sequence begins ${\mathrm{Tor}}_1(\mathbb{C},C)\to \mathbb{C}\otimes A\to \mathbb{C}\otimes B\to \mathbb{C}\otimes C\to 0$; the first term vanishes by step 2.1, so $0\to \mathbb{C}\otimes A\to \mathbb{C}\otimes B\to \mathbb{C}\otimes C\to 0$ is exact. Hence $M\mapsto \mathbb{C}{\otimes }_{U({\mathfrak{n}}^{-})}M$ is exact on Verma-filtered objects.