English
The subalgebra of polynomial functions on X is generated by the image of the indeterminate X under the polynomial-to-continuous-map algebra hom: polynomialFunctions X = Algebra.adjoin_R {toContinuousMapOnAlgHom X X}.
Русский
Подалгебра полином-функций на X порождается образцом X через соответствующее алгебра-гомоморфическое отображение: polynomialFunctions X = Algebra.adjoin_R {toContinuousMapOnAlgHom X X}.
LaTeX
$$$polynomialFunctions\\,X = Algebra.adjoin\\,R\\{toContinuousMapOnAlgHom\\,X\\ X\\}$$$
Lean4
/-- The algebra map from `R[X]` to continuous functions `C(R, R)`.
-/
@[simps]
def toContinuousMapAlgHom : R[X] →ₐ[R] C(R, R)
where
toFun p := p.toContinuousMap
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]
