createsLimitOfFullyFaithfulOfIso'

Lean4
/-- When `F` is fully faithful, to show that `F` creates the limit for `K` it suffices to show that a
limit point is in the essential image of `F`.
-/
def createsLimitOfFullyFaithfulOfIso' {K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful] {l : Cone (K ⋙ F)} (hl : IsLimit l)
    (X : C) (i : F.obj X ≅ l.pt) : CreatesLimit K F :=
  createsLimitOfFullyFaithfulOfLift' hl
    { pt := X
      π :=
        { app := fun j => F.preimage (i.hom ≫ l.π.app j)
          naturality := fun Y Z f => F.map_injective <| by simpa using (l.w f).symm } }
    (Cones.ext i fun j => by simp only [Functor.map_preimage, Functor.mapCone_π_app])
      -- Notice however that even if the isomorphism is `Iso.refl _`,
      -- this construction will insert additional identity morphisms in the cone maps,
      -- so the constructed limits may not be ideal, definitionally.
Похожие утверждения