Polynomials over subrings.

Given a field K with a subring R, in this file 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 intPolynomial. This is useful when dealing with integral elements in an extension of fields.

Main Definitions

• Polynomial.int : given a polynomial P. in K[X] with coefficients in a field K with a subring R such that all coefficients belong to R, P.int R is the corresponding polynomial in R[X].

def Polynomial.int {K : Type u_1} [Field K] (R : Subring K) (P : Polynomial K) (hP : ∀ (n : ℕ), P.coeff n ∈ R) : Polynomial ↥R

Given a polynomial in K[X] such that all coefficients belong to the subring R, intPolynomial is the corresponding polynomial in R[X].

Equations

• Polynomial.int R P hP = { toFinsupp := { support := P.support, toFun := fun (n : ℕ) => ⟨P.coeff n, ⋯⟩, mem_support_toFun := ⋯ } }

@[simp]

theorem Polynomial.int_coeff_eq {K : Type u_1} [Field K] (R : Subring K) (P : Polynomial K) (hP : ∀ (n : ℕ), P.coeff n ∈ R) (n : ℕ) : ↑((Polynomial.int R P hP).coeff n) = P.coeff n

@[simp]

theorem Polynomial.int_leadingCoeff_eq {K : Type u_1} [Field K] (R : Subring K) (P : Polynomial K) (hP : ∀ (n : ℕ), P.coeff n ∈ R) : ↑(Polynomial.int R P hP).leadingCoeff = P.leadingCoeff

@[simp]

theorem Polynomial.int_monic_iff {K : Type u_1} [Field K] (R : Subring K) (P : Polynomial K) (hP : ∀ (n : ℕ), P.coeff n ∈ R) : (Polynomial.int R P hP).Monic ↔ P.Monic

@[simp]

theorem Polynomial.int_natDegree {K : Type u_1} [Field K] (R : Subring K) (P : Polynomial K) (hP : ∀ (n : ℕ), P.coeff n ∈ R) : (Polynomial.int R P hP).natDegree = P.natDegree

@[simp]

theorem Polynomial.int_eval₂_eq {K : Type u_1} [Field K] (R : Subring K) (P : Polynomial K) (hP : ∀ (n : ℕ), P.coeff n ∈ R) {L : Type u_2} [Field L] [Algebra K L] (x : L) : Polynomial.eval₂ (algebraMap (↥R) L) x (Polynomial.int R P hP) = (Polynomial.aeval x) P