createsLimitOfFullyFaithfulOfLift'

Lean4

/-- When `F` is fully faithful, to show that `F` creates the limit for `K` it suffices to exhibit a lift
of a limit cone for `K ⋙ F`.
-/
def createsLimitOfFullyFaithfulOfLift' {K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful] {l : Cone (K ⋙ F)} (hl : IsLimit l)
    (c : Cone K) (i : F.mapCone c ≅ l) : CreatesLimit K F :=
  createsLimitOfReflectsIso' hl
    ⟨⟨c, i⟩, isLimitOfReflects F (IsLimit.ofIsoLimit hl i.symm)⟩
      -- 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.

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