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 inp. For example ifp = x⁴y+yzthenvars 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 inMvPolynomial σ Rwhich mathematicians might callX^s -
r : R -
i : σ, with corresponding monomialX i, often denotedX_iby mathematicians -
p : MvPolynomial σ R
theorem
MvPolynomial.vars_def
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
[DecidableEq σ]
(p : MvPolynomial σ R)
:
p.vars = p.degrees.toFinset
@[simp]
@[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]
@[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 : σ)
:
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)
:
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)
:
theorem
MvPolynomial.vars_mul
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
[DecidableEq σ]
(φ : MvPolynomial σ R)
(ψ : MvPolynomial σ R)
:
@[simp]
theorem
MvPolynomial.vars_pow
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(φ : MvPolynomial σ R)
(n : ℕ)
:
theorem
MvPolynomial.vars_prod
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{ι : Type u_3}
[DecidableEq σ]
{s : Finset ι}
(f : ι → MvPolynomial σ R)
:
(s.prod fun (i : ι) => 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]
[IsDomain A]
(a : A)
(ha : a ≠ 0)
(φ : MvPolynomial σ A)
:
theorem
MvPolynomial.vars_sum_subset
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{ι : Type u_3}
(t : Finset ι)
(φ : ι → MvPolynomial σ R)
[DecidableEq σ]
:
(t.sum fun (i : ι) => φ 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))
:
(t.sum fun (i : ι) => φ 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
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