instHasLimitsCommAlgCat — Mathlib

English

For a fixed commutative ring R, the category of commutative R-algebras has all limits of diagrams of any shape.

Русский

Для фиксированного кольца R категория коммутативных R-алгебр имеет все пределы диаграмм произвольной формы.

LaTeX

$$$\mathrm{HasLimits}(\mathrm{CommAlgCat}(R))$$$

Lean4

instance : HasLimits (CommAlgCat.{u} R) :=
  Adjunction.has_limits_of_equivalence (commAlgCatEquivUnder (.of R)).functor

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