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 full algebraic Verma dual is too large
Statement refuted
Fix a finite-dimensional complex semisimple Lie algebra , a Cartan subalgebra , and a positive Borel . Write , when , and .
False claim: replacing the restricted sum in Chevalley duality by the full algebraic dual always gives an object of .
For and any , the full Chevalley-twisted dual is not -semisimple and hence is not in .
Facts & Assumptions
Given: The setting above and the hypotheses in the statement refuted.
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)
For , the Verma module is the induced -module where is the quotient algebra of def-universal-enveloping-algebra-as-a-tensor-quotient and is def-one-dimensional-borel-module-of-weight-lambda. Write . Thus is the quotient of by the left ideal generated by for and for ; in particular, and . (Verma modules)
The weights of are exactly for ; every weight space is finite dimensional, and . (Weights of a Verma module lie below lambda)
Counterexample
The induced Verma model has basis for and . Define for all and extend linearly. This is an algebraic functional because vectors of are finite sums, although its nonzero weight coordinates are infinite. On the full twisted dual use the same formula as for restricted duality.
For every polynomial , . The values are pairwise distinct over , so a polynomial annihilating has infinitely many distinct zeros and must be the zero polynomial. Thus the -orbit of is infinite dimensional. A vector in a direct sum of eigenspaces has only finitely many eigencomponents and is annihilated by the product of their linear eigenvalue polynomials. Therefore this full dual cannot be a weight module.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
7 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 Lemma 3.2 and Construction 3.7, p.4 (standard reference, not scraped)