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 of a Cartan involution

Statement

Assume the Axiom of Choice. Every finite-dimensional real semisimple Lie algebra g0 has a Cartan involution (Cartan involution of a real semisimple Lie algebra).

Facts & Assumptions

Given: The Axiom of Choice; a finite-dimensional real semisimple Lie algebra g0 with Killing form B0; its complexification g=g0RC with Killing form B and canonical conjugation σ; and the real Lie algebra gR underlying g, with Killing form BR.

[A1]

The Axiom of Choice is The Axiom of Choice; it is inherited through the compact-form existence of [L2].

[L1]

The complexification g is semisimple, g=g0ig0 is a real direct sum with B the complex-bilinear extension of B0, and σ(X+iY)=XiY is a conjugate-linear bracket-preserving involution with fixed locus g0 (Complexification preserves semisimplicity, Real forms correspond to conjugate-linear involutions, Complexification of a real Lie algebra, Killing form).

[L2]

g has a compact real form u0 with conjugation τ and negative definite Killing form on u0, so that τ is a conjugate-linear bracket-preserving involution with fixed locus u0 and g=u0iu0 (Existence of a compact real form, Compact real form of a complex semisimple Lie algebra, Real forms correspond to conjugate-linear involutions).

[L3]

The Killing form of a finite-dimensional Lie algebra over a characteristic-zero field is symmetric and invariant, and such an algebra is semisimple if and only if its Killing form is nondegenerate; for a semisimple algebra every derivation is inner, Der=ad with Z(g)=0 (Trace forms are symmetric and invariant, Cartan's semisimplicity criterion, Derivations of semisimple Lie algebras are inner, Semisimple Lie algebras are centerless and perfect).

Proof

technique · direct
1.1

The adjoint operators of gR are the realifications of those of g, so the real trace of the realification of a complex-linear endomorphism is twice its complex trace and BR(Z,W)=2ReB(Z,W) for all Z,Wg. If Z lies in the radical of BR then ReB(Z,W)=0 for all W, and substituting iW gives ImB(Z,W)=0; hence Z=0 by nondegeneracy of B, so BR is nondegenerate and gR is semisimple, with every derivation inner and Z(gR)=0.

L3givenalgebra
1.2

The restriction of B to g0 is B0, because in a real basis of g0 the matrices of adX, Xg0, acting on g have the real block form of the realification of adX acting on g0. In particular B is real-valued on g0×g0, and B0 is nondegenerate since g0 is semisimple.

L1L3givenalgebra
1.3

The map τ is real-linear on gR with τ2=id and preserves brackets, and B(τZ,τW)=B(Z,W) for all Z,W: writing Z=X+iY, W=X+iY with X,Y,X,Yu0, both sides equal B(X,X)B(Y,Y)i(B(X,Y)+B(Y,X)) by complex bilinearity and symmetry of B. Hence BR(τZ,τW)=BR(Z,W).

L2L3algebra
2.1

τ is a Cartan involution of gR: for Z=X+iY0 with X,Yu0 one has (BR)τ(Z,Z)=BR(Z,τZ)=2ReB(Z,τZ)=2(B(X,X)+B(Y,Y))>0, since B(Z,τZ)=B(X,X)+B(Y,Y) and the Killing form of u0 is negative definite. Write Bτ:=(BR)τ for this inner product.

L2L3step 1.3algebra
3.1

Put ω:=στAut(gR), an invertible automorphism, and note τω=ω1τ, because both sides equal τστ. Invariance of BR under ω1 and under τ gives Bτ(ωZ,W)=BR(ωZ,τW)=BR(Z,ω1τW)=BR(Z,τωW)=Bτ(Z,ωW) for all Z,W, so ω is self-adjoint for Bτ; since ω is invertible, ρ:=ω2=ωω satisfies Bτ(ρZ,Z)=Bτ(ωZ,ωZ)>0 for Z0, so ρ is a self-adjoint positive definite automorphism of gR.

step 2.1algebra
4.1

By [L4] choose a Bτ-orthonormal eigenbasis of ρ with eigenvalues λj>0 and let ρr, rR, act as λjr on the eigenspace for λj. If X,Y are eigenvectors with eigenvalues λi,λj, then ρ[X,Y]=[ρX,ρY]=λiλj[X,Y], so ρr[X,Y]=(λiλj)r[X,Y]=[ρrX,ρrY] and, by bilinearity, ρrAut(gR); also ρr commutes with ρ and with ω.

L4step 3.1algebra
5.1

Let D act as logλj on the eigenspace for λj, so that exp(D)=ρ and D is self-adjoint for Bτ. For eigenvectors X,Y as in step 4.1, D[X,Y]=(logλi+logλj)[X,Y]=[DX,Y]+[X,DY], hence D is a derivation of gR by bilinearity; by step 1.1 there is a unique XgR with D=adX, and ρ=exp(adX) lies in the subgroup generated by the automorphisms exp(adW), WgR=g.

L4step 1.1step 4.1algebra
6.1

The powers of ρ satisfy ρrτ=τρr for all real r: from ρτ=ω2τ=ω(τω1)=(ωτ)ω1=τω1ω1=τρ1 one gets ρτX=λ1τX on an eigenvector of eigenvalue λ, and iteration gives the claim. Put φ:=ρ1/4, an automorphism of gR generated by the exp(adW). Then φτφ1σ=ρ1/4τρ1/4σ=ρ1/2τσ=ρ1/2ω1=ρ1/2ω=ωρ1/2=στρ1/2=σρ1/4τρ1/4=σφτφ1, using ρ1/2ω1=ρ1/2ω, the commutation of ω with powers of ρ, and τρ1/4=ρ1/4τ. Hence the involution ψ:=φτφ1 commutes with σ.

step 3.1step 4.1step 5.1algebra
7.1

ψ is again a Cartan involution of gR with Bψ(φZ,φW)=Bτ(Z,W) positive definite, because φ is an automorphism and τ is a Cartan involution by step 2.1. Since ψ commutes with σ and σ has fixed locus g0 by [L1], ψ preserves g0=gσ: for Xg0 one has σ(ψX)=ψ(σX)=ψX.

L1step 2.1step 6.1algebra
8.1

Define θ0:=ψg0 ⁣:g0g0, a real-linear map. It is an involution, since ψ2=id, and an automorphism of g0, since ψ is an automorphism of gR preserving g0.

step 7.1algebra
9.1

The form (B0)θ0(X,Y)=B0(X,θ0Y) is positive definite. Indeed, for X,Yg0 one has BR(X,ψY)=2ReB(X,ψY)=2B(X,ψY)=2B0(X,θ0Y) by steps 1.1, 1.2 and the reality of B on g0, so (B0)θ0(X,Y)=12Bψ(X,Y); the form Bψ is positive definite on all of gR by step 7.1, hence its restriction is positive definite. Therefore θ0 is a Cartan involution of g0, and the theorem follows.

step 1.1step 1.2step 7.1step 8.1A1algebra

Depends on

Used by

Dependency tree · two levels

36 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