English
Let M be a monoid acting on a monoid N in a way compatible with the multiplication on N. Then the map φ: M → N defined by φ(m) = m • 1_N is a monoid homomorphism; in particular φ(1_M) = 1_N and φ(mn) = φ(m) φ(n) for all m,n ∈ M. If the action is additive, φ_add(x) = x + ᵥ 0 defines an additive monoid homomorphism.
Русский
Пусть некие моноиды M и N имеют совместное действие M на N, совместимое с умножением на N. Тогда отображение φ: M → N, заданное φ(m) = m • 1_N, является моноид-гомоморфизм: φ(1_M) = 1_N и φ(mn) = φ(m) φ(n). В аддитивном случае аналогично φ_add(x) = x + ᵥ 0 задаёт аддитивный моноид-гомоморфизм.
LaTeX
$$$\exists \phi: M \to N \quad (\forall m\in M)(\phi(m)=m\cdot 1_N) \wedge (\forall m,n\in M)(\phi(mn)=\phi(m)\phi(n)) \wedge (\phi(1_M)=1_N)$$$
Lean4
/-- If the multiplicative action of `M` on `N` is compatible with multiplication on `N`, then
`fun x ↦ x • 1` is a monoid homomorphism from `M` to `N`. -/
@[to_additive (attr := simps) /-- If the additive action of `M` on `N` is compatible with addition on `N`, then
`fun x ↦ x +ᵥ 0` is an additive monoid homomorphism from `M` to `N`. -/
]
def smulOneHom {M N} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] : M →* N
where
toFun x := x • (1 : N)
map_one' := one_smul _ _
map_mul' x y := by rw [smul_one_mul, smul_smul]
