Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-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.

Maximal split abelian subspace and real rank

Definition

Assume the Axiom of Choice. Let g0 be a finite-dimensional real semisimple Lie algebra with a Cartan involution θ and Cartan decomposition g0=k0⊕p0 (Cartan involution of a real semisimple Lie algebra, Cartan decomposition of a real semisimple Lie algebra). A maximal split abelian subspace of g0 is a subspace a⊆p0 that is abelian for the bracket, that is [a,a]=0, and is maximal with this property among subspaces of p0; equivalently (since p0 is finite-dimensional, every abelian subspace of p0 is contained in a maximal one) a is a maximal abelian subspace of p0. The real rank of g0 is

rank⁡Rg0:=dim⁡a,

which is independent of the choice of a. The Lie-algebra form of the noncompact symmetric-pair construction in Riemannian symmetric pair of noncompact type applies to the pair (g0,θ) after its compact ideals are split off: those ideals lie in k0 and contribute nothing to p0, while the remaining ideal gnc has no compact ideal. This Lie-algebra datum does produce a symmetric pair. Namely, let G=Aut⁡(gnc)0. Its Lie algebra is Der⁡(gnc)=ad⁡gnc, and centerlessness identifies this with gnc (Lie algebra of the automorphism group, Derivations of semisimple Lie algebras are inner, Semisimple Lie algebras are centerless and perfect). The center of G is trivial: a central automorphism commutes with every etad⁡X, so differentiation gives ad⁡(AX)=ad⁡X for every X, and injectivity of ad⁡ gives A=1. Conjugation A↦θAθ is a global involution of G whose differential is θ under this identification. Thus (G,GΘ) is the required noncompact-type symmetric pair, and Maximal abelian subspaces of p are conjugate by K conjugates any two maximal abelian subspaces of its p0. They therefore have equal dimension. This downstream theorem is the well-definedness justification recorded in justified_by.

The terminology is related to the split real forms of Split real form: a real form g0 is split precisely when rank⁡Rg0 equals the complex rank of the complexification g0C, equivalently when a maximal abelian subspace a⊆p0 (any one, by Maximal abelian subspaces of p are conjugate by K) is a Cartan subalgebra of g0; in general rank⁡Rg0∈{0,1,…,rank⁡g0C}, with value 0 exactly for compact g0.

Depends on

Used by

Dependency tree · two levels

20 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