English
Given an algebra isomorphism f: A ≃ₐ[R] B, mapRangeAlgEquiv M f gives an algebra isomorphism MonoidAlgebra A M ≃ₐ[R] MonoidAlgebra B M.
Русский
Дано алгебра-изоморфизм f: A ≃ₐ[R] B, mapRangeAlgEquiv M f задаёт изоморфизм MonoidAlgebra A M ≃ₐ[R] MonoidAlgebra B M.
LaTeX
$$$\\mathrm{mapRangeAlgEquiv}\\ M f : MonoidAlgebra A M \\simeq_{\\mathsf{Alg}} MonoidAlgebra B M$$$
Lean4
/-- The algebra homomorphism of monoid algebras induced by a homomorphism of the base algebras. -/
@[to_additive /-- The algebra homomorphism of additive monoid algebras induced by a homomorphism of the base
algebras. -/
]
noncomputable def mapRangeAlgHom (f : A →ₐ[R] B) : MonoidAlgebra A M →ₐ[R] MonoidAlgebra B M
where
__ := mapRangeRingHom M f
commutes' := by simp
