mapRangeRingHom — Mathlib

English

The construction mapRangeRingHom provides a ring homomorphism between monoid algebras induced by a ring homomorphism on the coefficients, acting componentwise on the basis elements.

Русский

Конструкция mapRangeRingHom задаёт кольмовоморфизм между моноидальными алгебрами, индуцируемый гомоморфизмом колец на коэффициентах, действующим компонентно на базисные элементы.

LaTeX

$$$mapRangeRingHom\ M\ f : MonoidAlgebra R M \to MonoidAlgebra S M$$$

Lean4

/-- The ring homomorphism of monoid algebras induced by a homomorphism of the base rings. -/
noncomputable def mapRangeRingHom (f : R →+* S) : MonoidAlgebra R M →+* MonoidAlgebra S M :=
  liftNCRingHom (singleOneRingHom.comp f) (of S M) fun x y ↦ by simp [commute_iff_eq]

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