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 bounds the dominant cyclic module

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 λ be dominant integral. Then the cyclic module Mint(λ) of Dominant cyclic highest-weight presentation is finite-dimensional.

Facts & Assumptions

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

[A1]

The Axiom of Choice is assumed; it enters through the root-space theory supplying [L3] and through the Weyl-group suppliers [L6]–[L8] (The Axiom of Choice).

[L1]

v0 has weight λ, n+v=0, and fimi+1v=0 for chosen lowering vectors figαi; M=U(g)v is generated by v (The dominant cyclic generator survives).

[L2]

M=U(n)Cv, every weight of M satisfies μλ in the root order, and Mλ=Cv (Highest weight modules lie below the top weight, Root order on weights).

[L3]

For each i there is an sl2-triple (ei,fi,hαi) with [ei,fi]=hαi; a vector xgα maps Mμ into Mμ+α (The root sl_2 triple, Root vectors shift weights).

[L4]

A finite-dimensional sl2-module is a direct sum of irreducible submodules; an irreducible submodule has a top weight m0 and h-eigenvalues m,m2,,m, each on a one-dimensional subspace (Finite-dimensional representations of sl_2).

[L5]

The PBW monomials in an ordered basis of g adapted to g=nhn+ form a basis of U(g) (Triangular decomposition, Poincaré–Birkhoff–Witt theorem).

[L6]

Every element of the Weyl group W is a product of simple reflections (Weyl length equals inversion number), and W is finite (The Weyl group is finite and faithful).

[L7]

The open Weyl chambers are the connected components of the complement of the finitely many root hyperplanes, and W acts simply transitively on them; the fundamental chamber is C={(x,αi)>0} with closure C={(x,αi)0} (Open and closed Weyl chambers, Simple transitivity on Weyl chambers).

[L8]

λ is an integral element of E with λ=imiωi, mi0, and (λ,αi)=mi(αi,αi)/2; the form on E is a positive definite inner product (Dominant weights in fundamental coordinates, Fundamental weights, The roots form a reduced crystallographic Euclidean root system).

[L9]

Every positive root is a nonzero nonnegative integral combination of the simple roots, and the simple roots form a basis of E (Simple roots form a signed integral basis).

Proof

technique · direct
1.1

Fix i and consider the vectors fikv, k0; the sl2-commutation identity [ei,fik]=kfik1(hαi(k1)), proved by induction from [ei,fi]=hαi and [hαi,fi]=2fi, gives ei(fikv)=k(mik+1)fik1v and hαi(fikv)=(mi2k)fikv by [L1] and [L3], so the span of {fikv:k0} is an sl2-submodule of M.

A1L1L3
2.1

By [L1] fimi+1v=0, so the submodule of step 1.1 is spanned by v,fiv,,fimiv and is finite dimensional; hence v generates a finite-dimensional sl2-module for every i.

L1step 1.1
3.1

Let Mint:={wM:for every j the sl2-module generated by w is finite dimensional}. It is a linear subspace, because the module generated by w+w is contained in the sum of the modules generated by w and by w. Let wMint, xg, and fix j. Put S:=U(sl2(j))w, which is finite dimensional by the definition of Mint, and let X:=U(sl2(j))x for the adjoint action; this is finite dimensional because Xg. The representation identity y(xs)=[y,x]s+x(ys) for ysl2(j), xX, and sS shows that the finite-dimensional space span(XS) is an sl2(j)-submodule containing xw. Hence U(sl2(j))(xw)span(XS) is finite dimensional. Therefore xwMint for all xg, so Mint is a subrepresentation.

L3step 2.1
4.1

Since vMint by step 2.1 and M=U(g)v by [L1], the subrepresentation Mint is all of M; in particular every vector of M generates a finite-dimensional sl2-module for every i.

L1step 2.1step 3.1
5.1

Let μ be a weight of M and 0tMμ; fix i, put q=μ(hαi), and let T=U(sl2(i))t be the finite-dimensional module generated by t, which by [L4] is a direct sum of irreducible summands T=rTr; the q-eigenspace of hαi on T contains t and is the sum of its intersections with the Tr, so some summand T0 has a nonzero q-eigenspace; choose 0wT0 with hαiw=qw.

L4step 4.1
6.1

The summand T0 is irreducible with top weight m0 and eigenvalues m,m2,,m, so q=m2k for some k{0,,m}; if q>0 and fiqw=0, take the least j with 0j<q and fij+1w=0: then 0fijw lies in the kernel of fi in the eigenspace of eigenvalue q2j, and the submodule of the irreducible module T0 that it generates is spanned by its ei-orbit, of dimension m(q2j)2+1<m+1 because 2j2q2<m+q, so it is a nonzero proper submodule of T0, contradicting irreducibility; hence fiqw0. Applying the same argument inside each irreducible summand Tr with tr0, whose top weight mr0 satisfies q=mr2kr for some kr{0,,mr}, gives fiqtr0 for every r with tr0; since the summands are independent, this gives fiqt=rfiqtr0, and fiqtMμqαi is a nonzero vector by [L3]; if q<0 the same argument with ei gives 0eiqtMμqαi; if q=0 then μqαi=μ is already a weight, so in every case si(μ)=μqαi is a weight of M.

L3L4step 5.1
7.1

By step 6.1 the weight set of M is invariant under every simple reflection; since W is generated by the simple reflections by [L6], the weight set of M is W-invariant.

L6step 6.1
8.1

Every element of E lies in the closure of some open chamber: the union of the finitely many root hyperplanes is closed with empty interior, so any point is a limit of points outside it, each of which lies in a chamber, and since there are finitely many chambers some chamber contains a sequence converging to the point; by the simple transitivity of [L7] some wW carries that chamber to the fundamental chamber, so w(μ)C, that is, (wμ,αi)0 for all i.

L7step 7.1
9.1

The weight w(μ) of step 8.1 satisfies w(μ)λ by [L2], and only finitely many dominant weights are below λ: let ν be dominant with νλ and write n:=λν=iniαi with ni0. Both λ and ν are dominant, so (λ,αi)=mi(αi,αi)/20 and (ν,αi)0 for every i by [L8]; hence (λ,n)=ini(λ,αi)0 and (ν,n)=ini(ν,αi)0, and therefore (n,n)=(λ,n)(ν,n)(λ,n)λn for the positive definite inner product of [L8]. Thus nλ, and since the simple roots form a basis of E while all norms on E are equivalent, the nonnegative integers ni are bounded by a constant depending only on the chosen simple roots times λ; as ni is determined by ν, only finitely many dominant weights ν are below λ.

L2L8step 8.1
10.1

Each weight of M is W-conjugate to one of the finitely many dominant weights below λ by steps 7.1, 8.1 and 9.1, and W is finite by [L6]; hence M has only finitely many weights.

L6step 7.1step 8.1step 9.1
11.1

Each weight space Mμ is finite dimensional: by [L2] and [L5] the space M is spanned by the vectors uv with u a monomial in a basis f1,,fN of n consisting of root vectors fjgβj, and uvMμ forces λμ=jajβj with aj the exponents of u; writing λμ=iniαi and βj=ici(j)αi with ci(j)0 and using uniqueness of the simple-root coefficients in [L9] gives ni=jajci(j)ajci(j), and since each positive root has some ci(j)1 we get ajmaxini; thus only finitely many monomials contribute and Mμ is spanned by finitely many vectors.

L2L5L9step 10.1
12.1

Steps 10.1 and 11.1 show that M is a direct sum of finitely many finite-dimensional weight spaces, hence finite dimensional, as asserted.

step 10.1step 11.1

Depends on

Used by

Dependency tree · two levels

67 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