Category theory · existing Mathlib declaration

Freyd–Mitchell Embedding Theorem

Given any abelian category, Mathlib supplies some ring and a way to represent the category inside that ring's module category. Distinct arrows remain distinct, every arrow between represented objects comes from the original category, and finite limit and finite colimit constructions are preserved.

abelian category
module category
full functor
faithful functor
finite limits
finite colimits
exact embedding

The theorem at a glance

Freyd–Mitchell at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

A dark green and ivory theorem poster sends an abelian category downward into a highlighted proper subdiagram of modules over some ring and states full, faithful, finite-limit, and finite-colimit preservation. — The endpoint is an exact embedding into modules over some ring, not an equivalence with every module.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

Original pixels inspected after a targeted correction. The four stage labels are exactly C, AsSmall C, Ind opposite stage, and ModuleCat R; the three main arrow labels are exactly F, G, and H; every main arrow points left-to-right. The full-width bracket correctly assigns COMPOSITE FUNCTOR, FULL • FAITHFUL, and PRESERVES FINITE LIMITS • FINITE COLIMITS to the composite rather than one intermediate arrow. All labels are perfectly spelled and appear once. The cone and cocone insets are now fully unlabeled; the highlighted image in ModuleCat R is an unlabeled proper subdiagram surrounded by additional ambient nodes. There is no reverse arrow, equivalence symbol, arbitrary-limit wording, crop, watermark, pseudo-writing, or remaining mathematical/text defect. — A full, faithful functor embeds the abelian category into modules over some ring and preserves finite limits and finite colimits.

Complementary intuition

A mathematical landmark

The Freyd–Mitchell theorem connects abstract abelian categories with concrete module categories. It explains why many arguments about kernels, cokernels, exact sequences, and diagram chasing can be understood through module-like models without identifying the entire abstract category with every module over a ring.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

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

Selected evidence declaration text

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

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Claim boundary

No new theorem is claimed

This target indexes Mathlib's existential Freyd–Mitchell endpoint for a category C equipped with an Abelian instance: there exist a ring R and a functor F : C ⥤ ModuleCat R that is full, faithful, preserves finite limits, and preserves finite colimits. The universe of R and the module category is max u v. The statement is an embedding into a module category, not an equivalence onto that whole category.

Proof Atlas did not originate the Freyd–Mitchell theorem or Mathlib's declaration.
The selected theorem does not assert that C is equivalent to the entire category of modules over R.
The existentially supplied ring is not claimed to be a fixed familiar ring or canonical for every purpose.
The endpoint states preservation of finite limits and finite colimits, not arbitrary limits and colimits.
The generated explanation and visuals are not proof evidence.

Provenance

Origin and evidence stay separate

Existing declaration: CategoryTheory.Abelian.freyd_mitchell in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.freyd-mitchell-embedding-theorem.v001
Source handling: Verified upstream reference; no mirrored source package