Finite filtrations by highest-weight quotients

Given: The setting above and the hypotheses in the statement.

Fix a finite-dimensional complex semisimple Lie algebra $\mathfrak{g}$, a Cartan subalgebra $\mathfrak{h}$, and a positive Borel $\mathfrak{b}=\mathfrak{h}\oplus {\mathfrak{n}}^{+}$. Write $Q^{+}={\sum }_i{\mathbb{Z}}_{\ge 0}{\alpha }_i$, $\mu \le \lambda$ when $\lambda -\mu \in Q^{+}$, and $w\cdot \lambda =w(\lambda +\rho )-\rho$. Every $M\in \mathcal{O}$ has a finite-dimensional, $\mathfrak{b}$-stable, $\mathfrak{h}$-semisimple generating subspace $E$. There is a flag $0=E_0\subset E_1\subset \cdots \subset E_r=E$ of $\mathfrak{b}$-submodules whose quotients are one dimensional and annihilated by ${\mathfrak{n}}^{+}$. For $M=0$ take $E=0$ and the empty flag. (Finite Borel-stable generators and weight flags)

Let $x_1,\dots ,x_r$ be an ordered basis of a finite-dimensional complex Lie algebra $\mathfrak{g}$. Then the monomials $x_1^{a_1}{x}_2^{a_2}\cdots x_r^{a_r}(a_i\in {\mathbb{N}}_0)$ form a basis of $U(\mathfrak{g})$. In particular, multiplication identifies $\mathrm{gr}U(\mathfrak{g})$ with the symmetric algebra $S(\mathfrak{g})$ on the symbols of the $x_i$. (PBW gives an ordered monomial basis for the enveloping algebra)

For a $\mathfrak{g}$-module $V$, sending a homomorphism $T:M(\lambda )\to V$ to $T(v_{\lambda })$ is a bijection onto the vectors $v\in V$ of weight $\lambda$ annihilated by ${\mathfrak{n}}^{+}$. Here $M(\lambda )$ is def-verma-module. The nonzero vectors in this target are precisely the highest-weight vectors of weight $\lambda$ from def-highest-weight-vector-and-cyclic-highest-weight-module; the zero vector corresponds to the zero homomorphism. (The universal property of Verma modules)

Fix a finite-dimensional complex semisimple Lie algebra $\mathfrak{g}$, a Cartan subalgebra $\mathfrak{h}$, and a positive Borel $\mathfrak{b}=\mathfrak{h}\oplus {\mathfrak{n}}^{+}$. Write $Q^{+}={\sum }_i{\mathbb{Z}}_{\ge 0}{\alpha }_i$, $\mu \le \lambda$ when $\lambda -\mu \in Q^{+}$, and $w\cdot \lambda =w(\lambda +\rho )-\rho$. The category $\mathcal{O}$ is closed under submodules, quotients and finite direct sums and is an abelian category. If $0\to A\to E\to B\to 0$ is exact, $A,B\in \mathcal{O}$, and $E$ is $\mathfrak{h}$-semisimple, then $E\in \mathcal{O}$. The middle-term weight hypothesis is essential. (Category O is abelian and extension closed among weight modules)

Every Verma module $M(\lambda )$ and every quotient of it lies in $\mathcal{O}$; the proof verifies finite generation, weight decomposition, and local ${\mathfrak{n}}^{+}$-finiteness from the PBW weight cone (Verma and finite-dimensional weight modules belong to O).