instHasLimitsOfSizeSheafOfHasLimits

English

If C has all limits, then for every TopCat X, the category of sheaves on X with values in C has all limits of the same size.

Русский

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

LaTeX

$$$ [HasLimits C] \\Rightarrow \\ HasLimitsOfSize\\; (\\mathrm{Sheaf}\\; C\\; X). $$$

Lean4

instance [HasLimits C] (X : TopCat.{v}) : HasLimitsOfSize.{v, v} (Sheaf.{v} C X) where

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