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.
Classical real forms of the classical complex lie algebras
Statement
Assume the Axiom of Choice. Let be a complex simple Lie algebra of classical type , , or , realized as , , or (Classical types correspond to sl, so and sp, Classical complex matrix Lie algebras). Then, up to isomorphism and up to the admissible ranges and low-rank coincidences stated below, the real forms of are:
- for : and with , ; and with ;
- for : with , ;
- for : and with , ;
- for : with , , and .
The compact form occurs in each list at the signature , and the split form is for type , for , for and for ; within the inner families and the real rank is maximal exactly when (for type the corresponding painted root is the middle one). Among the low-rank coincidences are , , , , together with , , , , , and , together with the duplicate in the type- list.
Facts & Assumptions
Given: The Axiom of Choice; the classical complex matrix Lie algebras of Classical complex matrix Lie algebras with their types as in Classical types correspond to sl, so and sp; and the correspondence between real forms and conjugate-linear involutions of Real forms correspond to conjugate-linear involutions.
The Axiom of Choice is The Axiom of Choice; it enters through the classification theorem of [L3]. The explicit finite matrix constructions in steps 1.1 and 2.1 make no additional choice.
A real Lie subalgebra of a complex Lie algebra is a real form if and only if it is the fixed locus of a conjugate-linear involution of (Real forms correspond to conjugate-linear involutions, Real form of a complex Lie algebra).
The complex matrix algebras , and and their classical types are fixed by Classical complex matrix Lie algebras and Classical types correspond to sl, so and sp. A complex change of basis between two nondegenerate complex symmetric or alternating forms gives an isomorphic complex orthogonal or symplectic algebra, so Euclidean matrix models may be used to display conjugations.
Knapp's classification theorem and its tables identify the real forms of the four classical types with exactly the matrix families in the Statement, in the stated range normalization (Source, Figure 6.1 and Theorem 6.105(c), printed pp. 413--415 and 421--422). Etingof obtains the same families directly from the inner classes of (Source, Lecture 40, §40.3, printed pp. 188--189). This is the classical specialization of Classification of real semisimple lie algebras.
The compact form is characterized by negative-definite Killing form and the split form by a split Cartan subalgebra (Compact real form of a complex semisimple Lie algebra, Split real form). Knapp's restricted-root computation gives real rank for and and the source's table (6.110) records the stated real low-rank coincidences (printed pp. 422--426). The complex low-rank coincidences are those of [L2].
Proof
Put and . In the Euclidean orthogonal model, and in the standard symplectic model with form , the following are well-typed conjugate-linear involutive automorphisms: The displayed matrices have respectively sizes , , and ; in particular the last is by , with no odd-dimensional completion. Direct substitution in the defining symmetric or alternating form shows that each map preserves its complex algebra and squares to the identity.
The fixed loci in step 1.1 are respectively , , , , , and . For the orthogonal signature form, conjugation by identifies the fixed locus in the Euclidean skew-symmetric model with . By [L1] every fixed locus is therefore a real form of the indicated complex algebra.
The type-by-type classification [L3] says that the fixed loci of step 2.1 exhaust the real forms: type has the real, Hermitian-signature and, when is even, quaternionic forms; types and have the orthogonal signatures, with also having ; and type has the real symplectic and quaternionic-Hermitian forms. Thus no additional real-form class is missing.
Exchanging the positive and negative blocks gives , and . The compact classes are the members by [L4]. The real diagonal Cartan subalgebras show that , and are split, and the orthogonal form of signature is split in type .
The restricted-root computation in [L4] gives real rank for and , so within either signature family it is maximal exactly when . The same source table supplies the real low-rank coincidences in the Statement, while the complex coincidences are those of [L2]. These identifications account for the admissible-range repetitions and do not remove any class from step 3.1.
Steps 2.1 and 3.1 prove occurrence and exhaustion, step 3.2 identifies the compact and split members, and step 4.1 supplies the rank and low-rank clauses. Hence the displayed families are exactly the real forms of the four classical complex simple types, with the asserted normalization.
Remarks
Exhaustion. Every real form is accounted for by the classification theorem's enumeration of the real forms of the type, together with the source's identification of the classical entries with the matrix algebras , , , , , and (Knapp, Figure 6.1 of the source, printed pp. 413-415, and tables (6.107) and (6.110), printed pp. 424 and 426). The constructions of the proof exhibits each entry independently as the fixed locus of a conjugate-linear involution.
What is proved here. Every family is exhibited by a dimensionally correct conjugate-linear involution (in particular the operator uses the by matrix ), and the classification theorem supplies exhaustion. The compact, split, real-rank and low-rank clauses are then read with the exact range conventions of the cited tables.
Depends on
- Classification of real semisimple lie algebras
- Classical types correspond to sl, so and sp
- Real forms correspond to conjugate-linear involutions
- Classical complex matrix Lie algebras
- Real form of a complex Lie algebra
- Compact real form of a complex semisimple Lie algebra
- Split real form
- The Axiom of Choice
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
25 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, Lie Groups and Lie Algebras (standard reference, not scraped)