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.
Hyperbolic space as so zero n one mod so n
Example
Assume the Axiom of Choice and let . Write for the Lorentz form on , let
be the upper sheet of the hyperboloid, and let be the identity component of the group of -preserving matrices, . Then is a maximal compact subgroup of and the orbit map induces a diffeomorphism ; under it the Cartan metric of Riemannian symmetric pair of noncompact type is a -invariant Riemannian metric on real hyperbolic -space of constant sectional curvature ; equivalently the Cartan metric is times the standard normalization of curvature , namely the metric (Cartan decomposition gives the invariant metric and curvature of G mod K, Cartan decomposition identifies p with the noncompact symmetric space).
Facts & Assumptions
Given: The Axiom of Choice; an integer ; the Lorentz form with matrix ; the groups , and its identity component ; the hyperboloid and its point .
The Axiom of Choice is The Axiom of Choice; it enters through the closed-subgroup theorem, the quotient-manifold structure and the global Cartan decomposition used below.
Every closed subgroup of a finite-dimensional real Lie group is an embedded Lie subgroup; is a Lie group with Lie algebra ; and is a closed subgroup with Lie algebra (Cartan closed subgroup theorem, General and special linear Lie groups, Orthogonal and special orthogonal Lie groups). Closed and bounded subsets of a finite-dimensional real matrix space are compact by Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line.
A regular level set of a smooth map is an embedded submanifold whose tangent space at a point is the kernel of the differential (A regular level set is an embedded submanifold, The tangent space of a regular level set is the kernel).
The Killing form is , and a finite-dimensional characteristic-zero Lie algebra is semisimple exactly when its Killing form is nondegenerate (Killing form, Cartan's semisimplicity criterion).
For a Riemannian symmetric pair of noncompact type with Cartan decomposition , the form defines a -invariant Riemannian metric on with value at the origin, the curvature at the origin is for , and the sectional curvature of a plane with basis is ; moreover is diffeomorphic to by (Riemannian symmetric pair of noncompact type, Cartan decomposition gives the invariant metric and curvature of G mod K, Cartan decomposition identifies p with the noncompact symmetric space, Sectional curvature).
carries the unique smooth structure making the quotient map a submersion and the left -action smooth, and the orbit map , , is smooth and -equivariant (Homogeneous spaces of Lie groups, Quotient manifold by a closed Lie subgroup).
The matrix exponential is the Lie-group exponential of a matrix group, and the exponential map carries a neighborhood of diffeomorphically onto a neighborhood of the identity (Matrix exponential as the Lie-group exponential, The exponential map is a local diffeomorphism at zero). Consequently the subgroup generated by is the identity component: contains an open identity neighborhood and is therefore an open subgroup, while every path lies in the identity component, so ; the cosets of make both and its complement open in the connected group , forcing .
For a connected real semisimple Lie group with finite center and a global Cartan involution, its fixed subgroup is maximal compact (Maximal compact subgroups exist and are conjugate in a connected finite center semisimple Lie group).
Verification
The group is closed in , so [L1] makes it an embedded Lie subgroup. Differentiating gives ; conversely this condition implies by differentiation in , so it characterizes the Lie algebra. It consists of with . Determinant has values on , hence equals on its identity component . This component has the same Lie algebra. Write and for .
The level function has differential , nonzero at every . Thus [L2] gives tangent space and dimension . The upper sheet is the graph , hence connected. Its Lorentz tangent metric is positive: if , then and for . Every preserves this sheet, since the sign of the last coordinate of cannot change continuously on connected .
The group is compact, being closed and bounded in matrix space and hence compact by Heine--Borel in [L1], and is path connected: plane rotations can carry any unit first column to the first coordinate vector; after doing so the remaining block is in , and induction ends with . Each plane rotation has a path to the identity through its angle. Therefore lies in .
The basis satisfies and for . For fixed , its adjoint square is on each two-dimensional span of the rotations joining to a third spatial index, and on ; it vanishes on the remaining basis vectors. Its trace is . For fixed , its adjoint square is on each span of and the rotation joining (), and zero on the rest, giving trace . Mixed Killing pairings of different basis vectors vanish: conjugation by , , is a Lie-algebra automorphism, preserves the adjoint trace, and acts with distinct sign characters on and on . A sign choice therefore negates any mixed pairing while preserving it. This proves on the whole basis, hence bilinearly, . It is nondegenerate for every , including , so [L3] proves semisimplicity. The involution has eigenspaces and , with for . Since , no proper ideal contains , so the noncompact-type criterion of [L4] is satisfied.
The action is transitive: for with , put and with . The matrix exponential gives and belongs to ; uses the identity. The stabilizer of consists exactly of with , since it preserves and determinant one; these matrices are in by step 1.3. Thus it is .
The smooth orbit map factors through the quotient submersion to a smooth bijection by [L5] and step 2.2. Its derivative at , using , is , an isomorphism. Equivariance makes the derivative an isomorphism everywhere, so the inverse function theorem gives a local diffeomorphism everywhere; a bijective local diffeomorphism has a smooth inverse.
The center of is trivial. If is central, is fixed by ; the only spatial vector fixed by all spatial rotations for is zero. Since , it equals , so . Commuting with every and differentiating forces for every , hence . The group automorphism preserves , is involutive and differentiates to . Its fixed elements lie in both and , hence commute with and have block form ; the upper-sheet condition gives and determinant one gives . Thus . Together with step 2.1 this verifies all hypotheses of the symmetric-pair interface [L4].
Step 3.2 proves that is connected semisimple with finite center, that is a global Cartan involution, and that . Therefore [L7] applies directly and makes maximal compact.
The metric of [L4] is now applicable by step 3.2. At the origin by step 2.1. Under , the Lorentz metric is . Both metrics are -invariant, so the Cartan metric is times the Lorentz metric everywhere. For independent let . The bracket is , whose squared -norm is , while the Gram determinant of is . The sectional formula in [L4] therefore gives at the origin and, by transitivity, everywhere.
Scaling a metric by a constant preserves its Levi-Civita connection and its curvature operator of type : the same connection remains torsion free and metric compatible. The sectional numerator scales by and its Gram denominator by . Thus , the Lorentz metric from step 4.2, has curvature . At the Cartan curvature is ; at the direct trace proof remains valid. Rank is excluded because the algebra is abelian with zero Killing form and there are no tangent two-planes. AC covers the Lie-group, quotient, maximal-compact and symmetric-space interfaces; the finite matrix computations require no further choice.
Depends on
- Maximal compact subgroups exist and are conjugate in a connected finite center semisimple Lie group
- Riemannian symmetric pair of noncompact type
- Cartan decomposition gives the invariant metric and curvature of G mod K
- Cartan decomposition identifies p with the noncompact symmetric space
- The Axiom of Choice
- Sectional curvature
- Cartan involution of a real semisimple Lie algebra
- Cartan decomposition of a real semisimple Lie algebra
- Killing form
- Cartan's semisimplicity criterion
- Orthogonal and special orthogonal Lie groups
- General and special linear Lie groups
- Cartan closed subgroup theorem
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
- A regular level set is an embedded submanifold
- The tangent space of a regular level set is the kernel
- Homogeneous spaces of Lie groups
- Quotient manifold by a closed Lie subgroup
- Matrix exponential as the Lie-group exponential
- The exponential map is a local diffeomorphism at zero
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
104 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)