Variables of polynomials

This file establishes many results about the variable sets of a multivariate polynomial.

The variable set of a polynomial $P \in R[X]$ is a Finset containing each $x \in X$ that appears in a monomial in $P$.

Main declarations

• MvPolynomial.vars p : the finset of variables occurring in p. For example if p = x⁴y+yz then vars p = {x, y, z}

Notation

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

• σ τ : Type* (indexing the variables)

• R : Type* [CommSemiring 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

• r : R

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

• p : MvPolynomial σ R

vars

def MvPolynomial.vars {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) : Finset σ

vars p is the set of variables appearing in the polynomial p

Equations

• p.vars = p.degrees.toFinset

theorem MvPolynomial.vars_def {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) : p.vars = p.degrees.toFinset

@[simp]

theorem MvPolynomial.vars_0 {R : Type u} {σ : Type u_1} [CommSemiring R] : MvPolynomial.vars 0 = ∅

@[simp]

theorem MvPolynomial.vars_monomial {R : Type u} {σ : Type u_1} {r : R} {s : σ →₀ ℕ} [CommSemiring R] (h : r ≠ 0) : ((MvPolynomial.monomial s) r).vars = s.support

@[simp]

theorem MvPolynomial.vars_C {R : Type u} {σ : Type u_1} {r : R} [CommSemiring R] : (MvPolynomial.C r).vars = ∅

@[simp]

theorem MvPolynomial.vars_X {R : Type u} {σ : Type u_1} {n : σ} [CommSemiring R] [Nontrivial R] : (MvPolynomial.X n).vars = {n}

theorem MvPolynomial.mem_vars {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} (i : σ) : i ∈ p.vars ↔ ∃ d ∈ p.support, i ∈ d.support

theorem MvPolynomial.mem_support_not_mem_vars_zero {R : Type u} {σ : Type u_1} [CommSemiring R] {f : MvPolynomial σ R} {x : σ →₀ ℕ} (H : x ∈ f.support) {v : σ} (h : v ∉ f.vars) : x v = 0

theorem MvPolynomial.vars_add_subset {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) : (p + q).vars ⊆ p.vars ∪ q.vars

theorem MvPolynomial.vars_add_of_disjoint {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} [DecidableEq σ] (h : Disjoint p.vars q.vars) : (p + q).vars = p.vars ∪ q.vars

theorem MvPolynomial.vars_mul {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (φ : MvPolynomial σ R) (ψ : MvPolynomial σ R) : (φ * ψ).vars ⊆ φ.vars ∪ ψ.vars

@[simp]

theorem MvPolynomial.vars_one {R : Type u} {σ : Type u_1} [CommSemiring R] : MvPolynomial.vars 1 = ∅

theorem MvPolynomial.vars_pow {R : Type u} {σ : Type u_1} [CommSemiring R] (φ : MvPolynomial σ R) (n : ℕ) : (φ ^ n).vars ⊆ φ.vars

theorem MvPolynomial.vars_prod {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} [DecidableEq σ] {s : Finset ι} (f : ι → MvPolynomial σ R) : (∏ i ∈ s, f i).vars ⊆ s.biUnion fun (i : ι) => (f i).vars

The variables of the product of a family of polynomials are a subset of the union of the sets of variables of each polynomial.

theorem MvPolynomial.vars_C_mul {σ : Type u_1} {A : Type u_3} [CommRing A] [NoZeroDivisors A] (a : A) (ha : a ≠ 0) (φ : MvPolynomial σ A) : (MvPolynomial.C a * φ).vars = φ.vars

theorem MvPolynomial.vars_sum_subset {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (t : Finset ι) (φ : ι → MvPolynomial σ R) [DecidableEq σ] : (∑ i ∈ t, φ i).vars ⊆ t.biUnion fun (i : ι) => (φ i).vars

theorem MvPolynomial.vars_sum_of_disjoint {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (t : Finset ι) (φ : ι → MvPolynomial σ R) [DecidableEq σ] (h : Pairwise (Disjoint on fun (i : ι) => (φ i).vars)) : (∑ i ∈ t, φ i).vars = t.biUnion fun (i : ι) => (φ i).vars

theorem MvPolynomial.vars_map {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) [CommSemiring S] (f : R →+* S) : ((MvPolynomial.map f) p).vars ⊆ p.vars

theorem MvPolynomial.vars_map_of_injective {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) [CommSemiring S] {f : R →+* S} (hf : Function.Injective ⇑f) : ((MvPolynomial.map f) p).vars = p.vars

theorem MvPolynomial.vars_monomial_single {R : Type u} {σ : Type u_1} [CommSemiring R] (i : σ) {e : ℕ} {r : R} (he : e ≠ 0) (hr : r ≠ 0) : ((MvPolynomial.monomial (Finsupp.single i e)) r).vars = {i}

theorem MvPolynomial.vars_eq_support_biUnion_support {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) [DecidableEq σ] : p.vars = p.support.biUnion Finsupp.support

vars and eval

theorem MvPolynomial.eval₂Hom_eq_constantCoeff_of_vars {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] (f : R →+* S) {g : σ → S} {p : MvPolynomial σ R} (hp : ∀ i ∈ p.vars, g i = 0) : (MvPolynomial.eval₂Hom f g) p = f (MvPolynomial.constantCoeff p)

theorem MvPolynomial.aeval_eq_constantCoeff_of_vars {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] [Algebra R S] {g : σ → S} {p : MvPolynomial σ R} (hp : ∀ i ∈ p.vars, g i = 0) : (MvPolynomial.aeval g) p = (algebraMap R S) (MvPolynomial.constantCoeff p)

theorem MvPolynomial.eval₂Hom_congr' {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] {f₁ : R →+* S} {f₂ : R →+* S} {g₁ : σ → S} {g₂ : σ → S} {p₁ : MvPolynomial σ R} {p₂ : MvPolynomial σ R} : f₁ = f₂ → (∀ i ∈ p₁.vars, i ∈ p₂.vars → g₁ i = g₂ i) → p₁ = p₂ → (MvPolynomial.eval₂Hom f₁ g₁) p₁ = (MvPolynomial.eval₂Hom f₂ g₂) p₂

theorem MvPolynomial.hom_congr_vars {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] {f₁ : MvPolynomial σ R →+* S} {f₂ : MvPolynomial σ R →+* S} {p₁ : MvPolynomial σ R} {p₂ : MvPolynomial σ R} (hC : f₁.comp MvPolynomial.C = f₂.comp MvPolynomial.C) (hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (MvPolynomial.X i) = f₂ (MvPolynomial.X i)) (hp : p₁ = p₂) : f₁ p₁ = f₂ p₂

If f₁ and f₂ are ring homs out of the polynomial ring and p₁ and p₂ are polynomials, then f₁ p₁ = f₂ p₂ if p₁ = p₂ and f₁ and f₂ are equal on R and on the variables of p₁.

theorem MvPolynomial.exists_rename_eq_of_vars_subset_range {R : Type u} {σ : Type u_1} {τ : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (f : τ → σ) (hfi : Function.Injective f) (hf : ↑p.vars ⊆ Set.range f) : ∃ (q : MvPolynomial τ R), (MvPolynomial.rename f) q = p

theorem MvPolynomial.vars_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [CommSemiring R] [DecidableEq τ] (f : σ → τ) (φ : MvPolynomial σ R) : ((MvPolynomial.rename f) φ).vars ⊆ Finset.image f φ.vars

theorem MvPolynomial.mem_vars_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [CommSemiring R] (f : σ → τ) (φ : MvPolynomial σ R) {j : τ} (h : j ∈ ((MvPolynomial.rename f) φ).vars) : ∃ i ∈ φ.vars, f i = j

theorem MvPolynomial.leadingCoeff_toLex {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} [LinearOrder σ] : AddMonoidAlgebra.leadingCoeff (⇑toLex) p = MvPolynomial.coeff (ofLex (AddMonoidAlgebra.supDegree (⇑toLex) p)) p

theorem MvPolynomial.supDegree_toLex_C {R : Type u} {σ : Type u_1} [CommSemiring R] [LinearOrder σ] (r : R) : AddMonoidAlgebra.supDegree (⇑toLex) (MvPolynomial.C r) = 0

theorem MvPolynomial.leadingCoeff_toLex_C {R : Type u} {σ : Type u_1} [CommSemiring R] [LinearOrder σ] (r : R) : AddMonoidAlgebra.leadingCoeff (⇑toLex) (MvPolynomial.C r) = r