English
There is a canonical monoid homomorphism from the product of a semiring R and the additive-only viewpoint of a monoid M into the additive monoid algebra R[M], which sends (r, m) to the basis element corresponding to m scaled by r; i.e., (r, m) maps to r · δ_m. The stated construction reverses the product order in its argument presentation.
Русский
Существует канонический гомоморфизм моноидов из произведения кольца R и аддитивного представления моноида M в аддитивную алгебру моноидов R[M], отправляющий (r, m) в элемент базиса, соответствующий m, масштабированный на r; то есть (r, m) → r · δ_m. Замечание: порядок элементов в произведении здесь намеренно относится наоборот по отношению к стандартному представлению.
LaTeX
$$$\\text{There exists a monoid homomorphism } \\varphi: R \\times M \\to R[M] \\text{ defined by } \\varphi(r,m)=r\\cdot \\delta_m,$ where $\\delta_m$ is the basis element of $R[M]$ at $m$.$$
Lean4
/-- `Finsupp.single` as a `MonoidHom` from the product type into the additive monoid algebra.
Note the order of the elements of the product are reversed compared to the arguments of
`Finsupp.single`.
-/
@[simps]
def singleHom [AddZeroClass M] : R × Multiplicative M →* R[M]
where
toFun a := single a.2.toAdd a.1
map_one' := rfl
map_mul' _a _b := (single_mul_single ..).symm
