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.

Cartan subalgebra and roots of sl2

Example

In sl2(C)=Ch⊕Ce⊕Cf of The special linear Lie algebra sl2, with [h,e]=2e, [h,f]=−2f, [e,f]=h, the line h=Ch is a Cartan subalgebra; the roots are ±α, where α∈h∗ is determined by α(h)=2, with root spaces gα=Ce and g−α=Cf, so that sl2=h⊕Ce⊕Cf is its directly computed root-space decomposition. With the Killing form of Killing form, B(h,h)=8, and the Killing-dual vector and coroot of α are Hα=14h and hα=h, where here these names mean the directly verified identities B(Hα,H)=α(H) for every H∈h and hα=2Hα/α(Hα).

Facts & Assumptions

Given: The Lie algebra sl2(C)=Ch⊕Ce⊕Cf with the brackets of The special linear Lie algebra sl2, its one-dimensional subalgebra h=Ch, the functional α∈h∗ determined by α(h)=2, and the Killing form of Killing form.

[L1]

A finite-dimensional Lie algebra over a characteristic-zero field is semisimple if and only if its Killing form is nondegenerate (Cartan's semisimplicity criterion).

Verification

technique · direct
1.1givenL1algebra

Killing-form computation: ad⁡h=diag⁡(0,2,−2) on the basis (h,e,f), ad⁡e(h)=−2e, ad⁡e(e)=0, ad⁡e(f)=h, and ad⁡f(h)=2f, ad⁡f(e)=−h, ad⁡f(f)=0. Hence B(h,h)=8, B(e,f)=B(f,e)=4, and all other basis pairings vanish. The Killing matrix (800004040) has determinant −128≠0, so [L1] proves that sl2(C) is semisimple.

1.2givenalgebra

The subspace h=Ch is a Cartan subalgebra: it is one-dimensional, hence abelian and nilpotent, and Ng(h)={ah+be+cf:[ah+be+cf,h]∈Ch} equals Ch, because [h,h]=0, [e,h]=−2e and [f,h]=2f, so a normalizing element has b=c=0.

2.1givenstep 1.1step 1.2algebra

The eigenspaces of ad⁡h are Ch with eigenvalue 0, Ce with eigenvalue 2 and Cf with eigenvalue −2. Defining α∈h∗ by α(h)=2 and using Root and root space, the nonzero eigenspaces are gα=Ce and g−α=Cf, so Φ={±α} and the root-space decomposition is the displayed one.

3.1givenstep 1.1algebra∎

The dual vector Hα satisfies B(Hα,h)=α(h)=2; writing Hα=th gives 8t=2, so t=14 and Hα=14h; then α(Hα)=14⋅2=12=B(Hα,Hα), so the coroot is hα=2Hα/α(Hα)=2⋅14h/12=h.

Depends on

Used by

Dependency tree · two levels

16 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