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 only scalar multiples of a root that are roots are plus or minus the root
Statement
Assume the Axiom of Choice. Let be a Cartan subalgebra of a finite-dimensional complex semisimple Lie algebra and let be roots, where is the root set of Root and root space. Then .
Facts & Assumptions
Given: The Axiom of Choice, such and roots and .
The Axiom of Choice is The Axiom of Choice; it licenses the Killing-dual, coroot, root-triple, and opposite-bracket facts in [L1]--[L4].
For every root , its coroot is with the Killing-dual vector and (Coroot of a Lie-algebra root, Killing-dual vector of a root).
Cartan integers are integral: and for roots (Cartan integers are integers).
For every root there are , , and satisfying the relations (The root sl_2 triple).
Root-space brackets add their weights, and the opposite bracket is the line (Brackets of root spaces, The bracket of opposite root spaces is the root line).
The trace of a commutator of finite-dimensional endomorphisms is zero (For and , ).
Proof
Since by the defining equation , the coroots satisfy .
We first prove that twice a root is never a root. For a root , put . This is a finite direct sum because the root spaces are joint eigenspaces for distinct functionals in the finite-dimensional space . It is stable under the adjoint action of the triple in [L3]: and shift the root-space index by and , respectively, the exceptional opposite bracket lands in by [L4], and preserves every displayed summand.
By [L2] applied to the pair we get , and applied to the pair we get .
On one has , so [L5] makes its trace zero. Its eigenvalues on the displayed direct sum are on , on , and on . Therefore , so . Hence for every . Applying the same argument to the root gives for every ; in particular is not a root.
The two integrality statements say for some integer and , so divides and .
Now and , since and are not roots by step 2.2; and , since then would be twice the root , again contradicting step 2.2. Hence .
Depends on
- Cartan integers are integers
- Coroot of a Lie-algebra root
- Killing-dual vector of a root
- Root and root space
- The root sl_2 triple
- Brackets of root spaces
- The bracket of opposite root spaces is the root line
- For $A\in M_{m\times n}(F)$ and $B\in M_{n\times m}(F)$, $\operatorname{tr}(AB)=\operatorname{tr}(BA)$
- The Axiom of Choice
Used by
- All integer multiples of a root are roots False statement
- If alpha and beta are roots then alpha plus beta is always a root False statement
- The roots form a reduced crystallographic Euclidean root system Proposition
- Roots of a complex semisimple Lie algebra form a reduced crystallographic root system Theorem
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
- Pavel Etingof, MIT 18.745 Lie Groups and Lie Algebras I, Lectures 19–24 (standard reference, not scraped)