Weyl coinvariant hilbert series has order w dimension

Under the stated AC, [F1] makes multiplication by a basic invariant $f_i$ of degree $d_i$ injective on $S\mathrm{/}(f_1,\dots ,f_{i-1})$, with cokernel the next quotient. Taking finite dimensions in each degree multiplies its Hilbert series by $1-t^{d_i}$. Monomial counting gives $\mathrm{Hilb}(S,t)=(1-t{)}^{-r}$. Iterating therefore gives $\mathrm{Hilb}(S\mathrm{/}I,t)={\prod }_i(1-t^{d_i})\mathrm{/}(1-t{)}^r={\prod }_i(1+t+\cdots +t^{d_i-1})$. Evaluation at $t=1$ gives the finite dimension ${\prod }_i{d}_i$.

Fix $w\in W$, of order dividing $q=\mathrm{\mid }W\mathrm{\mid }$. On $V^{\ast }$ its operator $T$ satisfies $T^q=1$. The polynomial $z^q-1$ factors over $\mathbb{C}$ into distinct explicit roots $\exp (2\pi ia\mathrm{/}q)$. Lagrange polynomials for these roots give projections whose sum is identity and whose ranges are the corresponding eigenspaces: the polynomial identities hold modulo $z^q-1$, and evaluation at $T$ proves them. Thus a finite eigenbasis exists. If its eigenvalues are ${\lambda }_1,\dots ,{\lambda }_r$, the monomial basis of $S$ shows ${\sum }_{N\ge 0}\mathrm{tr}(w\mathrm{\mid }{S}_N)t^N={\prod }_j(1-{\lambda }_{j}t{)}^{-1}=\det (1-tw\mathrm{\mid }{V}^{\ast }{)}^{-1}$. This is a formal identity and also converges for $\mathrm{\mid }t\mathrm{\mid }<1$, since all $\mathrm{\mid }{\lambda }_j\mathrm{\mid }=1$.

On each finite-dimensional $S_N$, an idempotent has the direct decomposition into its kernel and image, and its trace is its image dimension. F3 and linearity of finite matrix trace give $\dim R_N=\mathrm{\mid }W{\mathrm{\mid }}^{-1}{\sum }_{w\in W}\mathrm{tr}(w\mathrm{\mid }{S}_N)$. Summing 1.2 and using F2 yields ${\prod }_i(1-t^{d_i}{)}^{-1}=\mathrm{\mid }W{\mathrm{\mid }}^{-1}{\sum }_w\det (1-tw\mathrm{\mid }{V}^{\ast }{)}^{-1}$. Multiply by $(1-t{)}^r$ and let real $t$ tend to $1$ from below. The left side tends to ${\prod }_i{d}_i^{-1}$. The identity summand on the right tends to $1\mathrm{/}\mathrm{\mid }W\mathrm{\mid }$. Every nonidentity operator has fewer than $r$ eigenvalues equal to one: 1.2 gives diagonalizability, and faithfulness excludes the identity operator. Its remaining factors have nonzero limits, so its contribution tends to zero. Hence ${\prod }_i{d}_i=\mathrm{\mid }W\mathrm{\mid }$.

Together 1.1 and 2.1 prove the claims. For $r=0$, faithfulness forces $W=\{1\}$, the products are empty products equal to $1$, and $S\mathrm{/}I=\mathbb{C}$. Degree-one invariants contribute the factor $1$ and do not obstruct the strict eigenvalue-count argument for a nonidentity element, even when $W$ has a fixed subspace. The finite eigenbasis selections in step 1.2 need no choice principle; the stated AC premise discharges [F1]'s current general regularity proof.