# Documentation

Mathlib.Data.MvPolynomial.Rename

# Renaming variables of polynomials #

This file establishes the rename operation on multivariate polynomials, which modifies the set of variables.

## Main declarations #

• MvPolynomial.rename
• MvPolynomial.renameEquiv

## Notation #

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

• σ τ α : Type* (indexing the variables)

• R S : Type* [CommSemiring R] [CommSemiring S] (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 elements of the coefficient ring

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

• p : MvPolynomial σ α

def MvPolynomial.rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : στ) :

Rename all the variables in a multivariable polynomial.

Instances For
@[simp]
theorem MvPolynomial.rename_C {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : στ) (r : R) :
↑() (MvPolynomial.C r) = MvPolynomial.C r
@[simp]
theorem MvPolynomial.rename_X {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : στ) (i : σ) :
↑() () = MvPolynomial.X (f i)
theorem MvPolynomial.map_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [] [] (f : R →+* S) (g : στ) (p : ) :
↑() (↑() p) = ↑() (↑() p)
@[simp]
theorem MvPolynomial.rename_rename {σ : Type u_1} {τ : Type u_2} {α : Type u_3} {R : Type u_4} [] (f : στ) (g : τα) (p : ) :
↑() (↑() p) = ↑(MvPolynomial.rename (g f)) p
@[simp]
theorem MvPolynomial.rename_id {σ : Type u_1} {R : Type u_4} [] (p : ) :
↑() p = p
theorem MvPolynomial.rename_monomial {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : στ) (d : σ →₀ ) (r : R) :
↑() (↑() r) = ↑() r
theorem MvPolynomial.rename_eq {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : στ) (p : ) :
↑() p =
theorem MvPolynomial.rename_injective {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : στ) (hf : ) :
def MvPolynomial.killCompl {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] {f : στ} (hf : ) :

Given a function between sets of variables f : σ → τ that is injective with proof hf, MvPolynomial.killCompl hf is the AlgHom 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.

Instances For
theorem MvPolynomial.killCompl_comp_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] {f : στ} (hf : ) :
= AlgHom.id R ()
@[simp]
theorem MvPolynomial.killCompl_rename_app {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] {f : στ} (hf : ) (p : ) :
↑() (↑() p) = p
@[simp]
theorem MvPolynomial.renameEquiv_apply {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [] (f : σ τ) (a : ) :
↑() a = ↑() a
def MvPolynomial.renameEquiv {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [] (f : σ τ) :

MvPolynomial.rename e is an equivalence when e is.

Instances For
@[simp]
theorem MvPolynomial.renameEquiv_refl {σ : Type u_1} (R : Type u_4) [] :
= AlgEquiv.refl
@[simp]
theorem MvPolynomial.renameEquiv_symm {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [] (f : σ τ) :
@[simp]
theorem MvPolynomial.renameEquiv_trans {σ : Type u_1} {τ : Type u_2} {α : Type u_3} (R : Type u_4) [] (e : σ τ) (f : τ α) :
theorem MvPolynomial.eval₂_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [] [] (f : R →+* S) (k : στ) (g : τS) (p : ) :
theorem MvPolynomial.eval₂Hom_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [] [] (f : R →+* S) (k : στ) (g : τS) (p : ) :
↑() (↑() p) = ↑(MvPolynomial.eval₂Hom f (g k)) p
theorem MvPolynomial.aeval_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [] [] (k : στ) (g : τS) (p : ) [Algebra R S] :
↑() (↑() p) = ↑(MvPolynomial.aeval (g k)) p
theorem MvPolynomial.rename_eval₂ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (k : στ) (p : ) (g : τ) :
↑() (MvPolynomial.eval₂ MvPolynomial.C (g k) p) = MvPolynomial.eval₂ MvPolynomial.C (↑() g) (↑() p)
theorem MvPolynomial.rename_prod_mk_eval₂ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (p : ) (j : τ) (g : σ) :
↑() (MvPolynomial.eval₂ MvPolynomial.C g p) = MvPolynomial.eval₂ MvPolynomial.C (fun x => ↑() (g x)) p
theorem MvPolynomial.eval₂_rename_prod_mk {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [] [] (f : R →+* S) (g : σ × τS) (i : σ) (p : ) :
MvPolynomial.eval₂ f g (↑() p) = MvPolynomial.eval₂ f (fun j => g (i, j)) p
theorem MvPolynomial.eval_rename_prod_mk {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (g : σ × τR) (i : σ) (p : ) :
↑() (↑() p) = ↑(MvPolynomial.eval fun j => g (i, j)) p
theorem MvPolynomial.exists_finset_rename {σ : Type u_1} {R : Type u_4} [] (p : ) :
s q, p = ↑(MvPolynomial.rename Subtype.val) q

Every polynomial is a polynomial in finitely many variables.

theorem MvPolynomial.exists_finset_rename₂ {σ : Type u_1} {R : Type u_4} [] (p₁ : ) (p₂ : ) :
s q₁ q₂, p₁ = ↑(MvPolynomial.rename Subtype.val) q₁ p₂ = ↑(MvPolynomial.rename Subtype.val) q₂

exists_finset_rename for two polynomials 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 MvPolynomial.exists_fin_rename {σ : Type u_1} {R : Type u_4} [] (p : ) :
n f _hf q, p = ↑() q

Every polynomial is a polynomial in finitely many variables.

theorem MvPolynomial.eval₂_cast_comp {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : στ) (c : →+* R) (g : τR) (p : ) :
@[simp]
theorem MvPolynomial.coeff_rename_mapDomain {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : στ) (hf : ) (φ : ) (d : σ →₀ ) :
MvPolynomial.coeff () (↑() φ) =
theorem MvPolynomial.coeff_rename_eq_zero {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : στ) (φ : ) (d : τ →₀ ) (h : ∀ (u : σ →₀ ), = d = 0) :
MvPolynomial.coeff d (↑() φ) = 0
theorem MvPolynomial.coeff_rename_ne_zero {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] (f : στ) (φ : ) (d : τ →₀ ) (h : MvPolynomial.coeff d (↑() φ) 0) :
u, = d 0
@[simp]
theorem MvPolynomial.constantCoeff_rename {σ : Type u_1} {R : Type u_4} [] {τ : Type u_6} (f : στ) (φ : ) :
MvPolynomial.constantCoeff (↑() φ) = MvPolynomial.constantCoeff φ
theorem MvPolynomial.support_rename_of_injective {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [] {p : } {f : στ} [] (h : ) :