LemmaStatement: Literature-sourcedProof: 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.

Noetherianity of the enveloping algebra

Statement

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.

Facts & Assumptions

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

[F1]

Let $x_{1}, \dots, x_{r}$ be an ordered basis of a finite-dimensional complex Lie algebra $g$ . Then the monomials $x_{1}^{a_{1}} x_{2}^{a_{2}} \dots x_{r}^{a_{r}} (a_{i} \in N_{0})$ form a basis of $U (g)$ . In particular, multiplication identifies $gr U (g)$ with the symmetric algebra $S (g)$ on the symbols of the $x_{i}$ . (PBW gives an ordered monomial basis for the enveloping algebra)

[F2]

Let $R$ be a Noetherian commutative ring. Then the polynomial ring $R [x]$ is a Noetherian commutative ring. No hypothesis beyond Noetherianity is placed on $R$ : it may have zero divisors, and it may be the zero ring. (Hilbert basis theorem: if $R$ is Noetherian then $R [x]$ is Noetherian)

Proof

1.1

Put $A = U (g)$ with its nonnegative PBW filtration. Then $gr A ≅ C [X_{1}, \dots, X_{d}]$ . A field is Noetherian since its only ideals are $0$ and itself; iterating the Hilbert basis theorem makes this polynomial ring Noetherian, also when $d = 0$ .

F1F2

2.1

For a left ideal $I$ , $gr I$ is a homogeneous ideal of $gr A$ . Choose finite homogeneous generators $σ (a_{j})$ and lift them to $a_{j} \in I$ of the same degrees. Homogeneous generators may be chosen by replacing generators of a homogeneous ideal by their homogeneous components. For $I = 0$ use the empty list.

constructstep 1.1

3.1

If $a \in I$ has degree $n$ , write its symbol as $\sum_{j} b_{j} σ (a_{j})$ with homogeneous $b_{j}$ of degree $n - \deg a_{j}$ , omitting negative degrees. Lift $b_{j}$ to $c_{j} \in A$ . Then $a - \sum_{j} c_{j} a_{j}$ has degree less than $n$ . Repetition terminates below degree zero, proving $I = \sum_{j} A a_{j}$ . This includes degree-zero elements.

algebrastep 2.1

4.1

For a right ideal use $gr I = \sum_{j} σ (a_{j}) b_{j}$ and subtract $\sum_{j} a_{j} c_{j}$ instead. Thus every left and every right ideal is finitely generated. An ascending chain stabilizes because its union is an ideal and its finitely many generators already belong to one member.

algebrastep 3.1∎

Depends on

Used by

Category O is abelian and extension closed among weight modules Theorem

Dependency tree · two levels

8 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

§15.1 p.79, Noetherian parenthesis (standard reference, not scraped)