Freyd-Mitchell gives a fully faithful exact functor from every small abelian category to a module category

For every small abelian category $\mathcal{A}$, there exist a unital ring $R$ and a covariant fully faithful exact functor

$\mathcal{A}⟶R\text{-}\mathbf{M}\mathbf{o}\mathbf{d}\mathrm{.}$

The result is traditionally called an embedding theorem, but under this library's stricter terminology it supplies a fully faithful exact functor, not necessarily a functor injective on objects. Equivalently, it identifies $\mathcal{A}$ up to equivalence with its essential image in the module category; it does not assert that $\mathcal{A}$ is equivalent to the whole module category.

This item is recorded rather than proved here. The smallness hypothesis is part of the statement, and the target is a category of unital left modules over a possibly noncommutative ring.

Nothing later in this page depends on this remark. The library uses it only as a statement of scope and as a contrast with the element-free proofs that follow on the exactness and diagram-lemma pages.