English
If f is a magma homomorphism between G and H, then Finsupp.mapDomain f induces a nonunital algebra homomorphism MonoidAlgebra A G → MonoidAlgebra A H.
Русский
Если f — гомоморфизм магм между G и H, то Finsupp.mapDomain f порождает небезединичную алгебра-гомоморфизм между моноидалгебрами: MonoidAlgebra A G → MonoidAlgebra A H.
LaTeX
$$$\\text{mapDomainNonUnitalAlgHom}\\, (k\\,A\\,f) : MonoidAlgebra A G \\to_{\\mathrm{NonUnitalAlg}} MonoidAlgebra A H$$$
Lean4
/-- If `f : G → H` is a homomorphism between two magmas, then
`Finsupp.mapDomain f` is a non-unital algebra homomorphism between their magma algebras. -/
@[to_additive (dont_translate := k) (attr := simps apply) /--
If `f : G → H` is a homomorphism between two additive magmas, then `Finsupp.mapDomain f` is a
non-unital algebra homomorphism between their additive magma algebras. -/
]
def mapDomainNonUnitalAlgHom (k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A] {G H F : Type*} [Mul G] [Mul H]
[FunLike F G H] [MulHomClass F G H] (f : F) : MonoidAlgebra A G →ₙₐ[k] MonoidAlgebra A H :=
{
(Finsupp.mapDomain.addMonoidHom f :
MonoidAlgebra A G →+ MonoidAlgebra A
H) with
map_mul' := fun x y => mapDomain_mul f x y
map_smul' := fun r x => mapDomain_smul r x }
