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.

The dominant cyclic generator survives

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, let λ be dominant integral, and let Mint(λ)=U(g)/Iλ be the cyclic module with canonical generator vλ of Dominant cyclic highest-weight presentation. Then vλ0, vλ is a weight vector of weight λ, and n+vλ=0.

Facts & Assumptions

Given: The Axiom of Choice, such g,h, a chosen positive system, a dominant integral λ with mi=λ,αi, lowering vectors figαi and the module M=Mint(λ) with generator vλ.

[A1]

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

[L1]

The chosen positive system gives the direct sum g=nhn+, and the PBW monomials in an ordered basis of g listing a basis of n first, then one of h, then one of n+, form a basis of U(g); in particular U(g)=U(n)U(h)U(n+) as a linear span and U(n) is spanned by monomials in a basis of n (Triangular decomposition, Poincaré–Birkhoff–Witt theorem).

[L2]

In the universal enveloping algebra, the product u1u2uk of elements of g has the bracket rule XYYX=[X,Y]; in particular for the sl2-triple (ei,fi,hαi) one has eififiei=hαi, hαififihαi=2fi (The root sl_2 triple, Universal enveloping algebra).

[L3]

The modules Mint(λ) are defined by the relations xvλ=0 for xn+, Hvλ=λ(H)vλ for Hh, and fimi+1vλ=0 (Dominant cyclic highest-weight presentation).

[L4]

Any module generated by a highest weight vector w of weight μ satisfies U(g)w=U(n)Cw and has all weights μ, and it has w as the only vector of weight μ up to scalars (Highest weight modules lie below the top weight, Root order on weights).

[L5]

In the Serre presentation, n+ is generated as a Lie algebra by the simple-root vectors ej, while [ej,fi]=0 for ij and [ei,fi]=hαi (Serre presentation theorem).

[L6]

The elements fimi+1 are nonzero, every positive root is a nonzero nonnegative integral combination of the linearly independent simple roots, and each simple root is positive (Simple roots form a signed integral basis, Poincaré–Birkhoff–Witt theorem).

Proof

technique · direct
1.1

Let JU(g) be the left ideal generated by n+ and the elements Hλ(H) with Hh, and let N=U(g)/J with v0=1+J; then n+v0=0 and Hv0=λ(H)v0 for Hh, and by [L1] every element of N is a linear combination of vectors uv0 with uU(n), so the linear map φ:U(n)N, φ(u)=uv0, is onto.

A1L1L3
2.1

The map φ is also injective. Let b=hn+. The linear functional χλ:bC defined by χλ(H+x)=λ(H) is a Lie-algebra homomorphism to the abelian Lie algebra C, because [b,b]n+. Its multiplicative extension to the tensor algebra kills every relation XYYX[X,Y], so the quotient definition in [L2] makes it an algebra homomorphism χλ:U(b)C. By the PBW basis of [L1] every uU(g) has a unique finite expansion u=AfAuA, with uAU(b) and fA ranging over the monomials in a basis of n. Define ρ(u)=Aχλ(uA)fA. Then ρ is the identity on U(n) and vanishes on J: for xn+ and Hh, one has χλ(x)=0 and χλ(Hλ(H)1)=0, so ρ(ux)=ρ(u(Hλ(H)1))=0 for every uU(g). Thus U(n)J=0, and φ is a linear isomorphism by step 1.1. In particular v00, and the action of U(n) on N corresponds under φ to left multiplication.

A1L1L2step 1.1
3.1

For each i set wi:=fimi+1v0=φ(fimi+1); this is nonzero by [L6] and step 2.1, and it has weight λ(mi+1)αi.

L6step 2.1
4.1

For every i the vector wi satisfies n+wi=0: for j=i one has eiwi=[ei,fimi+1]v0 by the product rule [L2] and eiv0=0, and the sl2-commutation identity [ei,fin]=nfin1(hαi(n1)) gives [ei,fimi+1]v0=(mi+1)fimi(hαimi)v0=0 because hαiv0=miv0; for ji one has [ej,fi]=0 by [L5], hence [ej,fimi+1]=0 and ejwi=fimi+1(ejv0)+[ej,fimi+1]v0=0. Thus every simple generator ej kills wi. The action is a Lie-algebra homomorphism, so a bracket of operators that each kill wi also kills wi; since the ej generate n+ by [L5], every element of n+ kills wi.

L2L3L5step 3.1
5.1

By steps 3.1 and 4.1 each wi is a highest weight vector of weight λ(mi+1)αi, so by [L4] its submodule Ki=U(g)wi has all weights λ(mi+1)αi; since (mi+1)αi is a nonzero element of Q+ by [L6] and λ(λ(mi+1)αi)=(mi+1)αiQ+, no weight of Ki equals λ, and wi0.

L4L6step 3.1step 4.1
6.1

Let K=iKi. A vector of weight λ in a sum of submodules lies in the sum of their λ-weight spaces, each of which is zero by step 5.1, so K has no weight λ; in particular v0K.

step 5.1
6.2

The left ideal Iλ defining Mint(λ) equals J+iU(g)fimi+1, because it is the left ideal generated by the generators of J together with the elements fimi+1; passing to the quotient by J and using the isomorphism of step 2.1 gives Iλ/J=i(U(g)fimi+1+J)/J=iKi=K.

A1step 5.1
7.1

Therefore Mint(λ)=U(g)/Iλ=N/K, and the canonical generator vλ=v0+K is nonzero by step 6.1.

step 6.1step 6.2
8.1

Finally vλ has weight λ, because Hvλ=λ(H)vλ holds in N and passes to the quotient, and n+vλ=0 for the same reason; hence vλ is a nonzero weight vector of weight λ killed by n+.

L3step 7.1
9.1

The class of the unit in Mint(λ) is nonzero, has weight λ, and is killed by n+, as asserted.

step 8.1

Depends on

Used by

Dependency tree · two levels

54 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