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 has a compact real form (Compact real form of a complex semisimple Lie algebra): a real form whose Killing form is negative definite.
Facts & Assumptions
Given: The Axiom of Choice and a finite-dimensional complex semisimple Lie algebra with Killing form .
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.
A Cartan subalgebra exists; with such a choice, the root system is finite, with one-dimensional root spaces, and for every root there are , and with , , , and for every root ; also 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).
is symmetric, invariant and nondegenerate, the center of is zero, the pairing induced by is nondegenerate, and in the triple above the trace formula gives (Cartan's semisimplicity criterion, Killing form, Opposite root spaces pair nondegenerately).
The root-vector basis of [L1] can be rescaled so that, in the notation of [L1], for every root and the structure constants , defined by when and when , are integers satisfying for all with ; in this normalization the coroots attached to any base form a basis of (Chevalley basis and real structure constants).
Proof technique: direct.
1.1 Fix the data of [L1]. For every root , invariance of and give , so . The trace formula computes on : in a basis consisting of a basis of together with one nonzero vector for each root , the operator has eigenvalues on and on the one-dimensional space , so the trace of is and equals that sum for . For with real every by the integrality recorded in [L1], and the two terms give . Hence no rescaling is needed for this, and the inverse rescaling , , preserves and leaves unchanged. [A1, L1, L2, algebra]
2.1 By the trace formula of step 1.1, for . For with real all values are real by [L1]; if then for some root , because an element of commuting with every root vector commutes with all of and so lies in the zero center recorded in [L2]. Hence for , that is, the restriction of to is positive definite. [L1, L2, step 1.1, algebra]
2.2 (Normalized basis and closure of ) Choose the root vectors as in [L3], so that , the structure constants are real and whenever ; write and abbreviate , , . Define Since these vectors span and the bracket is bilinear, it suffices to show that the bracket of any two of them again lies in . For the Cartan brackets , while and give with real coefficients because by [L1]. For the root-root brackets let . Expanding and using (the relation of [L3] with replaced by , legitimate here because ) together with gives where a term with vanishing structure constant is absent; all three are real linear combinations of generators. If then and give . Finally , and makes this also the case . Hence all brackets of generators lie in , so is a real Lie subalgebra of . [A1, L1, L3, step 1.1, algebra]
3.1 The complex span of is : from and one has for every root, and the span over by [L3]. Hence is a real form of . [L1, L3, step 2.2, algebra]
4.1 The form is negative definite on . On the Cartan part , so the restriction to , , is minus , which is negative definite by step 2.1. On each root direction, using step 1.1 and the weight decomposition, because the two weight components do not pair, hence and ; also the mixed term . For with real this gives . Generators of distinct weights pair to zero, so the planes are pairwise orthogonal and orthogonal to ; for a set of representatives of the pairs the sum is direct, and is negative definite. [L1, step 1.1, step 2.1, step 3.1, algebra]
5.1 By steps 3.1 and 4.1, is a real form of 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 and structure constants that are integers satisfying . The rescaling is genuine and its reality statement cannot be dispensed with: the normalization is preserved by every further rescaling , , while such a rescaling changes into and can destroy the reality of the structure constants; thus the reality of the 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 is not produced by a rescaling --- it holds in every normalization, by invariance of and the trace formula --- and it is preserved by the rescaling ; and the direct sum in step 4.1 runs over a set of representatives of the pairs , since .
Depends on
- Compact real form of a complex semisimple Lie algebra
- Chevalley basis and real structure constants
- Serre presentation theorem
- Existence of Cartan subalgebras
- Root-space decomposition
- Root spaces of a complex semisimple Lie algebra are one-dimensional
- Opposite root spaces pair nondegenerately
- The Axiom of Choice
- The root sl_2 triple
- Cartan's semisimplicity criterion
- Killing form
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
- Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed., Chapter VI (standard reference, not scraped)
- Pavel Etingof, MIT 18.745 Lie Groups and Lie Algebras I, Lectures 19-24 (standard reference, not scraped)