ofConesIso — Mathlib

English

If two functors F and G have isomorphic cone collections, and F has a limit, then G has a limit.

Русский

Если коллекции конусов двух функторов F и G изоморфны, и у F есть предел, то и у G есть предел.

LaTeX

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

Lean4

/-- If a functor `G` has the same collection of cones as a functor `F`
which has a limit, then `G` also has a limit. -/
theorem ofConesIso {J K : Type u₁} [Category.{v₁} J] [Category.{v₂} K] (F : J ⥤ C) (G : K ⥤ C) (h : F.cones ≅ G.cones)
    [HasLimit F] : HasLimit G :=
  HasLimit.mk ⟨_, IsLimit.ofRepresentableBy ((limit.isLimit F).representableBy.ofIso h)⟩

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