forget_preservesLimits — Mathlib

English

The forgetful functor from commutative rings to types preserves all limits; i.e., limits computed in CommRingCat agree with limits computed after forgetting to types.

Русский

Забывающий функтор из коммутативных колец в множества сохраняет все пределы; т. е. пределы в CommRingCat совпадают с пределами после забывания до множеств.

LaTeX

$$$\operatorname{PreservesLimits}\big(\text{forget }\mathrm{CommRingCat}\big)$ ⇔ \quad \forall F: J ⥤ \mathrm{CommRingCat},\ \operatorname{lim}_{J} F \cong \operatorname{lim}_{J} (\mathrm{forget} \circ F)$$$

Lean4

instance forget_preservesLimits : PreservesLimits (forget CommRingCat.{u}) :=
  CommRingCat.forget_preservesLimitsOfSize.{u, u}

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