English
If f is the identity on monoids, then mapDomainRingHom R (MonoidHom.id M) is the identity on MonoidAlgebra R M.
Русский
Если f — тождественный гомоморфизм на моноидах, то mapDomainRingHom R (MonoidHom.id M) — тождественный на MonoidAlgebra R M.
LaTeX
$$$ mapDomainRingHom R (MonoidHom.id M) = id (MonoidAlgebra R M) $$$
Lean4
/-- If `f : G → H` is a multiplicative homomorphism between two monoids, then
`Finsupp.mapDomain f` is a ring homomorphism between their monoid algebras. -/
@[to_additive (attr := simps) /-- If `f : G → H` is a multiplicative homomorphism between two monoids, then
`Finsupp.mapDomain f` is a ring homomorphism between their monoid algebras. -/
]
def mapDomainRingHom {F : Type*} [FunLike F M N] [MonoidHomClass F M N] (f : F) :
MonoidAlgebra R M →+* MonoidAlgebra R N
where
__ : MonoidAlgebra R M →+ MonoidAlgebra R N := Finsupp.mapDomain.addMonoidHom f
map_one' := mapDomain_one f
map_mul' := mapDomain_mul f
