[proofplan] Let $k$ be the commutative ring with identity from the theorem statement, and let $\operatorname{Sym}(k)$ be the ring of [symmetric functions](/page/Symmetric%20Function) over $k$. We prove injectivity of the homomorphism sending formal variables to the positive-degree elementary symmetric functions $e_m$ for $m \ge 1$; the degree-zero elementary symmetric function $e_0=1$ is not part of the family under consideration. Every polynomial relation involves only finitely many formal variables, so we test such a relation after projecting symmetric functions to a finite [polynomial ring](/page/Polynomial%20Ring) with at least that many ordinary variables. In that finite-variable ring, the [fundamental theorem of symmetric polynomials](/theorems/5179) says that the elementary symmetric polynomials form polynomial coordinates; hence a nonzero polynomial expression in the relevant coordinates cannot vanish. [/proofplan] [step:Reduce an algebraic relation to finitely many elementary symmetric functions] Define the $k$-algebra homomorphism \begin{align*} \Phi: k[T_1,T_2,T_3,\dots] &\to \operatorname{Sym}(k) \\ T_m &\mapsto e_m . \end{align*} To prove that the positive-degree family $e_1,e_2,e_3,\dots$ is [algebraically independent](/page/Algebraic%20Independence) over $k$, it is enough to prove that $\Phi$ is injective. The degree-zero elementary symmetric function $e_0=1$ is excluded, since adjoining $e_0$ would give the algebraic relation $e_0-1=0$. Let $F \in k[T_1,T_2,T_3,\dots]$ satisfy $\Phi(F)=0$. Since a polynomial contains only finitely many indeterminates, there exists $r \in \mathbb{N}$ such that \begin{align*} F \in k[T_1,\dots,T_r] \subset k[T_1,T_2,T_3,\dots]. \end{align*} We will prove $F=0$ in $k[T_1,\dots,T_r]$. [/step] [step:Specialize symmetric functions to $n$ variables] Choose an integer $n \ge r$. Let $\operatorname{Sym}_n(k)$ denote the subring of symmetric polynomials in $k[x_1,\dots,x_n]$. For each $m \in \{1,\dots,n\}$, let $e_{m,n} \in \operatorname{Sym}_n(k)$ denote the $m$-th elementary symmetric polynomial in the variables $x_1,\dots,x_n$. Let \begin{align*} \rho_n: \operatorname{Sym}(k) &\to \operatorname{Sym}_n(k) \end{align*} denote the specialization homomorphism associated to the standard stable, equivalently inverse-limit, definition of $\operatorname{Sym}(k)$: it sends a symmetric function to the symmetric polynomial obtained in the first $n$ variables by setting $x_j=0$ for every $j>n$. This homomorphism satisfies \begin{align*} \rho_n(e_m) = \begin{cases} e_{m,n}, & 1 \le m \le n,\\ 0, & m > n, \end{cases} \end{align*} because every monomial in $e_m$ using an index greater than $n$ is killed, while the remaining monomials are exactly the $m$-th elementary symmetric polynomial in $x_1,\dots,x_n$. Applying $\rho_n$ to the equality $\Phi(F)=0$ gives \begin{align*} F(e_{1,n},\dots,e_{r,n})=0 \end{align*} inside $\operatorname{Sym}_n(k)$. [/step] [step:Use the fundamental theorem of symmetric polynomials in $n$ variables] Since $k$ is a commutative ring with identity and $\operatorname{Sym}_n(k)$ is the subring of symmetric polynomials in $k[x_1,\dots,x_n]$, the hypotheses of the [Fundamental Theorem of Symmetric Polynomials](/page/Fundamental%20Theorem%20of%20Symmetric%20Polynomials) over a commutative ring with identity apply. Therefore the $k$-algebra homomorphism \begin{align*} \Psi_n: k[Y_1,\dots,Y_n] &\to \operatorname{Sym}_n(k) \\ Y_m &\mapsto e_{m,n} \end{align*} is an isomorphism. In particular, $\Psi_n$ is injective. Let \begin{align*} \iota_{r,n}: k[T_1,\dots,T_r] &\to k[Y_1,\dots,Y_n] \\ T_m &\mapsto Y_m \end{align*} be the natural inclusion of polynomial rings. The equality $F(e_{1,n},\dots,e_{r,n})=0$ is exactly \begin{align*} \Psi_n(\iota_{r,n}(F))=0. \end{align*} Since $\Psi_n$ is injective, $\iota_{r,n}(F)=0$ in $k[Y_1,\dots,Y_n]$. Since $\iota_{r,n}$ preserves every coefficient of every monomial in $T_1,\dots,T_r$, it is injective, and hence $F=0$ in $k[T_1,\dots,T_r]$. [guided] Recall the setup needed for this step. The homomorphism \begin{align*} \Phi: k[T_1,T_2,T_3,\dots] &\to \operatorname{Sym}(k) \\ T_m &\mapsto e_m \end{align*} was defined to test algebraic relations among the elementary symmetric functions. We fixed $F \in k[T_1,T_2,T_3,\dots]$ with $\Phi(F)=0$, then chose $r \in \mathbb{N}$ such that $F \in k[T_1,\dots,T_r]$. We now choose an integer $n \ge r$ and write $e_{m,n} \in \operatorname{Sym}_n(k)$ for the $m$-th elementary symmetric polynomial in $x_1,\dots,x_n$. Applying the specialization map $\rho_n: \operatorname{Sym}(k) \to \operatorname{Sym}_n(k)$ gives \begin{align*} F(e_{1,n},\dots,e_{r,n})=0 \end{align*} in $\operatorname{Sym}_n(k)$, because every $e_m$ with $m \le r \le n$ specializes to $e_{m,n}$. The point of passing to $n$ variables is that there is a concrete polynomial ring where the elementary symmetric polynomials are known to be independent coordinates. We choose $n \ge r$ because the possible relation $F$ involves only $T_1,\dots,T_r$, so all elementary symmetric polynomials appearing in the relation survive under specialization to $n$ variables. Since $k$ is a commutative ring with identity and $\operatorname{Sym}_n(k)$ is the subring of symmetric polynomials in $k[x_1,\dots,x_n]$, the hypotheses of the finite-variable form recorded in [Fundamental Theorem of Symmetric Polynomials](/page/Fundamental%20Theorem%20of%20Symmetric%20Polynomials) over a commutative ring with identity apply. Let \begin{align*} \Psi_n: k[Y_1,\dots,Y_n] &\to \operatorname{Sym}_n(k) \\ Y_m &\mapsto e_{m,n} \end{align*} be the homomorphism from a polynomial ring in $n$ formal variables to the ring of symmetric polynomials in $x_1,\dots,x_n$. The theorem says that $\Psi_n$ is an isomorphism: every symmetric polynomial in $x_1,\dots,x_n$ is uniquely expressible as a polynomial in $e_{1,n},\dots,e_{n,n}$. We use both parts of this statement only through injectivity. Injectivity means that if a polynomial expression in $e_{1,n},\dots,e_{n,n}$ is zero, then the corresponding formal polynomial in $Y_1,\dots,Y_n$ was already zero. Now define \begin{align*} \iota_{r,n}: k[T_1,\dots,T_r] &\to k[Y_1,\dots,Y_n] \\ T_m &\mapsto Y_m . \end{align*} This is the map that regards a polynomial in the first $r$ variables as a polynomial in $n$ variables that simply does not use $Y_{r+1},\dots,Y_n$. The specialization equality is \begin{align*} F(e_{1,n},\dots,e_{r,n})=0. \end{align*} By the definitions of $\Psi_n$ and $\iota_{r,n}$, this equality can be rewritten as \begin{align*} \Psi_n(\iota_{r,n}(F))=0. \end{align*} Since $\Psi_n$ is injective, we obtain \begin{align*} \iota_{r,n}(F)=0. \end{align*} It remains to justify that this forces $F=0$. The map $\iota_{r,n}$ does not combine monomials or alter coefficients; it sends each monomial \begin{align*} T_1^{a_1}\cdots T_r^{a_r} \end{align*} to the distinct monomial \begin{align*} Y_1^{a_1}\cdots Y_r^{a_r} \end{align*} in $k[Y_1,\dots,Y_n]$. Therefore a polynomial has image zero under $\iota_{r,n}$ exactly when all of its coefficients are zero. Hence $F=0$ in $k[T_1,\dots,T_r]$. [/guided] [/step] [step:Conclude injectivity of the universal homomorphism] We have shown that every $F \in k[T_1,T_2,T_3,\dots]$ satisfying $\Phi(F)=0$ is zero. Therefore $\ker \Phi=\{0\}$, so $\Phi$ is injective. Hence the positive-degree elementary symmetric functions $e_1,e_2,e_3,\dots$ are [algebraically independent](/page/Algebraic%20Independence) over $k$. [/step]