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: A → R-Mod.
This is quite the theorem and has several useful applications (it allows one to do diagram chasing in abstract abelian categories, etc.)
I have been asked to state and prove the theorem in class (a homological algebra course). However, by reading the texts I was recommended, I'm about to give in:
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. Impossible to do in 2:30 hours. To give you an idea, the course I'm taking is based in Rotman's "An Introduction to Homological Algebra" which works in R-Mod...
Mitchell's Theory of Categories is very hard to read, and also to prove the theorem you have tons of definitions and propositions and lemmas to prove.
Weibel's An Introduction to Homological Algebra 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!)
I'm starting to believe it's an impossible task. But maybe there are more modern proofs which require less heavy machinery and technicalities?