Alphabeta Math
TheoremStatement: 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.

Existence and uniqueness up to isomorphism of the split real form

Statement

Assume the Axiom of Choice. Every finite-dimensional complex semisimple Lie algebra g has a split real form (Split real form), and it is unique up to isomorphism of real Lie algebras.

Facts & Assumptions

Given: The Axiom of Choice and a finite-dimensional complex semisimple Lie algebra g; after the choices justified in [L0], write h for a Cartan subalgebra, Φ for its root system and Δ={α1,…,αr} for a base with Cartan matrix A; when a split real form of g is under discussion, write h1 for a Cartan subalgebra of it as in [L3].

[A1]

The Axiom of Choice is The Axiom of Choice; it is inherited from the Serre presentation theorem and root data of [L1] and [L2], from the conjugacy theorem of [L4] and from the Chevalley-basis statement [L6], whose statements carry the assumption.

[L0]

Every finite-dimensional complex semisimple Lie algebra has a Cartan subalgebra. For its finite reduced root system, a regular vector determines a positive system and its indecomposable positive roots form a base; the simple roots form a basis of the real root span and every root has integral coefficients of one sign (Existence of Cartan subalgebras, Positive systems and simple roots, Simple roots form a signed integral basis).

[L1]

The Serre presentation theorem, in both directions: g≅g(A) through the assignment Ei↦ei, Fi↦fi, Hi↦hi determined by a root sl2 triple (ei,fi,hi) over the base Δ (The root sl2 triple), the elements ei,fi,hi generating g and satisfying exactly the relations of the Serre algebra g(A); conversely, for any Cartan subalgebra h′ of g, any base Δ′ of Φ(g,h′) with Cartan matrix A and any root sl2 triples (ei′,fi′,hi′) over Δ′, the elements ei′,fi′,hi′ generate g and satisfy exactly the relations of g(A), so that Ei↦ei′, Fi↦fi′, Hi↦hi′ extends to an isomorphism g(A)→g; a homomorphism out of g(A) is defined by prescribing the images of the generators and checking the relations (Serre presentation theorem, Serre Lie algebra of a finite-type Cartan matrix, Lie algebra presented by generators and relations, The root sl2 triple).

[L2]

Let h′ be a Cartan subalgebra of g, Φ′=Φ(g,h′) its root system and hβ∈h′ the coroot of a root β, characterized by β(hβ)=2 and B(hβ,H)=2β(H)/β(Hβ) for H∈h′. Then Φ′ is finite, g=h′⊕⨁β∈Φ′gβ with one-dimensional root spaces, and for a base Δ′={α1′,…,αr′} of Φ′ the Cartan matrix is aij′=αj′(hαi′)=⟨αj′,αi′∨⟩=2(αj′,αi′)/(αi′,αi′), an integer determined by the inner product (λ,μ)=B(Hλ,Hμ) on span⁡RΦ′ (Roots of a complex semisimple Lie algebra form a reduced crystallographic root system, Root and root space, Coroot of a Lie-algebra root, Cartan matrix of a based root system, Cartan integers are integers).

[L3]

A real form g1 of g (Real form of a complex Lie algebra) is split if it contains a Cartan subalgebra h1 of g1 (Cartan subalgebra) such that all operators ad⁡H, H∈h1, are simultaneously diagonalizable over R; equivalently g1 has a basis in which all these operators are diagonal with real eigenvalues (Split real form).

[L4]

A subalgebra h′ of g is a Cartan subalgebra if and only if it is nilpotent and Ng(h′)=h′; every Cartan subalgebra of g is abelian and satisfies Ng(h′)=Cg(h′)=h′, and any two Cartan subalgebras of g are carried to one another by an inner automorphism in the connected adjoint group of g (Cartan subalgebra, Cartan subalgebras are exactly maximal toral subalgebras, Conjugacy of Cartan subalgebras, The Axiom of Choice).

[L5]

B is symmetric, invariant, nondegenerate, and preserved by every automorphism ψ of g: B(ψx,ψy)=B(x,y), because ad⁡ψx=ψ∘ad⁡x∘ψ−1 and B is a trace form. For x∈gβ and y∈g−β one has [x,y]=B(x,y)Hβ, where Hβ is the Killing-dual of β, and the pairing gβ×g−β→C given by B is nondegenerate (Killing form, Trace forms are symmetric and invariant, Killing-dual vector of a root, Opposite root spaces pair nondegenerately, Brackets of root spaces).

[L6]

The root-vector basis of (g,h) can be rescaled so that [eα,e−α]=hα for every root and the structure constants Nαβ, defined by [eα,eβ]=Nαβeα+β, are integers satisfying Nαβ=−N−α,−β; the real span span⁡R{hα,eα:α∈Φ} is then a split real form of g with integer structure constants in the basis {hα1,…,hαr}∪{eα:α∈Φ} (Chevalley basis and real structure constants).

Proof technique: direct.

1.1 Choose a Cartan subalgebra h and a base Δ by [L0]. By [L6] the root vectors of this Cartan data can be rescaled so that [eα,e−α]=hα, the structure constants Nαβ are integers with Nαβ=−N−α,−β, and g0:=span⁡R{hα,eα:α∈Φ} is a split real form of g with integer structure constants in the basis {hα1,…,hαr}∪{eα}. Write hi:=hαi, ei:=eαi and fi:=e−αi; then (ei,fi,hi) is a root sl2 triple over Δ, and the real span a of the iterated brackets of hi,ei,fi is a subalgebra of g0 containing these generators. Its complexification is a complex subalgebra of g containing ei,fi,hi, which generate g by [L1], so it equals g; hence dim⁡Ra=dim⁡Cg=dim⁡Rg0 and a=g0. In particular g has a split real form, generated by the Serre triple (ei,fi,hi). [A1, L0, L1, L6, algebra]

1.2 Let g1 be a split real form of g with split Cartan subalgebra h1 as in [L3], and put h′:=h1C. Then h′ is a Cartan subalgebra of g: it is nilpotent, because the lower central series of the real nilpotent Lie algebra h1 complexifies to the lower central series of h′; and it is self-normalizing, because if x=u+iv with u,v∈g1 satisfies [x,h′]⊆h′, then [u,h1],[v,h1]⊆h′∩g1=h1, so u,v∈Ng1(h1)=h1 and x∈h′. [L3, L4, algebra]

1.3 By [L4] there is an inner automorphism ψ of g with ψ(h′)=h. The transpose ψ∗, defined by ψ∗β=β∘ψ−1 on h′, carries Φ′:=Φ(g,h′) bijectively onto Φ, and since B is ψ-invariant by [L5] it is an isometry for the inner products (λ,μ)=B(Hλ,Hμ) of [L2]; therefore it preserves Cartan integers ⟨β,α∨⟩=2(β,α)/(α,α). Hence Δ′:=ψ∗−1(Δ) is a base of Φ′: it is a linearly independent subset of Φ′ with r elements, and every β′∈Φ′ is a nonnegative or nonpositive integral combination of Δ′, because ψ∗β′ is such a combination of the base Δ. Its Cartan matrix A′ equals A, since aij′=⟨αj′,αi′∨⟩=⟨ψ∗αj′,ψ∗αi′∨⟩=⟨αj,αi∨⟩=aij. [L2, L4, L5, algebra]

1.4 For every β∈Φ′ the space g1∩gβ is a real line. Indeed, by [L3] the operators ad⁡H with H∈h1 are simultaneously diagonalizable over R on g1; let g1=⨁λVλ be the decomposition into common eigenspaces. Complexifying gives g=⨁λVλC with VλC⊆gλC, where λC is the C-linear extension of λ; since h′ is a Cartan subalgebra with Cg(h′)=h′ by [L4] and the weight space of weight 0 is h′ by [L2], the zero eigenspace is V0=h1, the intersection h′∩g1 being h1. Every nonzero λ with Vλ≠0 satisfies VλC⊆gλC≠0, so λC∈Φ′, distinct nonzero λ have distinct extensions λC, and dim⁡RVλ=dim⁡CVλC≤1. Hence dim⁡Rg1=dim⁡Rh1+∑λ≠0dim⁡RVλ≤dim⁡Rh1+#{λ≠0:Vλ≠0}≤dim⁡Rh1+∣Φ′∣=dim⁡Ch′+dim⁡C⨁β∈Φ′gβ=dim⁡Cg=dim⁡Rg1, so all inequalities are equalities: each occurring nonzero λ contributes a distinct root and dim⁡RVλ=1, every root of Φ′ occurs, and g1∩gβ=Vβ is one-dimensional over R. [L2, L3, L4, algebra]

2.1 Choose 0≠xi∈g1∩gαi′ and let yi∈g1∩g−αi′ be the vector with [xi,yi]=hαi′; it exists and is unique because by [L5] one has [xi,y]=B(xi,y)Hαi′ for y∈g−αi′, where Hαi′ is the Killing-dual, and y↦B(xi,y) is a nonzero R-linear functional on the real line g1∩g−αi′ by the nondegeneracy of the pairing in [L5]; moreover Hαi′∈h1, since writing Hαi′=u+iv with u,v∈h1 and evaluating B(Hαi′,H)=αi′(H)∈R on H∈h1 gives B(v,h1)=0 and hence v=0, so the image of y↦[xi,y] is the real line Rhαi′. Put zi:=hαi′. Then zi∈h1, the relations [zi,xi]=αi′(zi)xi=2xi and [zi,yi]=−2yi hold by [L2], and [xi,yi]=zi by construction; so (xi,yi,zi) is a root sl2 triple over Δ′ with coroot zi. Applying [L1] to the Cartan subalgebra h′ and the base Δ′ of Φ′, the elements xi,yi,zi generate g and satisfy exactly the relations of g(A′)=g(A) (step 1.3). [L1, L2, L5, step 1.3, step 1.4]

3.1 Let g(A) be the Serre algebra of A. By [L1] the assignment Ei↦ei, Fi↦fi, Hi↦hi extends to an isomorphism ρ0:g(A)→g, and by [L1] and step 2.1 the assignment Ei↦xi, Fi↦yi, Hi↦zi extends to a homomorphism ρ1:g(A)→g. The image of ρ1 contains xi,yi,zi, which generate g, so ρ1 is surjective; since dim⁡g(A)=dim⁡g by [L1], it is an isomorphism. Let g(A)R be the real span of all iterated brackets of Ei,Fi,Hi in g(A); it is a real form of g(A), because these iterated brackets span g(A) over C. Now ρ0(g(A)R) is the real span of the iterated brackets of ei,fi,hi, which is g0 by step 1.1; and ρ1(g(A)R) is the real span of the iterated brackets of xi,yi,zi, a real subalgebra of g1 whose complexification is the complex span of the same brackets, namely g by step 2.1, so that it equals g1. Hence the restrictions of ρ0 and ρ1 to g(A)R are isomorphisms of real Lie algebras onto g0 and g1, and g0≅g1 by composition. [L1, step 1.1, step 2.1, algebra]

4.1 By step 1.1 a split real form of g exists, and by steps 1.2-3.1 every split real form g1 of g is isomorphic to g0. Hence every finite-dimensional complex semisimple Lie algebra has a split real form and any two split real forms are isomorphic as real Lie algebras, that is, the split real form is unique up to isomorphism. [A1, step 1.1, step 3.1] ∎

Remarks

The uniqueness comparison no longer assumes an integral Chevalley basis inside an arbitrary split real form. What the comparison actually uses is: the complexified split Cartan h′=h1C is a Cartan subalgebra of g (step 1.2), so the conjugacy theorem of [L4] makes the based root system of h′ isomorphic to the given one with the same Cartan matrix (step 1.3); the split condition makes each root space of g1 a real line (step 1.4, from the simultaneous diagonalization in [L3]); the Serre presentation theorem [L1] then supplies a root sl2 triple over that base whose elements generate g and satisfy exactly the relations of g(A) (step 2.1); and the comparison is completed through the Serre algebra g(A) and its real form g(A)R (step 3.1). The Chevalley normalization of [L6] --- Knapp's Theorem 6.6 with Lemma 6.4, printed pp. 350-353; equivalently the Chevalley presentation of Etingof \S 39.2 --- is used for the existence of the split real form g0 and its integral structure constants. The earlier draft additionally claimed that g1 carries an integral Chevalley-type basis; that claim is needed nowhere and is not asserted here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

81 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