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.

Restricted roots of sl n r

Example

Let n2 and let g0=sln(R) with the Cartan involution θ(X)=XT, so that p0={Xsln(R):XT=X} (Cartan involution and k plus p for sl n r). Let

a={diag(h1,,hn):h1++hn=0}

be the space of real diagonal traceless matrices, and let fia be the coordinate functional fi(H)=hi. Then a is a maximal abelian subspace of p0 and the restricted roots of (g0,a) are exactly the functionals fifj with ij, each of them with one-dimensional restricted root space

g0fifj=REij,

where Eij is the matrix unit; in particular the restricted root system is of type An1 and is reduced (Restricted root and restricted root space, Maximal split abelian subspace and real rank).

Facts & Assumptions

Given: An integer n2, the real Lie algebra g0=sln(R) of real traceless matrices, the Cartan involution θ(X)=XT with p0 the symmetric traceless matrices, the diagonal subspace a, and the matrix units Eij, ij.

[L1]

sln(R) is a real Lie algebra under [X,Y]=XYYX, with trX=0 for every element and [H,Eij]=(hihj)Eij for H=diag(h1,,hn) (General and special linear Lie groups, Lie algebras over a field).

[L2]

a consists of diagonal symmetric traceless matrices, hence is a subspace of p0; the Cartan decomposition of g0 is g0=k0p0 with k0=so(n) (Cartan involution and k plus p for sl n r, Cartan decomposition of a real semisimple Lie algebra).

[L3]

A restricted root of (g0,a) for a maximal abelian ap0 is a nonzero real functional λ on a whose restricted root space g0λ={Xg0:[H,X]=λ(H)X for all Ha} is nonzero, and its multiplicity is dimRg0λ; a maximal abelian subspace of p0 has dimension equal to the real rank (Restricted root and restricted root space, Maximal split abelian subspace and real rank).

[L4]

In the complex analogue, the diagonal traceless subalgebra of sln(C) is a Cartan subalgebra with roots εiεj and one-dimensional root spaces CEij (Diagonal Cartan subalgebra and roots of sl_n).

Proof technique: direct matrix computation.

1.1 The subspace a is a maximal abelian subspace of p0. It is abelian because its elements are diagonal, and it lies in p0 by [L2]. Conversely, let Xp0 satisfy [H,X]=0 for every Ha. Choosing H=diag(h1,,hn) with pairwise distinct entries hi (possible with ihi=0 in dimension n2), the identity [H,X]=i,j(hihj)XijEij of [L1] shows (hihj)Xij=0 for all i,j, so Xij=0 whenever ij: the centralizer of a in p0 is a itself, which is therefore maximal abelian. [given, L1, L2, algebra]

1.2 Every functional fifj with ij is a restricted root with REijg0fifj: for H=diag(h)a, [L1] gives [H,Eij]=(hihj)Eij=(fifj)(H)Eij, and Eij is a nonzero real matrix of trace zero, while fifj0 since ij. [given, L1, L3, algebra]

2.1 There are no further restricted roots. Let X=i,jxijEijg0 and suppose [H,X]=λ(H)X for every Ha. Comparing the (i,j)-entry using [L1] gives xij(fifj)(H)=xijλ(H)for every Ha. Thus, if an off-diagonal coefficient xij is nonzero, then λ(H)=(fifj)(H) for every H, so λ=fifj as functionals. If λ0, choose H with λ(H)0; the diagonal-entry equations then force every xii=0. Distinct functionals fifj have disjoint eigenspaces, so step 1.2 now gives g0fifj=REij. For λ=0, choose one diagonal Ha with pairwise distinct entries. If Xg00 then [H,X]=0, so the same entry computation forces every off-diagonal coefficient of X to vanish; as X is traceless, it is a diagonal traceless matrix and hence belongs to a. The reverse inclusion is immediate because diagonal matrices commute, so g00=a. Hence the nonzero restricted roots are exactly the fifj, each with multiplicity one. [step 1.1, step 1.2, L1, L3, algebra]

3.1 The decomposition is consistent dimensionally: dima=n1 and there are n(n1) roots each of multiplicity 1, so dimg0=(n1)+n(n1)=n21, which is the dimension of sln(R); the restricted root system {fifj:ij} is the standard realization of An1 and is reduced, since for every root fifj its double 2(fifj) is not of the form fkfl. [step 1.1, step 2.1, L3, algebra]

3.2 The computation matches the complex root computation of [L4]: the functionals fifj are the restrictions to the real diagonal traceless subspace of the root functionals εiεj of the complexification, and the real root space REij is the real form of CEij fixed by complex conjugation, which is why each multiplicity is 1. [step 2.1, L4, algebra]

4.1 Endpoints and scope: for n=2 there is a single pair of opposite roots ±(f1f2) with one-dimensional spaces RE12 and RE21, and dima=1; the case n=1 is excluded because sl1(R)=0 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