Kostant harmonic decomposition of the symmetric algebra

Fix finite bases of $\mathfrak{h}$ and $\mathfrak{n}$. Polynomial monomials identify $S$ with $S(\mathfrak{h})\otimes S(\mathfrak{n})$. Give a Cartan generator weight two and a root-space generator weight one; filter by total weight. This is an increasing filtration indexed by nonnegative integers and every polynomial has finite weight. A homogeneous polynomial of ordinary degree $d$ has weights between $d$ and $2d$, and its weight-$2d$ part is exactly its projection onto $S^d(\mathfrak{h})$. By F2 each $q_i$ has a unique homogeneous inverse image $p_i\in R$ of degree $d_i$. Its leading weighted part is $q_i$, since $q_i\mathrm{\ne }0$. F2 also gives $R=\mathbb{C}[p_1,\dots ,p_r]$ with algebraically independent generators.

Let $z^a$ range over the monomials in the fixed root-space basis, and set $e_{j,a}=b_j{z}^a$. In the polynomial algebra with its weight grading these form a free basis over $\mathbb{C}[q_1,\dots ,q_r]$: expand first in the independent root monomials, then use F3 for each coefficient. Their ordinary degrees are $\mathrm{deg}{b}_j+\mathrm{\mid }a\mathrm{\mid }$ and their weights are $2\mathrm{deg}{b}_j+\mathrm{\mid }a\mathrm{\mid }$. We prove that exactly the same polynomials form a graded free $R$-basis of $S$.

For spanning, take an ordinary homogeneous $s\in S_d$ of weight $N$. Express its leading weighted part uniquely in the basis from step 2.1. Since that basis and the $q_i$ are homogeneous for both degrees, only monomials $q^k{e}_{j,a}$ having ordinary degree $d$ and weight $N$ occur. Replace $q^k$ by $p^k$ and subtract this finite sum from $s$. Step 1.1 makes its leading part identical, so the remainder has strictly smaller weight and the same ordinary degree. Repeat; after at most $N+1$ decreases the remainder is zero. This proves spanning by finite expressions. For independence, suppose a nonzero finite expression $\sum c_{j,a}(p)e_{j,a}$ vanishes. Give the variables in each coefficient weight $2d_i$ and take the largest total weight among its nonzero monomials, including the weight of $e_{j,a}$. The leading part of the expression is the corresponding sum of $q$-coefficient terms in the free basis of step 2.1. Algebraic independence of the $q_i$ and that free basis show this sum is nonzero, a contradiction. Thus we have the stated free decomposition; ordinary degrees were preserved throughout.

Quotienting this free decomposition by $(p_1,\dots ,p_r)S=I$ shows that the classes of the $e_{j,a}$ form a homogeneous complex basis of $S\mathrm{/}I$. In each ordinary degree only finitely many of them occur: $j$ has finitely many possibilities and root monomials of bounded degree in finitely many variables form a finite set. F1 identifies $\mathcal{H}$ with $S\mathrm{/}I$ by the quotient map, degree by degree. Consequently, in every degree $d$, the spaces $(R\otimes \mathcal{H}{)}_d$ and $S_d$ have equal finite dimensions, by replacing each basis class of $S\mathrm{/}I$ in the free decomposition with its degree-preserving harmonic representative. This argument uses the canonical inverse of F1's quotient isomorphism, and makes no infinite sequence of basis choices.

Multiplication $R\otimes \mathcal{H}\to S$ is surjective by induction on ordinary degree. For homogeneous $s\in S_d$, F1 writes $s=h+i$ with $h\in {\mathcal{H}}_d$ and $i\in I_d$. The ideal $I$ is generated by the finitely many $p_i$, so its degree-$d$ part consists of sums ${\sum }_i{p}_i{s}_i$ with $s_i\in S_{d-d_i}$; obtain these homogeneous coefficients by taking components of any ideal expression. Each $d_i>0$, so the induction expresses every $s_i$ as a sum of invariant multiples of harmonics. Multiplying those expressions by $p_i$ proves the step. At degree zero the assertion follows from $I_0=0$. Equal finite dimensions from step 4.1 now make this surjection injective degreewise, hence an isomorphism on the algebraic graded direct sums.

The adjoint action is a derivation, annihilates $R$ and preserves $\mathcal{H}$ by F1. Therefore $x\cdot (rh)=r(x\cdot h)$, exactly the tensor-product action, so the isomorphism is $\mathfrak{g}$-equivariant. For $\mathfrak{g}=0$ all polynomial algebras are $\mathbb{C}$ and the map is scalar multiplication. The proof selected only finite bases and finitely many generators; all infinite monomial collections are explicitly indexed by finite tuples of nonnegative integers, and all reductions terminate. No AC is used.