I am struggling to understand Theorem V.2.1 in Christian Kassel's Quantum Groups page 95. The Theorem is stated as follows.
Let $L$ be a Lie algebra. Given any associative algebra $A$ and any morphism for Lie algebras $f$ from $L$ into $L(A)$, there exists a unique morphism of algebras $\varphi(U(L))\rightarrow A$ such that $\varphi\circ\iota_L=f$.
The proof he gives is as follows.
Proof. By definition of the tensor algebra, $f$ extends to a morphism of algebras $\bar{f}$ from $T(L)$ to $A$ defined by $\bar{f}(x_1...x_n)=f(x_1)...f(x_n)$ for $x_1,...,x_n$ in $L$. The existence of $\varphi$ follows from $\bar{f}(I(L))=\{0\}$. In order to prove this fact, we only have to show that $\bar{f}(xy-yx-[x,y])$ vanishes for any pair $(x,y)$ of elements of $L$. Now, $$ \bar{f}(xy-yx-[x,y])=f(x)f(y)-f(y)f(x)-f([x,y]), $$ which is zero since $f$ is a morphism of Lie algebras.
The uniqueness of $\varphi$ is due to the fact that $L$ generates the algebra $T(L)$ hence $U(L)$.
There is quite a lot going on here so if more clarification is needed comment and I will add it.
How is he defining $\varphi$? He simply says that it exists because $\bar{f}(I(L))=\{0\}$ and that it is unique because $L$ generates $T(L)$. I get that these statements are true but I cannot work out why he can simply claim existence and uniqueness.
Any help is greatly appreciated.
I was struggling to prove PBW as you did years ago. So I will write down the proof I summarized (which is essentially the same as the one you provided, but with more details of course.) Let me know if you have any questions.
Let us fix some notations first. Let $\mathfrak{g}$ be a Lie algebra, $\mathcal{T}(\mathfrak{g})$ and $\mathfrak{U(g)}$ be the associated tensor algebra and universal enveloping algebra respectively.
It is not hard to prove $\sigma([x,y])=\sigma(x)\sigma(y)-\sigma(y)\sigma(x).$
Bare this in mind, let's write down the universal property.
We first define an algebra homomorphism $\varphi':\mathcal{T}(\mathfrak{g})\to\mathcal{A}$ by $$\varphi'(x_1\otimes\cdots\otimes x_k)=\rho(x_1)\cdots\rho(x_k).$$Since $\rho$ is linear, the map $\varphi'$ is well-defined, and it is straightforward to check $\varphi'$ is a homomorphism. In particular, for all homogeneous $x,y$ in $\mathfrak{g}$, we have $$\varphi'(x\otimes y-y\otimes x-[x,y])=\rho(x)\rho(y)-\rho(y)\rho(x)-\rho([x,y]),$$which is $0$ by the hypothesis of $\rho$. Thus $\varphi'$ factors through to an algebra homomorphism $\varphi:\mathfrak{U(g)}\to\mathcal{A}$ such that $\varphi\circ\sigma=\rho$.
To prove uniqueness, let $\varphi':\mathfrak{U(g)}\to\mathcal{A}$ be another algebra homomorphism satisfying our assumption. Then for any $x\in\mathfrak{g}$, we have $\varphi'(\sigma(x))=\rho(x)=\varphi(\sigma(x))$. Thus $\varphi'=\varphi$ on $\mathfrak{U(g)}$ since $\sigma(\mathfrak{g})$ generates $\mathfrak{U(g)}$.