instHasLimitsOfShape — Mathlib

English

If D has limits of a given shape, then the category of J-sheaves on D has limits of that shape.

Русский

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

LaTeX

$$$(\text{HasLimitsOfShape } K D) \Rightarrow (\text{HasLimitsOfShape } K (\mathrm{Sh}(J,D))).$$$

Lean4

instance : HasLimitsOfShape K (Sheaf J D) :=
  hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (sheafToPresheaf J D)

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