---
tag: 8V296XR2M3
kind: statement
role: theorem
name: Freyd–Mitchell embedding theorem
msc: ["18E20", "18E10"]
uses: [Y9CZ3MTNF1, 28NQ0KRHD3, GRG8WEBSH5, S1G61TDW0K, JBSSXP4FFY, 0B1261B5ED, 1WV2THA6NY, 3MP41FQHZ5]
about: [Y9CZ3MTNF1]
sources:
  - url: https://en.wikipedia.org/wiki/Mitchell%27s_embedding_theorem
same_as:
  wikidata: Q1148215
  wikipedia: Mitchell's embedding theorem
---

## Statement

Let $\mathcal{A}$ be a small [[abelian category|Y9CZ3MTNF1]], that is, an abelian category whose objects form a set.
Then there exist a [[ring|0B1261B5ED]] $R$ with identity and a [[functor|28NQ0KRHD3]] $F \colon \mathcal{A} \to R\text{-}\mathrm{Mod}$ into the [[category of left $R$-modules|JBSSXP4FFY]] such that:

1. $F$ is [[full and faithful|GRG8WEBSH5]];
2. $F$ is an [[exact functor|S1G61TDW0K]].

## Remarks

The idea of the proof is to embed $\mathcal{A}$, by a Yoneda-type construction, into a category of left exact functors from $\mathcal{A}$ to abelian groups.
That category is abelian and has enough injectives and a generator, which leads to an abelian category with a projective generator $P$ containing a copy of $\mathcal{A}$.
One then takes $R$ to be the endomorphism ring of a suitable such generator and uses the functor $\Hom(P, -)$.
Since $F$ is full, faithful and exact, a diagram in $\mathcal{A}$ commutes, or a sequence in $\mathcal{A}$ is exact, exactly when its image under $F$ does.
So a diagram lemma such as the five lemma or the snake lemma can be proved in an arbitrary abelian category by chasing elements of modules.
For a large abelian category, one applies the theorem to a small full abelian subcategory that contains the given diagram and is closed under kernels and cokernels.

## Explanations

### L1 human

Abelian categories are an abstract setting for kernels, cokernels and exact sequences.
The theorem says that a small abelian category is, up to a faithful copy, just a part of a category of modules over some ring.
So nothing new can happen in an abstract abelian category that does not already happen for modules.

### L2 human

The main use of the theorem is to justify element chasing.
A statement about a finite diagram of objects and morphisms in an abelian category can be transferred to modules, proved there with elements, and transferred back.
This is why many texts prove diagram lemmas only for modules.
An alternative that stays inside the category is the method of [[pseudo-elements|1WV2THA6NY]].
The [[Gabriel–Popescu theorem|3MP41FQHZ5]] is a related embedding result for Grothendieck categories, where the functor is not exact but has an exact left adjoint.