Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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 g be a finite-dimensional complex semisimple Lie algebra, let hg be a Cartan subalgebra with root system Φ=Φ(g,h) (Root and root space) and let B be the Killing form (Killing form). For a root α let Hαh be its Killing-dual vector (Killing-dual vector of a root) and hα=2Hα/α(Hα) its coroot, so that α(hα)=2 (Coroot of a Lie-algebra root), and let (λ,μ):=B(Hλ,Hμ) be the inner product on E=spanRΦ of The roots form a reduced crystallographic Euclidean root system. Finally let nonzero vectors eα0gα be given for all αΦ. Then there are nonzero complex numbers cα such that the rescaled vectors eα:=cαeα0 have the following properties, where NαβC is defined by [eα,eβ]=Nαβeα+β when α+βΦ, and Nαβ:=0 when α+βΦ{0}; the pair β=α, for which [eα,eα]=hα is not a multiple of a root vector, is excluded from these definitions:

(i) [eα,eα]=hα for every αΦ; (ii) Nαβ=Nα,β for all α,βΦ with α+β0; (iii) if α,β,α+βΦ and β+nα with pnq is the α-string through β, then Nαβ=±(p+1); in particular every structure constant Nαβ is an integer.

Moreover the real span g0:=spanR{hα,eα:αΦ} is a real Lie subalgebra of g regarded as a real Lie algebra, with g=g0ig0; with respect to the basis {hα1,,hαr}{eα:αΦ} determined by a base Δ={α1,,αr} of Φ, all structure constants of g0 are integers, and g0 is a split real form of g (Real form of a complex Lie algebra, Split real form). Finally, if λα=((α,α)/2)1/2>0 and Xα:=λαeα for all α, then [Xα,Xα]=Hα and B(Xα,Xα)=1 for every α, and the constants Cαβ, defined by [Xα,Xβ]=CαβXα+β for α+βΦ and Cαβ:=0 for α+βΦ{0}, are real and satisfy Cαβ=Cα,β whenever α+β0.

Facts & Assumptions

Given: The Axiom of Choice; a finite-dimensional complex semisimple Lie algebra g with Cartan subalgebra h, root system Φ=Φ(g,h) and Killing form B; the coroots hα and the inner product (λ,μ)=B(Hλ,Hμ) on E=spanRΦ; and nonzero vectors eα0gα for αΦ.

[A1]

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.

[L1]

g=hαΦgα with dimgα=1 for every root, and [gα,gβ]gα+β, where g0=h and gγ=0 for γΦ{0} (Root-space decomposition, Root spaces of a complex semisimple Lie algebra are one-dimensional, Brackets of root spaces, Root and root space).

[L2]

B is bilinear, symmetric and invariant, B([x,y],z)=B(x,[y,z]); B(gα,gβ)=0 whenever α+β0; Bh is nondegenerate; and the pairing gα×gαC, (x,y)B(x,y), 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).

[L3]

Hαh satisfies B(Hα,H)=α(H) for all Hh, and α(Hα)=B(Hα,Hα)0, so that hα=2Hα/α(Hα) is defined and α(hα)=2 (Killing-dual vector of a root, Coroot of a Lie-algebra root, The Killing length of a root is nonzero).

[L4]

If αΦ and βΦ{0}, then {kZ:gβ+kα0} is an interval of consecutive integers {p,,q} with p,q0, and pq=β(hα)Z (The root-string property, Cartan integers are integers).

[L5]

(E,Φ) is a reduced crystallographic Euclidean root system for the inner product (λ,μ)=B(Hλ,Hμ), in which 2(β,α)/(α,α)=β(hα)Z for all roots and the abstract reflection xx2(x,α)α/(α,α) of Reduced crystallographic Euclidean root system agrees with sα; hR=spanR{hα:αΦ} is a real form of h with h=hRihR; for a base Δ={α1,,αr} of a positive system the coroots hα1,,hαr form a basis of hR; under the isomorphism EhR, λHλ, the abstract coroot α=2α/(α,α) of Coroot and dual root system maps to hα, and αΦZα=i=1rZαi (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).

[L6]

For vectors x,y in a real inner product space, (x,y)xy with equality if and only if x,y are linearly dependent (Cauchy–Schwarz: u,vuv, with equality exactly for linearly dependent vectors).

[L7]

If (e,f,h) satisfy [e,f]=h, [h,e]=2e and [h,f]=2f 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 m0 with weights m,m2,,m of h, each on a one-dimensional space (Finite-dimensional representations of sl_2).

[L8]

For a base Δ={α1,,αr} of Φ and root sl2 triples (ei,fi,hi) with hi=hαi, the elements ei,fi,hi generate g and satisfy the relations of the Serre Lie algebra g(A) of the Cartan matrix aij=αj(hi) of Cartan matrix of a based root system, so that the assignment of generators defines an isomorphism g(A)g; the Axiom of Choice is assumed here (Serre presentation theorem, Serre Lie algebra of a finite-type Cartan matrix, The Axiom of Choice).

Proof

technique · direct
1.1

Let xgα, ygα and Hh. By [L1] [x,y]g0=h, and [y,H]=[H,y]=α(H)y because ygα; invariance [L2] therefore gives B([x,y],H)=B(x,[y,H])=α(H)B(x,y)=B(B(x,y)Hα,H) by [L3]. As Hh was arbitrary, [x,y]B(x,y)Hα is B-orthogonal to h, hence zero by the nondegeneracy of Bh; that is, [x,y]=B(x,y)Hα.

L1L2L3algebra
1.2

(Cartan integers) Let α,βΦ be nonproportional and put n:=β(hα)=2(α,β)/(α,α) and n:=α(hβ)=2(α,β)/(β,β); both are integers by [L4] and [L5]. Then nn=4(α,β)2/((α,α)(β,β)) is an integer, while Cauchy-Schwarz [L6] and nonproportionality give 0(α,β)2<(α,α)(β,β), so nn{0,1,2,3}. Consequently n=0 if and only if n=0; n/n=(α,α)/(β,β) whenever n0; and n3.

L4L5L6algebra
2.1

By step 1.1 and [L3], [x,y]=hα holds for xgα, ygα exactly when B(x,y)=2/(α,α), where (α,α)=B(Hα,Hα)=α(Hα)0; moreover B(x,y)0 for all nonzero x,y, because the pairing of [L2] is nondegenerate and both gα and gα are one-dimensional by [L1], so that the nonzero functional B(x,) on the line gα vanishes only at 0.

L1L2L3step 1.1algebra
2.2

(Strings and their bounds) Let α,βΦ with α+βΦ, let {p,,q} be the α-string through β (so q1 because the index 1 lies in the string) and let {p,,q} be the β-string through α (so q1), as supplied by [L4]; then n=pq and n=pq by [L4]. The pair (α,β+qα) is nonproportional, since β+qαRα would force βRα and hence β=±α by the reducedness recorded in [L5], contradicting α+βΦ and α+β0; its Cartan integer is (β+qα)(hα)=β(hα)+2q=(pq)+2q=p+q, so step 1.2 gives p+q3. The same argument with α and β interchanged gives p+q3.

L4L5step 1.2algebra
3.1

(First normalization) Choose one representative in each pair {α,α}Φ and put cα:=1 for the chosen representatives while cα:=2/((α,α)B(eα0,eα0)) for their negatives, a nonzero number by step 2.1; then eα:=cαeα0 satisfies [eα,eα]=cαcαB(eα0,eα0)Hα=hα for every root α by step 1.1, so (i) of the statement holds for a rescaling of the given basis.

L3step 1.1step 2.1construct
3.2

(String-length identity) With the notation of step 2.2, q(α+β,α+β)=(p+1)(β,β). Indeed q1, p0 and p+q3 by step 2.2, so (p,q) is one of (0,1), (1,1), (2,1), (0,2), (1,2), (0,3); writing A=(α,α), P=(α,β) and C=(β,β) and using P=nA/2 with n=pq, the six cases are as follows. If (p,q) is (0,1) or (1,2), then n=1, so A+2P=0 and both sides of the identity equal qC=(p+1)C. If (p,q)=(1,1), then n=0, so P=0 and the identity becomes A+C=2C, that is A=C, which holds because the Cartan integer 2(α,α+β)/(α+β,α+β)=2A/(A+C) lies in Z by [L5] and in the open interval (0,2), hence equals 1. If (p,q)=(2,1), then n=1, so P=A/2 and the identity becomes A+2P=2C, that is A=C; here n=2P/C>0 satisfies n{1,2,3} by step 1.2 and also n=pqp+q21 by step 2.2, so n=1 and C=2P=A. If (p,q)=(0,2), then n=2 while n/n=A/C>0 gives n<0, so nn{0,1,2,3} of step 1.2 forces n=1, hence C=nA/n=2A and P=nA/2=A, and the identity becomes 2(A+2P+C)=2(A2A+2A)=2A=C. If (p,q)=(0,3), then n=3 and again n<0 with nn{0,1,2,3}, so n=1, hence C=3A and P=3A/2, and the identity becomes 3(A+2P+C)=3(A3A+3A)=3A=C.

L5step 1.2step 2.2algebra
3.3

(The string module is irreducible) Keep the notation of step 2.2 and put V:=i=pqgβ+iα. By [L1] the brackets with eα and eα shift the index i by ±1 and vanish past the ends of the string, while hα preserves each weight space gβ+iα, on which it acts by the scalar β(hα)+2i; hence V is a finite-dimensional module for the triple (eα,eα,hα) of [L7]. Its weights are β(hα)+2i=pq+2i for i=p,,q, that is the arithmetic progression (p+q),(p+q)+2,,p+q, each occurring on a one-dimensional space by [L1]. A decomposition of V into irreducibles [L7] has distinct highest weights, because every weight space is one-dimensional, and the top weight m:=p+q occurs exactly once; the irreducible summand of highest weight m has all the weights m,m2,,m with multiplicity one, so it exhausts the weight multiset of V, and V itself is irreducible of highest weight m.

L1L4L7step 2.2algebra
4.1

Any further rescaling eαtαeα with nonzero tα satisfies [tαeα,tαeα]=tαtαhα by step 3.1, so it preserves the relations (i) exactly when tαtα=1 for all α.

step 3.1algebra
4.2

(Base and generators) Let Δ={α1,,αr} be the base of a positive system of (E,Φ); such a base exists because regular vectors exist (Positive systems and simple roots) and it is a basis of E by [L5]. Put ei:=eαi and fi:=eαi for the vectors of step 3.1. Then [ei,fi]=hαi=hi, while [hi,ei]=αi(hi)ei=2ei and [hi,fi]=2fi by [L1] and αi(hi)=2 of [L3]; thus (ei,fi,hi) is a root sl2 triple with hi the coroot of αi.

L1L3L5step 3.1
4.3

(Coefficients along the string) Let v:=eβ+qα0. By step 3.3 the vector v is a highest weight vector: [eα,v]gβ+(q+1)α=0 by [L1] and the maximality of q. Since the weight spaces of V are one-dimensional, for each i{p,,q} there are nonzero ciC with eβ+iα=cifqiv, where f:=eα, and cq=1. Induction on k1, using [e,f]=hα, [hα,f]=2f and [hα,v]=mv with e:=eα, gives [e,fkv]=k(mk+1)fk1v; hence for piq1 we get [e,eβ+iα]=ci(qi)(p+i+1)fqi1v, that is Nα,β+iα=(ci/ci+1)(qi)(p+i+1).

L1L7step 3.3algebra
5.1

(Chevalley involution) The assignment eifi, fiei, hihi preserves the relations of the Serre algebra of [L8]: it fixes the relations [hi,hj]=0 up to sign, interchanges the relations [hi,ej]=aijej and [hi,fj]=aijfj, preserves [ei,fj]=δijhi in the form [fi,ej]=δijhi, and sends the Serre relations (adei)1aijej=0 and (adfi)1aijfj=0 into each other, because (ad(fi))1aij(fj)=±(adfi)1aijfj and (ad(ei))1aij(ej)=±(adei)1aijej both vanish. By the universal property of the presented algebra g(A) (Lie algebra presented by generators and relations), this relation-preserving assignment extends to a Lie algebra homomorphism ωA; it is bijective because ωA2 fixes the generators ei,fi,hi of g(A) and hence equals id, so ωA is an automorphism. Transported through the isomorphism g(A)g of [L8], it defines an automorphism ω of g with ω2=idg, ω(ei)=fi, ω(fi)=ei and ω(hi)=hi.

L8step 4.2algebra
5.2

(The opposite string) Applying steps 3.3 and 4.3 to the pair (β,α) in place of (β,α) — the α-string through β is {βjα:pjq}, because βjα=(β+jα) — produces a highest weight vector w:=eβ+pα and nonzero cj with eβjα=cjfp+jw and cp=1; here the bracket with eα=f lowers the f-power without an extra coefficient, so Nα,βjα=cj/cj+1 for pjq1.

L1step 3.3step 4.3algebra
6.1

Since ω(hi)=hi for all i and the hi=hαi form a basis of h by [L5], ω acts as id on h. If xgα and Hh, then [H,ωx]=[ω(H),ωx]=ω([H,x])=α(H)ωx, so ωxgα; as ω is bijective, ω(gα)=gα for every root α. In particular each ω(eα) is a nonzero element of the line gα, say ω(eα)=cαeα with cαC×, and applying ω twice gives cαcα=1.

L1L5step 5.1algebra
6.2

(Pairing of the two strings) By the invariance of B, B(fx,y)=B(x,fy) for all x,yg [L2]. Applying this qi times and using B(gγ,gδ)=0 unless γ+δ=0 [L2] together with the weights of v and w gives B(eβ+iα,eβiα)=cici(1)qiB(v,fmw), and fmw=(cq)1eβqα because eβjα=cjfp+jw at j=q. Also B(eγ,eγ)=2/(γ,γ) for every root γ: by step 1.1 the bracket [eγ,eγ] equals both B(eγ,eγ)Hγ and, by (i), the coroot hγ=2Hγ/(γ,γ) of [L3]. Comparing the two expressions for B(eβ+iα,eβiα) therefore gives cici(1)qi(cq)1/(β+qα,β+qα)=1/(β+iα,β+iα), that is cici=(1)qicq(β+qα,β+qα)/(β+iα,β+iα).

L1L2L3step 1.1step 4.3step 5.2algebra
7.1

(Second normalization) By step 4.1 the rescalings with tαtα=1 are exactly those preserving (i). Choose tαC× with tα2=1/cα for the numbers cα0 of step 6.1 and put tα:=1/tα, so that tαtα=1. For eα:=tαeα we then have [eα,eα]=hα by step 4.1, and ω(eα)=tαcαeα=tαcαtαeα=cαtα2eα=eα, because tαtα=1 gives eα=tαeα and because cαtα2=1.

step 4.1step 6.1choosealgebra
7.2

(Chevalley's identity) Dividing the relation of step 6.2 for the indices i and i+1, the unknown cq cancels and the sign flips, so cici/(ci+1ci+1)=(β+(i+1)α,β+(i+1)α)/(β+iα,β+iα); multiplying by the coefficient formulas of steps 4.3 and 5.2 gives Nα,β+iαNα,βiα=(qi)(p+i+1)(β+(i+1)α,β+(i+1)α)(β+iα,β+iα)=(p+i+1)2, the last equality by the string-length identity 3.2 applied to the pair (α,β+iα), whose string is β+iα+nα for pinqi; in particular, at i=0, NαβNα,β=(p+1)2.

step 3.2step 4.3step 5.2step 6.2algebra
8.1

(Sign relation) Let α,βΦ with α+βΦ. Applying ω to [eα,eβ]=Nαβeα+β and using ω(eγ)=eγ for all γ gives [eα,eβ]=Nαβ(eαβ), that is Nα,β=Nαβ; when α+βΦ{0} both brackets [eα,eβ] and [eα,eβ] vanish by [L1], so Nαβ=Nα,β=0. Hence Nαβ=Nα,β for all α,βΦ with α+β0, which is (ii) of the statement, the excluded case β=α being the one in which the constants are not defined.

L1step 5.1step 7.1algebra
9.1

(Integrality) The product NαβNα,β is unchanged by the rescaling of step 7.1: that rescaling replaces Nαβ by (tαtβ/tα+β)Nαβ and Nα,β by (tαtβ/tαβ)Nα,β=(tα+β/(tαtβ))Nα,β, because tγtγ=1, so the product is multiplied by 1. Hence step 7.2 gives NαβNα,β=(p+1)2 also for the vectors eα of step 7.1, and combining this with Nα,β=Nαβ of step 8.1 gives Nαβ2=(p+1)2, so Nαβ=±(p+1) for all α,βΦ with α+βΦ; this is (iii) of the statement, and together with the convention Nαβ=0 otherwise it shows that all constants Nαβ are integers. Moreover each eα=tαcαeα0 is a nonzero complex multiple of the given vector eα0, so the family produced is obtained from the given root-vector basis by rescaling, as required.

step 7.2step 8.1algebra
10.1

(Real form and integral structure) Let g0:=spanR{hα,eα:αΦ}. It is closed under brackets: [hR,hR]=0; [hα,eβ]=β(hα)eβ with β(hα)Z by [L4]; [eα,eβ]=Nαβeα+β with NαβZ by step 9.1; [eα,eα]=hα; and all brackets with α+βΦ{0} vanish by [L1]. Since h=hRihR by [L5] and the vectors eα form a basis of αΦgα, we get g=g0ig0, so that g0 is a real form of g. With respect to the basis {hα1,,hαr}{eα} the structure constants are integers, because hαiZhαi by the coroot-lattice statement of [L5]; and for HhR the operators adH are diagonalizable over R with eigenvalues α(H)R by [L1] and [L5]. Hence g0 is a split real form of g.

L1L4L5step 9.1algebra
11.1

(Dual normalization) Put λα=((α,α)/2)1/2>0, a positive real number, and Xα:=λαeα for all α; then also Xα=λαeα, because λα=λα. By step 3.1 and (i), [Xα,Xα]=λα2hα=(α,α)22Hα(α,α)=Hα and B(Xα,Xα)=λα22/(α,α)=1. Hence for α+βΦ the constants defined by [Xα,Xβ]=CαβXα+β are Cαβ=(λαλβ/λα+β)Nαβ, real numbers because λγ and Nαβ=±(p+1) are real; and Cαβ=Cα,β because λγ=λγ and Nαβ=Nα,β.

L3step 3.1step 8.1step 9.1algebra

Depends on

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