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 be a finite-dimensional complex semisimple Lie algebra with Cartan subalgebra and a fixed positive system, and let be dominant integral weights (Integral, dominant, and strictly dominant weights). Then the tensor product (Direct-sum, dual, Hom, and tensor representations) contains 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 , a fixed positive system, dominant integral , and the modules , .
The Axiom of Choice is assumed; it enters through the root-space theory used by the cited suppliers (The Axiom of Choice).
and are finite-dimensional irreducible highest weight modules with top lines and and with all weights bounded above by and respectively; the tensor product carries the action (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).
The tensor product is a finite direct sum of irreducibles 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.
The root order is a partial order with as its positive cone: if and then , and if in addition then , (Root order on weights, Simple roots form a signed integral basis).
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
The sum is dominant integral because its simple-coroot values are sums of nonnegative integers (Integral, dominant, and strictly dominant weights). The vector is nonzero and is a highest weight vector of weight : acts by by [L1], and .
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 of a weight of and a weight of (the direct sum decomposition of the tensor product into weight spaces has components of this form), so by [L1] and [L3] every weight satisfies .
The -weight space of the tensor product is the direct sum of the spaces over pairs with ; by [L3] the only pair with , and is , so this weight space is and has dimension one by [L1].
Decompose into irreducibles as in [L2], with ; the top weight of each summand is a weight of the tensor product, so by step 1.2, and unless because all weights of are 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 .
By step 3.1 the tensor product contains exactly one summand . Every other summand has highest weight by step 1.2 and cannot have equality, so its highest weight is strictly below . If , then , 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.
Depends on
- Every finite-dimensional module is a direct sum of highest-weight modules
- Highest-weight classification
- The highest-weight space is one-dimensional
- Highest weight modules lie below the top weight
- Root vectors shift weights
- Root order on weights
- Simple roots form a signed integral basis
- Highest-weight vectors and modules
- Direct-sum, dual, Hom, and tensor representations
- Weight and weight space
- Integral, dominant, and strictly dominant weights
- The Axiom of Choice
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
- Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)
- Alexander Kirillov Jr., An Introduction to Lie Groups and Lie Algebras (standard reference, not scraped)