Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

The root sl_2 triple

Statement

Assume the Axiom of Choice. Let α be a root of a finite-dimensional complex semisimple Lie algebra g with respect to a Cartan subalgebra h, with coroot hα as in Coroot of a Lie-algebra root. Then there are eαgα and fαgα with

[eα,fα]=hα,[hα,eα]=2eα,[hα,fα]=2fα.

Consequently the span of eα,fα,hα is a copy of sl2 inside g (The special linear Lie algebra sl_2).

Facts & Assumptions

Given: The Axiom of Choice, such g,h,α and the Killing form B.

[A1]

The Axiom of Choice is The Axiom of Choice; it licenses the Killing-dual, coroot, and opposite-root pairing facts in [L1]--[L3].

[L1]

The pairing gα×gαC, (x,y)B(x,y), is nondegenerate (Opposite root spaces pair nondegenerately).

[L2]

[gα,gα]=CHα (The bracket of opposite root spaces is the root line); the Killing form is invariant and its restriction to h is nondegenerate (Trace forms are symmetric and invariant, Orthogonality of root spaces and nondegeneracy on the Cartan subalgebra).

[L3]

B(Hα,H)=α(H) for Hh, and hα=2Hα/α(Hα) with α(Hα)=B(Hα,Hα)0, so α(hα)=2 (Coroot of a Lie-algebra root, Killing-dual vector of a root).

[L4]

The root spaces are the eigenspaces of adh (Root and root space), and [gα,gα]g0 (Brackets of root spaces).

Proof

technique · direct
1.1

Choose 0egα, which is possible because α is a root. By [L1] the linear functional yB(e,y) on the nonzero space gα is not identically zero, hence surjective onto C; choose fgα with B(e,f)=2/α(Hα), a nonzero number by [L3].

A1L1L3algebra
2.1

For every Hh, invariance and the root-space identity give B([e,f],H)=B(e,[f,H])=α(H)B(e,f)=B(B(e,f)Hα,H). Both [e,f] and Hα lie in h by [L2], so nondegeneracy of Bh yields [e,f]=B(e,f)Hα=2α(Hα)Hα=hα. By [L4] and [L3], [hα,e]=α(hα)e=2e and [hα,f]=2f. Thus all three bracket relations of The special linear Lie algebra sl_2 hold for (e,f,hα).

L2L3L4step 1.1algebra
3.1

Since 0egα and 0fgα lie in distinct root spaces while hαh, the three elements are linearly independent, so their span is three-dimensional and by step 2.1 is closed under the bracket with the relations of sl2; by The special linear Lie algebra sl_2 it is a copy of sl2. Setting eα=e and fα=f proves the statement.

step 1.1step 2.1algebra

Depends on

Used by

Dependency tree · two levels

25 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