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.
Restricted roots of sl n r
Example
Let and let with the Cartan involution , so that (Cartan involution and k plus p for sl n r). Let
be the space of real diagonal traceless matrices, and let be the coordinate functional . Then is a maximal abelian subspace of and the restricted roots of are exactly the functionals with , each of them with one-dimensional restricted root space
where is the matrix unit; in particular the restricted root system is of type and is reduced (Restricted root and restricted root space, Maximal split abelian subspace and real rank).
Facts & Assumptions
Given: An integer , the real Lie algebra of real traceless matrices, the Cartan involution with the symmetric traceless matrices, the diagonal subspace , and the matrix units , .
is a real Lie algebra under , with for every element and for (General and special linear Lie groups, Lie algebras over a field).
consists of diagonal symmetric traceless matrices, hence is a subspace of ; the Cartan decomposition of is with (Cartan involution and k plus p for sl n r, Cartan decomposition of a real semisimple Lie algebra).
A restricted root of for a maximal abelian is a nonzero real functional on whose restricted root space is nonzero, and its multiplicity is ; a maximal abelian subspace of has dimension equal to the real rank (Restricted root and restricted root space, Maximal split abelian subspace and real rank).
In the complex analogue, the diagonal traceless subalgebra of is a Cartan subalgebra with roots and one-dimensional root spaces (Diagonal Cartan subalgebra and roots of sl_n).
Proof technique: direct matrix computation.
1.1 The subspace is a maximal abelian subspace of . It is abelian because its elements are diagonal, and it lies in by [L2]. Conversely, let satisfy for every . Choosing with pairwise distinct entries (possible with in dimension ), the identity of [L1] shows for all , so whenever : the centralizer of in is itself, which is therefore maximal abelian. [given, L1, L2, algebra]
1.2 Every functional with is a restricted root with : for , [L1] gives , and is a nonzero real matrix of trace zero, while since . [given, L1, L3, algebra]
2.1 There are no further restricted roots. Let and suppose for every . Comparing the -entry using [L1] gives Thus, if an off-diagonal coefficient is nonzero, then for every , so as functionals. If , choose with ; the diagonal-entry equations then force every . Distinct functionals have disjoint eigenspaces, so step 1.2 now gives . For , choose one diagonal with pairwise distinct entries. If then , so the same entry computation forces every off-diagonal coefficient of to vanish; as is traceless, it is a diagonal traceless matrix and hence belongs to . The reverse inclusion is immediate because diagonal matrices commute, so . Hence the nonzero restricted roots are exactly the , each with multiplicity one. [step 1.1, step 1.2, L1, L3, algebra]
3.1 The decomposition is consistent dimensionally: and there are roots each of multiplicity , so , which is the dimension of ; the restricted root system is the standard realization of and is reduced, since for every root its double is not of the form . [step 1.1, step 2.1, L3, algebra]
3.2 The computation matches the complex root computation of [L4]: the functionals are the restrictions to the real diagonal traceless subspace of the root functionals of the complexification, and the real root space is the real form of fixed by complex conjugation, which is why each multiplicity is . [step 2.1, L4, algebra]
4.1 Endpoints and scope: for there is a single pair of opposite roots with one-dimensional spaces and , and ; the case is excluded because has no nonzero diagonal traceless element. The computation uses no choice principle, and the diagonal element with pairwise distinct entries exists by an explicit choice of coordinates. [given, step 2.1, step 3.1, algebra] ∎
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
36 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)