English
Interpretation of evaluation: for a fixed a in α, the map lapply a sends f ∈ α →₀ M to the element f(a) ∈ M, and is linear in f. It is the natural projection onto the a-th coordinate.
Русский
Интерпретация значения в точке: для фиксированного a ∈ α отображение lapply a отправляет f ∈ α →₀ M в элемент f(a) ∈ M и линейно в f. Это естественное проецирование на a-й коэффициент.
LaTeX
$$$\\forall a: \\alpha,\\; (lapply\,a): (\\alpha \\to_0 M) \\to M\\;\\text{ satisfies } (lapply\,a)(f)=f(a)$$$
Lean4
/-- Interpret `fun f : α →₀ M ↦ f a` as a linear map. -/
def lapply (a : α) : (α →₀ M) →ₗ[R] M :=
{ Finsupp.applyAddHom a with map_smul' := fun _ _ => rfl }
