TheoremStatement: Literature-sourcedProof: 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.

Cartan decomposition identifies p with the noncompact symmetric space

Statement

Assume the Axiom of Choice. Let $(G, K)$ be a Riemannian symmetric pair of noncompact type with Cartan decomposition $g_{0} = k_{0} \oplus p_{0}$ (Riemannian symmetric pair of noncompact type). Then the map $Φ : p_{0} ⟶ G / K, X ⟼ \exp (X) K,$ is a diffeomorphism; here $G / K$ carries the manifold structure of the quotient by the closed subgroup $K$ (Quotient manifold by a closed Lie subgroup).

Facts & Assumptions

Given: The Axiom of Choice; a connected real semisimple Lie group $G$ with finite center, a global Cartan involution $Θ$ , $K = G^{Θ}$ , the Cartan decomposition $g_{0} = k_{0} \oplus p_{0}$ , and the quotient map $q : G \to G / K$ .

[A1]

The Axiom of Choice is assumed (The Axiom of Choice), supplying L1 and the countable-choice assumptions of L2 and L3.

[L1]

The map $K \times p_{0} \to G$ , $(k, X) \mapsto k \exp X$ , is a diffeomorphism; $K$ is closed with Lie algebra $k_{0}$ (Global Cartan decomposition for a connected finite center semisimple Lie group).

[L2]

The quotient map $q : G \to G / K$ is a surjective smooth submersion (Quotient manifold by a closed Lie subgroup). Local submersion coordinates have the form $(u, v) \mapsto u$ (Local normal form for submersions).

[L3]

For real $s, t$ , $\exp ((s + t) X) = \exp (s X) \exp (t X)$ , so $\exp (- X) = \exp (X)^{- 1}$ (Exponential scales one-parameter subgroups).

Proof

technique · direct

1.1

Let $D : K \times p_{0} \to G$ be $D (k, X) = k \exp X$ . Define $D_{R} : p_{0} \times K \to G$ by $D_{R} (X, k) = \exp X k$ . It is a diffeomorphism: explicitly $D_{R} (X, k) = D (k^{- 1}, - X)^{- 1}$ by [L3], a composition of $D$ with the product diffeomorphism $(X, k) \mapsto (k^{- 1}, - X)$ and the smooth inversion diffeomorphism of $G$ . Thus every $g$ is uniquely $\exp X k$ , and its first coordinate $F (g) = X$ is smooth.

L1L3algebra

2.1

For $h \in K$ , $g h = \exp X (k h)$ , so uniqueness gives $F (g h) = F (g)$ . Hence $F$ factors as $\overline{F} \circ q$ for a unique set map $\overline{F} : G / K \to p_{0}$ . It is smooth: near any quotient point, fix the $v$ -coordinate in a local submersion chart of [L2] to obtain a smooth section $s$ of $q$ ; on that neighborhood $\overline{F} = F \circ s$ . Smoothness is local, so no global section choice is needed.

L2step 1.1algebra

3.1

The map $Φ (X) = q (\exp X)$ is smooth by [L1] and [L2]. Uniqueness in step 1.1 gives $F (\exp X) = X$ , hence $\overline{F} \circ Φ = id$ . Conversely, if $g = \exp X k$ , then $Φ (\overline{F} (g K)) = \exp X K = g K$ . These smooth maps are mutually inverse, proving the assertion. The zero-dimensional case is included: if $p_{0} = 0$ , [L1] gives $G = K$ and both sides are singletons.

L1L2step 1.1step 2.1algebraA1∎

Depends on

Used by

Hyperbolic space as so zero n one mod so n Example

Dependency tree · two levels

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