$\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.
Very often one has the feeling that set-theoretic issues are somewhat cheatable, and people feel like they have eluded foundations when they manage to cheat them. Even worse, some claim that foundations are irrelevant because each time they dare to be relevant, they can be cheated. What these people haven't understood is that the best foundation is the one that allows the most cheating (without falling apart).
In the relationship between foundation and practice, though, what matters the most is the phenomenology of every-day mathematics. In order to make this statement clear, let me state the uncheatable lemma. In the later discussion, we will see the repercussion of this lemma.
Lemma (The uncheatable).
A locally small, large-cocomplete category is a poset.
The lemma shows that no matter how fat are the sets where you enrich your category, there is no chance that the category is absolutely cocomplete.
Example. In the category of sets, the large coproduct of all sets is not a set. If you enlarge the universe in such a way that it is, then some other (even larger) coproduct will not exist. This is inescapable and always boils down to the Russel Paradox.
Remark. Notice that obvious analogs of this lemma are true also for categories based on Grothendieck Universes (as opposed to sets and classes). One can't escape the truth by changing its presentation.
Excursus. Very recently Thomas Forster, Adam Lewicki, Alice Vidrine have tried to reboot category theory in Stratified Set Theory in their paper Category Theory with Stratified Set Theory (arXiv: https://arxiv.org/abs/1911.04704). One could consider this as a kind of solution to the uncheatable lemma. But it's hard to tell whether it is a true solution or a more or less equivalent linguistic reformulation. This theory is at its early stages.
At this point one could say that I haven't shown any concrete problem, we all know that the class of all sets is not a set, and it appears as a piece of quite harmless news to us.
In the rest of the discussion, I will try to show that the uncheatable lemma has consequences in the daily use of category theory. Categories will be assumed to be locally small with respect to some category of sets. Let me recall a standard result from the theory of Kan extensions.
Lemma (Kan). Let $\mathsf{B} \stackrel{f}{\leftarrow} \mathsf{A} \stackrel{g}{\to} \mathsf{C}$ be a span where $\mathsf{A}$ is small and $\mathsf{C}$ is (small) cocomplete. The the left Kan extension $\mathsf{lan}_f g$ exists.
Kan extensions are a useful tool in everyday practice, with applications in many different topics of category theory. In this lemma (which is one of the most used in this topic) the set-theoretic issue is far from being hidden: $\mathsf{A}$ needs to be small (with respect to the size of $\mathsf{C})$! There is no chance that the lemma is true when $\mathsf{A}$ is a large category. Indeed since colimits can be computed via Kan extensions, the lemma would imply that every (small) cocomplete category is large cocomplete, which is not allowed by the uncheatable. Also, there is no chance to solve the problem by saying: well, let's just consider $\mathsf{C}$ to be large-cocomplete, again because of the the uncheatable.
This problem is hard to avoid because the size of the categories of our interest is as a fact always larger than the size of their inhabitants (this just means that most of the time Ob$\mathsf{C}$ is a proper class, as big as the size of the enrichment).
Notice that the Kan extension problem recovers the Adjoint functor theorem one, because adjoints are computed via Kan extensions of identities of large categories, $$\mathsf{R} = \mathsf{lan}_\mathsf{L}(1) \qquad \mathsf{L} = \mathsf{ran}_\mathsf{R}(1) .$$ Indeed, in that case, the solution set condition is precisely what is needed in order to cut down the size of some colimits that otherwise would be too large to compute, as can be synthesized by the sharp version of the Kan lemma.
Sharp Kan lemma. Let $\mathsf{B} \stackrel{f}{\leftarrow} \mathsf{A} \stackrel{g}{\to} \mathsf{C}$ be a span where $\mathsf{B}(f-,b)$ is a is small presheaf for every $b \in \mathsf{B}$ and $\mathsf{C}$ is (small) cocomplete. Then the left Kan extension $\mathsf{lan}_f g$ exists.
Indeed this lemma allows $\mathsf{A}$ to be large, but we must pay a tribute to its presheaf category: $f$ needs to be somehow locally small (with respect to the size of $\mathsf{C}$).
Kan lemma Fortissimo. Let $ \mathsf{A} \stackrel{f}{\to} \mathsf{B} $ be a functor. The following are equivalent:
- for every $g :\mathsf{A} \to \mathsf{C}$ where $\mathsf{C}$ is a small-cocomplete category, $\mathsf{lan}_f g$ exists.
- $\mathsf{lan}_f y$ exists, where $y$ is the Yoneda embedding in the category of small presheaves $y: \mathsf{A} \to \mathcal{P}(\mathsf{A})$.
- $\mathsf{B}(f-,b)$ is a is small presheaf for every $b \in \mathsf{B}$.
Even unconsciously, the previous discussion is one of the reasons of the popularity of locally presentable categories. Indeed, having a dense generator is a good compromise between generality and tameness. As an evidence of this, in the context of accessible categories the sharp Kan lemma can be simplified.
Tame Kan lemma. Let $\mathsf{B} \stackrel{f}{\leftarrow} \mathsf{A} \stackrel{g}{\to} \mathsf{C}$ be a span of accessible categories, where $f$ is an accessible functor and $\mathsf{C}$ is (small) cocomplete. Then the left Kan extension $\mathsf{lan}_f g$ exists (and is accessible).
Warning. The proof of the previous lemma is based on the density (as opposed to codensity) of $\lambda$-presentable objects in an accessible category. Thus the lemma is not valid for the right Kan extension.
References for Sharp. I am not aware of a reference for this result. It can follow from a careful analysis of Prop. A.7 in my paper Codensity: Isbell duality, pro-objects, compactness and accessibility. The structure of the proof remains the same, presheaves must be replaced by small presheaves.
References for Tame. This is an exercise, it can follow directly from the sharp Kan lemma, but it's enough to properly combine the usual Kan lemma, Prop A.1&2 of the above-mentioned paper, and the fact that accessible functors have arity.
This answer is connected to this other.
Best Answer
There are some things like what you ask for but as Tyler points out one needs restrictions on the categories one can consider.
Any algebraic triangulated category which is well generated is equivalent to a localization of the derived category of a small DG-category - this is a theorem of Porta (ref is M. Porta, The Popescu-Gabriel theorem for triangulated categories. arXiv:0706.4458). Here algebraic (in the sense of Keller) means that the category is equivalent as a triangulated category to the stable category of a Frobenius category (Schwede has a paper on this as well giving conditions in terms of Koszul type objects).
An answer (maybe closer to what you ask) is the following. If one has a Grothendieck abelian category then Gabriel-Popescu tells you it comes from a torsion theory on some category of modules. It turns out this lifts to the level of derived categories so one can view the derived category of a Grothendieck abelian category as a localization of the derived category of R-modules for some R (in particular it comes with a fully faithful embedding into the derived category of R-modules).