instHasLimitsOfSizeModuleCat — Mathlib

English

For a ring R, there is a local instance HasLimitsOfSize for the ModuleCat(R); in particular, ModuleCat(R) has limits of the specified size.

Русский

Для кольца R существует локальный экземпляр HasLimitsOfSize для ModuleCat(R); то есть у категорию модулей над R имеются пределы заданного размера.

LaTeX

$$$\\mathrm{HasLimitsOfSize}_{u,u+1}(\\mathrm{ModuleCat}\\ R)$$$

Lean4

local instance : HasLimitsOfSize.{u, u + 1} (ModuleCat.{u + 1} R) :=
  hasLimitsOfSizeShrink.{u, u + 1, u + 1, u} _

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