Polynomials over subrings

Given a ring K with a subring R, we construct a map from polynomials in K[X] with coefficients in R to R[X]. We provide several lemmas to deal with coefficients, degree, and evaluation of Polynomial.toSubring.

Main Definitions

• Polynomial.toSubring : given a polynomial P in K[X] whose coefficients all belong to a subring R of the ring K, P.toSubring R is the corresponding polynomial in R[X].

noncomputable def Polynomial.toSubring {R : Type u_1} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T) : Polynomial ↥T

Given a polynomial p and a subring T that contains the coefficients of p, return the corresponding polynomial whose coefficients are in T.

@[simp]

theorem Polynomial.coeff_toSubring {R : Type u_1} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T) {n : ℕ} : ↑((p.toSubring T hp).coeff n) = p.coeff n

theorem Polynomial.coeff_toSubring' {R : Type u_1} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T) {n : ℕ} : ↑((p.toSubring T hp).coeff n) = p.coeff n

@[simp]

theorem Polynomial.support_toSubring {R : Type u_1} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T) : (p.toSubring T hp).support = p.support

@[simp]

theorem Polynomial.degree_toSubring {R : Type u_1} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T) : (p.toSubring T hp).degree = p.degree

@[simp]

theorem Polynomial.natDegree_toSubring {R : Type u_1} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T) : (p.toSubring T hp).natDegree = p.natDegree

@[simp]

theorem Polynomial.monic_toSubring {R : Type u_1} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T) : (p.toSubring T hp).Monic ↔ p.Monic

@[simp]

theorem Polynomial.toSubring_zero {R : Type u_1} [Ring R] (T : Subring R) : toSubring 0 T ⋯ = 0

@[simp]

theorem Polynomial.toSubring_one {R : Type u_1} [Ring R] (T : Subring R) : toSubring 1 T ⋯ = 1

@[simp]

theorem Polynomial.map_toSubring {R : Type u_1} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T) : map T.subtype (p.toSubring T hp) = p

noncomputable def Polynomial.ofSubring {R : Type u_1} [Ring R] (T : Subring R) (p : Polynomial ↥T) : Polynomial R

Given a polynomial whose coefficients are in some subring, return the corresponding polynomial whose coefficients are in the ambient ring.

theorem Polynomial.coeff_ofSubring {R : Type u_1} [Ring R] (T : Subring R) (p : Polynomial ↥T) (n : ℕ) : (ofSubring T p).coeff n = ↑(p.coeff n)

@[simp]

theorem Polynomial.coeffs_ofSubring {R : Type u_1} [Ring R] (T : Subring R) {p : Polynomial ↥T} : ↑(ofSubring T p).coeffs ⊆ ↑T