toRingHom_toAddMonoidHom — Mathlib

English

Let f be an R-algebra hom A → B. Then the underlying additive monoid hom of f, viewed as a ring hom A →+* B and then as an additive monoid hom A →+ B, is exactly f viewed as an additive monoid hom. In particular, the function part is preserved by the coercions.

Русский

Пусть f — R-алгоморфизм A → B. Тогда отображение f, рассматриваемое как кольцевой гомоморфизм A →+* B, далее как аддитивный моноид-гомоморфизм A →+ B, совпадает с самим отображением f как AddMonoidHom. Другими словами, функции двух когерентных приведений совпадают.

LaTeX

$$$((f : A \\to+* B) : A \\to+ B) = f$$$

Lean4

@[simp]
theorem toRingHom_toAddMonoidHom (f : A →ₐ[R] B) : ((f : A →+* B) : A →+ B) = f :=
  rfl

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