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 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 with Killing form ; its complexification with Killing form and canonical conjugation ; and the real Lie algebra underlying , with Killing form .
The Axiom of Choice is The Axiom of Choice; it is inherited through the compact-form existence of [L2].
The complexification is semisimple, is a real direct sum with the complex-bilinear extension of , and is a conjugate-linear bracket-preserving involution with fixed locus (Complexification preserves semisimplicity, Real forms correspond to conjugate-linear involutions, Complexification of a real Lie algebra, Killing form).
has a compact real form with conjugation and negative definite Killing form on , so that is a conjugate-linear bracket-preserving involution with fixed locus and (Existence of a compact real form, Compact real form of a complex semisimple Lie algebra, Real forms correspond to conjugate-linear involutions).
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, with (Trace forms are symmetric and invariant, Cartan's semisimplicity criterion, Derivations of semisimple Lie algebras are inner, Semisimple Lie algebras are centerless and perfect).
A self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal basis of eigenvectors with real eigenvalues (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
The adjoint operators of are the realifications of those of , so the real trace of the realification of a complex-linear endomorphism is twice its complex trace and for all . If lies in the radical of then for all , and substituting gives ; hence by nondegeneracy of , so is nondegenerate and is semisimple, with every derivation inner and .
The restriction of to is , because in a real basis of the matrices of , , acting on have the real block form of the realification of acting on . In particular is real-valued on , and is nondegenerate since is semisimple.
The map is real-linear on with and preserves brackets, and for all : writing , with , both sides equal by complex bilinearity and symmetry of . Hence .
is a Cartan involution of : for with one has , since and the Killing form of is negative definite. Write for this inner product.
Put , an invertible automorphism, and note , because both sides equal . Invariance of under and under gives for all , so is self-adjoint for ; since is invertible, satisfies for , so is a self-adjoint positive definite automorphism of .
By [L4] choose a -orthonormal eigenbasis of with eigenvalues and let , , act as on the eigenspace for . If are eigenvectors with eigenvalues , then , so and, by bilinearity, ; also commutes with and with .
Let act as on the eigenspace for , so that and is self-adjoint for . For eigenvectors as in step 4.1, , hence is a derivation of by bilinearity; by step 1.1 there is a unique with , and lies in the subgroup generated by the automorphisms , .
The powers of satisfy for all real : from one gets on an eigenvector of eigenvalue , and iteration gives the claim. Put , an automorphism of generated by the . Then using , the commutation of with powers of , and . Hence the involution commutes with .
is again a Cartan involution of with positive definite, because is an automorphism and is a Cartan involution by step 2.1. Since commutes with and has fixed locus by [L1], preserves : for one has .
Define , a real-linear map. It is an involution, since , and an automorphism of , since is an automorphism of preserving .
The form is positive definite. Indeed, for one has by steps 1.1, 1.2 and the reality of on , so ; the form is positive definite on all of by step 7.1, hence its restriction is positive definite. Therefore is a Cartan involution of , and the theorem follows.
Depends on
- Complexification preserves semisimplicity
- Real forms correspond to conjugate-linear involutions
- Existence of a compact real form
- Conjugacy of compact real forms
- Cartan's semisimplicity criterion
- Derivations of semisimple Lie algebras are inner
- Semisimple Lie algebras are centerless and perfect
- Trace forms are symmetric and invariant
- Killing form
- Complexification of a real Lie algebra
- Cartan involution of a real semisimple Lie algebra
- Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space
- Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis
- The Axiom of Choice
- Compact real form of a complex semisimple Lie algebra
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
- 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)