Multivariate polynomials over a ring

Many results about polynomials hold when the coefficient ring is a commutative semiring. Some stronger results can be derived when we assume this semiring is a ring.

This file does not define any new operations, but proves some of these stronger results.

Notation

As in other polynomial files, we typically use the notation:

• σ : Type* (indexing the variables)

• R : Type* [CommRing R] (the coefficients)

• s : σ →₀ ℕ, a function from σ to ℕ which is zero away from a finite set. This will give rise to a monomial in MvPolynomial σ R which mathematicians might call X^s

• a : R

• i : σ, with corresponding monomial X i, often denoted X_i by mathematicians

• p : MvPolynomial σ R

instance MvPolynomial.instCommRingMvPolynomial {R : Type u} {σ : Type u_1} [CommRing R] : CommRing (MvPolynomial σ R)

Equations

• MvPolynomial.instCommRingMvPolynomial = AddMonoidAlgebra.commRing

@[simp]

theorem MvPolynomial.C_sub {R : Type u} (σ : Type u_1) (a : R) (a' : R) [CommRing R] : MvPolynomial.C (a - a') = MvPolynomial.C a - MvPolynomial.C a'

@[simp]

theorem MvPolynomial.C_neg {R : Type u} (σ : Type u_1) (a : R) [CommRing R] : MvPolynomial.C (-a) = -MvPolynomial.C a

@[simp]

theorem MvPolynomial.coeff_neg {R : Type u} (σ : Type u_1) [CommRing R] (m : σ →₀ ℕ) (p : MvPolynomial σ R) : MvPolynomial.coeff m (-p) = -MvPolynomial.coeff m p

@[simp]

theorem MvPolynomial.coeff_sub {R : Type u} (σ : Type u_1) [CommRing R] (m : σ →₀ ℕ) (p : MvPolynomial σ R) (q : MvPolynomial σ R) : MvPolynomial.coeff m (p - q) = MvPolynomial.coeff m p - MvPolynomial.coeff m q

@[simp]

theorem MvPolynomial.support_neg {R : Type u} (σ : Type u_1) [CommRing R] {p : MvPolynomial σ R} : (-p).support = p.support

theorem MvPolynomial.support_sub {R : Type u} (σ : Type u_1) [CommRing R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) : (p - q).support ⊆ p.support ∪ q.support

@[simp]

theorem MvPolynomial.degrees_neg {R : Type u} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) : (-p).degrees = p.degrees

theorem MvPolynomial.degrees_sub {R : Type u} {σ : Type u_1} [CommRing R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) : (p - q).degrees ≤ p.degrees ⊔ q.degrees

@[simp]

theorem MvPolynomial.degreeOf_neg {R : Type u} {σ : Type u_1} [CommRing R] (i : σ) (p : MvPolynomial σ R) : MvPolynomial.degreeOf i (-p) = MvPolynomial.degreeOf i p

theorem MvPolynomial.degreeOf_sub_le {R : Type u} {σ : Type u_1} [CommRing R] (i : σ) (p : MvPolynomial σ R) (q : MvPolynomial σ R) : MvPolynomial.degreeOf i (p - q) ≤ MvPolynomial.degreeOf i p ⊔ MvPolynomial.degreeOf i q

@[simp]

theorem MvPolynomial.vars_neg {R : Type u} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) : (-p).vars = p.vars

theorem MvPolynomial.vars_sub_subset {R : Type u} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) {q : MvPolynomial σ R} [DecidableEq σ] : (p - q).vars ⊆ p.vars ∪ q.vars

@[simp]

theorem MvPolynomial.vars_sub_of_disjoint {R : Type u} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) {q : MvPolynomial σ R} [DecidableEq σ] (hpq : Disjoint p.vars q.vars) : (p - q).vars = p.vars ∪ q.vars

@[simp]

theorem MvPolynomial.eval₂_sub {R : Type u} {S : Type v} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) {q : MvPolynomial σ R} [CommRing S] (f : R →+* S) (g : σ → S) : MvPolynomial.eval₂ f g (p - q) = MvPolynomial.eval₂ f g p - MvPolynomial.eval₂ f g q

theorem MvPolynomial.eval_sub {R : Type u} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) {q : MvPolynomial σ R} (f : σ → R) : (MvPolynomial.eval f) (p - q) = (MvPolynomial.eval f) p - (MvPolynomial.eval f) q

@[simp]

theorem MvPolynomial.eval₂_neg {R : Type u} {S : Type v} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) [CommRing S] (f : R →+* S) (g : σ → S) : MvPolynomial.eval₂ f g (-p) = -MvPolynomial.eval₂ f g p

theorem MvPolynomial.eval_neg {R : Type u} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) (f : σ → R) : (MvPolynomial.eval f) (-p) = -(MvPolynomial.eval f) p

theorem MvPolynomial.hom_C {S : Type v} {σ : Type u_1} [CommRing S] (f : MvPolynomial σ ℤ →+* S) (n : ℤ) : f (MvPolynomial.C n) = ↑n

@[simp]

theorem MvPolynomial.eval₂Hom_X {S : Type v} [CommRing S] {R : Type u} (c : ℤ →+* S) (f : MvPolynomial R ℤ →+* S) (x : MvPolynomial R ℤ) : MvPolynomial.eval₂ c (⇑f ∘ MvPolynomial.X) x = f x

A ring homomorphism f : Z[X_1, X_2, ...] → R is determined by the evaluations f(X_1), f(X_2), ...

def MvPolynomial.homEquiv {S : Type v} {σ : Type u_1} [CommRing S] : (MvPolynomial σ ℤ →+* S) ≃ (σ → S)

Ring homomorphisms out of integer polynomials on a type σ are the same as functions out of the type σ,

Equations

• One or more equations did not get rendered due to their size.

theorem MvPolynomial.degreeOf_sub_lt {R : Type u} {σ : Type u_1} [CommRing R] {x : σ} {f : MvPolynomial σ R} {g : MvPolynomial σ R} {k : ℕ} (h : 0 < k) (hf : ∀ m ∈ f.support, k ≤ m x → MvPolynomial.coeff m f = MvPolynomial.coeff m g) (hg : ∀ m ∈ g.support, k ≤ m x → MvPolynomial.coeff m f = MvPolynomial.coeff m g) : MvPolynomial.degreeOf x (f - g) < k

@[simp]

theorem MvPolynomial.totalDegree_neg {R : Type u} {σ : Type u_1} [CommRing R] (a : MvPolynomial σ R) : (-a).totalDegree = a.totalDegree

theorem MvPolynomial.totalDegree_sub {R : Type u} {σ : Type u_1} [CommRing R] (a : MvPolynomial σ R) (b : MvPolynomial σ R) : (a - b).totalDegree ≤ a.totalDegree ⊔ b.totalDegree

theorem MvPolynomial.totalDegree_sub_C_le {R : Type u} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) (r : R) : (p - MvPolynomial.C r).totalDegree ≤ p.totalDegree