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.
The support description of category O with finite generation
Statement
Fix a finite-dimensional complex semisimple Lie algebra , a Cartan subalgebra , and a positive Borel . Write , when , and .
Let be a finitely generated -semisimple -module. Then if and only if for some finite list of weights. In either case every is finite dimensional. The list may be empty for ; finite generation is an independent hypothesis.
Facts & Assumptions
Given: The setting above and the hypotheses in the statement.
Fix a finite-dimensional complex semisimple Lie algebra , a Cartan subalgebra , and a positive Borel . Write , when , and . The BGG category is the full subcategory of left -modules satisfying all three conditions: is finitely generated; where ; and is finite dimensional for each . Its morphisms are all -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)
Fix a finite-dimensional complex semisimple Lie algebra , a Cartan subalgebra , and a positive Borel . Write , when , and . Every has a finite-dimensional, -stable, -semisimple generating subspace . There is a flag of -submodules whose quotients are one dimensional and annihilated by . For take and the empty flag. (Finite Borel-stable generators and weight flags)
Let be an ordered basis of a finite-dimensional complex Lie algebra . Then the monomials form a basis of . In particular, multiplication identifies with the symmetric algebra on the symbols of the . (PBW gives an ordered monomial basis for the enveloping algebra)
Proof
Assume and choose the finite -stable weight space sum supplied by F2 (a finite-dimensional weight subspace, not necessarily a sum of full weight spaces). Ordering negative-root vectors before a basis of in PBW gives . Its support is contained in the union of over the finitely many weights of .
For a fixed , negative-root PBW monomials of weight have exponent sum bounded by the height of , since every positive root has positive integral height. There are finitely many such monomials. The surjection therefore has finite-dimensional weight spaces in its source, giving .
Conversely assume the finite-cone support condition. For a weight vector , a positive-root PBW monomial of weight can act nontrivially only if for some and . Thus . For each eligible , the height of is bounded by that fixed height. Only finitely many PBW monomials meet these bounds, so is finite dimensional. This does not presume finite-dimensional weight spaces.
Every vector is a finite sum of weight vectors, so the same local finiteness follows for it by summing their finite-dimensional orbit spaces. The two standing hypotheses now give , and the preceding forward proof gives finite weight spaces. Empty support means and all conclusions hold.
Depends on
Used by
- Finite weight spaces alone do not give category O Counterexample
- The Grothendieck group and character of O Definition
- A nonzero O-object has a highest-weight vector Lemma
- Finite weight-space detection of subquotients Lemma
- The center has finite-dimensional image on each O-object Lemma
- Finite-dimensional Hom spaces in O Proposition
- Finite-dimensional tensoring preserves O Proposition
- Verma and finite-dimensional weight modules belong to O Proposition
- Category O is abelian and extension closed among weight modules Theorem
- Every object of O has finite length Theorem
Dependency tree · two levels
11 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 Definition 15.1 and Lemma 15.3, p.79 (standard reference, not scraped)