instHasLimitsOfShapeSheaf — Mathlib

English

If C has limits of shape J, then for any TopCat X the category of sheaves with values in C over X has limits of shape J.

Русский

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

LaTeX

$$$ \\forall X \\; \\forall J \\; \\forall C,\\ [HasLimitsOfShape J\\; C]\\Rightarrow HasLimitsOfShape J\\; (Sheaf\\; C\\; X). $$$

Lean4

instance [HasLimitsOfShape J C] (X : TopCat.{t}) : HasLimitsOfShape J (Sheaf C X) :=
  hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (Sheaf.forget C X)

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