English
Let R be a ring. The category of left R-modules has all small limits (limits of diagrams whose size is bounded by a fixed cardinal). In particular, for any diagram J → Mod_R with |J| nowhere exceeding the chosen size, its limit exists in Mod_R.
Русский
Пусть R — кольцо. Категория левых модулей над R имеет все малые пределы (пределы диаграмм размерности, ограниченной константой). В частности для любой диаграммы J → Mod_R с размером J не превосходящим заданную величину предел существует в Mod_R.
LaTeX
$$$\operatorname{HasLimitsOfSize}_{v,v}(\mathrm{Mod}_R)$$$
Lean4
/-- Add this instance to help Lean with universe levels. -/
instance : HasLimitsOfSize.{v, v} (ModuleCat.{max v w} R) :=
ModuleCat.hasLimitsOfSize.{v, v, max v w}
/- We need to put this in this weird spot because we need to know that the category of modules
is balanced. -/
