Weight-transfer proof of irreducibility of symmetric powers (source code)

= Weight-transfer proof of irreducibility of symmetric powers
{title2=$E_{ij}\cdot x^a=a_jx^{a+e_i-e_j}$}

In the <symmetric power> $\operatorname{Sym}^m\mathbb C^n$ of the defining <unitary group> representation, diagonal <torus> weights are indexed by nonnegative integer tuples summing to $m$, with one monomial per <weight space>. Torus averaging extracts a monomial from any nonzero invariant complex subspace. The complexified <Lie algebra> acts by $E_{ij}=x_i\partial_{x_j}$ on the symmetric algebra. Whenever $a_j>0$, the displayed action moves one unit of degree from $j$ to $i$ with nonzero coefficient. Finite transfers connect every degree-$m$ monomial, so the subspace is the entire representation. The case $m=0$ is the one-dimensional trivial representation. This proof needs neither the <Weyl character formula> nor the <Weyl dimension formula>.