Alphabeta Math
PropositionStatement: 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 preserves semisimplicity

Statement

Let g0 be a finite-dimensional real Lie algebra with complexification gC (Complexification of a real Lie algebra). Then g0 is semisimple if and only if gC is semisimple.

Facts & Assumptions

Given: A finite-dimensional real Lie algebra g0 with complexification gC=g0RC and canonical real embedding ε(X)=X1.

[L1]

For a finite-dimensional Lie algebra l over a field of characteristic zero (in particular over R or C), the algebra is semisimple if and only if Bl is nondegenerate; the Killing form is the trace form of the adjoint representation, Bl(X,Y)=tr(adXadY) (Cartan's semisimplicity criterion, Killing form).

[L2]

The complexification carries the bracket [Xz,Yw]=[X,Y]zw and every element has a unique expression X1+iY1 with X,Yg0; the embedded copy of g0 is a real form, in particular a real Lie subalgebra (Complexification of a real Lie algebra).

Proof technique: direct.

1.1 We compute the Killing form of gC on embedded elements. Let X,Yg0 and choose a real basis u1,,un of g0. This is also a complex basis of gC: it spans over C because Xz=zε(X) and it is independent over C by [L2]; consequently ε is injective, since εX=0 for X=ktkuk means ktk(uk1)=0, which forces tk=0 for every k by that independence. In this basis the matrix of adε(X) has entries determined by [εX,εuk]=ε[X,uk], the R-linear extension of adX. Hence BgC(εX,εY)=tr(adεXadεY)=trR(adXadY)=Bg0(X,Y), using that the trace of the complexification of a real endomorphism equals its real trace computed in the real basis {uk}. [L1, L2, algebra]

2.1 The restriction map ZiZ is R-linear and injective on gC; by [L2] the R-span of ε(g0) and iε(g0) is all of gC, so every element is X1+iY1 and the assignment X+iY(X,Y) is a real vector-space isomorphism gCg0×g0. In particular, if a real form of the complex bilinear form BgC has no radical outside 0 then it is nondegenerate as a real form, and conversely. [L1, L2, step 1.1, algebra]

2.2 Suppose first that gC is semisimple, so that BgC is nondegenerate by [L1]. If Xg0 satisfies Bg0(X,Y)=0 for all Yg0, then by step 1.1, BgC(εX,εY)=0 for all Yg0. Complex bilinearity gives BgC(εX,Z)=0 for every ZgC: writing Z=εY+iεY with Y,Yg0, the pairing is BgC(εX,εY)+iBgC(εX,εY)=0. Nondegeneracy forces εX=0, hence X=0, so Bg0 is nondegenerate and g0 is semisimple by [L1]. [L1, L2, step 1.1, algebra]

3.1 Conversely suppose g0 is semisimple, so Bg0 is nondegenerate. Let ZgC satisfy BgC(Z,W)=0 for all W. Write Z=εX+iεY with X,Yg0. Taking first W=εU for Ug0 and using complex linearity in the second argument together with step 1.1 gives 0=BgC(εX,εU)+iBgC(εY,εU)=Bg0(X,U)+iBg0(Y,U), so both Bg0(X,U)=0 and Bg0(Y,U)=0 for all Ug0. Nondegeneracy gives X=Y=0 and hence Z=0, so BgC is nondegenerate and gC is semisimple by [L1]. The two implications together prove the equivalence. [L1, L2, step 1.1, step 2.2, algebra] ∎

Depends on

Used by

Dependency tree · two levels

10 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