createsLimitOfReflectsIsomorphismsOfPreserves

Lean4

/-- If `F` reflects isomorphisms, and we already know that the limit exists in the source and `F`
preserves it, then `F` creates that limit. -/
def createsLimitOfReflectsIsomorphismsOfPreserves {K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms] [HasLimit K]
    [PreservesLimit K F] : CreatesLimit K F :=
  createsLimitOfReflectsIso' (isLimitOfPreserves F (limit.isLimit _))
    ⟨⟨_, Iso.refl _⟩, limit.isLimit _⟩
      -- 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.

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