English
The forgetful functor forget₂ CommSemiRingCat SemiRingCat preserves limits of size; i.e., it reflects and preserves the shape-specific limits when passing from commutative semirings to semirings.
Русский
Функтор забывания forget₂ CommSemiRingCat SemiRingCat сохраняет пределы размерности; то есть сохраняются пределы заданной формы при переходе от коммутативных полугリング к полугリングу.
LaTeX
$$$ \\mathrm{forget₂ CommSemiRingCat SemiRingCat} \\;:\\; \\operatorname{PreservesLimitsOfSize} ( \\mathrm{forget} ) $$$
Lean4
/-- The forgetful functor from rings to semirings preserves all limits.
-/
instance forget₂SemiRing_preservesLimitsOfSize [UnivLE.{v, u}] :
PreservesLimitsOfSize.{w, v} (forget₂ CommSemiRingCat SemiRingCat.{u}) where
preservesLimitsOfShape
{_
_} :=
{
preservesLimit := fun {F} =>
preservesLimit_of_preserves_limit_cone (limitConeIsLimit.{v, u} F)
(SemiRingCat.HasLimits.limitConeIsLimit (F ⋙ forget₂ _ SemiRingCat)) }
