Freyd–Mitchell embedding theorem

Remarks

The idea of the proof is to embed $\mathcal{A}$, by a Yoneda-type construction, into a category of left exact functors from $\mathcal{A}$ to abelian groups. That category is abelian and has enough injectives and a generator, which leads to an abelian category with a projective generator $P$ containing a copy of $\mathcal{A}$. One then takes $R$ to be the endomorphism ring of a suitable such generator and uses the functor $\Hom(P, -)$. Since $F$ is full, faithful and exact, a diagram in $\mathcal{A}$ commutes, or a sequence in $\mathcal{A}$ is exact, exactly when its image under $F$ does. So a diagram lemma such as the five lemma or the snake lemma can be proved in an arbitrary abelian category by chasing elements of modules. For a large abelian category, one applies the theorem to a small full abelian subcategory that contains the given diagram and is closed under kernels and cokernels.

Going deeper

For a student

The main use of the theorem is to justify element chasing. A statement about a finite diagram of objects and morphisms in an abelian category can be transferred to modules, proved there with elements, and transferred back. This is why many texts prove diagram lemmas only for modules. An alternative that stays inside the category is the method of pseudo-elements. The Gabriel–Popescu theorem is a related embedding result for Grothendieck categories, where the functor is not exact but has an exact left adjoint.