PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-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.

Tensor-product multiplicities are character structure constants

Statement

Assume the Axiom of Choice. In the notation of Tensor-product multiplicities for finite-dimensional simple modules, for all $λ, μ \in Λ^{+}$ the following hold in the completed character ring $R$ of The completed formal character ring:

(i) $ch (L (λ) \otimes L (μ)) = \sum_{ν \in Λ^{+}} c_{λ μ}^{ν} ch L (ν)$ , a finite sum; (ii) if $V$ is any finite-dimensional $g$ -module and $ch V = \sum_{ν \in Λ^{+}} a_{ν} ch L (ν)$ with integers $a_{ν}$ (finitely many nonzero), then $a_{ν} = [V : L (ν)]$ for every $ν$ , so the expansion coefficients of the character are exactly the composition multiplicities and the elements $ch L (ν)$ , $ν \in Λ^{+}$ , are linearly independent in $R$ ; (iii) for every weight $γ \in h^{*}$ one has the weight-multiplicity formula $\dim (L (λ) \otimes L (μ))_{γ} = \sum_{σ + τ = γ} m_{λ} (σ) m_{μ} (τ),$ a finite sum, where $m_{λ} (σ) = \dim L (λ)_{σ}$ and $m_{μ} (τ) = \dim L (μ)_{τ}$ (The formal character of a finite-dimensional weight module, Weight and weight space).

Facts & Assumptions

Given: AC and dominant integral weights $λ, μ \in Λ^{+}$ , with the decomposition $L (λ) \otimes L (μ) ≅ ⨁_{ν} L (ν)^{\oplus c_{λ μ}^{ν}}$ of Tensor-product multiplicities for finite-dimensional simple modules.

[F1]

Every finite-dimensional $g$ -module is the direct sum of its weight spaces, the tensor product of two finite-dimensional modules has weight spaces $(V \otimes W)_{γ} = ⨁_{σ + τ = γ} V_{σ} \otimes W_{τ}$ , and the formal character is additive over direct sums and multiplicative over tensor products in the completed ring $R$ (Finite-dimensional modules decompose into weight spaces, Weight and weight space, Formal characters are additive and multiplicative, The completed formal character ring).

[F2]

For each $ν \in Λ^{+}$ the module $L (ν)$ is the unique simple module of highest weight $ν$ , its highest weight space is one-dimensional, and every weight of $L (ν)$ lies in $ν - Q_{+}$ , so $ν$ is the maximum of the weights of $L (ν)$ in the root order; moreover every finite-dimensional module is completely reducible (Highest-weight classification, Highest weight modules lie below the top weight, Root order on weights, Tensor-product multiplicities for finite-dimensional simple modules).

Proof

1.1F1givenalgebra

Part (i) is the multiplicativity and additivity of the formal character applied to the decomposition: the tensor product distributes over the direct sum, so $ch (L (λ) \otimes L (μ)) = \sum_{ν} c_{λ μ}^{ν} ch L (ν)$ in $R$ ; the sum is finite by Tensor-product multiplicities for finite-dimensional simple modules.

1.2F1F2givenalgebra

Part (ii), comparison of coefficients. Let $V$ be finite-dimensional with decomposition $V ≅ ⨁_{ν} L (ν)^{\oplus a_{ν}^{'}}$ , $a_{ν}^{'} = [V : L (ν)]$ . Then $ch V = \sum_{ν} a_{ν}^{'} ch L (ν)$ . Suppose also $ch V = \sum_{ν} a_{ν} ch L (ν)$ with integers $a_{ν}$ , both sums finite. Let $ν_{0}$ be maximal in the root order among the indices with $a_{ν_{0}} \neq a_{ν_{0}}^{'}$ (if there is none, the two families are equal). Evaluating both characters in the weight $ν_{0}$ and using that $m_{η} (ν_{0}) = 0$ unless $ν_{0} \leq η$ with equality only for $η = ν_{0}$ , while $m_{ν_{0}} (ν_{0}) = 1$ [F2], gives $0 = \dim V_{ν_{0}} - \dim V_{ν_{0}} = \sum_{η \geq ν_{0}} (a_{η} - a_{η}^{'}) m_{η} (ν_{0}) = (a_{ν_{0}} - a_{ν_{0}}^{'}) \neq 0,$ a contradiction. Hence $a_{ν} = a_{ν}^{'} = [V : L (ν)]$ for all $ν$ .

2.1F1F2step 1.1step 1.2algebra

Part (ii), linear independence. Suppose $\sum_{ν \in F} b_{ν} ch L (ν) = 0$ with a finite nonempty set $F$ and integers $b_{ν}$ , not all zero. Split at the $ν$ with $b_{ν} > 0$ and $b_{ν} < 0$ and let $V^{+} = ⨁_{ν \in F, b_{ν} > 0} L (ν)^{\oplus b_{ν}}$ and $V^{-} = ⨁_{ν \in F, b_{ν} < 0} L (ν)^{\oplus (- b_{ν})}$ ; the vanishing of the alternating sum gives $ch V^{+} = ch V^{-}$ in $R$ . Both are characters of finite-dimensional modules, so by step 1.2 the multiplicity families $(b_{ν})_{ν : b_{ν} > 0}$ and $(- b_{ν})_{ν : b_{ν} < 0}$ agree on every $ν$ , forcing $b_{ν} = 0$ against the choice of $F$ . Hence the characters $ch L (ν)$ are linearly independent.

3.1F1givenalgebra∎

Part (iii): by the tensor-product weight-space formula of [F1], $(L (λ) \otimes L (μ))_{γ} = ⨁_{σ + τ = γ} L (λ)_{σ} \otimes L (μ)_{τ}$ , and taking dimensions gives $\dim (L (λ) \otimes L (μ))_{γ} = \sum_{σ + τ = γ} m_{λ} (σ) m_{μ} (τ)$ ; only the finitely many pairs of weights of $L (λ)$ and $L (μ)$ can contribute, so the sum is finite.

Depends on

Used by

Dependency tree · two levels

45 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

P. Etingof, Lie Groups and Lie Algebras II (MIT 18.755, Spring 2024), complete lecture notes (standard reference, not scraped)
R. Goodman and N. R. Wallach, Symmetry, Representations, and Invariants, Graduate Texts in Mathematics 255, Springer 2009 (standard reference, not scraped)