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 weight-space detection of subquotients
Statement
Fix a finite-dimensional complex semisimple Lie algebra , a Cartan subalgebra , and a positive Borel . Write , when , and .
Suppose . Every nonzero subquotient of has for some . In particular the number of strict inclusions in any finite chain of submodules of is at most
where distinct weights in the orbit are counted once.
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 category is closed under submodules, quotients and finite direct sums and is an abelian category. If is exact, , and is -semisimple, then . The middle-term weight hypothesis is essential. (Category O is abelian and extension closed among weight modules)
Fix a finite-dimensional complex semisimple Lie algebra , a Cartan subalgebra , and a positive Borel . Write , when , and . Every nonzero contains a nonzero weight vector killed by . (A nonzero O-object has a highest-weight vector)
Let and be the central characters obtained from highest weights and . Then where . (Central characters are dot-Weyl orbits)
Every central element acts on a cyclic highest-weight module by a scalar. In particular, each cyclic highest-weight module has a well-defined central character in the sense of def-central-character-of-a-lie-algebra-module. (Central elements act by scalars on cyclic highest-weight modules)
Fix a finite-dimensional complex semisimple Lie algebra , a Cartan subalgebra , and a positive Borel . Write , when , and . Every decomposes canonically into finitely many nonzero generalized central-character submodules: For each summand there is a single such that . The decomposition of zero is empty. (Generalized central-character summands)
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 a cyclic highest-weight module have highest vector of weight . Then every acts by the scalar . (The Harish-Chandra projection computes the highest-weight scalar)
Proof
By closure, a nonzero subquotient is in . Choose a nonzero highest-weight vector . A common power of kills and hence . On the cyclic highest-weight module , F4 gives scalar central action and F7 identifies its scalar as . Thus forces for each .
The exact central-character criterion now gives . The Weyl group is finite, and all weight spaces of an object are finite dimensional, so the displayed detector is finite. For a short exact sequence of weight modules, taking any fixed weight is exact (decompose a lift into weight components). Thus is additive on subquotients of .
Every nonzero factor of a strict chain has detector at least one by the first two steps. Additivity bounds the number of strict inclusions by , whether the chain is written ascending or descending. If the detector is zero there is no nonzero subquotient; in particular , with no strict inclusions.
Depends on
- Category O is abelian and extension closed among weight modules
- A nonzero O-object has a highest-weight vector
- Central characters are dot-Weyl orbits
- Central elements act by scalars on cyclic highest-weight modules
- Generalized central-character summands
- The support description of category O with finite generation
- The Harish-Chandra projection computes the highest-weight scalar
Used by
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
- Etingof, §15.1 Lemma 15.9, p.81: finite weight-space detector method (standard reference, not scraped)
- Chen, Lecture 6 §2 Corollary 2.3 and Theorem 2.4 proof, pp.5–6: finite Weyl-orbit labels (standard reference, not scraped)