English
There is a canonical evaluation map 'applyℓ′' that sends a vector v ∈ M to the R-linear map (M →ₗ[R] M₂) → M₂ defined by f ↦ f(v); this map is linear in its arguments.
Русский
Существует каноническое отображение_eval, которое отправляет v ∈ M в R-линейное отображение (M →ₗ[R] M₂) → M₂, задаваемое f ↦ f(v); это отображение линейно по каждому аргументу.
LaTeX
$$$ (Apply\!\_\!\ell')(v) : (M \to_\ell[R] M_2) \to_\ell[R] M_2 \,\text{defined by } (Apply\!\_\!\ell')(v)(f) = f(v). $$$
Lean4
/-- Applying a linear map at `v : M`, seen as `S`-linear map from `M →ₗ[R] M₂` to `M₂`.
See `LinearMap.applyₗ` for a version where `S = R`. -/
@[simps]
def applyₗ' : M →+ (M →ₗ[R] M₂) →ₗ[S] M₂
where
toFun
v :=
{ toFun := fun f => f v
map_add' := fun f g => f.add_apply g v
map_smul' := fun x f => f.smul_apply x v }
map_zero' := LinearMap.ext fun f => f.map_zero
map_add' _ _ := LinearMap.ext fun f => f.map_add _ _
