isLimitOfIsIsoLimMapπ — Mathlib

Lean4
/-- If `J` is connected, `F : J ⥤ C` and `c` is a cone on `F`, then to check that `c` is a
limit it is sufficient to check that `limMap c.π` is an isomorphism. The converse is also
true, see `Cone.isLimit_iff_isIso_limMap_π`. -/
def isLimitOfIsIsoLimMapπ {F : J ⥤ C} [HasLimit F] (c : Cone F) [IsIso (limMap c.π)] : IsLimit c :=
  by
  refine
    IsLimit.ofIsoLimit (limit.isLimit _)
      (Cones.ext ((asIso (limMap c.π)).symm ≪≫ (limit.isLimit _).conePointUniqueUpToIso (isLimitConstCone J c.pt)) ?_)
  intro j
  simp only [limit.cone_x, Functor.const_obj_obj, limit.cone_π, Iso.trans_hom, Iso.symm_hom, asIso_inv, assoc,
    IsIso.eq_inv_comp, limMap_π]
  congr 1
  simp [← Iso.inv_comp_eq_id]
Похожие утверждения