Hom to costandards counts Verma-flag factors

Given: The Axiom of Choice, a Verma-filtered object $X$, and a weight $\nu$.

A Verma flag of length $n$ has a top step $0\to K\to X\to \mathrm{\Delta }(\mu )\to 0$ in which $K$ is Verma-filtered of length $n-1$, and the multiplicities are additive along the step: $(X:\mathrm{\Delta }(\nu ))=(K:\mathrm{\Delta }(\nu ))+{\delta }_{\mu \nu }$; the zero object has the empty flag and all multiplicities zero (Finite Verma flags and their multiplicities).

For all weights $\mu ,\nu$ one has $\dim {\mathrm{Hom}}_{\mathcal{O}}(\mathrm{\Delta }(\mu ),\mathrm{\nabla }(\nu ))={\delta }_{\mu \nu }$ and ${\mathrm{Ext}}_{\mathcal{O}}^1(\mathrm{\Delta }(\mu ),\mathrm{\nabla }(\nu ))=0$; and ${\mathrm{Hom}}_{\mathcal{O}}(0,-)=0={\mathrm{Ext}}_{\mathcal{O}}^1(0,-)$ (Standard-costandard Hom and Ext-one orthogonality).

Category $\mathcal{O}$ is abelian and has enough projectives (Category O is abelian and extension closed among weight modules, Category O has enough projectives). The exact contravariant equivalence $D$ exchanges projectives and injectives: $\mathrm{Hom}(-,D(P))\cong \mathrm{Hom}(P,D(-))$ is exact for projective $P$. Dualizing a projective epimorphism $P\twoheadrightarrow D(Y)$ therefore embeds $Y$ into the injective $D(P)$, proving enough injectives (Restricted duality is exact and involutive on O). Finitely generated $U(\mathfrak{g})$-modules have a set of representatives, since they are quotients of $U(\mathfrak{g}{)}^n$ for finite $n$. Work on a set-sized skeleton of $\mathcal{O}$; under AC choose a projective epimorphism onto and an injective embedding of each object, then recursively cover kernels and embed cokernels to supply resolutions. AC implies DC by selecting successors in any serial relation. Fix these resolution systems and use the canonical comparison identifications of The balanced Ext bifunctor. For a short exact sequence $0\to M^{\mathrm{\prime }}\to M\to M^{\mathrm{\prime }\mathrm{\prime }}\to 0$ in $\mathcal{O}$ and every $N$ there is a natural exact sequence $0\to \mathrm{Hom}(M^{\mathrm{\prime }\mathrm{\prime }},N)\to \mathrm{Hom}(M,N)\to \mathrm{Hom}(M^{\mathrm{\prime }},N)\to {\mathrm{Ext}}^1(M^{\mathrm{\prime }\mathrm{\prime }},N)\to {\mathrm{Ext}}^1(M,N)\to {\mathrm{Ext}}^1(M^{\mathrm{\prime }},N)$ (The long exact Ext sequence in the first variable).