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.
Dominant weights in fundamental coordinates
Statement
Assume the Axiom of Choice. Let be a finite-dimensional complex semisimple Lie algebra with Cartan subalgebra and a chosen base of simple roots, and let be the fundamental weights (Fundamental weights). For the following are equivalent:
(i) is dominant integral (Integral, dominant, and strictly dominant weights);
(ii) with integers .
Facts & Assumptions
Given: The Axiom of Choice, such and a chosen base of simple roots with fundamental weights .
The Axiom of Choice is assumed; it enters through the root-space theory supplying the real form and the coroot basis of [L1] (The Axiom of Choice).
The simple coroots form a basis of ; the simple roots form a basis of ; and the fundamental weights are the dual basis to the simple coroots, , and form a basis of the weight lattice (The roots form a reduced crystallographic Euclidean root system, Simple roots form a signed integral basis, Fundamental weights, Root, coroot, weight, and coweight lattices).
is integral when for all , dominant integral when all these integers are nonnegative, and every integral functional lies in ; for the expansion in the dual basis is (Integral, dominant, and strictly dominant weights).
Proof
Assume (i): then by [L2] and for every , so the expansion of [L2] exhibits in the form (ii).
Conversely assume (ii), say with ; then by [L1], and by the duality of [L1] we get for each .
By [L2] the pairings of step 1.2 are exactly the values that make dominant integral; hence (ii) implies (i), and steps 1.1 and 2.1 prove the equivalence.
Depends on
Used by
Dependency tree · two levels
27 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
- Alexander Kirillov Jr., An Introduction to Lie Groups and Lie Algebras (standard reference, not scraped)
- Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)