preservesLimit_of_isIso_post — Mathlib

English

There is an instance that the functor lim (K ⥤ D ⥤ C) preserves colimits of shape J in the Grothendieck sense.

Русский

Существует экземпляр, утверждающий сохранение колимитов формы J функционором lim по категории Гротендик.

LaTeX

$$$\\text{PreservesColimitsOfShape } J \\; (\\mathrm{lim} )$$$

Lean4

/-- If the comparison morphism `G.obj (limit F) ⟶ limit (F ⋙ G)` is an isomorphism, then `G`
preserves limits of `F`. -/
theorem preservesLimit_of_isIso_post [IsIso (limit.post F G)] : PreservesLimit F G :=
  preservesLimit_of_preserves_limit_cone (limit.isLimit F)
    (by
      convert IsLimit.ofPointIso (limit.isLimit (F ⋙ G))
      assumption)

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