Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass
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.

Diagonal Cartan subalgebra and roots of sln

Example

For n≥2 let sln(C)={X∈Mn(C):tr⁡X=0} be the Lie algebra of traceless complex n×n matrices under the commutator, so that n=2 recovers The special linear Lie algebra sl2. Let h={diag⁡(x1,…,xn):∑ixi=0} be the diagonal traceless subalgebra, and let εi∈h∗ be the restriction of the coordinate functional H↦xi. Then h is a Cartan subalgebra of sln(C), the roots are the functionals εi−εj with i≠j, and the corresponding root spaces are the lines gεi−εj=CEij, so Φ={εi−εj:i≠j} has n(n−1) elements.

Facts & Assumptions

Given: The integers n≥2, the Lie algebra sln(C) of traceless matrices under the commutator, its diagonal traceless subalgebra h, and the matrix units Eij; root spaces are those of Root and root space, and nilpotence and normalizers are those of Cartan subalgebra and Normalizer of a Lie subalgebra.

[L1]

The Killing form of sln(C) is K(X,Y)=2ntr⁡(XY) and is nondegenerate for n≥2; a finite-dimensional characteristic-zero Lie algebra is semisimple if and only if its Killing form is nondegenerate (Classical simple Lie algebras and their Killing forms, Cartan's semisimplicity criterion).

Verification

technique · direct
1.1L1

By [L1], sln(C) is semisimple.

1.2givenalgebra

h is a Cartan subalgebra: it is abelian, hence nilpotent, and its normalizer is itself. Indeed if X=∑abxabEab satisfies [X,H]∈h for every diagonal traceless H, take H=diag⁡(1,2,…,n)−n+12I, whose diagonal entries are pairwise distinct; then [X,H]=∑ab(hb−ha)xabEab has no off-diagonal component, so (hb−ha)xab=0 and hence xab=0 whenever a≠b. Thus X is diagonal, and being in sln it lies in h.

1.3givenalgebra

For H=diag⁡(x1,…,xn)∈h and a matrix unit Eij one computes [H,Eij]=(xi−xj)Eij; note xi−xj depends only on H, so the functional εi−εj on h is well defined and Eij is a nonzero eigenvector for the eigenvalue (εi−εj)(H).

2.1givenstep 1.1step 1.2step 1.3algebra∎

By steps 1.1 and 1.2, the root-space decomposition of Root-space decomposition applies. Step 1.3 exhibits, for every pair i≠j, the nonzero vector Eij∈gεi−εj; conversely every simultaneous h-eigenvector is a linear combination of those Eij whose indices give that functional, and the functionals εi−εj for distinct ordered pairs are distinct while the diagonal matrices give the zero weight. Hence the roots are exactly the n(n−1) functionals εi−εj, i≠j, with one-dimensional root spaces CEij.

Depends on

Used by

Dependency tree · two levels

31 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