Let A be an abelian category. In the stacks project this means that A has a set of objects, and that

• A is a pre-additive category with a zero object and direct sums, i.e., an additive category,
• A has all kernels and cokernels (and hence all finite limits and all finite colimits), and
• Coim(f) = Im(f) for all morphisms f in A

Martin Olsson pointed out that there is a simple direct argument which proves that in such a category any epimorphism (called a surjection in the following) is a universal epimorphism, see Lemma Tag 05PK. Using this fact we obtain a site C whose underlying category is simply A and where a covering is the same thing as a single surjective morphism. Then the Yoneda functor gives a fully faithful, exact functor

A —> Ab(C), X —> h_X

into the category of abelian sheaves, see Lemma Tag 05PN. Combining this with results on abelian sheaves one obtains a proof of Mitchell’s embedding theorem for abelian categories, see Remark Tag 05PR.

I like the argument phrased in this way because I already know about sites, sheaves, etc. It in some sense explains to me (and hopefully an additional handful of readers here) why the embedding theorem should be true. Moreover, I want to make the point that for all applications I can imagine the embedding into the category of abelian sheaves on a site is sufficient.