essImage — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The essential image of a functor is closed under the limits it preserves. -/
protected theorem essImage [HasLimitsOfShape J C] [PreservesLimitsOfShape J F] [F.Full] [F.Faithful] :
    ClosedUnderLimitsOfShape J F.essImage := fun G _c hc hG ↦
  ⟨limit (Functor.essImage.liftFunctor G F hG),
    ⟨IsLimit.conePointsIsoOfNatIso (isLimitOfPreserves F (limit.isLimit _)) hc
        (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩

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