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.

Restricted self-duality of simple highest-weight modules

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(λ+ρ)ρ.

For every highest weight λ, D(L(λ))L(λ) as g-modules.

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(λ+ρ)ρ. For an h-semisimple module M with finite-dimensional weight spaces, its restricted Chevalley dual is D(M)=μhMμ,(xφ)(m)=φ(τ(x)m)(xU(g)). Here each functional is extended by zero on the other weight spaces and τ is the fixed anti-involution of def-chevalley-contravariant-form. In particular τ(h)=h and D(M)μ=Mμ. A map f:MN induces D(f):D(N)D(M) by precomposition. The action law follows from τ(xy)=τ(y)τ(x); a root vector of weight α sends Mμ to Mμ+α, so the restricted sum is stable. This is a complex-linear algebraic dual, with no conjugation. Ordinary Lie-module duality has a minus sign and reverses weights; twisting that dual by the Lie automorphism xτ(x) gives the convention used here. (Restricted Chevalley dual)

[F2]

The proper submodule J(λ) which is the sum of all proper submodules is the unique maximal submodule of M(λ). The quotient L(λ):=M(λ)/J(λ) is simple and is its unique simple quotient. (A Verma module has a unique simple quotient)

[F3]

The weights of M(λ) are exactly λβ for βQ+; every weight space is finite dimensional, and M(λ)λ=Cvλ. (Weights of a Verma module lie below lambda)

[F4]

For a g-module V, sending a homomorphism T:M(λ)V to T(vλ) is a bijection onto the vectors vV of weight λ annihilated by n+. Here M(λ) is def-verma-module. The nonzero vectors in this target are precisely the highest-weight vectors of weight λ from def-highest-weight-vector-and-cyclic-highest-weight-module; the zero vector corresponds to the zero homomorphism. (The universal property of Verma modules)

Proof

1.1

The simple Verma quotient L=L(λ) has finite-dimensional weight spaces, support in λQ+, and a nonzero one-dimensional highest line. These follow from the Verma weight formula and the fact that a proper submodule cannot contain its generating top vector. Therefore D(L) has the same weight dimensions, and its top line is killed by n+.

F1F2F3
2.1

If S were a nonzero proper submodule of D(L), it would be a weight submodule. Finite-dimensionality of each weight space implies that its annihilator SL is nonzero (some weight component of S is proper) and proper (some functional in S is nonzero). It is a g-submodule, since φ(xm)=(τ(x)φ)(m) and S is stable. This contradicts simplicity of L. Hence D(L) is simple without first presuming it is finitely generated.

F1F2algebrastep 1.1
3.1

A nonzero vector of the top line gives a nonzero Verma map M(λ)D(L) by the universal property. It is surjective by simplicity, and the unique simple quotient identifies its target with L(λ).

F4F2step 2.1

Depends on

Used by

Dependency tree · two levels

9 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