English
The forgetful functor forget₂ from CommMonCat to MonCat preserves limits of all sizes, i.e., the forgetful construction commutes with taking limits across sizes.
Русский
Забывающая функция forget₂ от CommMonCat к MonCat сохраняет пределы всех размеров; забывающая процедура коммутирует с взятием предела по размеру.
LaTeX
$$$\text{forget₂Mon_preservesLimitsOfSize}$$$
Lean4
/-- The forgetful functor from commutative monoids to monoids preserves all limits.
This means the underlying type of a limit can be computed as a limit in the category of monoids. -/
@[to_additive (relevant_arg := 100) AddCommMonCat.forget₂AddMonPreservesLimitsOfSize /-- The forgetful functor from
additive commutative monoids to additive monoids preserves all limits.
This means the underlying type of a limit can be computed as a limit in the category of additive
monoids. -/
]
instance forget₂Mon_preservesLimitsOfSize [UnivLE.{v, u}] :
PreservesLimitsOfSize.{w, v} (forget₂ CommMonCat.{u} MonCat.{u}) where preservesLimitsOfShape {J} 𝒥 := { }
