English
Given a map f: σ → S1 where S1 is an algebra over R, there exists an R-algebra homomorphism aeval f: MvPolynomial σ R → S1 sending each X_s to f(s); this is the universal evaluation map.
Русский
При задании отображения X_s → f(s) существует единственный R-алгеброгомомоморфизм aeval f: MvPolynomial σ R → S1, и он равен универсальному оценочному отображению.
LaTeX
$$$\\exists! \\phi: MvPolynomial σ R \\to[R] S_1 \\text{ с } \\phi(X_s) = f(s) \\;\\forall s \\in σ$ и $\\phi$ — R-алгеброгомоморфизм$$
Lean4
/-- A map `σ → S₁` where `S₁` is an algebra over `R` generates an `R`-algebra homomorphism
from multivariate polynomials over `σ` to `S₁`. -/
def aeval : MvPolynomial σ R →ₐ[R] S₁ :=
{ eval₂Hom (algebraMap R S₁) f with commutes' := fun _r => eval₂_C _ _ _ }
