English
For every diagram F from a small category J to the category of commutative rings, the limit of F computed in the category of rings, when viewed through the forgetful functor to types, coincides with the limit of the underlying sets of the rings in Type.
Русский
Для произвольного диаграммного отображения F: J ⥤ CommRingCat, предел F, вычисленный в категории колец, при рассмотрении через забывающий функтор в типы равен пределy базовых множеств колец в типах.
LaTeX
$$$\displaystyle \varprojlim_{J} F \cong \varprojlim_{J} (\text{Forget} \circ F)$$$
Lean4
/-- The forgetful functor from commutative rings to types preserves all limits.
(That is, the underlying types could have been computed instead as limits in the category of types.)
-/
instance forget_preservesLimitsOfSize [UnivLE.{v, u}] : PreservesLimitsOfSize.{w, v} (forget CommRingCat.{u}) where
preservesLimitsOfShape
{_
_} :=
{
preservesLimit := fun {F} =>
preservesLimit_of_preserves_limit_cone.{w, v} (limitConeIsLimit.{v, u} F)
(Types.Small.limitConeIsLimit.{v, u} _) }
