Alphabeta Math
LemmaStatement: 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.

Simple-root integrability relations

Statement

Assume the Axiom of Choice. Let g be a finite-dimensional complex semisimple Lie algebra with Cartan subalgebra h and a chosen positive system with simple roots α1,…,αr, let λ be dominant integral with mi=⟨λ,αi∨⟩ (Integral, dominant, and strictly dominant weights), and let V be a finite-dimensional highest weight module of highest weight λ with highest weight vector vλ (Highest-weight vectors and modules). For every simple root αi and a lowering vector fi∈g−αi with [ei,fi]=hαi for a suitable ei (The root sl2 triple), fi mi+1vλ=0.

Facts & Assumptions

Given: The Axiom of Choice, such g,h, a dominant integral λ with mi=⟨λ,αi∨⟩, a finite-dimensional highest weight module V of highest weight λ, and for each i a pair ei∈gαi, fi∈g−αi forming, together with hαi, a copy of sl2.

[A1]

The Axiom of Choice is assumed; it enters through the root-space theory supplying [L1] and through [L3] (The Axiom of Choice).

[L1]

For every i, [ei,fi]=hαi, [hαi,ei]=2ei and [hαi,fi]=−2fi (The root sl2 triple).

[L2]

vλ≠0 is killed by n+ and satisfies hαi⋅vλ=λ(hαi)vλ=mivλ (Highest-weight vectors and modules, Integral, dominant, and strictly dominant weights).

[L3]

A finite-dimensional sl2-module is a direct sum of irreducibles, and an irreducible submodule with highest weight m≥0 has dimension m+1 and weights m,m−2,…,−m (Finite-dimensional representations of sl2).

Proof

technique · direct
1.1A1L1L2

Fix i and consider W=U(span⁡{ei,fi,hαi})vλ, the sl2-submodule of V generated by vλ; it is finite dimensional because V is, and ei⋅vλ=0 while hαi⋅vλ=mivλ by [L1] and [L2].

2.1L3step 1.1

By [L3] write W=⨁a=1sWa as a direct sum of irreducible sl2-submodules, and write vλ=∑ava with va∈Wa. Because every Wa is stable under ei and hαi, uniqueness of the direct sum and step 1.1 give eiva=0 and hαiva=miva for every a.

3.1L3step 2.1

For every a with va≠0, step 2.1 makes va a highest weight vector of the irreducible module Wa with highest weight mi. By [L3], fimi+1va=0; the same equality is trivial when va=0. Summing over a gives fimi+1vλ=0 in W.

4.1step 3.1∎

Since W⊆V, the vanishing of step 3.1 holds in V; as i was arbitrary, fimi+1vλ=0 for every simple root, which is the assertion.

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