English
The Freyd-Mitchell embedding functor is full.
Русский
Функтор вложения Фрейда–Митчелла является полным.
LaTeX
$$$\mathrm{Full}(\mathrm{FreydMitchell.functor}(C))$$$
Lean4
/-- Pull back a `HasExactLimitsOfShape J` along a functor which preserves and reflects finite colimits
and preserves limits of shape `J`
-/
theorem domain_of_functor {D : Type*} (J : Type*) [Category D] [Category J] [HasLimitsOfShape J C]
[HasLimitsOfShape J D] [HasExactLimitsOfShape J D] (F : C ⥤ D) [PreservesFiniteColimits F]
[ReflectsFiniteColimits F] [HasFiniteColimits C] [PreservesLimitsOfShape J F] : HasExactLimitsOfShape J C where
preservesFiniteColimits :=
{
preservesFiniteColimits
I :=
{
preservesColimit
{G} :=
{
preserves {c}
hc := by
constructor
apply isColimitOfReflects F
refine
(IsColimit.equivOfNatIsoOfIso (isoWhiskerLeft G (preservesLimitNatIso F).symm) ((_ ⋙ lim).mapCocone c)
_ ?_)
(isColimitOfPreserves _ hc)
refine Cocones.ext ((preservesLimitNatIso F).symm.app _) fun i ↦ ?_
simp only [Functor.comp_obj, lim_obj, Functor.mapCocone_pt, isoWhiskerLeft_inv, Iso.symm_inv,
Cocones.precompose_obj_pt, whiskeringRight_obj_obj, Functor.const_obj_obj, Cocones.precompose_obj_ι,
NatTrans.comp_app, whiskerLeft_app, preservesLimitNatIso_hom_app, Functor.mapCocone_ι_app,
Functor.comp_map, whiskeringRight_obj_map, lim_map, Iso.app_hom, Iso.symm_hom,
preservesLimitNatIso_inv_app, Category.assoc]
rw [← Iso.eq_inv_comp]
exact (preservesLimitNatIso F).inv.naturality _ } } }
