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=h⊕n+. Write Q+=∑iZ≥0α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=h⊕n+. Write Q+=∑iZ≥0αi, μ≤λ when λ−μ∈Q+, and w⋅λ=w(λ+ρ)−ρ. For an h-semisimple module M with finite-dimensional weight spaces, its restricted Chevalley dual is D(M)=⨁μ∈h∗Mμ∗,(xφ)(m)=φ(τ(x)m)(x∈U(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:M→N 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 v∈V 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.1F1F2F3

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+.

2.1F1F2algebrastep 1.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 S⊥⊂L 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.

3.1F4F2step 2.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(λ).

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