Finite length of modules in category O (source code)

= Finite length of modules in category O

Every object $M$ of <Category O> has a finite <composition series of a module>. Choose weight-vector generators and let $T$ be the sum of their finite-dimensional weight spaces. The centre preserves $T$; the kernel of its action on $T$ has finite codimension and, by centrality, annihilates all generators and hence all of $M$. Thus only finitely many <central characters> can appear in subquotients. The <Harish-Chandra isomorphism> makes each such character correspond to one finite Weyl orbit of shifted highest weights. Let $S$ be the resulting finite set of possible highest weights.

Every nonzero subquotient has a highest-weight vector from its bounded-above support, and a common central eigenvector can be chosen in the finite-dimensional highest-weight space. Its weight belongs to $S$. The integer $d(N)=\sum_{\nu\in S}\dim N_\nu$ is therefore finite, additive on short exact sequences and positive for every nonzero subquotient $N$. Each strict refinement of a submodule chain consumes at least one unit of $d(M)$, bounding its length and proving the claim.