instRingObjForget — Mathlib

English

For any R-algebra S, the underlying ring structure on the forgetful object (forget₂ (AlgCat R)) .obj S is precisely the ring structure on S.carrier.

Русский

Для любого R-алгебраического объекта S соответствующая на забывающем функторе структура кольца на объекте равна кольцу на носителе S.

LaTeX

$$$\\text{Ring}((\\mathrm{forget}(\\mathrm{AlgCat}\\ R)).\\mathrm{obj} S)$$$

Lean4

instance {S : AlgCat.{v} R} : Ring ((forget (AlgCat R)).obj S) :=
  (inferInstance : Ring S.carrier)

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