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.
Chevalley basis and real structure constants
Statement
Assume the Axiom of Choice. Let be a finite-dimensional complex semisimple Lie algebra, let be a Cartan subalgebra with root system (Root and root space) and let be the Killing form (Killing form). For a root let be its Killing-dual vector (Killing-dual vector of a root) and its coroot, so that (Coroot of a Lie-algebra root), and let be the inner product on of The roots form a reduced crystallographic Euclidean root system. Finally let nonzero vectors be given for all . Then there are nonzero complex numbers such that the rescaled vectors have the following properties, where is defined by when , and when ; the pair , for which is not a multiple of a root vector, is excluded from these definitions:
(i) for every ; (ii) for all with ; (iii) if and with is the -string through , then ; in particular every structure constant is an integer.
Moreover the real span is a real Lie subalgebra of regarded as a real Lie algebra, with ; with respect to the basis determined by a base of , all structure constants of are integers, and is a split real form of (Real form of a complex Lie algebra, Split real form). Finally, if and for all , then and for every , and the constants , defined by for and for , are real and satisfy whenever .
Facts & Assumptions
Given: The Axiom of Choice; a finite-dimensional complex semisimple Lie algebra with Cartan subalgebra , root system and Killing form ; the coroots and the inner product on ; and nonzero vectors for .
The Axiom of Choice is assumed (The Axiom of Choice); it enters only through the Serre presentation theorem [L8] and the Euclidean root-system structure [L5], whose statements carry the assumption.
with for every root, and , where and for (Root-space decomposition, Root spaces of a complex semisimple Lie algebra are one-dimensional, Brackets of root spaces, Root and root space).
is bilinear, symmetric and invariant, ; whenever ; is nondegenerate; and the pairing , , is nondegenerate (Killing form, Trace forms are symmetric and invariant, Orthogonality of root spaces and nondegeneracy on the Cartan subalgebra, Opposite root spaces pair nondegenerately).
satisfies for all , and , so that is defined and (Killing-dual vector of a root, Coroot of a Lie-algebra root, The Killing length of a root is nonzero).
If and , then is an interval of consecutive integers with , and (The root-string property, Cartan integers are integers).
is a reduced crystallographic Euclidean root system for the inner product , in which for all roots and the abstract reflection of Reduced crystallographic Euclidean root system agrees with ; is a real form of with ; for a base of a positive system the coroots form a basis of ; under the isomorphism , , the abstract coroot of Coroot and dual root system maps to , and (The roots form a reduced crystallographic Euclidean root system, Positive systems and simple roots, Simple roots form a signed integral basis, Root, coroot, weight, and coweight lattices).
For vectors in a real inner product space, with equality if and only if are linearly dependent (Cauchy–Schwarz: , with equality exactly for linearly dependent vectors).
If satisfy , and as in The special linear Lie algebra sl_2, then every finite-dimensional module is a direct sum of irreducible submodules, and every irreducible nonzero module has an integer with weights of , each on a one-dimensional space (Finite-dimensional representations of sl_2).
For a base of and root triples with , the elements generate and satisfy the relations of the Serre Lie algebra of the Cartan matrix of Cartan matrix of a based root system, so that the assignment of generators defines an isomorphism ; the Axiom of Choice is assumed here (Serre presentation theorem, Serre Lie algebra of a finite-type Cartan matrix, The Axiom of Choice).
Proof
Let , and . By [L1] , and because ; invariance [L2] therefore gives by [L3]. As was arbitrary, is -orthogonal to , hence zero by the nondegeneracy of ; that is, .
(Cartan integers) Let be nonproportional and put and ; both are integers by [L4] and [L5]. Then is an integer, while Cauchy-Schwarz [L6] and nonproportionality give , so . Consequently if and only if ; whenever ; and .
By step 1.1 and [L3], holds for , exactly when , where ; moreover for all nonzero , because the pairing of [L2] is nondegenerate and both and are one-dimensional by [L1], so that the nonzero functional on the line vanishes only at .
(Strings and their bounds) Let with , let be the -string through (so because the index lies in the string) and let be the -string through (so ), as supplied by [L4]; then and by [L4]. The pair is nonproportional, since would force and hence by the reducedness recorded in [L5], contradicting and ; its Cartan integer is , so step 1.2 gives . The same argument with and interchanged gives .
(First normalization) Choose one representative in each pair and put for the chosen representatives while for their negatives, a nonzero number by step 2.1; then satisfies for every root by step 1.1, so (i) of the statement holds for a rescaling of the given basis.
(String-length identity) With the notation of step 2.2, . Indeed , and by step 2.2, so is one of , , , , , ; writing , and and using with , the six cases are as follows. If is or , then , so and both sides of the identity equal . If , then , so and the identity becomes , that is , which holds because the Cartan integer lies in by [L5] and in the open interval , hence equals . If , then , so and the identity becomes , that is ; here satisfies by step 1.2 and also by step 2.2, so and . If , then while gives , so of step 1.2 forces , hence and , and the identity becomes . If , then and again with , so , hence and , and the identity becomes .
(The string module is irreducible) Keep the notation of step 2.2 and put . By [L1] the brackets with and shift the index by and vanish past the ends of the string, while preserves each weight space , on which it acts by the scalar ; hence is a finite-dimensional module for the triple of [L7]. Its weights are for , that is the arithmetic progression , each occurring on a one-dimensional space by [L1]. A decomposition of into irreducibles [L7] has distinct highest weights, because every weight space is one-dimensional, and the top weight occurs exactly once; the irreducible summand of highest weight has all the weights with multiplicity one, so it exhausts the weight multiset of , and itself is irreducible of highest weight .
Any further rescaling with nonzero satisfies by step 3.1, so it preserves the relations (i) exactly when for all .
(Base and generators) Let be the base of a positive system of ; such a base exists because regular vectors exist (Positive systems and simple roots) and it is a basis of by [L5]. Put and for the vectors of step 3.1. Then , while and by [L1] and of [L3]; thus is a root triple with the coroot of .
(Coefficients along the string) Let . By step 3.3 the vector is a highest weight vector: by [L1] and the maximality of . Since the weight spaces of are one-dimensional, for each there are nonzero with , where , and . Induction on , using , and with , gives ; hence for we get , that is .
(Chevalley involution) The assignment , , preserves the relations of the Serre algebra of [L8]: it fixes the relations up to sign, interchanges the relations and , preserves in the form , and sends the Serre relations and into each other, because and both vanish. By the universal property of the presented algebra (Lie algebra presented by generators and relations), this relation-preserving assignment extends to a Lie algebra homomorphism ; it is bijective because fixes the generators of and hence equals , so is an automorphism. Transported through the isomorphism of [L8], it defines an automorphism of with , , and .
(The opposite string) Applying steps 3.3 and 4.3 to the pair in place of — the -string through is , because — produces a highest weight vector and nonzero with and ; here the bracket with lowers the -power without an extra coefficient, so for .
Since for all and the form a basis of by [L5], acts as on . If and , then , so ; as is bijective, for every root . In particular each is a nonzero element of the line , say with , and applying twice gives .
(Pairing of the two strings) By the invariance of , for all [L2]. Applying this times and using unless [L2] together with the weights of and gives , and because at . Also for every root : by step 1.1 the bracket equals both and, by (i), the coroot of [L3]. Comparing the two expressions for therefore gives , that is .
(Second normalization) By step 4.1 the rescalings with are exactly those preserving (i). Choose with for the numbers of step 6.1 and put , so that . For we then have by step 4.1, and , because gives and because .
(Chevalley's identity) Dividing the relation of step 6.2 for the indices and , the unknown cancels and the sign flips, so ; multiplying by the coefficient formulas of steps 4.3 and 5.2 gives , the last equality by the string-length identity 3.2 applied to the pair , whose string is for ; in particular, at , .
(Sign relation) Let with . Applying to and using for all gives , that is ; when both brackets and vanish by [L1], so . Hence for all with , which is (ii) of the statement, the excluded case being the one in which the constants are not defined.
(Integrality) The product is unchanged by the rescaling of step 7.1: that rescaling replaces by and by , because , so the product is multiplied by . Hence step 7.2 gives also for the vectors of step 7.1, and combining this with of step 8.1 gives , so for all with ; this is (iii) of the statement, and together with the convention otherwise it shows that all constants are integers. Moreover each is a nonzero complex multiple of the given vector , so the family produced is obtained from the given root-vector basis by rescaling, as required.
(Real form and integral structure) Let . It is closed under brackets: ; with by [L4]; with by step 9.1; ; and all brackets with vanish by [L1]. Since by [L5] and the vectors form a basis of , we get , so that is a real form of . With respect to the basis the structure constants are integers, because by the coroot-lattice statement of [L5]; and for the operators are diagonalizable over with eigenvalues by [L1] and [L5]. Hence is a split real form of .
(Dual normalization) Put , a positive real number, and for all ; then also , because . By step 3.1 and (i), and . Hence for the constants defined by are , real numbers because and are real; and because and .
Depends on
- Root and root space
- Root-space decomposition
- Root spaces of a complex semisimple Lie algebra are one-dimensional
- Brackets of root spaces
- Killing form
- Trace forms are symmetric and invariant
- Orthogonality of root spaces and nondegeneracy on the Cartan subalgebra
- Opposite root spaces pair nondegenerately
- Killing-dual vector of a root
- Coroot of a Lie-algebra root
- The Killing length of a root is nonzero
- The root-string property
- Cartan integers are integers
- The roots form a reduced crystallographic Euclidean root system
- Reduced crystallographic Euclidean root system
- Cauchy–Schwarz: $|\langle u,v\rangle|\leq\lVert u\rVert\lVert v\rVert$, with equality exactly for linearly dependent vectors
- Finite-dimensional representations of sl_2
- The special linear Lie algebra sl_2
- Serre presentation theorem
- Serre Lie algebra of a finite-type Cartan matrix
- Lie algebra presented by generators and relations
- Cartan matrix of a based root system
- Positive systems and simple roots
- Simple roots form a signed integral basis
- Coroot and dual root system
- Root, coroot, weight, and coweight lattices
- Real form of a complex Lie algebra
- Split real form
- The Axiom of Choice
Used by
Dependency tree · two levels
72 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
- Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)
- Pavel Etingof, Lie Groups and Lie Algebras, Lectures 39-40 (standard reference, not scraped)