English
Let M be a monoid with unit and multiplication, and N a commutative monoid. For each m in M, evaluation at m defines a monoid homomorphism from the monoid M →* N to N; collecting these evaluations yields a monoid homomorphism ev: M →* (M →* N) →* N, defined by ev(m)(φ) = φ(m).
Русский
Пусть M — моноид с единицей и умножением, а N — коммутативный моноид. Для фиксированного элемента m ∈ M отображение φ ↦ φ(m) задаёт моноидомоморфизм из моноидоморфизмов M →* N в N. Совокупность таких отображений образует моноидоморфизм ev: M →* (M →* N) →* N, заданный ev(m)(φ) = φ(m).
LaTeX
$$$\\mathrm{ev} : M \\to^* (M \\to^* N) \\to^* N\\quad \\text{where} \\quad \\mathrm{ev}(m)(\\varphi) = \\varphi(m).$$$
Lean4
/-- Evaluation of a `MonoidHom` at a point as a monoid homomorphism. See also `MonoidHom.apply`
for the evaluation of any function at a point. -/
@[to_additive (attr := simps!) /-- Evaluation of an `AddMonoidHom` at a point as an additive monoid homomorphism.
See also `AddMonoidHom.apply` for the evaluation of any function at a point. -/
]
def eval [MulOneClass M] [CommMonoid N] : M →* (M →* N) →* N :=
(MonoidHom.id (M →* N)).flip
