English
There is an algebra homomorphism mapDomainAlgHom k A f from MonoidAlgebra A G to MonoidAlgebra A H associated to a suitable function f: G → H, defined so that it extends mapDomain on the underlying monoid algebras and preserves algebra structure.
Русский
Существует алгебра-гомоморфизм mapDomainAlgHom k A f: MonoidAlgebra A G → MonoidAlgebra A H, связанный с отображением f: G → H, который расширяет mapDomain и сохраняет алгебраическую структуру.
LaTeX
$$$\\mathrm{mapDomainAlgHom}\\ k\;A\\;f : MonoidAlgebra A G \\to_{\\mathsf{Alg}} MonoidAlgebra A H.$$$
Lean4
/-- If `f : G → H` is a multiplicative homomorphism between two monoids, then
`Finsupp.mapDomain f` is an algebra homomorphism between their monoid algebras. -/
@[to_additive (attr := simps!) /-- If `f : G → H` is an additive homomorphism between two additive monoids, then
`Finsupp.mapDomain f` is an algebra homomorphism between their additive monoid algebras. -/
]
def mapDomainAlgHom (k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A] {H F : Type*} [Monoid H] [FunLike F G H]
[MonoidHomClass F G H] (f : F) : MonoidAlgebra A G →ₐ[k] MonoidAlgebra A H :=
{ mapDomainRingHom A f with commutes' := mapDomain_algebraMap A f }
