Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Simple highest-weight modules are classified by highest weight

Statement

Assume the Axiom of Choice. Let g be a finite-dimensional complex semisimple Lie algebra with Cartan subalgebra h and a fixed positive system. Then two finite-dimensional simple highest weight g-modules for this positive system are isomorphic if and only if their highest weights are equal.

Facts & Assumptions

Given: The Axiom of Choice, such g,h, a fixed positive system, and finite-dimensional simple highest weight modules V,W.

[A1]

The Axiom of Choice is assumed; it enters through the root-space theory used by the cited suppliers (The Axiom of Choice).

[L1]

A finite-dimensional irreducible module V0 has a highest weight λ(V): it contains a highest weight vector, and all its weights are λ(V) for every such highest weight; the module is generated by any of its highest weight vectors (Every finite-dimensional irreducible module has a highest-weight vector, An irreducible module is generated by its highest-weight vector, Highest weight modules lie below the top weight, Highest-weight vectors and modules).

[L2]

The highest weight λ(V) is unique: if λ and λ both occur as highest weights of V, then the relations of [L1] give λλ and λλ, so λ=λ by antisymmetry of the root order (Root order on weights).

[L3]

Every highest weight of a finite-dimensional irreducible module is dominant integral (Finite-dimensional highest weights are dominant integral, Integral, dominant, and strictly dominant weights).

[L4]

L(λ)=Mint(λ)/Nλ is a finite-dimensional simple highest weight module of highest weight λ for every dominant integral λ (Unique simple quotient of the dominant cyclic module, Dominant simple highest-weight modules are finite-dimensional).

[L5]

A finite-dimensional highest weight module V of highest weight λ satisfies fimi+1vλ=0 for mi=λ,αi and its highest weight vector vλ; these are exactly the relations defining Mint(λ), so the map Mint(λ)V, u+Iλuvλ, is a well-defined surjective module map (Simple-root integrability relations, Dominant cyclic highest-weight presentation).

Proof

technique · direct
1.1

Assume V and W have the same highest weight λ; then λ is dominant integral by [L3], so L(λ) exists and is finite dimensional by [L4].

L3L4A1
1.2

Choose a highest weight vector vλ of V; by [L5] the classification relations hold in V, so the map φ:Mint(λ)V with φ(u+Iλ)=uvλ is a well-defined surjective module map; its kernel K is a submodule of Mint(λ) and is proper because vλ0.

L5
1.3

Conversely an isomorphism ψ:VW of g-modules carries weights to weights bijectively (it intertwines the h-action), so the set of weights of W is the image of that of V; by [L1] and [L2] each of V and W has a unique highest weight, and uniqueness of the maximum of a finite weight set under the partial order gives λ(V)=λ(W).

L1L2
2.1

The quotient Mint(λ)/KV is simple by hypothesis, so K is a maximal proper submodule of Mint(λ); by [L4] the unique maximal proper submodule is Nλ, so K=Nλ and VL(λ).

L4step 1.2
3.1

Hence any two finite-dimensional simple highest weight modules of highest weight λ are both isomorphic to L(λ), so equal highest weights force isomorphism.

step 2.1
4.1

Step 1.3 proves that an isomorphism forces equal highest weights and step 3.1 proves that equal highest weights force isomorphism, so the two directions of the equivalence are established.

step 1.3step 3.1

Depends on

Used by

Dependency tree · two levels

36 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