Alphabeta Math
PropositionStatement: 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.

Top summand in a tensor product

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, and let λ,μ be dominant integral weights (Integral, dominant, and strictly dominant weights). Then the tensor product V(λ)V(μ) (Direct-sum, dual, Hom, and tensor representations) contains V(λ+μ) as a summand with multiplicity one, and every other irreducible summand has highest weight strictly below λ+μ in the root order (Root order on weights).

Facts & Assumptions

Given: The Axiom of Choice, such g,h, a fixed positive system, dominant integral λ,μ, and the modules V(λ), V(μ).

[A1]

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

[L1]

V(λ) and V(μ) are finite-dimensional irreducible highest weight modules with top lines Cvλ and Cvμ and with all weights bounded above by λ and μ respectively; the tensor product carries the action x(vw)=xvw+vxw (Highest-weight classification, The highest-weight space is one-dimensional, Highest weight modules lie below the top weight, Direct-sum, dual, Hom, and tensor representations).

[L2]

The tensor product is a finite direct sum of irreducibles L(ν) with ν dominant integral, (Every finite-dimensional module is a direct sum of highest-weight modules, Highest-weight classification). For each such summand all weights are ν by Highest weight modules lie below the top weight, and its ν-weight space has dimension one by The highest-weight space is one-dimensional.

[L3]

The root order is a partial order with Q+ as its positive cone: if ν1λ and ν2μ then ν1+ν2λ+μ, and if in addition ν1+ν2=λ+μ then ν1=λ, ν2=μ (Root order on weights, Simple roots form a signed integral basis).

[L4]

A highest-weight module is generated by negative-root operators on its highest vector (Highest weight modules lie below the top weight), and a root operator shifts a weight by its root (Root vectors shift weights). Distinct weight spaces are independent (Weight and weight space).

Proof

technique · direct
1.1

The sum λ+μ is dominant integral because its simple-coroot values are sums of nonnegative integers (Integral, dominant, and strictly dominant weights). The vector vλvμ is nonzero and is a highest weight vector of weight λ+μ: n+ acts by x(vλvμ)=xvλvμ+vλxvμ=0 by [L1], and H(vλvμ)=(λ+μ)(H)vλvμ.

A1L1
1.2

By [L4], negative-root words applied to a highest vector span each factor and are weight vectors or zero. Independence of distinct weight spaces therefore gives a direct weight-space decomposition of each factor; finite dimensionality makes it a finite sum. Tensoring bases of those spaces gives a weight basis of the tensor product under the action in [L1]. Every weight of the tensor product is a sum ν1+ν2 of a weight of V(λ) and a weight of V(μ) (the direct sum decomposition of the tensor product into weight spaces has components of this form), so by [L1] and [L3] every weight satisfies ν1+ν2λ+μ.

L1L3L4
2.1

The (λ+μ)-weight space of the tensor product is the direct sum of the spaces V(λ)ν1V(μ)ν2 over pairs with ν1+ν2=λ+μ; by [L3] the only pair with ν1λ, ν2μ and ν1+ν2=λ+μ is (λ,μ), so this weight space is V(λ)λV(μ)μ=C(vλvμ) and has dimension one by [L1].

L1L3step 1.2
3.1

Decompose V(λ)V(μ)=rWr into irreducibles as in [L2], with WrL(νr); the top weight νr of each summand is a weight of the tensor product, so νrλ+μ by step 1.2, and (Wr)λ+μ=0 unless νr=λ+μ because all weights of L(νr) are νr by [L2]; each summand with top weight λ+μ contributes exactly one dimension by [L2], so comparison with step 2.1 shows that exactly one summand has highest weight λ+μ.

L2step 1.2step 2.1
4.1

By step 3.1 the tensor product contains exactly one summand L(λ+μ)V(λ+μ). Every other summand has highest weight νrλ+μ by step 1.2 and cannot have equality, so its highest weight is strictly below λ+μ. If g=0, then h=0, both highest-weight modules are one-dimensional, and the conclusion is a single trivial summand. More generally zero dominant weights are allowed throughout: their top lines remain nonzero, and no division by a weight occurs. This is the assertion.

L2step 1.2step 3.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 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