instHasLimitsOfShapePresheaf — Mathlib

English

If the base category C has limits, then the presheaf category over X has limits as well.

Русский

Если в базовой категории C существуют пределы, то категория прешейфов над X тоже имеет пределы.

LaTeX

$$$\\text{HasLimits } C \\Rightarrow \\text{HasLimits } (\\mathrm{Presheaf}~C~X)$$$

Lean4

instance [HasLimitsOfShape J C] (X : TopCat.{t}) : HasLimitsOfShape J (Presheaf C X) :=
  functorCategoryHasLimitsOfShape

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