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.

Highest-weight classification

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 the maps V⟼λ(V),λ⟼L(λ) are mutually inverse bijections between the isomorphism classes of finite-dimensional irreducible representations of g and the dominant integral weights (Integral, dominant, and strictly dominant weights); here λ(V) is the highest weight of V (Highest-weight vectors and modules) and L(λ) is the simple quotient of Mint(λ).

Facts & Assumptions

Given: The Axiom of Choice, such g,h and a fixed positive system.

[A1]

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

[L1]

Every nonzero finite-dimensional irreducible module V contains a highest weight vector and, when generated by one, satisfies V=U(n−)Cv with all weights ≤λ; the highest weight is unique (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 of a finite-dimensional irreducible module is dominant integral (Finite-dimensional highest weights are dominant integral).

[L3]

For dominant integral λ the module L(λ) is a finite-dimensional simple highest weight module of highest weight λ (Unique simple quotient of the dominant cyclic module, Dominant simple highest-weight modules are finite-dimensional).

[L4]

Two finite-dimensional simple highest weight modules are isomorphic if and only if their highest weights agree (Simple highest-weight modules are classified by highest weight).

Proof

technique · direct
1.1L1L2A1

The assignment V↦λ(V) is well defined on isomorphism classes of nonzero finite-dimensional irreducible modules by [L1] and takes values in the dominant integral weights by [L2].

1.2L3

The assignment λ↦L(λ) is defined on all dominant integral weights by [L3], and L(λ) is a nonzero finite-dimensional irreducible module whose highest weight is λ.

1.3L1L2L3L4

For every nonzero finite-dimensional irreducible V we have V≅L(λ(V)): both are finite-dimensional simple highest weight modules with the same highest weight λ(V), so [L4] applies.

2.1L3step 1.3

Conversely, if λ is dominant integral then the highest weight of L(λ) is λ by [L3]; hence the two assignments are inverse to one another on isomorphism classes.

3.1L4step 1.3step 2.1∎

Every dominant integral weight therefore occurs (through L(λ)), and no two distinct dominant integral weights give isomorphic modules by [L4]; every finite-dimensional irreducible representation occurs as L(λ(V)) by step 1.3. This is the asserted bijection.

Depends on

Used by

Dependency tree · two levels

37 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