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.

Conjugacy of compact real forms

Statement

Assume the Axiom of Choice. Let g be a finite-dimensional complex semisimple Lie algebra and let u1,u2 be two compact real forms of g. Then there is an inner automorphism φ of g with φ(u1)=u2; here an automorphism is called inner when it is a finite product of factors exp⁡(ad⁡W), W∈g. In particular any two compact real forms of g are isomorphic as real Lie algebras.

Facts & Assumptions

Given: The Axiom of Choice; a finite-dimensional complex semisimple Lie algebra g with Killing form B; two compact real forms u1,u2 with associated conjugations τ1,τ2; 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 from the compact-form theory of [L1].

[L1]

Each ui is a real form of g whose Killing form is negative definite, and the associated conjugation τi(X+iY)=X−iY (X,Y∈ui) is a conjugate-linear Lie-algebra involution with fixed locus ui, so that ui={Z:τiZ=Z} and g=ui⊕iui (Real forms correspond to conjugate-linear involutions, Real form of a complex Lie algebra, Compact real form of a complex semisimple Lie algebra, Existence of a compact real form).

[L2]

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

[L3]

A self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal basis of eigenvectors with real eigenvalues, and every self-adjoint endomorphism is normal (Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis, Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space).

Proof

technique · direct
1.1L2givenalgebra

Regarded as a real Lie algebra, gR has the same underlying set as g and its adjoint operators are the realifications of those of g: for Z∈g the real-linear map ad⁡Z on gR is the realification of the complex-linear ad⁡Z on g. Since the real trace of the realification of a complex-linear endomorphism is twice its complex trace, BR(Z,W)=2Re⁡B(Z,W) for all Z,W∈g. If Z lies in the radical of BR, then Re⁡B(Z,W)=0 for every W, and substituting iW gives −Im⁡B(Z,W)=0; hence B(Z,W)=0 for every W and Z=0 by nondegeneracy of B. Thus BR is nondegenerate and gR is semisimple by the criterion, so every derivation of gR is inner and Z(gR)=0.

1.2L1L2algebra

For each i the map τi is real-linear with τi2=id and preserves brackets, and for all Z,W∈g one has B(τiZ,τiW)=B(Z,W)‾: writing Z=X+iY and W=X′+iY′ with X,Y,X′,Y′∈ui and using complex bilinearity and symmetry of B, both sides equal B(X,X′)−B(Y,Y′)−i(B(X,Y′)+B(Y,X′)). Consequently BR(τiZ,τiW)=2Re⁡B(Z,W)‾=BR(Z,W): the form BR is τi-invariant.

2.1L1L2step 1.2algebra

Each τi is a Cartan involution of gR. Indeed, for Z=X+iY≠0 with X,Y∈ui one computes (BR)τi(Z,Z)=−BR(Z,τiZ)=−2Re⁡B(Z,τiZ)=−2(B(X,X)+B(Y,Y)), using B(Z,τiZ)=B(X+iY,X−iY)=B(X,X)+B(Y,Y). Both summands are ≤0 and each vanishes only at 0 because the Killing form of ui is negative definite, so (BR)τi(Z,Z)>0 for Z≠0; the form is symmetric and bilinear, hence positive definite, and τi is a Cartan involution.

3.1L2step 2.1algebra

Put ω:=τ2τ1∈Aut⁡(gR), an invertible automorphism, and put B1:=(BR)τ1. The identity τ1ω=ω−1τ1 holds because both sides equal τ1τ2τ1. Invariance of BR under ω−1 and under τ1 therefore gives, for all Z,W, B1(ωZ,W)=−BR(ωZ,τ1W)=−BR(Z,ω−1τ1W)=−BR(Z,τ1ωW)=B1(Z,ωW), so ω is self-adjoint for the inner product B1. Since ω is invertible, ρ:=ω2=ω∗ω satisfies B1(ρZ,Z)=B1(ωZ,ωZ)>0 for Z≠0: the automorphism ρ is self-adjoint and positive definite for B1.

3.2L2step 2.1algebra

Let θ,θ′ be Cartan involutions of a real semisimple Lie algebra with θθ′=θ′θ and let Y satisfy θY=Y, θ′Y=−Y. Then 0<Bθ(Y,Y)=−BR(Y,θY)=−BR(Y,Y) and 0<Bθ′(Y,Y)=−BR(Y,θ′Y)=+BR(Y,Y), a contradiction; hence the simultaneous (+1,−1) eigenspace of (θ,θ′) is zero. Exchanging the roles of θ and θ′ shows that the (−1,+1) eigenspace is zero too, so θ=θ′ on gR.

4.1L3step 3.1algebra

By [L3] there is a B1-orthonormal basis of gR consisting of eigenvectors of ρ, with eigenvalues λ1,…,λn>0. For real r define ρr as the endomorphism acting as λjr on the eigenspace of ρ for λj. If X,Y are eigenvectors with eigenvalues λi,λj, then from ρ∈Aut⁡(gR) one gets ρ[X,Y]=[ρX,ρY]=λiλj[X,Y], so [X,Y] lies in the eigenspace for λiλj; hence ρr[X,Y]=(λiλj)r[X,Y]=[ρrX,ρrY], and by bilinearity ρr is an automorphism of gR. Also ρr is a function of ρ, so it commutes with ρ and with ω.

5.1L3step 1.1step 4.1algebra

Define the endomorphism D of gR to act as log⁡λj on the eigenspace for λj, so that exp⁡(D)=ρ and D is self-adjoint for B1; for eigenvectors X,Y as in step 4.1, D[X,Y]=(log⁡λi+log⁡λj)[X,Y]=[DX,Y]+[X,DY], and by bilinearity D is a derivation of gR. By step 1.1 there is a unique X∈gR with D=ad⁡X, and then ρ=exp⁡(ad⁡X) lies in the subgroup generated by the automorphisms exp⁡(ad⁡W), W∈gR=g.

5.2step 3.1step 4.1algebra

The real powers of ρ satisfy ρrτ1=τ1ρ−r for all r: on an eigenvector X of ρ with eigenvalue λ and using τ1ρ=ρ−1τ1 (which follows from ρτ1=ω2τ1=ω(τ1ω−1)=(ωτ1)ω−1=τ1ω−1ω−1=τ1ρ−1, that is, ρτ1=τ1ρ−1) one gets ρτ1X=τ1ρ−1X=λ−1τ1X, and iteration gives ρrτ1X=λ−rτ1X=τ1ρ−rX. Put φ:=ρ1/4, so that φ is an automorphism of gR lying in the subgroup generated by the exp⁡(ad⁡W). Then φτ1φ−1τ2=ρ1/4τ1ρ−1/4τ2=ρ1/2τ1τ2=ρ1/2ω−1=ρ−1/2ω=ωρ−1/2=τ2τ1ρ−1/2=τ2ρ1/4τ1ρ−1/4=τ2φτ1φ−1, using ρ1/2ω−1=ρ−1/2ρω−1=ρ−1/2ω, the commutation of ω with powers of ρ, and τ1ρ−1/4=ρ1/4τ1.

6.1step 2.1step 5.2step 3.2algebra

By step 5.2 the involution ψ:=φτ1φ−1 commutes with τ2. It is again a Cartan involution of gR: Bψ(φZ,φW)=B1(Z,W) is positive definite because φ is an automorphism and τ1 is a Cartan involution by step 2.1. Hence step 3.2 gives ψ=τ2, that is, τ2=φτ1φ−1.

7.1L1step 5.1step 6.1A1algebra∎

Taking fixed loci and using [L1], u2={Z:τ2Z=Z}={Z:φτ1φ−1Z=Z}=φ{Z:τ1Z=Z}=φ(u1). The automorphism φ is complex-linear because ρ=ω2 is a composition of two conjugate-linear maps and its eigenspaces are therefore complex subspaces, so φ is complex-linear; it is a finite product of factors exp⁡(ad⁡W) with W∈g, hence an inner automorphism of g. Restricting φ to the real form u1 gives a real Lie-algebra isomorphism onto u2, and the theorem follows.

Depends on

Used by

Dependency tree · two levels

31 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