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.
Polar cartan decomposition of sl n r
Example
Assume the Axiom of Choice. Let and let be the Cartan decomposition of Cartan involution and k plus p for sl n r, so that and (Cartan decomposition of a real semisimple Lie algebra). Then every has a unique factorization
with the matrix exponential; equivalently, the global Cartan decomposition of is its polar factorization, and the multiplication map is a diffeomorphism (Global Cartan decomposition for a connected finite center semisimple Lie group).
Facts & Assumptions
Given: The Axiom of Choice; an integer ; the Lie group with Lie algebra ; the Cartan decomposition with and the symmetric traceless matrices of Cartan involution and k plus p for sl n r; and an element .
The Axiom of Choice is The Axiom of Choice; it enters only through the global Cartan decomposition of [L5] and the smooth structure of .
is an embedded Lie subgroup of with Lie algebra , and is the determinant-one subgroup of with Lie algebra (General and special linear Lie groups, Orthogonal and special orthogonal Lie groups).
Every endomorphism of a finite-dimensional real inner product space has a polar decomposition with non-negative and an isometry on the orthogonal complement of ; the factor is unique and is unique when is invertible (Every endomorphism has a polar decomposition T = SU with U non-negative and S an isometry on the orthogonal complement of ker T, and S is unique exactly when T is invertible).
A self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis with real eigenvalues (Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis).
For a matrix Lie group the Lie-group exponential is the matrix exponential (Matrix exponential as the Lie-group exponential).
If is a connected real semisimple Lie group with finite center and for a global Cartan involution with differential that fixes pointwise, then , , is a diffeomorphism (Global Cartan decomposition for a connected finite center semisimple Lie group, Cartan decomposition of a real semisimple Lie algebra).
Determinant is multiplicative, , and exactly when is invertible (Determinant multiplicativity follows from the top exterior power, If is invertible over a commutative ring, then , For , the determinant over a commutative ring by the Leibniz formula, and for a real matrix).
The real algebra is semisimple and is its Cartan involution with symmetric traceless anti-fixed space (Cartan involution and k plus p for sl n r, Cartan decomposition of a real semisimple Lie algebra).
Verification
Put , the non-negative square root of the self-adjoint positive definite matrix . By [L3] the matrix is self-adjoint with an orthonormal eigenbasis and positive eigenvalues , because is invertible and for .
The group is path connected. For a unit vector , a rotation of the plane spanned by sends to and is joined to the identity by varying its angle. If , use a rotation through in the plane; if , use the identity. For apply this to its first column; after this rotation the matrix is with . Induction, ending with , expresses every as a product of rotations, each with a path to the identity.
The determinant of is : by [L6] and , while by step 1.1, so .
Define by the spectral decomposition with orthogonal and . Then is self-adjoint, and for every , so the matrix exponential of [L4] gives .
Define , which is well defined because is invertible with positive eigenvalues. Then and by [L6], so by [L1].
The trace of vanishes: by step 2.1, so by [L7].
Existence: steps 3.1, 2.2 and 3.2 give with and .
Define on . It is a smooth involutive automorphism, differentiates to , and has fixed group . To compute the center, a central matrix commutes with for every and real , hence with every . Comparing entries of forces all off-diagonal entries of to vanish and its diagonal entries to be equal. Thus with real , so the center consists of and, only when is even, . It is finite and fixed pointwise by . Semisimplicity and the Cartan differential are [L7]. Finally, is path connected without assuming the global theorem: by step 4.1, , and joins to inside , since diagonalization gives . Step 1.2 joins to . Every hypothesis of [L5] is therefore established.
Uniqueness: suppose with and . Both and are self-adjoint positive definite, since the eigenvalues of and are real by self-adjointness and exponentiate to positive numbers, and both are orthogonal. By the uniqueness clause of [L2] for the invertible element the non-negative factor is unique, so and ; then because the self-adjoint logarithm is unique: both and commute with , hence preserve each eigenspace of , and on the eigenspace for the eigenvalue the equality forces every eigenvalue of the self-adjoint operator to lie in , hence to equal the real number .
Consequently the map , , is a bijection by steps 4.1 and 5.2 and a diffeomorphism by [L5] applied as in step 5.1; its inverse is with .
The argument includes repeated eigenvalues, since the logarithm is scalar on each positive eigenspace. The zero logarithm gives the orthogonal elements of . Although is the stated scope, at both factors and the group are singletons. More generally the orthogonal polar factor is special orthogonal whenever , since ; the stronger condition additionally makes . AC covers the cited Lie-group and global Cartan interfaces; no arbitrary eigenbasis selection over an indexed family is needed in the finite matrix calculations.
Depends on
- Global Cartan decomposition for a connected finite center semisimple Lie group
- The Axiom of Choice
- General and special linear Lie groups
- Orthogonal and special orthogonal Lie groups
- Cartan involution and k plus p for sl n r
- Cartan decomposition of a real semisimple Lie algebra
- Every endomorphism has a polar decomposition T = SU with U non-negative and S an isometry on the orthogonal complement of ker T, and S is unique exactly when T is invertible
- Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis
- Matrix exponential as the Lie-group exponential
- For $n\ge1$, the determinant over a commutative ring by the Leibniz formula, and $|\det A|$ for a real matrix
- If $A$ is invertible over a commutative ring, then $\det(A^{-1})=\det(A)^{-1}$
- Determinant multiplicativity follows from the top exterior power
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
67 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)