English
There exists a ring R and a functor F: C → Mod_R such that F is full, faithful, and preserves finite limits and finite colimits.
Русский
Существует кольцо R и функтор F: C → Mod_R такой, что F полно, инъективно·полнофункционален и сохраняет конечные пределы и ко-пределы.
LaTeX
$$$\exists R\, (\mathrm{Ring}(R)) \land \exists F: C \to \mathrm{Mod}_R, F.Full \land F.Faithful \land \mathrm{PreservesFiniteLimits} F \land \mathrm{PreservesFiniteColimits} F$$$
Lean4
/-- The Freyd-Mitchell embedding theorem. See also `FreydMitchell.functor` for a functor which
has the relevant instances. -/
@[stacks 05PP]
theorem 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 :=
⟨_, _, FreydMitchell.functor C, inferInstance, inferInstance, inferInstance, inferInstance⟩
