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.
Finite Weyl positive roots and simple reflections
Statement
For the preceding finite reduced crystallographic root system, regular vectors exist, is finite, and the simple positive roots are a basis of . Every root has integral coordinates in this basis of one sign. Each permutes and sends to . The simple reflections generate , and every root is the image of a simple root under their group. The simple coroots similarly form an integral basis of the coroot group, and is the lattice generated by their dual basis; preserves . All assertions are choice-free, including rank zero.
Facts & Assumptions
Given: The finite Euclidean root system and its conventions.
All root, reflection, positivity and lattice definitions are those of Finite Weyl root system, lattice and chamber conventions.
Proof
Choose any finite basis of . For each nonzero root , the polynomial is nonzero, since nondegeneracy and spanning prevent all its coefficients vanishing. A nonzero degree- real polynomial has at most roots: division by at a zero and induction prove this assertion. Finitely many such polynomials therefore have only finitely many forbidden real values. Choose one other value and take . In rank zero take . Also acts on the finite spanning set and an operator fixing every root is the identity; this injects into a finite permutation group. Hence is finite.
If independent roots have , the positive integers and obey , by the strict Cauchy–Schwarz inequality. The latter follows directly by minimizing over real . Thus at least one of equals one. The corresponding root reflection produces , proving it is a root. If distinct simple positive roots had positive inner product, apply this result to one and the negative of the other. Their difference would be a root; whichever sign it has expresses one of the simple roots as a sum of two positive roots, a contradiction. Distinct simple roots therefore have nonpositive inner products.
Every positive root is a sum of simple roots with nonnegative integer coefficients. If not simple, split it into two positive roots. Both have smaller -value, and induction on the position in the finite ordered list of positive -values terminates the splitting. Thus the simple roots span . They are independent: in a nontrivial real relation separate the positive and negative coefficients to obtain with disjoint index sets and strictly positive coefficients. Neither side can be empty, since pairing with would then give a contradiction; it also shows . Step 1.2 gives , contradicting positive definiteness. Hence they are a basis. Negating gives the negative-root coordinates as well.
For , its simple expansion has a positive coefficient at some index other than : otherwise reducedness would make . Reflection changes only the coefficient at . Its image is a root and still has that other positive coefficient, so step 2.1 makes every coefficient nonnegative. Thus is positive. The involution then permutes all these positive roots and reverses .
The coroot set is a finite reduced crystallographic root system: , its double dual is , and its two integer pairings interchange those of . Its positive roots are positive scalar multiples of the positive roots of , and every positive coroot has nonnegative real coordinates in the basis . Apply step 2.1's simple-basis conclusion to this dual system. The cone spanned by its positive roots is exactly the cone generated by the , since those coroots themselves belong to it. The extreme rays of a cone spanned by a basis are exactly its basis rays: a vector with two positive coordinates splits into two nonproportional cone vectors, whereas a single-coordinate vector cannot. The dual simple roots must therefore lie on exactly these rays. Reducedness gives that they are precisely the . Their integer positive expansions give .
Suppose a positive root is not simple. Since , some . Its positive integral coroot pairing means with an integer . By step 3.1 this root stays positive and has smaller integer height . Repeating finitely many times reaches a simple root. Therefore every positive root is in the group orbit of a simple root; a negative root is obtained by first negating that simple root with its reflection. For any orthogonal , direct substitution gives . Consequently every root reflection lies in the group generated by the , proving that this group is .
Let be the basis dual to under the nondegenerate form. Step 3.2 implies . Reflection invariance of the root and coroot sets gives invariance of . If and , then ; hence preserves . Every basis and root list used was finite. In rank zero all lists are empty, their groups are zero and is trivial, so the same conclusions hold.
Depends on
Used by
- Bruhat order on a finite Weyl group Definition
- Weyl discriminant and reflecting hyperplane arrangement Definition
- Weyl orbit sum in a group algebra Definition
- Finite semisimple Cartan, root and string structure Lemma
- Finite Weyl closed chambers and stabilizers Lemma
- Finite Weyl strong exchange and deletion Lemma
- The affine simple root alpha zero is delta minus the highest root Lemma
- Weyl orbit sums form a basis of finite Weyl invariants Lemma
- Affine denominator separates real and imaginary root factors Proposition
- Affine Weyl group is a coroot lattice semidirect product Proposition
Dependency tree · one level
1 result within one dependency step 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, Lie Groups and Lie Algebras, §§21–22; local sign-change proofs fill the chamber argument (standard reference, not scraped)