Type of a module with a Verma filtration

Assume the Axiom of Choice (The Axiom of Choice). Let $M$ be an object of the category $\mathcal{O}$ of The classical BGG category O. A Verma filtration of $M$ is a finite increasing filtration by $\mathfrak{g}$-submodules

$0=M_0\subseteq M_1\subseteq \cdots \subseteq M_n=M$

such that for every $j$ there is a weight ${\psi }_j$ with $M_j\mathrm{/}{M}_{j-1}\cong M({\psi }_j)$, the Verma module of Verma modules. When such a filtration exists, $M$ is called Verma-filtered and one writes

$\mathrm{Typ}M=\{{\psi }_1,\dots ,{\psi }_n\},$

a finite multiset of weights, its type. The multiset is independent of the chosen filtration: passing to classes in the Grothendieck group of The Grothendieck group and character of O gives $[M]={\sum }_j[M({\psi }_j)]$, and by Simple and standard bases of K0(O) the classes of the Verma modules involved have pairwise distinct characters and are linearly independent in the relevant block, so the multiset of weights is recovered from $[M]$. Consequently $\mathrm{Typ}$ is well defined. The standard example is a finite direct sum $M={⨁}_{r=1}^{n}M({\psi }_r)$, which is Verma-filtered with type $\{{\psi }_1,\dots ,{\psi }_n\}$ by taking the partial sums of the summands. Verma-filteredness is also preserved by tensoring with a finite-dimensional $\mathfrak{g}$-module: Finite-dimensional tensoring preserves O keeps the module in $\mathcal{O}$, and the type of the tensor product is computed by the page's tensoring lemma. In particular the type of a Verma filtration is a coarser invariant than a composition series (Composition series and composition factors of an object): it records the successive Verma quotients, not the simple factors.