TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06

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.

The universal property of Verma modules

Statement

For a $g$ -module $V$ , sending a homomorphism $T : M (λ) \to V$ to $T (v_{λ})$ is a bijection onto the vectors $v \in V$ of weight $λ$ annihilated by $n^{+}$ . Here $M (λ)$ is Verma modules. The nonzero vectors in this target are precisely the highest-weight vectors of weight $λ$ from Highest-weight vectors and cyclic highest-weight modules; the zero vector corresponds to the zero homomorphism.

Facts & Assumptions

Given: A $g$ -module $V$ and $v \in V$ with $h v = λ (h) v$ and $n^{+} v = 0$ .

Proof

technique · direct

1.1

Define $T (u \otimes c_{λ}) = u v$ . If $b = h + x \in b = h \oplus n^{+}$ , then $b v = λ (h) v$ , exactly the scalar by which $b$ acts on $c_{λ}$ ; hence $T (u b \otimes c_{λ}) = T (u \otimes b c_{λ})$ and $T$ descends to the induced module.

givenconstruct

2.1

The descended map is $g$ -linear and sends $v_{λ}$ to $v$ . Conversely a homomorphism is determined by $v_{λ}$ , since that vector generates $M (λ)$ ; its image necessarily has the two displayed properties.

givenalgebra∎

Depends on

Used by

The Shapovalov determinant formula Theorem

Dependency tree · two levels

5 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

Pavel Etingof, Lie Groups and Lie Algebras I & II, Proposition 25.10 (standard reference, not scraped)