forget₂Mon_preservesLimits — Mathlib

English

Let J be a category and F: J ⥤ CommMonCat. Then the forgetful functor forget₂ from CommMonCat to MonCat preserves limits of shape J (i.e., the limit in CommMonCat is mapped to the limit in MonCat).

Русский

Пусть J — категория и F: J ⥤ CommMonCat. Тогда забывающий функтор forget₂: CommMonCat → MonCat сохраняет пределы формы J (то есть предел в CommMonCat отображается в предел в MonCat).

LaTeX

$$$\operatorname{PreservesLimits}(\mathrm{forget_2}\,\text{CommMonCat}, \text{MonCat})$$$

Lean4

@[to_additive]
instance forget₂Mon_preservesLimits : PreservesLimits (forget₂ CommMonCat.{u} MonCat.{u}) :=
  CommMonCat.forget₂Mon_preservesLimitsOfSize.{u, u}

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