[proofplan] We first record that $U(\mathfrak g)$ is left Noetherian, using the Poincare-Birkhoff-Witt theorem and the standard filtered-graded Hilbert basis argument. This gives finite generation for submodules of objects of $\mathcal O$. We then check that the weight-space condition, finite-dimensionality of weight spaces, and local $U(\mathfrak n^+)$-finiteness pass to submodules, quotients, kernels, images, cokernels, and finite direct sums. Finally, finite length follows because objects of $\mathcal O$ are Noetherian and, by the classical contragredient duality theorem for BGG category $\mathcal O$, also Artinian. [/proofplan] [step:Prove that $U(\mathfrak g)$ is left Noetherian] Give $U(\mathfrak g)$ its standard increasing PBW filtration $F_0U(\mathfrak g)\subseteq F_1U(\mathfrak g)\subseteq\cdots$, where $F_dU(\mathfrak g)$ is the complex span of products of at most $d$ elements of $\mathfrak g$. By the [citetheorem:8827], the associated graded algebra satisfies \begin{align*} \operatorname{gr}U(\mathfrak g)\cong S(\mathfrak g) \end{align*} as graded complex algebras. Since $\mathfrak g$ is finite-dimensional over $\mathbb C$, the symmetric algebra $S(\mathfrak g)$ is a polynomial algebra in finitely many variables over $\mathbb C$. Hence $S(\mathfrak g)$ is Noetherian by the [Hilbert basis theorem](/theorems/860). We now use the standard filtered-graded Noetherian transfer theorem: if an algebra $A$ has an exhaustive increasing filtration such that $\operatorname{gr}A$ is left Noetherian, then $A$ is left Noetherian. Applying this to $A=U(\mathfrak g)$ proves that $U(\mathfrak g)$ is left Noetherian. Therefore every left $U(\mathfrak g)$-submodule of a finitely generated left $U(\mathfrak g)$-module is finitely generated. [/step] [step:Show that submodules of objects of $\mathcal O$ remain in $\mathcal O$] Let $M\in\mathcal O$, and let $L\subseteq M$ be a left $U(\mathfrak g)$-submodule. Since $U(\mathfrak g)$ is left Noetherian and $M$ is finitely generated, the module $L$ is finitely generated over $U(\mathfrak g)$. We next prove that $L$ is an $\mathfrak h$-weight module. Since $L$ is a $U(\mathfrak g)$-submodule, it is stable under the action of $\mathfrak h$. Let $v\in L$. Because $M$ is a weight module, there are pairwise distinct weights $\lambda_1,\dots,\lambda_r\in\mathfrak h^*$ and vectors $v_i\in M_{\lambda_i}$ such that \begin{align*} v=\sum_{i=1}^r v_i. \end{align*} Fix $i\in\{1,\dots,r\}$. Choose $h_i\in\mathfrak h$ such that the scalars $\lambda_1(h_i),\dots,\lambda_r(h_i)$ separate $\lambda_i(h_i)$ from the other values. This is possible because the complement in $\mathfrak h$ of the finitely many hyperplanes \begin{align*} \{h\in\mathfrak h:\lambda_i(h)=\lambda_j(h)\} \end{align*} for $j\ne i$ is nonempty. Define the polynomial $p_i(T)\in\mathbb C[T]$ by \begin{align*} p_i(T)=\prod_{j\ne i}\frac{T-\lambda_j(h_i)}{\lambda_i(h_i)-\lambda_j(h_i)}. \end{align*} Then $p_i(h_i)$ acts on $v$ as the projection onto the $\lambda_i$-weight component, so \begin{align*} p_i(h_i)\cdot v=v_i. \end{align*} Since $L$ is stable under $h_i$, it is stable under $p_i(h_i)$, and therefore $v_i\in L$. Hence every $v\in L$ is the sum of its weight components inside $L$, and \begin{align*} L=\bigoplus_{\lambda\in\mathfrak h^*}(L\cap M_\lambda). \end{align*} Thus $L$ is an $\mathfrak h$-weight module with weight spaces \begin{align*} L_\lambda=L\cap M_\lambda. \end{align*} Since $L_\lambda\subseteq M_\lambda$ and $M_\lambda$ is finite-dimensional, $L_\lambda$ is finite-dimensional. Finally, let $v\in L$. Since $M$ is locally $U(\mathfrak n^+)$-finite, the complex [vector space](/page/Vector%20Space) $U(\mathfrak n^+)\cdot v$ is finite-dimensional as a subspace of $M$. The same space is also the $U(\mathfrak n^+)$-span of $v$ inside $L$, so $L$ is locally $U(\mathfrak n^+)$-finite. Therefore $L\in\mathcal O$. [guided] The only subtle point is the weight decomposition for the submodule. It is not enough to know that $L$ is stable under $\mathfrak h$; we must prove that if a vector of $L$ decomposes into weight components in $M$, then each component still lies in $L$. Let $v\in L$. Since $M$ is a weight module, $v$ has a finite weight decomposition \begin{align*} v=\sum_{i=1}^r v_i, \end{align*} where $\lambda_1,\dots,\lambda_r\in\mathfrak h^*$ are pairwise distinct and $v_i\in M_{\lambda_i}$. To isolate one component $v_i$, choose $h_i\in\mathfrak h$ such that $\lambda_i(h_i)\ne \lambda_j(h_i)$ for every $j\ne i$. Such an $h_i$ exists because each equality $\lambda_i(h)=\lambda_j(h)$ cuts out a proper hyperplane in $\mathfrak h$, and finitely many proper hyperplanes cannot cover the whole complex vector space $\mathfrak h$. Now define \begin{align*} p_i(T)=\prod_{j\ne i}\frac{T-\lambda_j(h_i)}{\lambda_i(h_i)-\lambda_j(h_i)} \end{align*} as a polynomial in one variable. Since $h_i$ acts on $M_{\lambda_j}$ by the scalar $\lambda_j(h_i)$, the operator $p_i(h_i)$ acts as the identity on $M_{\lambda_i}$ and as zero on every $M_{\lambda_j}$ with $j\ne i$. Therefore \begin{align*} p_i(h_i)\cdot v=v_i. \end{align*} Because $L$ is a $U(\mathfrak g)$-submodule, it is stable under $h_i$ and hence under every polynomial in $h_i$. Thus $v_i\in L$. This proves \begin{align*} L=\bigoplus_{\lambda\in\mathfrak h^*}(L\cap M_\lambda). \end{align*} The other defining properties of $\mathcal O$ are inherited directly. Finite generation follows from the left Noetherian property of $U(\mathfrak g)$, proved in the previous step. Each space $L\cap M_\lambda$ is finite-dimensional because it is a subspace of the finite-dimensional vector space $M_\lambda$. Finally, if $v\in L$, then $U(\mathfrak n^+)\cdot v$ computed in $L$ is the same vector space as $U(\mathfrak n^+)\cdot v$ computed in $M$, and it is finite-dimensional because $M$ is locally $U(\mathfrak n^+)$-finite. Hence $L\in\mathcal O$. [/guided] [/step] [step:Show that quotients of objects of $\mathcal O$ remain in $\mathcal O$] Let $M\in\mathcal O$, let $L\subseteq M$ be a left $U(\mathfrak g)$-submodule, and set \begin{align*} Q:=M/L. \end{align*} Since $M$ is finitely generated over $U(\mathfrak g)$, the quotient $Q$ is finitely generated over $U(\mathfrak g)$. By the previous step, $L$ is a weight submodule, so \begin{align*} L=\bigoplus_{\lambda\in\mathfrak h^*}(L\cap M_\lambda). \end{align*} The quotient $Q$ is therefore a weight module with weight spaces \begin{align*} Q_\lambda=(M_\lambda+L)/L\cong M_\lambda/(L\cap M_\lambda). \end{align*} Each $Q_\lambda$ is finite-dimensional because it is a quotient of the finite-dimensional complex vector space $M_\lambda$. Let $q\in Q$, and choose $m\in M$ whose image in $Q$ is $q$. The quotient map \begin{align*} \pi:M\to Q \end{align*} satisfies \begin{align*} U(\mathfrak n^+)\cdot q=\pi(U(\mathfrak n^+)\cdot m). \end{align*} Since $M$ is locally $U(\mathfrak n^+)$-finite, the vector space $U(\mathfrak n^+)\cdot m$ is finite-dimensional, and its image under $\pi$ is finite-dimensional. Thus $Q$ is locally $U(\mathfrak n^+)$-finite. Therefore $Q\in\mathcal O$. [/step] [step:Deduce that $\mathcal O$ is an abelian subcategory] Let $f:M\to N$ be a morphism in $\mathcal O$. Since $\mathcal O$ is defined as a full subcategory of left $U(\mathfrak g)$-modules, its morphisms are exactly the $U(\mathfrak g)$-module homomorphisms between its objects. The kernel $\ker f$ is a left $U(\mathfrak g)$-submodule of $M$, so $\ker f\in\mathcal O$ by the submodule result. The image $\operatorname{im}f$ is a left $U(\mathfrak g)$-submodule of $N$, so $\operatorname{im}f\in\mathcal O$. The cokernel is the quotient \begin{align*} \operatorname{coker}f=N/\operatorname{im}f, \end{align*} so $\operatorname{coker}f\in\mathcal O$ by the quotient result. Thus kernels, images, and cokernels computed in the ambient category of left $U(\mathfrak g)$-modules remain in $\mathcal O$, and $\mathcal O$ is a full abelian subcategory. [/step] [step:Check closure under finite direct sums] Let $M_1,\dots,M_r$ be objects of $\mathcal O$, and define \begin{align*} M:=\bigoplus_{i=1}^r M_i. \end{align*} A finite union of finite generating sets for the $M_i$ is a finite generating set for $M$, so $M$ is finitely generated over $U(\mathfrak g)$. Its weight spaces are \begin{align*} M_\lambda=\bigoplus_{i=1}^r (M_i)_\lambda. \end{align*} Each $M_\lambda$ is finite-dimensional because it is a finite [direct sum](/page/Direct%20Sum) of finite-dimensional complex vector spaces. If $m=(m_1,\dots,m_r)\in M$, then \begin{align*} U(\mathfrak n^+)\cdot m\subseteq \bigoplus_{i=1}^r U(\mathfrak n^+)\cdot m_i. \end{align*} The right-hand side is finite-dimensional because each $M_i$ is locally $U(\mathfrak n^+)$-finite. Hence $M$ is locally $U(\mathfrak n^+)$-finite, and therefore $M\in\mathcal O$. [/step] [step:Prove that every object of $\mathcal O$ is Noetherian and Artinian] Let $M\in\mathcal O$. Since $M$ is finitely generated over the left Noetherian algebra $U(\mathfrak g)$, the module $M$ is Noetherian. We use the classical contragredient duality theorem for BGG category $\mathcal O$ in the following form. For the fixed triangular decomposition determined by $\mathfrak h$ and $\Phi^+$, choose the standard Chevalley anti-involution $\omega:U(\mathfrak g)\to U(\mathfrak g)$, which fixes $\mathfrak h$ and interchanges the positive and negative root spaces. If $X\in\mathcal O$, the restricted dual \begin{align*} X^\vee:=\bigoplus_{\lambda\in\mathfrak h^*}X_\lambda^* \end{align*} becomes a left $U(\mathfrak g)$-module by \begin{align*} (u\cdot \varphi)(x):=\varphi(\omega(u)\cdot x) \end{align*} for $u\in U(\mathfrak g)$, $\varphi\in X^\vee$, and $x\in X$. The theorem asserts that $X^\vee\in\mathcal O$ and that $X\mapsto X^\vee$ is an exact contravariant equivalence from $\mathcal O$ to itself. Its hypotheses are satisfied here because $\mathfrak g$ is finite-dimensional complex semisimple and the triangular decomposition comes from the Cartan subalgebra $\mathfrak h$ and the positive root system $\Phi^+$. Let \begin{align*} M=N_0\supseteq N_1\supseteq N_2\supseteq\cdots \end{align*} be a descending chain of subobjects in $\mathcal O$. For each $i\geq 0$, define the annihilator subspace \begin{align*} N_i^\perp:=\{\varphi\in M^\vee:\varphi(n)=0\text{ for every }n\in N_i\}. \end{align*} Because $N_i$ is a $U(\mathfrak g)$-submodule and the action on $M^\vee$ is defined through the anti-involution $\omega$, the subspace $N_i^\perp$ is stable under $U(\mathfrak g)$; hence it is a subobject of $M^\vee$. Since $N_{i+1}\subseteq N_i$, every functional vanishing on $N_i$ also vanishes on $N_{i+1}$, so \begin{align*} N_0^\perp\subseteq N_1^\perp\subseteq N_2^\perp\subseteq\cdots \end{align*} is an ascending chain of subobjects of $M^\vee$. Since $M^\vee\in\mathcal O$, it is finitely generated over the left Noetherian algebra $U(\mathfrak g)$, and hence $M^\vee$ is Noetherian. Therefore this ascending chain stabilizes. Exactness and faithfulness of contragredient duality identify $N_i^\perp$ with the image of the dual map \begin{align*} (M/N_i)^\vee\to M^\vee. \end{align*} Thus equality $N_i^\perp=N_{i+1}^\perp$ implies that the dual of the quotient map $M/N_{i+1}\to M/N_i$ is an isomorphism. Since the duality functor is faithful and reflects isomorphisms, the quotient map $M/N_{i+1}\to M/N_i$ is an isomorphism, and therefore $N_i=N_{i+1}$. Hence the original descending chain stabilizes, so $M$ is Artinian. [/step] [step:Conclude finite length] We have proved that every object $M\in\mathcal O$ is Noetherian and Artinian. By the standard Jordan-Hölder finiteness criterion for abelian categories, an object that is both Noetherian and Artinian has finite length: every strictly increasing chain and every strictly decreasing chain of subobjects terminates, so any process of refining a finite filtration by inserting a proper nonzero subobject must stop after finitely many steps. Therefore every object of $\mathcal O$ admits a finite composition series. This proves that every object of $\mathcal O$ has finite length and completes the proof. [/step]