Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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.

Finite weight-space detection of subquotients

Statement

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=hn+. Write Q+=iZ0αi, μλ when λμQ+, and wλ=w(λ+ρ)ρ.

Suppose MOχλ. Every nonzero subquotient T of M has Tμ0 for some μWλ. In particular the number of strict inclusions in any finite chain of submodules of M is at most

dλ(M)=μWλdimMμ,

where distinct weights in the orbit are counted once.

Facts & Assumptions

Given: The setting above and the hypotheses in the statement.

[F1]

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=hn+. Write Q+=iZ0αi, μλ when λμQ+, and wλ=w(λ+ρ)ρ. The category O is closed under submodules, quotients and finite direct sums and is an abelian category. If 0AEB0 is exact, A,BO, and E is h-semisimple, then EO. The middle-term weight hypothesis is essential. (Category O is abelian and extension closed among weight modules)

[F2]

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=hn+. Write Q+=iZ0αi, μλ when λμQ+, and wλ=w(λ+ρ)ρ. Every nonzero MO contains a nonzero weight vector killed by n+. (A nonzero O-object has a highest-weight vector)

[F3]

Let χλ and χμ be the central characters obtained from highest weights λ and μ. Then χλ=χμif and only ifμWλ, where Wλ:={w(λ+ρ)ρ:wW}. (Central characters are dot-Weyl orbits)

[F4]

Every central element acts on a cyclic highest-weight module by a scalar. In particular, each cyclic highest-weight module has a well-defined central character in the sense of def-central-character-of-a-lie-algebra-module. (Central elements act by scalars on cyclic highest-weight modules)

[F5]

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=hn+. Write Q+=iZ0αi, μλ when λμQ+, and wλ=w(λ+ρ)ρ. Every MO decomposes canonically into finitely many nonzero generalized central-character submodules: M=χMχ. For each summand there is a single N1 such that mχNMχ=0. The decomposition of zero is empty. (Generalized central-character summands)

[F6]

Fix a finite-dimensional complex semisimple Lie algebra g, a Cartan subalgebra h, and a positive Borel b=hn+. Write Q+=iZ0αi, μλ when λμQ+, and wλ=w(λ+ρ)ρ. Let M be a finitely generated h-semisimple g-module. Then MO if and only if suppMi=1r(λiQ+) for some finite list of weights. In either case every Mμ is finite dimensional. The list may be empty for M=0; finite generation is an independent hypothesis. (The support description of category O with finite generation)

[F7]

Let a cyclic highest-weight module have highest vector of weight μ. Then every zZ(U(g)) acts by the scalar pr(z)(μ)=χμ(z). (The Harish-Chandra projection computes the highest-weight scalar)

Proof

1.1

By closure, a nonzero subquotient T is in O. Choose a nonzero highest-weight vector vTμ. A common power of mχλ kills M and hence T. On the cyclic highest-weight module U(g)v, F4 gives scalar central action and F7 identifies its scalar as χμ(z). Thus (zχλ(z))Nv=0 forces χμ(z)=χλ(z) for each zZ.

F1F2F4F5F7
2.1

The exact central-character criterion now gives μWλ. The Weyl group is finite, and all weight spaces of an O object are finite dimensional, so the displayed detector is finite. For a short exact sequence of weight modules, taking any fixed weight is exact (decompose a lift into weight components). Thus dλ is additive on subquotients of M.

F6F3algebrastep 1.1
3.1

Every nonzero factor of a strict chain has detector at least one by the first two steps. Additivity bounds the number of strict inclusions by dλ(M), whether the chain is written ascending or descending. If the detector is zero there is no nonzero subquotient; in particular M=0, with no strict inclusions.

algebrastep 2.1

Depends on

Used by

Dependency tree · two levels

21 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