The Freyd-Mitchell embedding theorem

Let C be an abelian category. We construct a ring FreydMitchell.EmbeddingRing C and a functor FreydMitchell.embedding : C ⥤ ModuleCat.{max u v} (EmbeddingRing C) which is full, faithful and exact.

Overview over the proof

The usual stategy to prove the Freyd-Mitchell embedding theorem is as follows:

1. Prove that if D is a Grothendieck abelian category and F : C ⥤ Dᵒᵖ is a functor from a small category, then there is a functor G : Dᵒᵖ ⥤ ModuleCat R for a suitable R such that G is faithful and exact and F ⋙ G is full.
2. Find a suitable Grothendieck abelian category D and a full, faithful and exact functor F : C ⥤ Dᵒᵖ.

To prove (1), we proceed as follows:

1. Using the Special Adjoint Functor Theorem and the duality between subobjects and quotients in abelian categories, we have that Grothendieck abelian categories have all limits (this is shown in Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic).
2. Using the small object argument, it is shown that Grothendieck abelian categories have enough injectives (see Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives).
3. Putting these two together, it follows that Grothendieck abelian categories have an injective cogenerator (see Mathlib.CategoryTheory.Generator.Abelian).
4. By taking a coproduct of copies of the injective cogenerator, we find a projective separator G in Dᵒᵖ such that every object in the image of F is a quotient of G. Then the additive Hom functor Hom(G, ·) : Dᵒᵖ ⥤ Module (End G)ᵐᵒᵖ is faithful (because G is a separator), left exact (because it is a hom functor), right exact (because G is projective) and full (because of a combination of the aforementioned properties, see Mathlib.CategoryTheory.Abelian.Yoneda). We put this all together in the file Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite.

To prove (2), there are multiple options.

• Some sources (for example Freyd's "Abelian Categories") choose D := LeftExactFunctor C Ab. The main difficulty with this approach is that it is not obvious that D is abelian. This approach has a very algebraic flavor and requires a relatively large armount of ad-hoc reasoning.
• In the Stacks project, it is suggested to choose D := Sheaf J Ab for a suitable Grothendieck topology on Cᵒᵖ and there are reasons to believe that this D is in fact equivalent to LeftExactFunctor C Ab. This approach translates many of the interesting properties along the sheafification adjunction from a category of Ab-valued presheaves, which in turn inherits many interesting properties from the category of abelian groups.
• Kashiwara and Schapira choose D := Ind Cᵒᵖ, which can be shown to be equivalent to LeftExactFunctor C Ab (see the file Mathlib.CategoryTheory.Preadditive.Indization). This approach deduces most interesting properties from the category of types.

When work on this theorem commenced in early 2022, all three apporaches were quite out of reach. By the time the theorem was proved in early 2025, both the Sheaf approach and the Ind approach were available in mathlib. The code below uses D := Ind Cᵒᵖ.

Implementation notes

In the literature you will generally only find this theorem stated for small categories C. In Lean, we can work around this limitation by passing from C to AsSmall.{max u v} C, thereby enlarging the category of modules that we land in (which should be inconsequential in most applications) so that our embedding theorem applies to all abelian categories. If C was already a small category, then this does not change anything.

References

• https://stacks.math.columbia.edu/tag/05PL
• [M. Kashiwara, P. Schapira, Categories and Sheaves][Kashiwara2006], Section 9.6

instance CategoryTheory.Abelian.FreydMitchell.instNonemptyAsSmall {C : Type u} [Category.{v, u} C] [Abelian C] : Nonempty (AsSmall C)

def CategoryTheory.Abelian.FreydMitchell.EmbeddingRing (C : Type u) [Category.{v, u} C] [Abelian C] : Type (max u v)

Given an abelian category C, this is a ring such that there is a full, faithful and exact embedding C ⥤ ModuleCat (EmbeddingRing C).

It is probably not a good idea to unfold this.

Equations

• CategoryTheory.Abelian.FreydMitchell.EmbeddingRing C = CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing CategoryTheory.Ind.yoneda.rightOp

noncomputable instance CategoryTheory.Abelian.FreydMitchell.instRingEmbeddingRing {C : Type u} [Category.{v, u} C] [Abelian C] : Ring (EmbeddingRing C)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Abelian.FreydMitchell.functor (C : Type u) [Category.{v, u} C] [Abelian C] : Functor C (ModuleCat (EmbeddingRing C))

This is the full, faithful and exact embedding C ⥤ ModuleCat (EmbeddingRing C). The fact that such a functor exists is called the Freyd-Mitchell embedding theorem.

It is probably not a good idea to unfold this.

Equations

• CategoryTheory.Abelian.FreydMitchell.functor C = (CategoryTheory.Abelian.FreydMitchell.F✝ C).comp ((CategoryTheory.Abelian.FreydMitchell.G✝ C).comp (CategoryTheory.Abelian.FreydMitchell.H✝ C))

instance CategoryTheory.Abelian.FreydMitchell.instFaithfulModuleCatEmbeddingRingFunctor {C : Type u} [Category.{v, u} C] [Abelian C] : (functor C).Faithful

instance CategoryTheory.Abelian.FreydMitchell.instFullModuleCatEmbeddingRingFunctor {C : Type u} [Category.{v, u} C] [Abelian C] : (functor C).Full

instance CategoryTheory.Abelian.FreydMitchell.instPreservesFiniteLimitsModuleCatEmbeddingRingFunctor {C : Type u} [Category.{v, u} C] [Abelian C] : Limits.PreservesFiniteLimits (functor C)

instance CategoryTheory.Abelian.FreydMitchell.instPreservesFiniteColimitsModuleCatEmbeddingRingFunctor {C : Type u} [Category.{v, u} C] [Abelian C] : Limits.PreservesFiniteColimits (functor C)

theorem CategoryTheory.Abelian.freyd_mitchell (C : Type u) [Category.{v, u} C] [Abelian C] : ∃ (R : Type (max u v)) (x : Ring R) (F : Functor C (ModuleCat R)), F.Full ∧ F.Faithful ∧ Limits.PreservesFiniteLimits F ∧ Limits.PreservesFiniteColimits F

The Freyd-Mitchell embedding theorem. See also FreydMitchell.functor for a functor which has the relevant instances.

Stacks Tag 05PP