Renaming variables of polynomials
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^sr : Relements of the coefficient ringi : σ, with corresponding monomialX i, often denotedX_iby mathematiciansp : mv_polynomial σ α
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) :
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_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) :