TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Category O is abelian and extension closed among weight modules

Statement

The category $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 O$ , and $E$ is $h$ -semisimple, then $E \in O$ . The middle-term weight hypothesis is essential.

Facts & Assumptions

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

[F1]

Fix a finite-dimensional complex semisimple Lie algebra $g$ , a Cartan subalgebra $h$ , and a positive Borel $b = h \oplus n^{+}$ . Write $Q^{+} = \sum_{i} Z_{\geq 0} α_{i}$ , $μ \leq λ$ when $λ - μ \in Q^{+}$ , and $w \cdot λ = w (λ + ρ) - ρ$ . The BGG category $O$ is the full subcategory of left $U (g)$ -modules $M$ satisfying all three conditions: $M$ is finitely generated; $M = ⨁_{μ \in h^{*}} M_{μ}$ where $M_{μ} = {v : h v = μ (h) v for all h \in h}$ ; and $U (n^{+}) v$ is finite dimensional for each $v \in M$ . Its morphisms are all $g$ -linear maps. The zero module is included, generated by the empty set. The enveloping and triangular conventions are those of thm-pbw-ordered-monomial-basis-for-the-enveloping-algebra and thm-triangular-decomposition-from-a-chosen-positive-root-system. (The classical BGG category O)

[F2]

Fix a finite-dimensional complex semisimple Lie algebra $g$ , a Cartan subalgebra $h$ , and a positive Borel $b = h \oplus n^{+}$ . Write $Q^{+} = \sum_{i} Z_{\geq 0} α_{i}$ , $μ \leq λ$ when $λ - μ \in Q^{+}$ , and $w \cdot λ = w (λ + ρ) - ρ$ . Let $M$ be a finitely generated $h$ -semisimple $g$ -module. Then $M \in O$ if and only if $supp M \subset ⋃_{i = 1}^{r} (λ_{i} - Q^{+})$ for some finite list of weights. In either case every $M_{μ}$ is finite dimensional. The list may be empty for $M = 0$ ; finite generation is an independent hypothesis. (The support description of category O with finite generation)

[F3]

Fix a finite-dimensional complex semisimple Lie algebra $g$ , a Cartan subalgebra $h$ , and a positive Borel $b = h \oplus n^{+}$ . Write $Q^{+} = \sum_{i} Z_{\geq 0} α_{i}$ , $μ \leq λ$ when $λ - μ \in Q^{+}$ , and $w \cdot λ = w (λ + ρ) - ρ$ . For every finite-dimensional complex Lie algebra $g$ (semisimplicity is unnecessary here), $U (g)$ is left and right Noetherian. (Noetherianity of the enveloping algebra)

[F4]

For every ring $R$ , the category $R - M o d$ of left $R$ -modules is an abelian category. (Modules over a ring form an abelian category)

[F5]

For any ordered basis of a finite-dimensional complex Lie algebra, the corresponding ordered monomials form a basis of its enveloping algebra. (PBW gives an ordered monomial basis for the enveloping algebra)

[F6]

For $λ \in h^{*}$ , the Verma module is $M (λ) = U (g) \otimes_{U (b)} C_{λ}$ . (Verma modules)

Proof

1.1

Write $R = U (g)$ . Every submodule of $R^{r}$ is finitely generated: for $r = 1$ this is left Noetherianity; for $r > 1$ project to the last coordinate, lift finite generators of the image ideal, and adjoin generators of the kernel, a submodule of $R^{r - 1}$ . The case $r = 0$ is zero. Taking inverse images under $R^{r} ↠ M$ proves that every submodule of a finitely generated module is finitely generated.

F3algebra

2.1

A submodule of a weight module is a sum of weight spaces: for the finitely many components of a vector choose $h \in h$ separating their distinct weights and apply the interpolation polynomials in $h$ . Quotients therefore inherit weight decompositions, and exact sequences of weight modules are exact at each weight. Submodules and quotients inherit local $n^{+}$ -finiteness, and quotients inherit finite generation. Finite direct sums inherit all three axioms, including the empty sum.

F1algebrastep 1.1

3.1

Kernels and cokernels of $O$ -maps are thus the ambient module kernels and cokernels. The full subcategory contains zero and finite biproducts; the ambient image-coimage isomorphism remains inside it. The module-category abelian axioms therefore hold in $O$ .

F4step 2.1

4.1

For the asserted extension, choose generators of $A$ and lifts of finitely many generators of $B$ . They generate $E$ , since subtracting their $R$ -linear combinations leaves an element of $A$ . Weightwise exactness gives $supp E = supp A \cup supp B$ . Each is in finitely many downward cones; the assumed weight decomposition and finite generation of $E$ allow F2 to be applied. Thus $E \in O$ , also when either end is zero.

F2algebrastep 3.1

5.1

The weight hypothesis cannot be omitted. For $g = {s l}_{2}$ , let $V = C v \oplus C w$ be a $b$ -module with $e v = e w = 0$ , $h v = λ v$ , and $h w = λ w + v$ . Then $0 \to C_{λ} \to V \to C_{λ} \to 0$ is exact. Ordering a PBW basis with $f$ before a basis of $b$ shows that $U (g)$ is free as a right $U (b)$ -module, so induction is exact and gives $0 \to M (λ) \to E \to M (λ) \to 0$ for $E = U (g) \otimes_{U (b)} V$ . Each end lies in $O$ : its PBW basis $f^{k} v_{λ}$ consists of weight vectors, it is cyclic, and $e$ acts locally nilpotently. But PBW also gives $1 \otimes v \neq 0$ in $E$ , while $(h - λ) (1 \otimes w) = 1 \otimes v$ and $(h - λ)^{2} (1 \otimes w) = 0$ . Thus $h$ is not semisimple on $E$ , so $E \notin O$ .

F1F5F6algebra∎

Depends on

Used by

The Grothendieck group and character of O Definition
Finite filtrations by highest-weight quotients Lemma
Finite weight-space detection of subquotients Lemma
Generalized central-character summands Lemma
Splitting finite-length modules across separated simple classes Lemma
Verma self-extensions in O split Lemma
Restricted duality is exact and involutive on O Proposition
The simple objects of O Theorem

Dependency tree · two levels

21 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Chen, Lecture 2 §3 Lemma 3.3 and Warning 3.4, p.5 (standard reference, not scraped)
Chen, Lecture 8 §3 Theorem 3.9 proof, p.5: extension closure in the weight-module category (standard reference, not scraped)