Freyd-Mitchell's embedding theorem Freyd–Mitchell's embedding theorem states that: if $A$ is a small abelian category, then there exists a ring R and a full, faithful and exact functor $F\colon A \to R\text{-}\mathrm{Mod}$.
I have been trying to find a proof which does not rely on so many technicalities as the ones I have found. I have leafed through:

*

*Freyd's Abelian Categories says that the text, excepting the exercises, tries to be a geodesic leading to the theorem. If you take out the exercises, probably the text is 120 pages long...


*Mitchell's Theory of Categories (pdf) is very hard to read, and also to prove the theorem you have tons of definitions and propositions and lemmas to prove. For example, the study of AB-5 categories (C3 in Mitchell's notation) is fairly tedious.


*Weibel's An Introduction to Homological Algebra (pdf) redirects me to Swan, The Theory of Sheaves, a book which is unavailable in my university's library. I've leafed through Swan's Algebraic K-Theory: the theorem is proved, but it is also long, hard and painful to read, and assumes a lot of knowledge I don't have (I had never seen a weakly effaceable functor, or a Serre subcategory; and it certainly is not well known to me that the category of additive functors from a small abelian category to the category of abelian groups is well-powered, right complete, and has injective envelopes!)
Maybe there are more modern proofs which require less heavy machinery and technicalities?
 A: $\DeclareMathOperator{\Hom}{Hom}\newcommand{\amod}{\mathscr{A}\text{-}{\bf Mod}}\newcommand{\scrA}{\mathscr{A}}\newcommand{\scrE}{\mathscr{E}}\newcommand{\Ab}{\mathbf{Ab}}\DeclareMathOperator{\Lex}{\mathbf{Lex}}\DeclareMathOperator{\coker}{Coker}$I only know one proof of the embedding theorem—the expositions differ heavily in terminology but the approaches all are equivalent, as far as I can tell. I think the proof in Swan's book on K-theory makes the relation between the Freyd-Mitchell approach and Gabriel's approach pretty clear. Let me just say that there is no cheap way of getting the Freyd-Mitchell embedding theorem since there is a considerable amount of work you need to invest in order to get all the details straight. On the other hand, if you manage to feel comfortable with the details, you will have learned quite a good amount of standard tools of homological algebra, so I think it's well worth the effort.
Think of the category of functors $\scrA \to \Ab$ as $\scrA$-modules, that's why the notation $\amod$ is fairly common. The Yoneda embedding $A \mapsto \Hom(A,{-})$ even yields a fully faithful contravariant functor $y\colon \scrA\to\amod$.
The category $\amod$ inherits a bunch of nice properties of the category $\Ab$ of abelian groups:


*

*It is abelian.

*It is complete and cocomplete ((co-)limits can be computed pointwise on objects)

*The functors $\Hom(A,{-})$ are injective and $\prod_{A \in\scrA} \Hom{(A,{-})}$ is an injective cogenerator.

*Since there is an injective cogenerator, the category $\amod$ is well-powered.

*etc.


However, the Yoneda embedding is not exact: If $0 \to A' \to A \to A'' \to 0$ is a short exact sequence, we only have an exact sequence
$$0 \to \Hom(A',{-}) \to \Hom(A,{-}) \to \Hom(A'',{-})$$
in $\amod$.
It turns out that the functor $Q = \coker{(\Hom(A,{-}) \to \Hom(A'',{-}))}$ is “weakly effaceable”, so we would want it to be zero in order to get an exact functor. How can we achieve this? Well, just force them to be zero: say a morphism $f\colon F \to G$ in $\amod$ is an isomorphism if both its kernel and its cokernel are weakly effaceable. If this works then a weakly effaceable functor $E$ is isomorphic to zero because $E \to 0$ has $E$ as kernel. Now the full subcategory $\scrE$ of weakly effaceable functors is a Serre subcategory, so we may form the Gabriel quotient $\amod/\scrE$. By its construction, isomorphisms in the Gabriel quotient have precisely the description above.
On the other hand, the category $\Lex(\scrA,\Ab)$ of left exact functors $\scrA \to \Ab$ is abelian. This is far from obvious when you start from the definitions. However, $\Lex(\scrA,\Ab)$ sits comfortably inside the abelian category $\amod$. The inclusion has an exact left adjoint (!) (= “sheafification”), so again ${\bf Lex}({\scr A}, \Ab)$ inherits many useful properties from $\amod$. Moreover, the kernel of the left adjoint can be identified with the weakly effaceable functors, and that's why $\Lex{(\scrA, \Ab)} = \amod/\scrE$.
All this work shows that $A \mapsto \Hom{(A,{-})}$ is a fully faithful and exact embedding of $\scrA$ into ${\Lex}{(\scrA, \Ab)}$, so it remains to show that the latter can be embedded into a category of modules. This is well described in Weibel's or Swan's books, so I won't elaborate on that point and content myself by saying that you simply need to look at the endomorphism ring of an injective cogenerator.
As for references, I think you can't do much better than Freyd's book. Don't be too intimidated by Swan's exposition in his K-theory book. If you're really interested in understanding this proof, I think it's worth reading the two expositions (first Freyd, then Swan). There also is a proof in volume 2 of Borceux's Handbook of categorical algebra with a more “hands on” approach.
