I was reading this pdf and was wondering if the following is valid proof for basis of these algebraic objects: The general idea is to construct a vector space $_kS$ such that we have the maps, $$ \varphi :U(X) \rightarrow {_k}S \text{ and } \varphi^{-1}:{_kS} \rightarrow U(X) $$
Let me prove the case for a basis for symmetric power, $Sym^n(V)$ for a $d$ dimensional vector space $V$.
Claim: $\{e_{i_1} \cdot \cdots \cdot e_{i_n} \} _{1 \le i_1 \le \cdots \le i_n \le d }$ forms a basis for $Sym^n(V)$.
Lemma 1.1: The multilinear $\mu$ is symmetric if and only if the value $\mu(e_{i_1}, \ldots, e_{i_n}) = w_{{i_1}\cdots_{i_n}}$ is always invariant under switching $i_j, i_{j'}$ for distinct $1 \le j ,j' \le n$.
Proof: $\dim V=d$. Define $_kS = \bigoplus_{1 \le i_1 \le \cdots \le i_n \le d } k e_{i_1, \cdots, i_n }$. We define multiplinear map, $$ \varphi':V^{\times n} \rightarrow {_kS} \text{ by } e_I \mapsto e_{I'}$$ where $I', I $ are $n$-tuples taking values in between $1$ to $d$. $I'$ is a reordering of $I$ increasing order. The map is symmetric multilinear by lemma 1.1. By universal property exists $k$-linear map, $$ \varphi: Sym^n(V) \rightarrow {_kS}, \quad e_{i_1} \cdot \cdots \cdot e_{i_n} \mapsto e_{i_1, \cdots, i_n} \text{ for } 1\le i_1 \le \cdots i_n \le d $$ Conversely, there exists a map $\psi: {_kS} \rightarrow Sym^n(V)$ such that $e_{i_1, \ldots, i_n} \mapsto e_{i_1} \cdot \cdots \cdot e_{i_n}. $
These two maps are mutual inverse, hence $_kS \cong Sym^n(V)$ giving desired basis for $Sym^n(V)$.
So this proof avoids construction of linear functionals which is a lot simpler?
This looks good, and is a very neat idea.
But there is a simple way that this is relates to the bilinear form approach: consider the dual basis $e_I^* \in ({}_kS)^*$. Then $$ e_I^*(\phi(x)) = \langle (e^*)_I, x\rangle $$ where $$ (e^*)_I = \prod_{i\in I}e^*_i \in Sym^n(V^*) $$ and $e^*_i \in V^*$ is the dual basis of $e_i$.
An advantage of the bilinear form approach is that we can apply it to the whole space $Sym(V)$ all at once without decomposing into symmetric powers. I would also not call the above simpler than the bilinear form approach; if we define $Sym(V)$ as a quotient of the tensor algebra $T(V)$, then the bilinear form $Sym(V^*)\times Sym(V) \to K$ (the field of scalars) is just the projection of the canonical, easily defined form $T(V^*)\times T(V) \to K$.
But trying to extend this idea to $Sym(V)$, we could form $$ S = \bigoplus_k {}_kS $$ and define a product in the obvious way. Let $\phi : V \to S$ be the canonical map. Now for any $v, w \in V$ we see easily that $\phi(v)\phi(w) = \phi(w)\phi(v)$, so $\phi$ extends uniquely to a homomorphism on $Sym(V)$. Now $\phi(e_I) = e_I$ essentially by definition, and has an inverse by definition of $S$ as a direct sum.
Even though we can do this, I would still prefer the bilinear form approach: