TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-23 (gpt-6-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.

Finite-dimensional simple modules are classified by dominant highest weights

Statement

Every finite-dimensional simple $g$ -module is a cyclic highest-weight module whose highest weight is dominant integral, and for each dominant integral weight

$λ = \sum_{i = 1}^{r} m_{i} ω_{i} (m_{i} \in N_{0}),$

there exists, up to isomorphism, a unique finite-dimensional simple module $L (λ)$ with highest weight $λ$ .

Facts & Assumptions

Given: A complex semisimple Lie algebra $g$ with chosen simple roots $α_{1}, \dots, α_{r}$ and fundamental weights $ω_{1}, \dots, ω_{r}$ .

[F1]

Finite semisimple PBW and highest-weight construction constructs the Verma module and its unique simple quotient $L (λ)$ ; for dominant integral $λ$ that quotient is finite-dimensional, and every finite-dimensional simple module occurs uniquely this way.

[F2]

Fundamental weights for a chosen simple root system expresses a dominant integral weight uniquely as $\sum_{i} m_{i} ω_{i}$ with $m_{i} \in N_{0}$ .

Proof

technique · direct

1.1F1given

The finite PBW and highest-weight construction in [F1] proves that every finite-dimensional simple $g$ -module is generated by a highest-weight vector of a unique dominant integral weight $λ$ , and is isomorphic to $L (λ)$ . This is a cyclic highest-weight module in the stated sense.

2.1F1F2step 1.1

By [F2], the weight from step 1.1 is exactly $λ = \sum_{i} m_{i} ω_{i}$ with $m_{i} \in N_{0}$ . The rank-one integrality and nonnegativity needed for this assertion are established in [F1].

3.1F1step 1.1step 2.1∎

Conversely, for each $λ$ of the form in step 2.1, [F1] constructs a finite-dimensional simple $L (λ)$ and proves uniqueness up to isomorphism. Together with step 1.1 this gives both directions of the classification.

Depends on

Used by

Dependency tree · two levels

12 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 (standard reference, not scraped)