Examples of applications of the Freyd-Mitchell embedding theorem. The Freyd-Mitchell embedding theorem states the following:

Let $\mathcal{A}$ be a small abelian category. There exists a unital ring $R$ and a full, faithful and exact functor $F\colon\mathcal{A}\rightarrow R\mathcal{Mod}$, where $R\mathcal{Mod}$ is the (abelian) category of (left) $R$-modules.

I am searching for (elementary and non-elementary, useful and non-useful) applications of this theorem. I am also interested in applications, for which one does not necessarly need the embedding theorem.
The only "real" application I know at the moment is all about diagram chasing: 

Checking exactness of diagrams in arbitrary abelian categories can be done by checking those in the categories of $R$-modules, where one can apply element-wise diagram chasing. 

(This can be made precise, what is e.g. done in Freyd's "Abelian Categories - An Introduction to the Theory of Functors".)
 A: An interesting class of examples comes from the following construction, also due to Freyd.  Let $\mathcal{T}$ be a small triangulated category.  Form a new category $\mathcal{A}$, with one object $I(u)$ for each morphism $u$ in $\mathcal{T}$.  The morphisms from $I(u:A\to B)$ to $I(v:C\to D)$ are the pairs $(f:A\to C,g:B\to D)$ such that $gu=vf$, modulo those for which $gu=vf=0$.  There is a functor $J:\mathcal{T}\to\mathcal{A}$ given by $J(X)=I(1_X)$.  One can show that $\mathcal{A}$ is abelian, that $J$ is full and faithful, and that the essential image of $J$ is the subcategory of projective objects, which is the same as the subcategory of injective objects.
I think that the embedding theorem is much less obvious for these abelian categories than it is for the more usual examples.
As a special case, we can take $\mathcal{T}$ to be the category of finite spectra in the sense of stable homotopy theory.  The embedding theorem, combined with the above construction, tells us that $\mathcal{T}$ embeds in the category of $R$-modules for some $R$ (which is not unique).  Freyd also conjectured more specifically that in this case the stable homotopy functor gives a full and faithful embedding of $\mathcal{T}$ in the category of modules over the ring of stable homotopy groups of spheres (and he proved that many interesting consequences would follow from that).  This conjecture is still wide open half a century later.  
