Alphabeta Math
ExampleConstruction: AI-adaptedVerification: 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.

Polar cartan decomposition of sl n r

Example

Assume the Axiom of Choice. Let n2 and let g0=sln(R)=k0p0 be the Cartan decomposition θ(X)=XT of Cartan involution and k plus p for sl n r, so that k0=so(n) and p0={Xsln(R):XT=X} (Cartan decomposition of a real semisimple Lie algebra). Then every gSLn(R) has a unique factorization

g=kexpX,kSO(n),Xp0,

with exp the matrix exponential; equivalently, the global Cartan decomposition of SLn(R) is its polar factorization, and the multiplication map SO(n)×p0SLn(R) is a diffeomorphism (Global Cartan decomposition for a connected finite center semisimple Lie group).

Facts & Assumptions

Given: The Axiom of Choice; an integer n2; the Lie group SLn(R) with Lie algebra sln(R); the Cartan decomposition g0=k0p0 with k0=so(n) and p0 the symmetric traceless matrices of Cartan involution and k plus p for sl n r; and an element gSLn(R).

[A1]

The Axiom of Choice is The Axiom of Choice; it enters only through the global Cartan decomposition of [L5] and the smooth structure of SLn(R).

[L1]

SLn(R)={A:detA=1} is an embedded Lie subgroup of GLn(R) with Lie algebra sln(R), and SO(n) is the determinant-one subgroup of O(n) with Lie algebra so(n) (General and special linear Lie groups, Orthogonal and special orthogonal Lie groups).

[L2]

Every endomorphism T of a finite-dimensional real inner product space has a polar decomposition T=SU with U=TT non-negative and S an isometry on the orthogonal complement of kerT; the factor U is unique and S is unique when T 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).

[L3]

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).

[L4]

For a matrix Lie group the Lie-group exponential is the matrix exponential eX=k0Xk/k! (Matrix exponential as the Lie-group exponential).

[L5]

If G is a connected real semisimple Lie group with finite center and K=GΘ for a global Cartan involution with differential θ that fixes Z(G) pointwise, then K×p0G, (k,X)kexpX, is a diffeomorphism (Global Cartan decomposition for a connected finite center semisimple Lie group, Cartan decomposition of a real semisimple Lie algebra).

[L7]

The real algebra sln(R) is semisimple and θ(X)=XT 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

technique · direct matrix computation
1.1

Put P:=gTg, the non-negative square root of the self-adjoint positive definite matrix gTg. By [L3] the matrix P is self-adjoint with an orthonormal eigenbasis and positive eigenvalues λ1,,λn>0, because g is invertible and gTgv,v=gv2>0 for v0.

givenL2L3algebra
1.2

The group SO(n) is path connected. For a unit vector v, a rotation of the plane spanned by v,e1 sends v to e1 and is joined to the identity by varying its angle. If v=e1, use a rotation through π in the (e1,e2) plane; if v=e1, use the identity. For RSO(n) apply this to its first column; after this rotation the matrix is diag(1,R) with RSO(n1). Induction, ending with SO(1)={1}, expresses every R as a product of rotations, each with a path to the identity.

L1algebra
2.1

The determinant of P is 1: det(P)2=det(P2)=det(gTg)=det(gT)det(g)=(detg)2=1 by [L6] and detg=1, while detP=λ1λn>0 by step 1.1, so detP=1.

step 1.1L6algebra
2.2

Define X:=logP by the spectral decomposition P=Qdiag(λ1,,λn)QT with Q orthogonal and X:=Qdiag(logλ1,,logλn)QT. Then X is self-adjoint, and Xk=Qdiag((logλ1)k,,(logλn)k)QT for every k0, so the matrix exponential of [L4] gives expX=Qdiag(λ1,,λn)QT=P.

step 1.1L3L4algebra
3.1

Define k:=gP1, which is well defined because P is invertible with positive eigenvalues. Then kTk=P1gTgP1=P1P2P1=I and detk=detgdetP1=1 by [L6], so kSO(n) by [L1].

step 1.1step 2.1L1L6algebra
3.2

The trace of X vanishes: trX=i=1nlogλi=log(λ1λn)=logdetP=0 by step 2.1, so Xp0 by [L7].

L7step 2.1step 2.2algebra
4.1

Existence: steps 3.1, 2.2 and 3.2 give g=kP=kexpX with kSO(n) and Xp0.

step 3.1step 2.2step 3.2
5.1

Define Θ(g)=(gT)1 on G=SLn(R). It is a smooth involutive automorphism, differentiates to XT, and has fixed group SO(n). To compute the center, a central matrix commutes with I+tEijG for every ij and real t, hence with every Eij. Comparing entries of zEij=Eijz forces all off-diagonal entries of z to vanish and its diagonal entries to be equal. Thus z=λI with real λn=1, so the center consists of I and, only when n is even, I. It is finite and fixed pointwise by Θ. Semisimplicity and the Cartan differential are [L7]. Finally, G is path connected without assuming the global theorem: by step 4.1, g=kexpX, and tkexp(tX) joins k to g inside G, since diagonalization gives detexp(tX)=exp(ttrX)=1. Step 1.2 joins I to k. Every hypothesis of [L5] is therefore established.

L1L3L4L5L7step 1.2step 4.1algebra
5.2

Uniqueness: suppose g=kexpX=kexpX with k,kSO(n) and X,Xp0. Both expX and expX are self-adjoint positive definite, since the eigenvalues of X and X are real by self-adjointness and exponentiate to positive numbers, and both k,k are orthogonal. By the uniqueness clause of [L2] for the invertible element g the non-negative factor is unique, so expX=expX=P and k=k; then X=X because the self-adjoint logarithm is unique: both X and X commute with P=expX=expX, hence preserve each eigenspace of P, and on the eigenspace for the eigenvalue λ>0 the equality eX=eX=λI forces every eigenvalue of the self-adjoint operator XEλ to lie in logλ+2πiZ, hence to equal the real number logλ.

step 3.1step 2.2step 4.1L2L3algebra
6.1

Consequently the map SO(n)×p0SLn(R), (k,X)kexpX, is a bijection by steps 4.1 and 5.2 and a diffeomorphism by [L5] applied as in step 5.1; its inverse is g(gP1,logP) with P=gTg.

step 4.1step 5.2step 5.1L5L2
7.1

The argument includes repeated eigenvalues, since the logarithm is scalar on each positive eigenspace. The zero logarithm gives the orthogonal elements of G. Although n2 is the stated scope, at n=1 both factors and the group are singletons. More generally the orthogonal polar factor is special orthogonal whenever detg>0, since detP=detg; the stronger condition detg=1 additionally makes trlogP=0. 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.

A1L6step 6.1algebra

Depends on

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