English
The evaluation-to-function map acts as a monoid hom from C(α, β) to α → β. It preserves the monoid structure, sending constant one to the constant one and products to pointwise products.
Русский
Оценочная карта отображает C(α, β) в α → β как гомоморф моноида: сохраняет единицу и произведение отображений через точечное произведение.
LaTeX
$$$\operatorname{coeFnMonoidHom}: C(\alpha, \beta) \to (\alpha \to \beta)$; $\big(\operatorname{coeFnMonoidHom}(f)\big)(x)=f(x)$; $\operatorname{coeFnMonoidHom}(1)=1$, $\operatorname{coeFnMonoidHom}(f\cdot g)=\operatorname{coeFnMonoidHom}(f)\cdot\operatorname{coeFnMonoidHom}(g)$$$
Lean4
/-- Coercion to a function as a `MonoidHom`. Similar to `MonoidHom.coeFn`. -/
@[to_additive (attr := simps) /-- Coercion to a function as an `AddMonoidHom`. Similar to `AddMonoidHom.coeFn`. -/
]
def coeFnMonoidHom [Monoid β] [ContinuousMul β] : C(α, β) →* α → β
where
toFun f := f
map_one' := coe_one
map_mul' := coe_mul
