Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
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.

Weight-lambda vectors are singular at a maximal label

Statement

Assume the Axiom of Choice (The Axiom of Choice). In the setting of Truncation at a finite downward-closed ideal of a linkage class, let Γ be a finite downward-closed ideal of a linkage class C and let λ∈Γ be maximal in Γ.

  1. If ν is a weight of an object X of OΓ with ν≥λ in the root order of Root order on weights, then ν=λ; equivalently, no object of OΓ has a weight λ+β with β∈Q+∖{0}.
  2. Consequently every vector of weight λ in every X∈OΓ is annihilated by n+: for x∈n+ of weight α>0 and v∈Xλ, the vector xv has weight λ+α and hence vanishes by (1). Thus Xλn+=Xλ for every X∈OΓ.
  3. The weight functor X↦Xλ is exact on all h-semisimple g-modules, hence on OΓ.

Maximality of λ is used only in (1). Incomparable maximal labels do not invalidate (1): its antecedent requires ν≥λ, and any composition label above such a ν is then comparable to λ and forced equal to it. What can fail is the stronger assertion that every weight of every object lies below one specified maximal label; a simple with an incomparable highest weight refutes that stronger assertion.

Facts & Assumptions

Given: The Axiom of Choice, a finite downward-closed ideal Γ of a linkage class C, a maximal element λ∈Γ, and an object X∈OΓ.

[F1]

OΓ is the full subcategory of objects of O all of whose simple composition factors are L(μ) with μ∈Γ; membership depends only on the isomorphism class, and Γ is a finite lower set for the root order (Truncation at a finite downward-closed ideal of a linkage class). Maximality of λ means that μ∈Γ and λ≤μ imply μ=λ.

[F2]

The simple objects of O are exactly the L(μ); L(μ) is the unique simple quotient of the Verma module M(μ), and the weights of M(μ) are exactly μ−Q+ with finite weight spaces (The simple objects of O, A Verma module has a unique simple quotient, Weights of a Verma module lie below lambda).

[F3]

For a short exact sequence 0→A→X→B→0 of h-semisimple modules, a functional is a weight of X exactly when it is a weight of A or of B: the corresponding sequence of weight spaces is exact at each weight (Category O is abelian and extension closed among weight modules). Iterating along a composition series, every weight of X is a weight of some composition factor (Composition series and composition factors of an object).

[F4]

The root order is transitive and antisymmetric (Root order on weights), and a root vector of weight α maps Xν into Xν+α (Weight and weight space, The classical BGG category O).

Proof

technique · direct: reduce a top weight to a composition factor, force equality by maximality, and read off singularity and exactness
1.1F1F2F3F4given

Let ν be a weight of X∈OΓ with ν≥λ. By [F3] the weight ν occurs in some composition factor L(μ) of X, and μ∈Γ because X∈OΓ. By [F2], ν is then a weight of M(μ), so ν≤μ. From λ≤ν≤μ and transitivity in [F4] we get λ≤μ with μ∈Γ, so maximality of λ gives μ=λ; then λ≤ν≤λ and antisymmetry give ν=λ. Hence no object of OΓ has a weight λ+β with β∈Q+∖{0}.

1.2F4givenalgebra

The weight functor X↦Xλ is exact on h-semisimple g-modules: given a short exact sequence 0→X′→iX→pX′′→0, injectivity of iλ is immediate, and if x′′∈Xλ′′ lifts to x∈X, then writing x=∑νxν as a finite sum of weight vectors gives x′′=p(x)=∑νp(xν) with p(xν) of weight ν; by the directness of the weight decomposition of X′′ all terms with ν≠λ vanish and x′′=p(xλ), so pλ is surjective.

2.1F4step 1.1step 1.2∎

By step 1.1 no object of OΓ has a weight strictly above λ in the sense of λ+β with β∈Q+∖{0}: if v∈Xλ is nonzero and x∈n+ has weight α>0, then xv∈Xλ+α by [F4], and λ+α>λ; if xv≠0 it would be a weight vector of weight λ+α, contradicting step 1.1. Hence xv=0 for every x∈n+ and Xλn+=Xλ. Together with the exactness of the weight functor in step 1.2 this proves all 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