Injectivity of Rewrite Rule in a Free Lie Algebra Let $L$ be a free Lie algebra (over $\mathbb{Q}$) on generators $x_1, x_2, \ldots, x_n$, and let $V_k$ be the subspace spanned by the $k$-fold brackets.  Let $U_1 = \mathrm{span}\{ x_i | i< n\}\subseteq V_1$ and let $W_n \subseteq V_n$ be the span of the $n$-fold brackets that involve $x_n$ at least once.
The bracket defines a function $V_k\otimes V_\ell \to V_{k+\ell}$ (which is what I think of as bracketing and rewriting in terms of a chosen basis, but actually it's just bracketing). 
Question:  Is the composition 
$$
U_1 \otimes W_m \to  V_1\otimes V_m \to V_{m+1}
$$
injective?  ($m$ has no particular relation to $n$)
I have asked MAPLE to compute the dimensions of these vector spaces and it seems that the dimension of the target is generally large enough to accommodate such an injection (though I haven't proved a dimension inequality yet).
 A: Yes.  Embed the free Lie algebra in the free associative algebra, then consider the monomial with $x_n$ as far right as possible (i.e., with the largest number of other $\{x_i,i\leq n\}$ before it): it won't be cancelled.  Let me now give details.
Consider $F$ the free (associative but non-commutative) algebra (over $\mathbb{Q}$) on generators $x_1,\ldots,x_n$.  Let $[P,Q]_F = P Q - Q P \in F$ be the usual commutator for elements $P,Q\in F$.  Consider $L_F$ the smallest subset of $F$ containing $x_1,\ldots,x_n$ which is closed under commutators and linear combinations.  Then $L_F$ endowed with the Lie bracket $[\cdot,\cdot]_F$ is isomorphic to the free Lie algebra $L$.
Under this isomorphism, $U_1$ is still the span of $x_1,\ldots,x_{n-1}$, and $W_m$ is included in the vector space $W^F_m$ of polynomials in $x_1,\ldots,x_n$ with no monomial independent of $x_n$.  An element of $U_1\otimes W^F_m$ is $\sum_{i=1}^{n-1} x_i \otimes P_i$ for some $P_i\in W^F_m$.  Its image under the composition you care about is $S = \sum_{i=1}^{n-1} (x_i P_i - P_i x_i)$.  Since everything is linear, we just need to show that $S \neq 0$ assuming that not all $P_i = 0$.
Among all monomials of all $P_i$, consider $m = x_{a_1} \cdots x_{a_k} x_n x_{b_1} \cdots x_{b_l}$ with $k$ maximal.  Say it is in $P_j$.  Then $S$ contains the monomial $x_j m = x_j x_{a_1} \cdots x_{a_k} x_n x_{b_1} \cdots x_{b_l}$ with some non-zero coefficient coming from $x_j P_j$, and this monomial does not appear in any other term of $S$.  Indeed, the monomial cannot appear in $x_i P_i$ for $i\neq j$ since it starts with $x_j$ and not $x_i$, and the monomial cannot appear in $P_i x_i$ for any $i$ since this would require the presence in $P_i$ of a monomial $m'$ starting with $x_j x_{a_1} \cdots x_{a_k} x_n$, which contradicts the maximality of $k$.
It is probably possible to extend the proof to show that $U_k \otimes W_m \to V_{k + m}$ is injective, where $U_k$ is the span of $(k-1)$-fold brackets of $\{x_i, i<n\}$.
