Renaming variables of polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file establishes the rename operation on multivariate polynomials,
which modifies the set of variables.
Main declarations #
Notation #
As in other polynomial files, we typically use the notation:
-
σ τ α : Type*(indexing the variables) -
R S : Type*[comm_semiring R][comm_semiring S](the coefficients) -
s : σ →₀ ℕ, a function fromσtoℕwhich is zero away from a finite set. This will give rise to a monomial inmv_polynomial σ Rwhich mathematicians might callX^s -
r : Relements of the coefficient ring -
i : σ, with corresponding monomialX i, often denotedX_iby mathematicians -
p : mv_polynomial σ α
noncomputable
def
mv_polynomial.rename
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(f : σ → τ) :
mv_polynomial σ R →ₐ[R] mv_polynomial τ R
Rename all the variables in a multivariable polynomial.
Equations
@[simp]
theorem
mv_polynomial.rename_C
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(f : σ → τ)
(r : R) :
@[simp]
theorem
mv_polynomial.rename_X
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(f : σ → τ)
(i : σ) :
⇑(mv_polynomial.rename f) (mv_polynomial.X i) = mv_polynomial.X (f i)
theorem
mv_polynomial.map_rename
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
{S : Type u_5}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S)
(g : σ → τ)
(p : mv_polynomial σ R) :
⇑(mv_polynomial.map f) (⇑(mv_polynomial.rename g) p) = ⇑(mv_polynomial.rename g) (⇑(mv_polynomial.map f) p)
@[simp]
theorem
mv_polynomial.rename_rename
{σ : Type u_1}
{τ : Type u_2}
{α : Type u_3}
{R : Type u_4}
[comm_semiring R]
(f : σ → τ)
(g : τ → α)
(p : mv_polynomial σ R) :
⇑(mv_polynomial.rename g) (⇑(mv_polynomial.rename f) p) = ⇑(mv_polynomial.rename (g ∘ f)) p
@[simp]
theorem
mv_polynomial.rename_id
{σ : Type u_1}
{R : Type u_4}
[comm_semiring R]
(p : mv_polynomial σ R) :
⇑(mv_polynomial.rename id) p = p
theorem
mv_polynomial.rename_monomial
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(f : σ → τ)
(d : σ →₀ ℕ)
(r : R) :
⇑(mv_polynomial.rename f) (⇑(mv_polynomial.monomial d) r) = ⇑(mv_polynomial.monomial (finsupp.map_domain f d)) r
theorem
mv_polynomial.rename_eq
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(f : σ → τ)
(p : mv_polynomial σ R) :
⇑(mv_polynomial.rename f) p = finsupp.map_domain (finsupp.map_domain f) p
theorem
mv_polynomial.rename_injective
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(f : σ → τ)
(hf : function.injective f) :
noncomputable
def
mv_polynomial.kill_compl
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
{f : σ → τ}
(hf : function.injective f) :
mv_polynomial τ R →ₐ[R] mv_polynomial σ R
Given a function between sets of variables f : σ → τ that is injective with proof hf,
kill_compl hf is the alg_hom from R[τ] to R[σ] that is left inverse to
rename f : R[σ] → R[τ] and sends the variables in the complement of the range of f to 0.
Equations
- mv_polynomial.kill_compl hf = mv_polynomial.aeval (λ (i : τ), dite (i ∈ set.range f) (λ (h : i ∈ set.range f), mv_polynomial.X (⇑((equiv.of_injective f hf).symm) ⟨i, h⟩)) (λ (h : i ∉ set.range f), 0))
theorem
mv_polynomial.kill_compl_comp_rename
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
{f : σ → τ}
(hf : function.injective f) :
(mv_polynomial.kill_compl hf).comp (mv_polynomial.rename f) = alg_hom.id R (mv_polynomial σ R)
@[simp]
theorem
mv_polynomial.kill_compl_rename_app
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
{f : σ → τ}
(hf : function.injective f)
(p : mv_polynomial σ R) :
⇑(mv_polynomial.kill_compl hf) (⇑(mv_polynomial.rename f) p) = p
@[simp]
theorem
mv_polynomial.rename_equiv_apply
{σ : Type u_1}
{τ : Type u_2}
(R : Type u_4)
[comm_semiring R]
(f : σ ≃ τ)
(ᾰ : mv_polynomial σ R) :
⇑(mv_polynomial.rename_equiv R f) ᾰ = ⇑(mv_polynomial.rename ⇑f) ᾰ
noncomputable
def
mv_polynomial.rename_equiv
{σ : Type u_1}
{τ : Type u_2}
(R : Type u_4)
[comm_semiring R]
(f : σ ≃ τ) :
mv_polynomial σ R ≃ₐ[R] mv_polynomial τ R
mv_polynomial.rename e is an equivalence when e is.
@[simp]
@[simp]
theorem
mv_polynomial.rename_equiv_symm
{σ : Type u_1}
{τ : Type u_2}
(R : Type u_4)
[comm_semiring R]
(f : σ ≃ τ) :
@[simp]
theorem
mv_polynomial.rename_equiv_trans
{σ : Type u_1}
{τ : Type u_2}
{α : Type u_3}
(R : Type u_4)
[comm_semiring R]
(e : σ ≃ τ)
(f : τ ≃ α) :
(mv_polynomial.rename_equiv R e).trans (mv_polynomial.rename_equiv R f) = mv_polynomial.rename_equiv R (e.trans f)
theorem
mv_polynomial.eval₂_rename
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
{S : Type u_5}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S)
(k : σ → τ)
(g : τ → S)
(p : mv_polynomial σ R) :
mv_polynomial.eval₂ f g (⇑(mv_polynomial.rename k) p) = mv_polynomial.eval₂ f (g ∘ k) p
theorem
mv_polynomial.eval₂_hom_rename
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
{S : Type u_5}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S)
(k : σ → τ)
(g : τ → S)
(p : mv_polynomial σ R) :
⇑(mv_polynomial.eval₂_hom f g) (⇑(mv_polynomial.rename k) p) = ⇑(mv_polynomial.eval₂_hom f (g ∘ k)) p
theorem
mv_polynomial.aeval_rename
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
{S : Type u_5}
[comm_semiring R]
[comm_semiring S]
(k : σ → τ)
(g : τ → S)
(p : mv_polynomial σ R)
[algebra R S] :
⇑(mv_polynomial.aeval g) (⇑(mv_polynomial.rename k) p) = ⇑(mv_polynomial.aeval (g ∘ k)) p
theorem
mv_polynomial.rename_eval₂
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(k : σ → τ)
(p : mv_polynomial σ R)
(g : τ → mv_polynomial σ R) :
⇑(mv_polynomial.rename k) (mv_polynomial.eval₂ mv_polynomial.C (g ∘ k) p) = mv_polynomial.eval₂ mv_polynomial.C (⇑(mv_polynomial.rename k) ∘ g) (⇑(mv_polynomial.rename k) p)
theorem
mv_polynomial.rename_prodmk_eval₂
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(p : mv_polynomial σ R)
(j : τ)
(g : σ → mv_polynomial σ R) :
⇑(mv_polynomial.rename (prod.mk j)) (mv_polynomial.eval₂ mv_polynomial.C g p) = mv_polynomial.eval₂ mv_polynomial.C (λ (x : σ), ⇑(mv_polynomial.rename (prod.mk j)) (g x)) p
theorem
mv_polynomial.eval₂_rename_prodmk
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
{S : Type u_5}
[comm_semiring R]
[comm_semiring S]
(f : R →+* S)
(g : σ × τ → S)
(i : σ)
(p : mv_polynomial τ R) :
mv_polynomial.eval₂ f g (⇑(mv_polynomial.rename (prod.mk i)) p) = mv_polynomial.eval₂ f (λ (j : τ), g (i, j)) p
theorem
mv_polynomial.eval_rename_prodmk
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(g : σ × τ → R)
(i : σ)
(p : mv_polynomial τ R) :
⇑(mv_polynomial.eval g) (⇑(mv_polynomial.rename (prod.mk i)) p) = ⇑(mv_polynomial.eval (λ (j : τ), g (i, j))) p
theorem
mv_polynomial.exists_finset_rename
{σ : Type u_1}
{R : Type u_4}
[comm_semiring R]
(p : mv_polynomial σ R) :
∃ (s : finset σ) (q : mv_polynomial {x // x ∈ s} R), p = ⇑(mv_polynomial.rename coe) q
Every polynomial is a polynomial in finitely many variables.
theorem
mv_polynomial.exists_finset_rename₂
{σ : Type u_1}
{R : Type u_4}
[comm_semiring R]
(p₁ p₂ : mv_polynomial σ R) :
∃ (s : finset σ) (q₁ q₂ : mv_polynomial ↥s R), p₁ = ⇑(mv_polynomial.rename coe) q₁ ∧ p₂ = ⇑(mv_polynomial.rename coe) q₂
exists_finset_rename for two polyonomials at once: for any two polynomials p₁, p₂ in a
polynomial semiring R[σ] of possibly infinitely many variables, exists_finset_rename₂ yields
a finite subset s of σ such that both p₁ and p₂ are contained in the polynomial semiring
R[s] of finitely many variables.
theorem
mv_polynomial.exists_fin_rename
{σ : Type u_1}
{R : Type u_4}
[comm_semiring R]
(p : mv_polynomial σ R) :
∃ (n : ℕ) (f : fin n → σ) (hf : function.injective f) (q : mv_polynomial (fin n) R), p = ⇑(mv_polynomial.rename f) q
Every polynomial is a polynomial in finitely many variables.
theorem
mv_polynomial.eval₂_cast_comp
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(f : σ → τ)
(c : ℤ →+* R)
(g : τ → R)
(p : mv_polynomial σ ℤ) :
mv_polynomial.eval₂ c (g ∘ f) p = mv_polynomial.eval₂ c g (⇑(mv_polynomial.rename f) p)
@[simp]
theorem
mv_polynomial.coeff_rename_map_domain
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(f : σ → τ)
(hf : function.injective f)
(φ : mv_polynomial σ R)
(d : σ →₀ ℕ) :
mv_polynomial.coeff (finsupp.map_domain f d) (⇑(mv_polynomial.rename f) φ) = mv_polynomial.coeff d φ
theorem
mv_polynomial.coeff_rename_eq_zero
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(f : σ → τ)
(φ : mv_polynomial σ R)
(d : τ →₀ ℕ)
(h : ∀ (u : σ →₀ ℕ), finsupp.map_domain f u = d → mv_polynomial.coeff u φ = 0) :
mv_polynomial.coeff d (⇑(mv_polynomial.rename f) φ) = 0
theorem
mv_polynomial.coeff_rename_ne_zero
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
(f : σ → τ)
(φ : mv_polynomial σ R)
(d : τ →₀ ℕ)
(h : mv_polynomial.coeff d (⇑(mv_polynomial.rename f) φ) ≠ 0) :
∃ (u : σ →₀ ℕ), finsupp.map_domain f u = d ∧ mv_polynomial.coeff u φ ≠ 0
@[simp]
theorem
mv_polynomial.constant_coeff_rename
{σ : Type u_1}
{R : Type u_4}
[comm_semiring R]
{τ : Type u_2}
(f : σ → τ)
(φ : mv_polynomial σ R) :
theorem
mv_polynomial.support_rename_of_injective
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[comm_semiring R]
{p : mv_polynomial σ R}
{f : σ → τ}
[decidable_eq τ]
(h : function.injective f) :
(⇑(mv_polynomial.rename f) p).support = finset.image (finsupp.map_domain f) p.support