Grothendieck abelian categories have functorial injective embeddings

By [L1], fix a generator $U$. For any object $M$, iterate the functor [L3] transfinitely: $M=M_0\to M_1\to M_2\to \cdots \mathrm{.}$ By [L4] and [L5], every transition map is monic, so the composite $M\to M_{\lambda }$ is a monomorphism for every limit stage $\lambda$.

Choose a limit stage $\lambda$ as in [L5]. Then [L6] makes $M_{\lambda }$ injective. Because [L3] is functorial at successor stages and colimits preserve that functoriality at limit stages, the assignment $M\mapsto M_{\lambda }$ is a functor, and the composite $M\to M_{\lambda }$ is natural.

Writing $E(M):=M_{\lambda }$, the maps ${\eta }_M:M\to E(M)$ give functorial injective embeddings. The detecting lemma [L2] is the reason the transfinite construction closes at stage $\lambda$.