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.
Finite-dimensional tensoring preserves O
Statement
Fix a finite-dimensional complex semisimple Lie algebra , a Cartan subalgebra , and a positive Borel . Write , when , and .
If is a finite-dimensional -semisimple -module, the functor with diagonal action is exact and maps into itself.
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 . 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. (The support description of category O with finite generation)
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
Choose a basis of and finitely many weight generators of . Let be the -submodule generated by all . It contains for every . Induct on the length of a word in Lie algebra elements. If is already in for every , then lies in . Since such words span , , proving finite generation. Empty bases or generators give the zero tensor product.
The tensor weight decomposition is , a finite sum over weights of . Its support is a finite union of translates by those weights of the finitely many support cones for . The support criterion gives .
Tensoring a vector-space exact sequence with gives a direct sum of copies of that exact sequence after choosing a basis. The resulting maps commute with the diagonal -action, so this is exact in . The assertion includes and one-dimensional .
Depends on
Used by
Nothing in the library uses this result yet.
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
- §2 Lemma 2.5, p.3 (standard reference, not scraped)