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.

Complexification dichotomy for a real simple lie algebra

Statement

Assume the Axiom of Choice. Let g0 be a finite-dimensional real simple Lie algebra (Simple, semisimple, and reductive Lie algebras) with complexification g=g0RC (Complexification of a real Lie algebra). Then exactly one of the following holds:

  1. g is a complex simple Lie algebra;
  2. g=sσ(s) is a direct sum of two simple ideals interchanged by the canonical conjugation σ of g over g0 (Complexification has a canonical conjugation with fixed algebra g zero), and the two ideals are isomorphic complex Lie algebras. In this case g0 is isomorphic, as a real Lie algebra, to the complex simple Lie algebra s regarded as a real Lie algebra.

In particular a real simple Lie algebra is either a complex simple Lie algebra viewed as a real Lie algebra, or a noncomplex simple Lie algebra whose complexification is simple.

Facts & Assumptions

Given: AC; a finite-dimensional real simple Lie algebra g0 that is nonabelian with no nonzero proper ideal, with complexification g=g0RC and canonical conjugation σ; and the notation of Simple, semisimple, and reductive Lie algebras, Complexification of a real Lie algebra and Complexification has a canonical conjugation with fixed algebra g zero.

[A1]

We assume The Axiom of Choice, including the hypotheses of the Cartan-existence and Chevalley-basis results in [L6].

[L1]

A Lie algebra is simple if it is nonabelian and has no nonzero proper ideal, and semisimple if its radical is zero; a solvable ideal of a semisimple algebra is zero (Simple, semisimple, and reductive Lie algebras).

[L2]

The complexification gC of a finite-dimensional real Lie algebra g0 carries the bracket [Xz,Yw]=[X,Y]zw, every element has a unique expression X1+iY1 with X,Yg0, and g0 embeds as a real form (Complexification of a real Lie algebra).

[L3]

The canonical conjugation σ(Xz)=Xzˉ is a well-defined conjugate-linear bracket-preserving involution of g with fixed locus g01, so it is additive and real-linear, σ2=id, and σ(iz)=iσ(z) for zg (Complexification has a canonical conjugation with fixed algebra g zero).

[L4]

g0 is semisimple if and only if g is semisimple (Complexification preserves semisimplicity).

[L5]

Every finite-dimensional semisimple Lie algebra over a characteristic-zero field is a finite direct sum of simple ideals, and the simple ideals are nonabelian with trivial center and satisfy [l,l]=l (Semisimple Lie algebras decompose into simple ideals, Semisimple Lie algebras are centerless and perfect).

[L6]

Under AC, every complex semisimple Lie algebra has a Cartan subalgebra; relative to it, the algebra has a root-space decomposition with one-dimensional root spaces and admits a Chevalley basis with integer, hence real, structure constants (Existence of Cartan subalgebras, Root-space decomposition, Root spaces of a complex semisimple Lie algebra are one-dimensional, Chevalley basis and real structure constants, Cartan subalgebra).

Proof

technique · direct
1.1

g0 is semisimple: its radical is an ideal, and the only ideals of the nonabelian simple algebra g0 are 0 and g0, so either the radical is zero and g0 is semisimple, or the radical is g0. The latter is impossible: the nonzero derived ideal [g0,g0] must equal g0 by simplicity, so the derived series never reaches zero.

L1
1.2

σ is a conjugate-linear involutive automorphism of g, hence additive and real-linear with σ2=idg, its fixed locus is exactly g0, and σ(iX)=iσ(X) for every Xg.

L2L3
2.1

g is semisimple by [L4] and step 1.1, so it is a nonzero finite direct sum g=g1gn of simple ideals. Moreover every ideal a of g is the sum of the simple ideals it contains: the projection pj ⁣:ggj is a Lie algebra homomorphism, so pj(a) is an ideal of the simple algebra gj and is therefore 0 or gj; and pj(a)0 forces gja, because for xa with xj:=pj(x)0 one has [x,gj]=[xj,gj]agj, which would be zero if agj=0 and would then put the nonzero xj in the center Z(gj)=0. Hence the simple ideals are exactly the minimal nonzero ideals, and [gj,gj]=gj0 for every j.

L1L5step 1.1
3.1

Let π be the permutation of {1,,n} determined by σ(gi)=gπ(i), which is well defined because σ carries simple ideals to nonzero simple ideals by step 1.2 and step 2.1; then π is transitive. Suppose it has at least two orbits, let O be one of them and put W=iOgi and W=iOgi. Both are nonzero ideals of g, both are σ-stable because O and its complement are unions of orbits, and g=WW. Every Xg0 is σ-fixed, so by uniqueness of the decomposition its components in W and W are σ-fixed as well by step 1.2; hence g0=(g0W)(g0W), and each summand is an ideal of g0 because it is the intersection of the subalgebra g0 with an ideal of g. Both summands are nonzero: for any nonzero x in either sigma-stable complex ideal, the two fixed vectors x+σx and i(xσx) cannot both vanish. Thus g0 would have two nonzero proper ideals, contradicting simplicity. Hence π is transitive.

step 1.2step 2.1
4.1

All orbits of π have one or two elements: applying σ twice to σ(gi)=gπ(i) gives gi=gπ(π(i)) by step 1.2, so π2=id and every orbit of the resulting involution has at most two elements. Transitivity and nonzero g therefore give n=1 or n=2, with the two ideals exchanged in the latter case.

step 1.2step 3.1
4.2

In the case n=2 the projection p ⁣:gg1 restricts to an isomorphism of real Lie algebras g0(g1)R, where (g1)R denotes the complex Lie algebra g1 with scalars restricted to R. Indeed p is a Lie algebra homomorphism; it is injective on g0 because g0g2=0, an element of that intersection being σ-fixed and at the same time lying in g1 by σ(g2)=g1; and it is surjective because for xg1 the element x+σx lies in g0 by step 1.2 and is mapped to x. Moreover σ restricts to a conjugate-linear isomorphism g1g2, so g2 is isomorphic to the complex conjugate Lie algebra g1.

step 1.2step 3.1
5.1

If n=1, then g=g1 is a complex simple Lie algebra, which is alternative 1 of the Statement. If n=2, then g=g1g2 with g2=σ(g1) and both ideals simple; by step 4.2 the real Lie algebra g0 is isomorphic to (g1)R, so g0 is the complex simple algebra g1 regarded as a real Lie algebra. The two ideals are isomorphic as complex Lie algebras: by [L6], choose a Chevalley basis (bj) of g1 with real structure constants [bi,bj]=kcijkbk. If (bj) denotes the corresponding basis of the conjugate algebra g1, then bjbj is complex-linear and bracket-preserving because every cijk is real. Thus g1g1, while the conjugate-linear isomorphism σ:g1g2 is equivalently a complex-linear isomorphism g1g2; hence g2g1. This is alternative 2. The alternatives are disjoint because a direct sum of two nonzero ideals is not simple.

A1L6step 4.1step 4.2
6.1

Finally, if g0 is a complex Lie algebra with complex structure J, extend J complex-linearly to its complexification. Then J2=1 and [JX,Y]=J[X,Y]=[X,JY], so the +i and i eigenspaces are ideals and their sum is the whole complexification. They are interchanged by canonical conjugation since J is defined over R. Both are nonzero: for 0Xg0, the vectors XiJX and X+iJX are nonzero and lie in the respective eigenspaces, by the unique real-imaginary decomposition of [L2]. Hence case 1 cannot occur for a complex algebra regarded as real. Together with step 5.1 this proves the last assertion as well.

L2L3step 5.1algebra

Depends on

Used by

Dependency tree · two levels

62 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