instAlgebraObjForget — Mathlib

English

Given a commutative R-algebra object A in CommAlgCat R, the underlying ring (obtained by forgetting the CommAlgCat structure) carries a canonical Algebra structure over R.

Русский

Для объекта A, являющегося коммутативной R-алгеброй в CommAlgCat R, его базовая структура кольца под забыванием содержит каноническую структуру R-алгебры.

LaTeX

$$$\text{Algebra}_R\big(((\text{forget } CommAlgCat\ R)).\mathrm{obj} A\big)$$$

Lean4

instance : Algebra R ((forget (CommAlgCat R)).obj A) :=
  inferInstanceAs <| Algebra R A

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