Weyl-invariant polynomials on the Cartan extend to invariant polynomials on $\mathfrak{g}$

By [F0] under the stated Choice assumption, fix a positive system for the root system of the supplied Cartan. Fix a degree $n$. For each dominant integral weight $\lambda$, let $L(\lambda )$ be supplied by Finite-dimensional simple modules are classified by dominant highest weights and define $F_{\lambda ,n}(x):={\mathrm{tr}}_{L(\lambda )}({\rho }_{\lambda }(x{)}^n)\mathrm{.}$ Conjugation of ${\rho }_{\lambda }(x)$ does not change its trace, so $F_{\lambda ,n}\in S^n(\mathfrak{g}{)}^{\mathfrak{g}}$. On $h\in \mathfrak{h}$ its value is the sum of $\mu (h{)}^n$ over the weights $\mu$ of $L(\lambda )$, with multiplicity.

Let $M_{\lambda ,n}(h):={\sum }_{\mu \in W\lambda }\mu (h{)}^n\mathrm{.}$ Apply the finite inverse expansion in [F2] to the linear map $e^{\mu }\mapsto \mu (h{)}^n$. Step 1.1 then makes every $M_{\lambda ,n}$ a finite linear combination of restrictions of the $F_{\nu ,n}$.

The pure powers ${\mathrm{\ell }}^n$ with $\mathrm{\ell }\in {\mathfrak{h}}^{\ast }$ span $S^n(\mathfrak{h})$ by polarization. Dominant integral weights still suffice: in fundamental-weight coordinates they contain ${\mathbb{N}}_0^r$, and a polynomial vanishing on this grid is zero by induction on $r$, using the one-variable fact that a nonzero polynomial has finitely many roots. Thus the powers of dominant weights span, since any linear functional annihilating them gives a homogeneous polynomial vanishing on the grid. Averaging over the finite Weyl group [F1] shows that the orbit averages $M_{\lambda ,n}\mathrm{/}\mathrm{\mid }W\lambda \mathrm{\mid }$ span $S^n(\mathfrak{h}{)}^W$. Together with step 2.1, this proves that every homogeneous Weyl invariant of degree $n$ is the restriction of an element of $S^n(\mathfrak{g}{)}^{\mathfrak{g}}$.

Apply step 3.1 to every homogeneous component of $p$ and sum the resulting invariant extensions to obtain $P\in S(\mathfrak{g}{)}^{\mathfrak{g}}$ with $P{\mathrm{\mid }}_{\mathfrak{h}}=p$. If $P^{\mathrm{\prime }}$ is another extension, then $P-P^{\mathrm{\prime }}$ restricts to zero, so An invariant polynomial is determined by its restriction to a Cartan subalgebra gives $P=P^{\mathrm{\prime }}$. Thus the extension is unique.