English
There is an R-algebra homomorphism from R[X] to C(X,R) given by p ↦ p.toContinuousMapOn X; i.e., the polynomial-to-continuous-map map on X is an algebra homomorphism.
Русский
Существует R-алгебра-гомоморфизм от R[X] к C(X,R), заданный p ↦ p.toContinuousMapOn X; т.е. отображение полиномов на X является алгебра-гомоморфизмом.
LaTeX
$$$toContinuousMapOnAlgHom(X) : R[X] \\to_A[R] C(X,R)$ with\\ toFun p := p.toContinuousMapOn X$$
Lean4
/-- The algebra map from `R[X]` to continuous functions `C(X, R)`, for any subset `X` of `R`.
-/
@[simps]
def toContinuousMapOnAlgHom (X : Set R) : R[X] →ₐ[R] C(X, R)
where
toFun p := p.toContinuousMapOn X
map_zero' := by
ext
simp
map_add' _
_ := by
ext
simp
map_one' := by
ext
simp
map_mul' _
_ := by
ext
simp
commutes'
_ := by
ext
simp [Algebra.algebraMap_eq_smul_one]
