essImage — Mathlib

English

If F : C ⥤ D preserves colimits of shape J and F.Full and F.Faithful, then the essential image of F is closed under colimits of shape J

Русский

Если F : C ⥤ D сохраняет колимиты формы J и F полно и точно, то образ по существу F замкнут по колимитам формы J

LaTeX

$$$\\text{ClosedUnderColimitsOfShape } J\\ F.essImage$$$

Lean4

/-- The essential image of a functor is closed under the colimits it preserves. -/
protected theorem essImage [HasColimitsOfShape J C] [PreservesColimitsOfShape J F] [F.Full] [F.Faithful] :
    ClosedUnderColimitsOfShape J F.essImage := fun G _c hc hG ↦
  ⟨colimit (Functor.essImage.liftFunctor G F hG),
    ⟨IsColimit.coconePointsIsoOfNatIso (isColimitOfPreserves F (colimit.isColimit _)) hc
        (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩

Похожие утверждения