forget_preservesLimits — Mathlib

English

The forgetful functor from AddCommMonCat to Type preserves all limits (i.e., limits can be computed in the category of types and then given a compatible additive commutative monoid structure).

Русский

Забывающий функтор от AddCommMonCat к типам сохраняет все пределы (пределы можно вычислять в типах и затем на них задаётся соответствующая добавочно-коммутативная моноидная структура).

LaTeX

$$$\operatorname{PreservesLimitsOfSize}(\mathrm{forget\, AddCommMonCat})$$$

Lean4

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

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