English
There is a canonical algebra homomorphism from the space of C^n-valued smooth maps to the function space by evaluating at each point, i.e., the map sending f to the function x ↦ f(x).
Русский
Существуeет канонический алгебра-гомоморфизм из пространства C^n-дифференцируемых отображений в пространство функций по отображению f ↦ (x ↦ f(x)).
LaTeX
$$$\\mathrm{coeFnAlgHom}: \\mathrm{C^n(I,N; 𝓘(\\mathbb{k},A),A)} \\to_{\\mathbb{k}} N \\to A\\quad\\text{is an algebra homomorphism}\\; f \\mapsto (x \\mapsto f(x)).$$$
Lean4
/-- Coercion to a function as an `AlgHom`. -/
@[simps]
def coeFnAlgHom : C^n⟮I, N; 𝓘(𝕜, A), A⟯ →ₐ[𝕜] N → A
where
toFun := (↑)
commutes' _ := rfl
map_zero' := ContMDiffMap.coe_zero
map_one' := ContMDiffMap.coe_one
map_add' := ContMDiffMap.coe_add
map_mul' := ContMDiffMap.coe_mul
