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 Euler-character identity for a finite-dimensional simple module
Statement
Assume the Axiom of Choice (The Axiom of Choice). Let . In the Grothendieck group of the linkage block of (The Grothendieck group and character of O, Simple and standard bases of K0(O)) the finite alternating sum of Verma classes equals the class of the simple module:
Equivalently, applying the character homomorphism and the Verma character (The formal character of a Verma module),
the Weyl numerator identity in the form needed by the Weyl character formula. Proof: an exact finite complex has vanishing alternating sum of classes.
Facts & Assumptions
Given: The Axiom of Choice, a dominant integral weight , the BGG resolution of , and the Grothendieck group of the linkage block of with its character homomorphism.
is an exact sequence in , and (The BGG resolution of a finite-dimensional simple module, The Bruhat graph and the BGG Verma sum in degree k).
The Grothendieck group is the abelian group with generators the classes of objects and relations for every short exact sequence ; consequently an exact sequence gives , and . The classes of the simple modules and of the Verma modules each form a basis of (The Grothendieck group and character of O, Simple and standard bases of K0(O)).
The formal character is additive on exact sequences and hence defines a homomorphism from to the group of formal characters; (The formal character of a Verma module, The Grothendieck group and character of O).
All and lie in the linkage block of ; the block decomposition splits into a direct sum of subcategories, and the corresponding projection of Grothendieck groups is additive on classes. Hence an identity between classes of objects of the block that holds in holds in the Grothendieck group of the block (Central-character summands refine into linkage blocks, The Grothendieck group and character of O).
Proof
The resolution of [F1] is a finite exact sequence . By the additivity of [F2] applied successively to its short exact sequences, ; by the direct-sum rule and [F1], . Substituting gives . All the modules involved lie in the linkage block of , so by [F4] this identity holds in the Grothendieck group of that block.
Applying the character homomorphism of [F3] to the identity of step 1.1 and using the Verma character gives , the common factor being independent of .
Steps 1.1 and 2.1 are exactly the two asserted identities: the alternating sum of Verma classes in the Grothendieck group of the linkage block, and the Weyl numerator form of the character identity.
Depends on
- The BGG resolution of a finite-dimensional simple module
- The Grothendieck group and character of O
- Simple and standard bases of K0(O)
- The formal character of a Verma module
- Central-character summands refine into linkage blocks
- The Axiom of Choice
- The Bruhat graph and the BGG Verma sum in degree k
- Finite-dimensional tensoring preserves O
Used by
Dependency tree · two levels
43 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
- Fan Zhou, The classical and the functorial BGG resolutions (Columbia thesis 2021), Part I Sec. 3.3, pp. 11-13 (standard reference, not scraped)
- P. Etingof, Lie Groups and Lie Algebras II (18.755), Sec. 26.1 and Sec. 26.3 (Weyl character formula, Theorem 26.4), pp. 139-142 (standard reference, not scraped)