Alphabeta Math
ExampleConstruction: AI-adaptedVerification: 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.

Complex simple lie algebra viewed as a real simple algebra

Example

Let s be a finite-dimensional complex simple Lie algebra and let sR be the same real vector space with the bracket restricted to real scalars, regarded as a real Lie algebra. Then sR is a simple real Lie algebra, and its complexification is C-isomorphic to s⊕s‾, where s‾ is s with the conjugate complex structure, with the canonical conjugation of the real form interchanging the two factors. This is the complex-as-real case of the dichotomy of Complexification dichotomy for a real simple lie algebra.

Facts & Assumptions

Given: A finite-dimensional complex simple Lie algebra s with multiplication by i written J, and the real Lie algebra sR obtained by restricting scalars.

[L1]

sR is a real Lie algebra whose bracket is the restriction of the bracket of s; J is R-linear with J2=−id and J[X,Y]=[JX,Y]=[X,JY], and the complexification (sR)C carries the bracket extending the one of sR (Complexification of a real Lie algebra).

[L2]

The Killing form of sR is BR(X,Y)=2Re⁡Bs(X,Y), and a finite-dimensional real Lie algebra is semisimple exactly when its Killing form is nondegenerate (Killing form, Cartan's semisimplicity criterion).

[L3]

Every ideal of a finite-dimensional semisimple Lie algebra is a direct sum of simple ideals with an ideal complement, hence is itself semisimple; a semisimple Lie algebra equals its own derived algebra (Ideals and quotients of semisimple Lie algebras, Semisimple Lie algebras are centerless and perfect).

[L4]

The complexification (sR)C carries the canonical conjugation σ(X+iY)=X−iY, whose fixed locus is the embedded copy of sR, and complexification preserves semisimplicity (Complexification has a canonical conjugation with fixed algebra g zero, Complexification of a real Lie algebra, Complexification preserves semisimplicity).

Proof technique: direct computation with ideals and with the explicit isomorphism.

1.1 The real Lie algebra sR is semisimple: its Killing form is BR(X,Y)=2Re⁡Bs(X,Y) because the adjoint operators of sR are the C-linear operators ad⁡X viewed over R and the real trace of a complex-linear operator is twice the real part of its complex trace, so if BR(X,Y)=0 for all Y, then replacing Y by JY and using Bs(X,JY)=iBs(X,Y) gives Im⁡Bs(X,Y)=0 as well, hence Bs(X,⋅)=0 and X=0; thus BR is nondegenerate and [L2] applies. [given, L1, L2, algebra]

2.1 For every ideal a⊆sR one has a=[a,sR]: by [L3] applied to the semisimple algebra sR of step 1.1, a is semisimple and satisfies a=[a,a], so a=[a,a]⊆[a,sR]⊆a. [step 1.1, L3, algebra]

3.1 Every ideal is J-stable: if X∈a and X=∑j[Xj,Yj] with Xj∈a and Yj∈sR as in step 2.1, then JX=∑jJ[Xj,Yj]=∑j[Xj,JYj]∈[a,sR]=a by [L1]. Hence a real ideal of sR is a complex subspace and a complex ideal of s. [step 2.1, L1, algebra]

4.1 Consequently sR is simple over R: since s is complex simple, a complex ideal is 0 or s, so every ideal of sR is 0 or sR; the algebra is nonabelian because s is nonabelian, so it is simple. [step 3.1, algebra]

5.1 Define s‾ to be the real space s with the complex structure −J; it is a complex Lie algebra with the same bracket. Then the map L:(sR)C→s⊕s‾, L(X+iY)=(X+JY, X−JY), is a C-linear isomorphism of complex vector spaces: it is additive and R-bilinear in the obvious way, its inverse is (U,V)↦12(U+V)+i 12J−1(U−V), and L(i(X+iY))=L(−Y+iX)=(−Y+JX, −Y−JX)=(J(X+JY), −J(X−JY)), which is i times L(X+iY) in the complex structure (J,−J) of s⊕s‾. Dimension counts agree: both sides have complex dimension 2dim⁡Cs. [given, step 4.1, algebra]

6.1 The map L preserves brackets: for X,Y,X′,Y′∈sR one has [L(X+iY),L(X′+iY′)]=([X+JY,X′+JY′], [X−JY,X′−JY′]) and L([X+iY,X′+iY′])=L([X,X′]−[Y,Y′]+i([X,Y′]+[Y,X′]))=([X,X′]−[Y,Y′]+J([X,Y′]+[Y,X′]), [X,X′]−[Y,Y′]−J([X,Y′]+[Y,X′])), and the two expressions agree because [JY,JY′]=J2[Y,Y′]=−[Y,Y′] and [JY,X′]=J[Y,X′] by [L1]. Hence L is an isomorphism of complex Lie algebras. [step 5.1, L1, algebra]

7.1 The canonical conjugation of (sR)C, namely σ(X+iY)=X−iY, corresponds under L to the swap of the two factors: L(σ(X+iY))=L(X−iY)=(X−JY, X+JY), which is the interchange of the entries of L(X+iY)=(X+JY,X−JY); its fixed locus is the image of sR under the embedding, in agreement with [L4]. [step 5.1, step 6.1, L4, algebra]

8.1 Combining the steps: sR is a simple real Lie algebra by step 4.1, and its complexification is isomorphic to s⊕s‾ by steps 5.1 and 6.1, with the canonical conjugation of the real form acting as the swap of the two factors by step 7.1. This realizes the complex-as-real alternative of Complexification dichotomy for a real simple lie algebra directly, from the explicit isomorphism L and without using any supplementary clause of that theorem: a complex simple algebra regarded as real has a complexification that is a direct sum of two simple ideals interchanged by conjugation, and the example supplies the isomorphism and the swap. [step 4.1, step 5.1, step 6.1, step 7.1]

9.1 Endpoints and scope: s is nonabelian by hypothesis, so sR has nonzero bracket and simplicity is not vacuous; for s=sl2(C) the real dimension dim⁡RsR=6 equals dim⁡C(s⊕s‾) computed over C as 3+3, in agreement with step 5.1; the zero algebra is excluded because it is not simple, and every step is a finite computation, so the argument uses no choice principle. [given, step 5.1, step 7.1, algebra] ∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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