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)
:
@[simp]
@[simp]
theorem
MvPolynomial.vars_monomial
{R : Type u}
{σ : Type u_1}
{r : R}
{s : σ →₀ ℕ}
[CommSemiring R]
(h : r ≠ 0)
:
MvPolynomial.vars ((MvPolynomial.monomial s) r) = s.support
@[simp]
theorem
MvPolynomial.vars_C
{R : Type u}
{σ : Type u_1}
{r : R}
[CommSemiring R]
:
MvPolynomial.vars (MvPolynomial.C r) = ∅
@[simp]
theorem
MvPolynomial.vars_X
{R : Type u}
{σ : Type u_1}
{n : σ}
[CommSemiring R]
[Nontrivial R]
:
MvPolynomial.vars (MvPolynomial.X n) = {n}
theorem
MvPolynomial.mem_vars
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{p : MvPolynomial σ R}
(i : σ)
:
i ∈ MvPolynomial.vars p ↔ ∃ d ∈ MvPolynomial.support p, 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 ∈ MvPolynomial.support f)
{v : σ}
(h : v ∉ MvPolynomial.vars f)
:
x v = 0
theorem
MvPolynomial.vars_add_subset
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
[DecidableEq σ]
(p : MvPolynomial σ R)
(q : MvPolynomial σ R)
:
MvPolynomial.vars (p + q) ⊆ MvPolynomial.vars p ∪ MvPolynomial.vars q
theorem
MvPolynomial.vars_add_of_disjoint
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{p : MvPolynomial σ R}
{q : MvPolynomial σ R}
[DecidableEq σ]
(h : Disjoint (MvPolynomial.vars p) (MvPolynomial.vars q))
:
MvPolynomial.vars (p + q) = MvPolynomial.vars p ∪ MvPolynomial.vars q
theorem
MvPolynomial.vars_mul
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
[DecidableEq σ]
(φ : MvPolynomial σ R)
(ψ : MvPolynomial σ R)
:
MvPolynomial.vars (φ * ψ) ⊆ MvPolynomial.vars φ ∪ MvPolynomial.vars ψ
@[simp]
theorem
MvPolynomial.vars_pow
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(φ : MvPolynomial σ R)
(n : ℕ)
:
MvPolynomial.vars (φ ^ n) ⊆ MvPolynomial.vars φ
theorem
MvPolynomial.vars_prod
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{ι : Type u_3}
[DecidableEq σ]
{s : Finset ι}
(f : ι → MvPolynomial σ R)
:
MvPolynomial.vars (Finset.prod s fun (i : ι) => f i) ⊆ Finset.biUnion s fun (i : ι) => MvPolynomial.vars (f i)
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)
:
MvPolynomial.vars (MvPolynomial.C a * φ) = MvPolynomial.vars φ
theorem
MvPolynomial.vars_sum_subset
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{ι : Type u_3}
(t : Finset ι)
(φ : ι → MvPolynomial σ R)
[DecidableEq σ]
:
MvPolynomial.vars (Finset.sum t fun (i : ι) => φ i) ⊆ Finset.biUnion t fun (i : ι) => MvPolynomial.vars (φ i)
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 : ι) => MvPolynomial.vars (φ i)))
:
MvPolynomial.vars (Finset.sum t fun (i : ι) => φ i) = Finset.biUnion t fun (i : ι) => MvPolynomial.vars (φ i)
theorem
MvPolynomial.vars_map
{R : Type u}
{S : Type v}
{σ : Type u_1}
[CommSemiring R]
(p : MvPolynomial σ R)
[CommSemiring S]
(f : R →+* S)
:
MvPolynomial.vars ((MvPolynomial.map f) p) ⊆ MvPolynomial.vars p
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.vars ((MvPolynomial.map f) p) = MvPolynomial.vars p
theorem
MvPolynomial.vars_monomial_single
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(i : σ)
{e : ℕ}
{r : R}
(he : e ≠ 0)
(hr : r ≠ 0)
:
MvPolynomial.vars ((MvPolynomial.monomial (Finsupp.single i e)) r) = {i}
theorem
MvPolynomial.vars_eq_support_biUnion_support
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(p : MvPolynomial σ R)
[DecidableEq σ]
:
MvPolynomial.vars p = Finset.biUnion (MvPolynomial.support p) 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 ∈ MvPolynomial.vars p, 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 ∈ MvPolynomial.vars p, 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 ∈ MvPolynomial.vars p₁, i ∈ MvPolynomial.vars p₂ → 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 : RingHom.comp f₁ MvPolynomial.C = RingHom.comp f₂ MvPolynomial.C)
(hv : ∀ i ∈ MvPolynomial.vars p₁, i ∈ MvPolynomial.vars p₂ → 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 : ↑(MvPolynomial.vars p) ⊆ 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.vars ((MvPolynomial.rename f) φ) ⊆ Finset.image f (MvPolynomial.vars φ)
theorem
MvPolynomial.mem_vars_rename
{R : Type u}
{σ : Type u_1}
{τ : Type u_2}
[CommSemiring R]
(f : σ → τ)
(φ : MvPolynomial σ R)
{j : τ}
(h : j ∈ MvPolynomial.vars ((MvPolynomial.rename f) φ))
:
∃ i ∈ MvPolynomial.vars φ, f i = j