Solution (source code)

= Solution

For a decreasing integer tuple $\lambda=(\lambda_1,\ldots,\lambda_m)$, let $\mu_i=\lambda_i-\lambda_m$. Then $\mu$ is a partition and the <highest-weight classification of rational GL representations> defines
$$
D_\lambda(V)=(\det V)^{\lambda_m}\otimes D_\mu(V).
$$
This is a <determinant twist> of a <Schur module>. Every irreducible rational $GL_m$ representation becomes <polynomial> after multiplication by a sufficiently large positive <determinant> power, which clears all matrix-entry denominators. The <polynomial> degree decomposition and <Schur–Weyl duality> then identify it with a Schur <module>. Undoing the twist gives exactly one decreasing integer tuple $\lambda$. Distinct tuples have distinct highest torus weights, so these are the complete pairwise nonisomorphic irreducible <rational representations>.

The <Weyl character formula> specializes to
$$
\varphi_\lambda(\operatorname{diag}(x_1,\ldots,x_m))=
\frac{\det(x_j^{\lambda_i+m-i})}{\det(x_j^{m-i})}
=(x_1\cdots x_m)^{\lambda_m}s_\mu(x).
$$
It is a symmetric <Laurent polynomial> in the <eigenvalues>. Equality extends from the dense set of <diagonalizable> matrices to all invertible matrices: both the <character> and the expression in the characteristic-polynomial coefficients are <regular functions> on $GL_m$. For a <polynomial representation> this also extends to every endomorphism of $V$. \b[For a general <rational representation>, the printed claim at singular endomorphisms needs this qualification]: for example $\det^{-1}$ is undefined at a singular matrix. The displayed formula is valid on $GL_m$, and on all of $\operatorname{End}(V)$ when $\lambda_m\ge0$.

To compute the degree, set $x_j=e^{tc_j}$ with distinct $c_j$ and take $t\to0$. For $\ell_i=\lambda_i+m-i$ and $d=\binom m2$, the <leading coefficient of an exponential alternant> is
$$
\det(e^{t\ell_i c_j})=
\frac{t^d}{\prod_{k=0}^{m-1}k!}\prod_{i<j}(\ell_i-\ell_j)\prod_{i<j}(c_i-c_j)+O(t^{d+1}).
$$
Indeed, expand every exponential in powers of $t$. The first nonzero <determinant> uses the distinct powers $0,1,\ldots,m-1$; its coefficient is the product of the two <Vandermonde determinants> divided by $\prod k!$. Taking the same expansion in the denominator cancels the powers and the $c$ factors, giving the <Weyl dimension formula>
$$
\boxed{\deg\varphi_\lambda=\dim D_\lambda(V)=\prod_{i<j}\frac{\lambda_i-\lambda_j+j-i}{j-i}.}
$$
This proof works for negative $\lambda_m$ as well, since <determinant> twists have dimension one.

Every finite-dimensional rational <module> is completely reducible. The <characters> of its irreducible constituents are linearly independent: each Schur Laurent <character> has its highest dominant monomial $x^\lambda$ with coefficient $1$, and only lower weights besides it. In a finite relation, choose a lexicographically highest remaining weight; its coefficient must vanish, and iterate. Therefore equal <characters> give equal multiplicities of every irreducible constituent, proving \b[rational <modules> with the same <character> are isomorphic].

Finally the <symmetric algebra> of $V\oplus\Lambda^2V$ has the formal torus <character>
$$
\operatorname{ch}\!\left(\bigoplus_{j\ge0}S^j(V\oplus\Lambda^2V)\right)
=\prod_i(1-x_i)^{-1}\prod_{i<j}(1-x_ix_j)^{-1}.
$$
Each factor sums the symmetric powers of a one-dimensional weight space; the <exterior square> has weights $x_ix_j$ for $i<j$. The permitted Schur identity makes this $\sum_\lambda s_\lambda(x)$. In each fixed scalar degree there are only finitely many terms, so complete reducibility and <character> independence apply degree by degree without a convergence assumption. Thus the <multiplicity-free symmetric-algebra model for polynomial GL representations> contains \b[each irreducible <polynomial representation> exactly once]. The word irreducible is necessary: arbitrary reducible <polynomial> <modules>, such as two copies of the trivial <module>, do not each occur once in a multiplicity-free sum.