Grothendieck abelian categories have functorial injective embeddings

By [L1], fix a generator $U$ and, using [A1], fix representatives of its subobjects once for the functor [L3]. The set of these subobjects has a cardinality $\kappa$ under [A1]; composition with $N\rightarrowtail U$ bounds the number of subobjects of every $N\subseteq U$ by $\kappa$. Put $\nu =\max (\kappa ,{\mathrm{\aleph }}_0)$; by [L8], write $\nu ={\mathrm{\aleph }}_{\alpha }$, and set $\lambda ={\mathrm{\aleph }}_{\alpha +1}$. The successor aleph exists and [A1, L7] give $\mathrm{cf}(\lambda )=\lambda >\kappa$. This choice of $\lambda$ depends on $U$, not on $M$.

For any object $M$, iterate the fixed functor [L3] to the common ordinal $\lambda$ from step 1.1. By [L4, L5], every transition map is monic, so $M\to M_{\lambda }$ is monic. Since $\lambda$ is a limit ordinal and its cofinality exceeds $\kappa$, [L6] makes $M_{\lambda }$ injective. The same fixed representative set and ordinal work for every $M$; successor-stage functoriality and the universal property of limit-stage colimits therefore make $M\mapsto M_{\lambda }$ a functor and $M\to M_{\lambda }$ 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$.