English
The Freyd-Mitchell embedding functor is faithful (and thus reflects morphisms).
Русский
Функтор вложения Фрейда–Митчелла сохранен (faithful) и тем самым инъективно отображает морфизмы.
LaTeX
$$$\mathrm{Faithful}(\mathrm{FreydMitchell.functor}(C))$$$
Lean4
/-- Pull back a `HasExactColimitsOfShape J` along a functor which preserves and reflects finite limits
and preserves colimits of shape `J`
-/
theorem domain_of_functor {D : Type*} (J : Type*) [Category J] [Category D] [HasColimitsOfShape J C]
[HasColimitsOfShape J D] [HasExactColimitsOfShape J D] (F : C ⥤ D) [PreservesFiniteLimits F]
[ReflectsFiniteLimits F] [HasFiniteLimits C] [PreservesColimitsOfShape J F] : HasExactColimitsOfShape J C where
preservesFiniteLimits :=
{
preservesFiniteLimits
I :=
{
preservesLimit
{G} :=
{
preserves {c}
hc := by
constructor
apply isLimitOfReflects F
refine
(IsLimit.equivOfNatIsoOfIso (isoWhiskerLeft G (preservesColimitNatIso F).symm) ((_ ⋙ colim).mapCone c)
_ ?_)
(isLimitOfPreserves _ hc)
exact
Cones.ext ((preservesColimitNatIso F).symm.app _) fun i ↦
(preservesColimitNatIso F).inv.naturality _ } } }
