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 compact real form

Statement

Assume the Axiom of Choice. Every finite-dimensional complex semisimple Lie algebra g has a compact real form (Compact real form of a complex semisimple Lie algebra): a real form k0 whose Killing form Bk0×k0 is negative definite.

Facts & Assumptions

Given: The Axiom of Choice and a finite-dimensional complex semisimple Lie algebra g with Killing form B.

[A1]

The Axiom of Choice is The Axiom of Choice; it enters through the Cartan and root data of [L1] and through the normalization statement [L3], whose statements carry the assumption.

[L1]

A Cartan subalgebra h exists; with such a choice, the root system Φ is finite, g=hαΦgα with one-dimensional root spaces, and for every root α there are eαgα, fαgα and Hαh with [eα,fα]=Hα, α(Hα)=2, [Hα,eα]=2eα, [Hα,fα]=2fα and β(Hα)Z for every root β; also [gα,gβ]gα+β and the Cartan integers are rational (Existence of Cartan subalgebras, Root-space decomposition, Root spaces of a complex semisimple Lie algebra are one-dimensional, The root sl_2 triple, Serre presentation theorem).

[L2]

B is symmetric, invariant and nondegenerate, the center of g is zero, the pairing gα×gα induced by B is nondegenerate, and in the triple above the trace formula gives B(Hα,Hα)=2B(eα,fα) (Cartan's semisimplicity criterion, Killing form, Opposite root spaces pair nondegenerately).

[L3]

The root-vector basis of [L1] can be rescaled so that, in the notation of [L1], [eα,fα]=Hα for every root α and the structure constants Nαβ, defined by [eα,eβ]=Nαβeα+β when α+βΦ and Nαβ:=0 when α+βΦ{0}, are integers satisfying Nαβ=Nα,β for all α,βΦ with α+β0; in this normalization the coroots Hα1,,Hαr attached to any base Δ={α1,,αr} form a basis of h (Chevalley basis and real structure constants).

Proof technique: direct.

1.1 Fix the data of [L1]. For every root α, invariance of B and [eα,fα]=Hα give B(Hα,Hα)=B([eα,fα],Hα)=B(eα,[fα,Hα])=2B(eα,fα), so B(eα,fα)=12B(Hα,Hα). The trace formula computes B on h: in a basis consisting of a basis H1,,Hr of h together with one nonzero vector eγgγ for each root γ, the operator adH has eigenvalues 0 on h and γ(H) on the one-dimensional space gγ, so the trace of adHadH is γΦγ(H)γ(H) and B(H,H) equals that sum for H,Hh. For H=αtαHα with real tα every γ(H)R by the integrality γ(Hα)Z recorded in [L1], and the two terms γ=±α give B(Hα,Hα)=γΦγ(Hα)28>0. Hence B(eα,fα)=12B(Hα,Hα)>0for every root α; no rescaling is needed for this, and the inverse rescaling (λαeα,λα1fα), λα>0, preserves [eα,fα] and leaves B(eα,fα) unchanged. [A1, L1, L2, algebra]

2.1 By the trace formula of step 1.1, B(H,H)=γΦγ(H)γ(H) for H,Hh. For H=αtαHα with real tα all values γ(H) are real by [L1]; if H0 then γ(H)0 for some root γ, because an element of h commuting with every root vector commutes with all of g and so lies in the zero center recorded in [L2]. Hence B(H,H)=γγ(H)2>0 for H0, that is, the restriction of B to hR:=αRHα is positive definite. [L1, L2, step 1.1, algebra]

2.2 (Normalized basis and closure of k0) Choose the root vectors as in [L3], so that [eα,fα]=Hα, the structure constants Nαβ are real and Nαβ=Nα,β whenever α+β0; write fγ=eγ and abbreviate Aα:=eαfα, Bα:=i(eα+fα), Tα:=iHα. Define k0:=spanR({Tα:αΦ}{Aα:αΦ}{Bα:αΦ}). Since these vectors span k0 and the bracket is bilinear, it suffices to show that the bracket of any two of them again lies in k0. For the Cartan brackets [Tα,Tβ]=0, while [Hα,eβfβ]=β(Hα)(eβ+fβ) and [Hα,eβ+fβ]=β(Hα)(eβfβ) give [Tα,Aβ]=β(Hα)Bβk0,[Tα,Bβ]=β(Hα)Aβk0, with real coefficients because β(Hα)ZR by [L1]. For the root-root brackets let α±β. Expanding and using Nα,β=Nα,β (the relation of [L3] with (α,β) replaced by (α,β), legitimate here because βα) together with Nα,β=Nαβ gives [Aα,Aβ]=NαβAα+βNα,βAαβ,[Aα,Bβ]=NαβBα+β+Nα,βBαβ, [Bα,Bβ]=NαβAα+βNα,βAαβ, where a term with vanishing structure constant is absent; all three are real linear combinations of generators. If β=±α then Aα=Aα and Bα=Bα give [Aα,Aα]=0=[Bα,Bα]. Finally [Aα,Bα]=[eαfα,i(eα+fα)]=i([eα,fα][fα,eα])=2iHα=2Tα, and Bα=Bα makes this also the case β=α. Hence all brackets of generators lie in k0, so k0 is a real Lie subalgebra of g. [A1, L1, L3, step 1.1, algebra]

3.1 The complex span of k0 is g: from AαiBα=2eα and Aα+iBα=2fα one has eα,fαCk0 for every root, and the Hα=iTα span h over C by [L3]. Hence k0 is a real form of g. [L1, L3, step 2.2, algebra]

4.1 The form is negative definite on k0. On the Cartan part B(Tα,Tβ)=B(Hα,Hβ), so the restriction to ihR, hR=αRHα, is minus BhR, which is negative definite by step 2.1. On each root direction, using step 1.1 and the weight decomposition, B(eα,eα)=0=B(fα,fα) because the two weight components do not pair, hence B(Aα,Aα)=2B(eα,fα)<0 and B(Bα,Bα)=2B(eα,fα)<0; also the mixed term B(Aα,Bα)=i[B(eα,eα)B(fα,fα)]=0. For X=aAα+bBα with real (a,b)(0,0) this gives B(X,X)=2B(eα,fα)(a2+b2)<0. Generators of distinct weights pair to zero, so the planes Wα=RAαRBα are pairwise orthogonal and orthogonal to ihR; for a set Φ+ of representatives of the pairs {α,α} the sum k0=ihRαΦ+Wα is direct, and Bk0 is negative definite. [L1, step 1.1, step 2.1, step 3.1, algebra]

5.1 By steps 3.1 and 4.1, k0 is a real form of g whose Killing form is negative definite, that is, a compact real form in the sense of Compact real form of a complex semisimple Lie algebra. The theorem follows. [step 3.1, step 4.1, A1] ∎

Remarks

The closure computation of step 2.2 rests on the normalized root-vector basis supplied by Chevalley basis and real structure constants, which proves Knapp's Theorem 6.6 together with Lemma 6.4 (printed pp. 350--353) and the equivalent Chevalley presentation of Etingof \S 39.4: after a rescaling of the root vectors one has [eα,eα]=Hα and structure constants that are integers satisfying Nαβ=Nα,β. The rescaling is genuine and its reality statement cannot be dispensed with: the normalization [eγ,fγ]=Hγ is preserved by every further rescaling eγaγeγ, fγaγ1fγ, while such a rescaling changes Nαβ into aαaβaα+β1Nαβ and can destroy the reality of the structure constants; thus the reality of the Nαβ is not a consequence of the sl_2-triple normalization and is imported from Chevalley basis and real structure constants. Two further points of the earlier draft were corrected during this run and are used above: the value B(eα,fα)=12B(Hα,Hα)>0 is not produced by a rescaling --- it holds in every normalization, by invariance of B and the trace formula --- and it is preserved by the rescaling (eα,fα)(λαeα,λα1fα); and the direct sum in step 4.1 runs over a set of representatives Φ+ of the pairs {α,α}, since Wα=Wα.

Depends on

Used by

Dependency tree · two levels

60 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