Degrees of a polynomial under two coefficient maps

If two ring homomorphisms φ and ψ send exactly the same coefficients of a polynomial p to zero, then p.map φ vanishes exactly when p.map ψ does, and the two have the same degree. This is how the zero pattern of finitely many coefficients fixes the degrees of specialized polynomials, for instance at two points of a base set on which a projection set used in cylindrical algebraic decomposition is sign-invariant.

theorem Polynomial.degree_map_eq_of_map_coeff_eq_zero_iff {R : Type u_1} {S : Type u_2} {T : Type u_3} [Semiring R] [Semiring S] [Semiring T] {φ : R →+* S} {ψ : R →+* T} {p : Polynomial R} (h : ∀ i ≤ p.natDegree, φ (p.coeff i) = 0 ↔ ψ (p.coeff i) = 0) : (map φ p).degree = (map ψ p).degree

If φ and ψ send the same coefficients of p to zero, then p.map φ and p.map ψ have the same degree. Only the coefficients up to p.natDegree need to be checked.

theorem Polynomial.map_eq_zero_iff_of_map_coeff_eq_zero_iff {R : Type u_1} {S : Type u_2} {T : Type u_3} [Semiring R] [Semiring S] [Semiring T] {φ : R →+* S} {ψ : R →+* T} {p : Polynomial R} (h : ∀ i ≤ p.natDegree, φ (p.coeff i) = 0 ↔ ψ (p.coeff i) = 0) : map φ p = 0 ↔ map ψ p = 0

If φ and ψ send the same coefficients of p to zero, then p.map φ vanishes exactly when p.map ψ does. Only the coefficients up to p.natDegree need to be checked.

theorem Polynomial.natDegree_map_eq_of_map_coeff_eq_zero_iff {R : Type u_1} {S : Type u_2} {T : Type u_3} [Semiring R] [Semiring S] [Semiring T] {φ : R →+* S} {ψ : R →+* T} {p : Polynomial R} (h : ∀ i ≤ p.natDegree, φ (p.coeff i) = 0 ↔ ψ (p.coeff i) = 0) : (map φ p).natDegree = (map ψ p).natDegree

If φ and ψ send the same coefficients of p to zero, then p.map φ and p.map ψ have the same natDegree. Only the coefficients up to p.natDegree need to be checked.