English
For each point x in M, the evaluation-at-x map from the algebra of smooth maps C^∞⟮I, M; 𝕜⟯⟨x⟩ to 𝕜 is the structural map that endows 𝕜 with a C^∞-algebra structure via evaluation.
Русский
Для каждой точки x из M отображение идентификации по точке x из алгебры гладких отображений C^∞⟮I, M; 𝕜⟯⟨x⟩ в 𝕜 задаёт алгебраическую структуру над 𝕜, получаемую через эвалюацию в x.
LaTeX
$$$$ ext{There is a canonical } \mathbb{K}\text{-algebra structure on } \mathbb{K} \, \text{induced by } \operatorname{eval}_x: C^∞\langle I,M;\mathbb{K}\rangle\langle x\rangle \to \mathbb{K}. $$$$
Lean4
/-- `ContMDiffMap.evalRingHom` gives rise to an algebra structure of `C^∞⟮I, M; 𝕜⟯` on `𝕜`. -/
instance evalAlgebra {x : M} : Algebra C^∞⟮I, M; 𝕜⟯⟨x⟩ 𝕜 :=
(ContMDiffMap.evalRingHom x : C^∞⟮I, M; 𝕜⟯⟨x⟩ →+* 𝕜).toAlgebra
