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.

Highest weight modules lie below the top weight

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, and let V be a representation generated by a highest weight vector v of weight λ (Highest-weight vectors and modules). Then V=U(n−)v=U(n−)Cv, every weight μ of V is of the form μ=λ−∑iniαi with ni∈Z≥0, so that μ≤λ in the root order (Root order on weights), and Vλ=Cv.

Facts & Assumptions

Given: The Axiom of Choice, such g,h, a chosen positive system, and a module V generated by a highest weight vector v of weight λ.

[A1]

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

[L1]

The chosen positive system gives the direct sum g=n−⊕h⊕n+ with n± the span of the root spaces g±α, α∈Φ+ (Triangular decomposition, Positive and negative nilpotent subalgebras and the Borel).

[L2]

For an ordered basis x1,…,xN of a finite-dimensional complex Lie algebra, the monomials x1a1⋯xNaN form a basis of its universal enveloping algebra (Poincaré–Birkhoff–Witt theorem); applied to g with an ordered basis beginning with a basis of n−, continuing with a basis of h and ending with a basis of n+, this gives U(g)=U(n−)U(h)U(n+) as a linear span, and applied to n− it gives that the monomials in a basis of n− span U(n−).

[L3]

The action of g on V extends to a unital action of U(g), and the subrepresentation generated by v is U(g)v (Lie representations are U(g)-modules, Highest-weight vectors and modules).

[L4]

If x∈gα and w∈Vμ, then x⋅w∈Vμ+α (Root vectors shift weights).

[L5]

Every positive root is a nonzero nonnegative integral combination of the simple roots, each root space is one-dimensional, and the simple roots are linearly independent (Simple roots form a signed integral basis, Root spaces of a complex semisimple Lie algebra are one-dimensional).

Proof

technique · direct
1.1A1L3

V=U(g)v by [L3], because V is the subrepresentation generated by v.

2.1A1L1L2L3step 1.1

Applying [L2] and using that n+⋅v=0 and H⋅v=λ(H)v for H∈h gives U(g)v=U(n−)U(h)U(n+)v=U(n−)Cv.

3.1A1L2L4L5step 2.1

Fix a basis f1,…,fN of n− consisting of root vectors fj∈g−α(j) with α(j)∈Φ+; by [L2] the monomials in the fj span U(n−), so every element of V is a linear combination of vectors fj1a1⋯fjkak⋅v, and by [L4] and [L5] the weight of such a vector is λ−∑rarα(jr), a functional of the form λ−∑iniαi with ni≥0.

4.1step 3.1

By step 3.1 every weight of V lies in λ−Q+ and satisfies μ≤λ in the root order (Root order on weights).

4.2L5step 3.1

For the top weight, a monomial fj1a1⋯fjkak has weight λ exactly when ∑rarα(jr)=0; since the α(jr) are nonzero elements of Q+ and the simple roots are linearly independent by [L5], this forces ar=0 for every r, so the only monomial of weight λ is the empty one and Vλ=Cv.

5.1step 2.1step 4.1step 4.2∎

Steps 2.1, 4.1 and 4.2 prove the three assertions.

Depends on

Used by

Dependency tree · two levels

41 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