forget₂Ring_preservesLimits — Mathlib

English

The forgetful functor from CommRingCat to CommSemiRingCat preserves limits of size.

Русский

Функтор забывания CommRingCat → CommSemiRingCat сохраняет пределы размерности.

LaTeX

$$$\mathrm{forget}_2: \mathrm{CommRingCat} \to \mathrm{CommSemiRingCat}$ preserves limits of size.$$

Lean4

instance forget₂Ring_preservesLimits : PreservesLimits (forget₂ CommRingCat RingCat.{u}) :=
  CommRingCat.forget₂Ring_preservesLimitsOfSize.{u, u}

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