Constructions relating polynomial functions and continuous functions.

Main definitions

• Polynomial.toContinuousMapOn p X: for X : Set R, interprets a polynomial p as a bundled continuous function in C(X, R).
• Polynomial.toContinuousMapOnAlgHom: the same, as an R-algebra homomorphism.
• polynomialFunctions (X : Set R) : Subalgebra R C(X, R): polynomial functions as a subalgebra.
• polynomialFunctions_separatesPoints (X : Set R) : (polynomialFunctions X).SeparatesPoints: the polynomial functions separate points.

def Polynomial.toContinuousMap {R : Type u_1} [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] (p : Polynomial R) : C(R, R)

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

Equations

• p.toContinuousMap = { toFun := fun (x : R) => Polynomial.eval x p, continuous_toFun := ⋯ }

@[simp]

theorem Polynomial.toContinuousMap_apply {R : Type u_1} [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] (p : Polynomial R) (x : R) : p.toContinuousMap x = Polynomial.eval x p

theorem Polynomial.toContinuousMap_X_eq_id {R : Type u_1} [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] : Polynomial.X.toContinuousMap = ContinuousMap.id R

def Polynomial.toContinuousMapOn {R : Type u_1} [Semiring R] [TopologicalSpace R] [TopologicalSemiring 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.toContinuousMapOn X = { toFun := fun (x : ↑X) => p.toContinuousMap ↑x, continuous_toFun := ⋯ }

@[simp]

theorem Polynomial.toContinuousMapOn_apply {R : Type u_1} [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] (p : Polynomial R) (X : Set R) (x : ↑X) : (p.toContinuousMapOn X) x = p.toContinuousMap ↑x

theorem Polynomial.toContinuousMapOn_X_eq_restrict_id {R : Type u_1} [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] (s : Set R) : Polynomial.X.toContinuousMapOn s = ContinuousMap.restrict s (ContinuousMap.id R)

@[simp]

theorem Polynomial.aeval_continuousMap_apply {R : Type u_1} {α : Type u_2} [TopologicalSpace α] [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] (g : Polynomial R) (f : C(α, R)) (x : α) : ((Polynomial.aeval f) g) x = Polynomial.eval (f x) g

def Polynomial.toContinuousMapAlgHom {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] : Polynomial R →ₐ[R] C(R, R)

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

Equations

• Polynomial.toContinuousMapAlgHom = { toFun := fun (p : Polynomial R) => p.toContinuousMap, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Polynomial.toContinuousMapAlgHom_apply {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] (p : Polynomial R) : Polynomial.toContinuousMapAlgHom p = p.toContinuousMap

def Polynomial.toContinuousMapOnAlgHom {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring 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.toContinuousMapOnAlgHom X = { toFun := fun (p : Polynomial R) => p.toContinuousMapOn X, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Polynomial.toContinuousMapOnAlgHom_apply {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] (X : Set R) (p : Polynomial R) : (Polynomial.toContinuousMapOnAlgHom X) p = p.toContinuousMapOn X

noncomputable def polynomialFunctions {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring 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

• polynomialFunctions X = Subalgebra.map (Polynomial.toContinuousMapOnAlgHom X) ⊤

@[simp]

theorem polynomialFunctions_coe {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] (X : Set R) : ↑(polynomialFunctions X) = Set.range ⇑(Polynomial.toContinuousMapOnAlgHom X)

theorem polynomialFunctions_separatesPoints {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] (X : Set R) : (polynomialFunctions X).SeparatesPoints

theorem polynomialFunctions.comap_compRightAlgHom_iccHomeoI (a b : ℝ) (h : a < b) : Subalgebra.comap (ContinuousMap.compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions unitInterval) = polynomialFunctions (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].

theorem polynomialFunctions.eq_adjoin_X {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] (s : Set R) : polynomialFunctions s = Algebra.adjoin R {(Polynomial.toContinuousMapOnAlgHom s) Polynomial.X}

theorem polynomialFunctions.le_equalizer {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (s : Set R) (φ ψ : C(↑s, R) →ₐ[R] A) (h : φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X)) : polynomialFunctions s ≤ AlgHom.equalizer φ ψ

theorem polynomialFunctions.starClosure_eq_adjoin_X {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] [StarRing R] [ContinuousStar R] (s : Set R) : (polynomialFunctions s).starClosure = StarAlgebra.adjoin R {(Polynomial.toContinuousMapOnAlgHom s) Polynomial.X}

theorem polynomialFunctions.starClosure_le_equalizer {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R] {A : Type u_2} [StarRing R] [ContinuousStar R] [Semiring A] [StarRing A] [Algebra R A] (s : Set R) (φ ψ : C(↑s, R) →⋆ₐ[R] A) (h : φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X)) : (polynomialFunctions s).starClosure ≤ StarAlgHom.equalizer φ ψ