Constructions relating polynomial functions and continuous functions. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

polynomial.to_continuous_map_on p X: for X : set R, interprets a polynomial p as a bundled continuous function in C(X, R).
polynomial.to_continuous_map_on_alg_hom: the same, as an R-algebra homomorphism.
polynomial_functions (X : set R) : subalgebra R C(X, R): polynomial functions as a subalgebra.
polynomial_functions_separates_points (X : set R) : (polynomial_functions X).separates_points: the polynomial functions separate points.

def polynomial.to_continuous_map {R : Type u_1} [semiring R] [topological_space R] [topological_semiring R] (p : polynomial R) :

C(R, R)

Every polynomial with coefficients in a topological semiring gives a (bundled) continuous function.

Equations

p.to_continuous_map = {to_fun := λ (x : R), polynomial.eval x p, continuous_to_fun := _}

source

@[simp]

theorem polynomial.to_continuous_map_apply {R : Type u_1} [semiring R] [topological_space R] [topological_semiring R] (p : polynomial R) (x : R) :

⇑(p.to_continuous_map) x = polynomial.eval x p

source

@[simp]

theorem polynomial.to_continuous_map_on_apply {R : Type u_1} [semiring R] [topological_space R] [topological_semiring R] (p : polynomial R) (X : set R) (x : ↥X) :

⇑(p.to_continuous_map_on X) x = ⇑(p.to_continuous_map) ↑x

source

def polynomial.to_continuous_map_on {R : Type u_1} [semiring R] [topological_space R] [topological_semiring R] (p : polynomial R) (X : set R) :

C(↥X, R)

A polynomial as a continuous function, with domain restricted to some subset of the semiring of coefficients.

(This is particularly useful when restricting to compact sets, e.g. [0,1].)

Equations

p.to_continuous_map_on X = {to_fun := λ (x : ↥X), ⇑(p.to_continuous_map) ↑x, continuous_to_fun := _}

source

@[simp]

theorem polynomial.aeval_continuous_map_apply {R : Type u_1} {α : Type u_2} [topological_space α] [comm_semiring R] [topological_space R] [topological_semiring R] (g : polynomial R) (f : C(α, R)) (x : α) :

⇑(⇑(polynomial.aeval f) g) x = polynomial.eval (⇑f x) g

source

def polynomial.to_continuous_map_alg_hom {R : Type u_1} [comm_semiring R] [topological_space R] [topological_semiring R] :

polynomial R →ₐ[R] C(R, R)

The algebra map from R[X] to continuous functions C(R, R).

Equations

polynomial.to_continuous_map_alg_hom = {to_fun := λ (p : polynomial R), p.to_continuous_map, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem polynomial.to_continuous_map_alg_hom_apply {R : Type u_1} [comm_semiring R] [topological_space R] [topological_semiring R] (p : polynomial R) :

⇑polynomial.to_continuous_map_alg_hom p = p.to_continuous_map

source

def polynomial.to_continuous_map_on_alg_hom {R : Type u_1} [comm_semiring R] [topological_space R] [topological_semiring R] (X : set R) :

polynomial R →ₐ[R] C(↥X, R)

The algebra map from R[X] to continuous functions C(X, R), for any subset X of R.

Equations

polynomial.to_continuous_map_on_alg_hom X = {to_fun := λ (p : polynomial R), p.to_continuous_map_on X, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem polynomial.to_continuous_map_on_alg_hom_apply {R : Type u_1} [comm_semiring R] [topological_space R] [topological_semiring R] (X : set R) (p : polynomial R) :

⇑(polynomial.to_continuous_map_on_alg_hom X) p = p.to_continuous_map_on X

source

noncomputable def polynomial_functions {R : Type u_1} [comm_semiring R] [topological_space R] [topological_semiring R] (X : set R) :

subalgebra R C(↥X, R)

The subalgebra of polynomial functions in C(X, R), for X a subset of some topological semiring R.

Equations

polynomial_functions X = subalgebra.map (polynomial.to_continuous_map_on_alg_hom X) ⊤

source

@[simp]

theorem polynomial_functions_coe {R : Type u_1} [comm_semiring R] [topological_space R] [topological_semiring R] (X : set R) :

↑(polynomial_functions X) = set.range ⇑(polynomial.to_continuous_map_on_alg_hom X)

source

theorem polynomial_functions_separates_points {R : Type u_1} [comm_semiring R] [topological_space R] [topological_semiring R] (X : set R) :

(polynomial_functions X).separates_points

source

theorem polynomial_functions.comap_comp_right_alg_hom_Icc_homeo_I (a b : ℝ) (h : a < b) :

subalgebra.comap (continuous_map.comp_right_alg_hom ℝ ℝ (Icc_homeo_I a b h).symm.to_continuous_map) (polynomial_functions unit_interval) = polynomial_functions (set.Icc a b)

The preimage of polynomials on [0,1] under the pullback map by x ↦ (b-a) * x + a is the polynomials on [a,b].