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 dominant cyclic generator survives
Statement
Assume the Axiom of Choice. Let be a finite-dimensional complex semisimple Lie algebra with Cartan subalgebra and a chosen positive system, let be dominant integral, and let be the cyclic module with canonical generator of Dominant cyclic highest-weight presentation. Then is a weight vector of weight , and .
Facts & Assumptions
Given: The Axiom of Choice, such , a chosen positive system, a dominant integral with , lowering vectors and the module with generator .
The Axiom of Choice is assumed; it enters through the root-space theory supplying [L1], [L2] and [L4] and through the Serre theorem [L5] (The Axiom of Choice).
The chosen positive system gives the direct sum , and the PBW monomials in an ordered basis of listing a basis of first, then one of , then one of , form a basis of ; in particular as a linear span and is spanned by monomials in a basis of (Triangular decomposition, Poincaré–Birkhoff–Witt theorem).
In the universal enveloping algebra, the product of elements of has the bracket rule ; in particular for the -triple one has , (The root sl_2 triple, Universal enveloping algebra).
The modules are defined by the relations for , for , and (Dominant cyclic highest-weight presentation).
Any module generated by a highest weight vector of weight satisfies and has all weights , and it has as the only vector of weight up to scalars (Highest weight modules lie below the top weight, Root order on weights).
In the Serre presentation, is generated as a Lie algebra by the simple-root vectors , while for and (Serre presentation theorem).
The elements are nonzero, every positive root is a nonzero nonnegative integral combination of the linearly independent simple roots, and each simple root is positive (Simple roots form a signed integral basis, Poincaré–Birkhoff–Witt theorem).
Proof
Let be the left ideal generated by and the elements with , and let with ; then and for , and by [L1] every element of is a linear combination of vectors with , so the linear map , , is onto.
The map is also injective. Let . The linear functional defined by is a Lie-algebra homomorphism to the abelian Lie algebra , because . Its multiplicative extension to the tensor algebra kills every relation , so the quotient definition in [L2] makes it an algebra homomorphism . By the PBW basis of [L1] every has a unique finite expansion , with and ranging over the monomials in a basis of . Define . Then is the identity on and vanishes on : for and , one has and , so for every . Thus , and is a linear isomorphism by step 1.1. In particular , and the action of on corresponds under to left multiplication.
For each set ; this is nonzero by [L6] and step 2.1, and it has weight .
For every the vector satisfies : for one has by the product rule [L2] and , and the -commutation identity gives because ; for one has by [L5], hence and . Thus every simple generator kills . The action is a Lie-algebra homomorphism, so a bracket of operators that each kill also kills ; since the generate by [L5], every element of kills .
By steps 3.1 and 4.1 each is a highest weight vector of weight , so by [L4] its submodule has all weights ; since is a nonzero element of by [L6] and , no weight of equals , and .
Let . A vector of weight in a sum of submodules lies in the sum of their -weight spaces, each of which is zero by step 5.1, so has no weight ; in particular .
The left ideal defining equals , because it is the left ideal generated by the generators of together with the elements ; passing to the quotient by and using the isomorphism of step 2.1 gives .
Therefore , and the canonical generator is nonzero by step 6.1.
Finally has weight , because holds in and passes to the quotient, and for the same reason; hence is a nonzero weight vector of weight killed by .
The class of the unit in is nonzero, has weight , and is killed by , as asserted.
Depends on
- Dominant cyclic highest-weight presentation
- Universal enveloping algebra
- Highest weight modules lie below the top weight
- Root order on weights
- Triangular decomposition
- Poincaré–Birkhoff–Witt theorem
- Serre presentation theorem
- The root sl_2 triple
- Integral, dominant, and strictly dominant weights
- Positive and negative nilpotent subalgebras and the Borel
- Simple roots form a signed integral basis
- The Axiom of Choice
Used by
Dependency tree · two levels
54 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
- Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)
- Alexander Kirillov Jr., An Introduction to Lie Groups and Lie Algebras (standard reference, not scraped)