hasLimit_of_iso — Mathlib

English

If two functors F and G are naturally isomorphic via α and F has a limit, then G also has a limit: HasLimit G.

Русский

Если два функторa F и G естественно изоморфны через α и у F есть предел, то и у G есть предел: HasLimit G.

LaTeX

$$$\\mathrm{HasLimit}(G)$$$

Lean4

/-- If a functor `F` has a limit, so does any naturally isomorphic functor.
-/
theorem hasLimit_of_iso {F G : J ⥤ C} [HasLimit F] (α : F ≅ G) : HasLimit G :=
  HasLimit.mk
    { cone := (Cones.postcompose α.hom).obj (limit.cone F)
      isLimit := (IsLimit.postcomposeHomEquiv _ _).symm (limit.isLimit F) }

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