functorCategoryHasLimit — Mathlib

English

If C has limits of shape J, then the functor category J ⥤ C has limits of shape J

Русский

Если в категории C существуют пределы формы J, то в категории функторов J ⥤ C пределы формы J тоже существуют

LaTeX

$$$\\text{HasLimitsOfShape } J\\ C \\Rightarrow \\text{HasLimitsOfShape } J\\ (\\mathrm{Functor}\\ K C)$$$

Lean4

instance functorCategoryHasLimit (F : J ⥤ K ⥤ C) [∀ k, HasLimit (F.flip.obj k)] : HasLimit F :=
  HasLimit.mk
    { cone := combineCones F fun _ => getLimitCone _
      isLimit := combinedIsLimit _ _ }

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