[Freyd–Mitchell's embedding theorem][1] 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](http://www.tac.mta.ca/tac/reprints/articles/3/tr3abs.html)_ 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](https://www.sciencedirect.com/bookseries/pure-and-applied-mathematics/vol/17/suppl/C)_ ([pdf](https://www.maths.ed.ac.uk/~v1ranick/papers/mitchell.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](https://doi.org/10.1017/CBO9781139644136)_ ([pdf](https://people.math.rochester.edu/faculty/doug/otherpapers/weibel-hom.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](https://doi.org/10.1007/BFb0080281)_: 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?

  [1]: https://en.wikipedia.org/wiki/Mitchell's_embedding_theorem