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.
Restricted self-duality of simple highest-weight modules
Statement
Fix a finite-dimensional complex semisimple Lie algebra , a Cartan subalgebra , and a positive Borel . Write , when , and .
For every highest weight , as -modules.
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 . For an -semisimple module with finite-dimensional weight spaces, its restricted Chevalley dual is Here each functional is extended by zero on the other weight spaces and is the fixed anti-involution of def-chevalley-contravariant-form. In particular and . A map induces by precomposition. The action law follows from ; a root vector of weight sends to , so the restricted sum is stable. This is a complex-linear algebraic dual, with no conjugation. Ordinary Lie-module duality has a minus sign and reverses weights; twisting that dual by the Lie automorphism gives the convention used here. (Restricted Chevalley dual)
The proper submodule which is the sum of all proper submodules is the unique maximal submodule of . The quotient is simple and is its unique simple quotient. (A Verma module has a unique simple quotient)
The weights of are exactly for ; every weight space is finite dimensional, and . (Weights of a Verma module lie below lambda)
For a -module , sending a homomorphism to is a bijection onto the vectors of weight annihilated by . Here is def-verma-module. The nonzero vectors in this target are precisely the highest-weight vectors of weight from def-highest-weight-vector-and-cyclic-highest-weight-module; the zero vector corresponds to the zero homomorphism. (The universal property of Verma modules)
Proof
The simple Verma quotient has finite-dimensional weight spaces, support in , and a nonzero one-dimensional highest line. These follow from the Verma weight formula and the fact that a proper submodule cannot contain its generating top vector. Therefore has the same weight dimensions, and its top line is killed by .
If were a nonzero proper submodule of , it would be a weight submodule. Finite-dimensionality of each weight space implies that its annihilator is nonzero (some weight component of is proper) and proper (some functional in is nonzero). It is a -submodule, since and is stable. This contradicts simplicity of . Hence is simple without first presuming it is finitely generated.
A nonzero vector of the top line gives a nonzero Verma map by the universal property. It is surjective by simplicity, and the unique simple quotient identifies its target with .
Depends on
Used by
- The regular integral sl2 block Example
- Restricted duality is exact and involutive on O Proposition
Dependency tree · two levels
9 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
- Lecture 8 §3 Proposition 3.10, p.5 (standard reference, not scraped)