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} [CommSemiring R] (f : σ → τ) : MvPolynomial σ R →ₐ[R] MvPolynomial τ R

Rename all the variables in a multivariable polynomial.

Equations

• MvPolynomial.rename f = MvPolynomial.aeval (MvPolynomial.X ∘ f)

theorem MvPolynomial.rename_C {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (r : R) : (MvPolynomial.rename f) (MvPolynomial.C r) = MvPolynomial.C r

@[simp]

theorem MvPolynomial.rename_X {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (i : σ) : (MvPolynomial.rename f) (MvPolynomial.X i) = MvPolynomial.X (f i)

theorem MvPolynomial.map_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] (f : R →+* S) (g : σ → τ) (p : MvPolynomial σ R) : (MvPolynomial.map f) ((MvPolynomial.rename g) p) = (MvPolynomial.rename g) ((MvPolynomial.map f) p)

@[simp]

theorem MvPolynomial.rename_rename {σ : Type u_1} {τ : Type u_2} {α : Type u_3} {R : Type u_4} [CommSemiring R] (f : σ → τ) (g : τ → α) (p : MvPolynomial σ R) : (MvPolynomial.rename g) ((MvPolynomial.rename f) p) = (MvPolynomial.rename (g ∘ f)) p

@[simp]

theorem MvPolynomial.rename_id {σ : Type u_1} {R : Type u_4} [CommSemiring R] (p : MvPolynomial σ R) : (MvPolynomial.rename id) p = p

theorem MvPolynomial.rename_monomial {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (d : σ →₀ ℕ) (r : R) : (MvPolynomial.rename f) ((MvPolynomial.monomial d) r) = (MvPolynomial.monomial (Finsupp.mapDomain f d)) r

theorem MvPolynomial.rename_eq {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (p : MvPolynomial σ R) : (MvPolynomial.rename f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p

theorem MvPolynomial.rename_injective {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (hf : Function.Injective f) : Function.Injective ⇑(MvPolynomial.rename f)

def MvPolynomial.killCompl {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {f : σ → τ} (hf : Function.Injective f) : MvPolynomial τ R →ₐ[R] MvPolynomial σ R

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.

Equations

• MvPolynomial.killCompl hf = MvPolynomial.aeval fun (i : τ) => if h : i ∈ Set.range f then MvPolynomial.X ((Equiv.ofInjective f hf).symm ⟨i, h⟩) else 0

theorem MvPolynomial.killCompl_C {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {f : σ → τ} (hf : Function.Injective f) (r : R) : (MvPolynomial.killCompl hf) (MvPolynomial.C r) = MvPolynomial.C r

theorem MvPolynomial.killCompl_comp_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {f : σ → τ} (hf : Function.Injective f) : (MvPolynomial.killCompl hf).comp (MvPolynomial.rename f) = AlgHom.id R (MvPolynomial σ R)

@[simp]

theorem MvPolynomial.killCompl_rename_app {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {f : σ → τ} (hf : Function.Injective f) (p : MvPolynomial σ R) : (MvPolynomial.killCompl hf) ((MvPolynomial.rename f) p) = p

@[simp]

theorem MvPolynomial.renameEquiv_apply {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [CommSemiring R] (f : σ ≃ τ) (a : MvPolynomial σ R) : (MvPolynomial.renameEquiv R f) a = (MvPolynomial.rename ⇑f) a

def MvPolynomial.renameEquiv {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [CommSemiring R] (f : σ ≃ τ) : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R

MvPolynomial.rename e is an equivalence when e is.

Equations

• MvPolynomial.renameEquiv R f = { toFun := ⇑(MvPolynomial.rename ⇑f), invFun := ⇑(MvPolynomial.rename ⇑f.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem MvPolynomial.renameEquiv_refl {σ : Type u_1} (R : Type u_4) [CommSemiring R] : MvPolynomial.renameEquiv R (Equiv.refl σ) = AlgEquiv.refl

@[simp]

theorem MvPolynomial.renameEquiv_symm {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [CommSemiring R] (f : σ ≃ τ) : (MvPolynomial.renameEquiv R f).symm = MvPolynomial.renameEquiv R f.symm

@[simp]

theorem MvPolynomial.renameEquiv_trans {σ : Type u_1} {τ : Type u_2} {α : Type u_3} (R : Type u_4) [CommSemiring R] (e : σ ≃ τ) (f : τ ≃ α) : (MvPolynomial.renameEquiv R e).trans (MvPolynomial.renameEquiv R f) = MvPolynomial.renameEquiv R (e.trans f)

theorem MvPolynomial.eval₂_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] (f : R →+* S) (k : σ → τ) (g : τ → S) (p : MvPolynomial σ R) : MvPolynomial.eval₂ f g ((MvPolynomial.rename k) p) = MvPolynomial.eval₂ f (g ∘ k) p

theorem MvPolynomial.eval_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (k : σ → τ) (g : τ → R) (p : MvPolynomial σ R) : (MvPolynomial.eval g) ((MvPolynomial.rename k) p) = (MvPolynomial.eval (g ∘ k)) p

theorem MvPolynomial.eval₂Hom_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] (f : R →+* S) (k : σ → τ) (g : τ → S) (p : MvPolynomial σ R) : (MvPolynomial.eval₂Hom f g) ((MvPolynomial.rename k) 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} [CommSemiring R] [CommSemiring S] (k : σ → τ) (g : τ → S) (p : MvPolynomial σ R) [Algebra R S] : (MvPolynomial.aeval g) ((MvPolynomial.rename k) p) = (MvPolynomial.aeval (g ∘ k)) p

theorem MvPolynomial.rename_eval₂ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (k : σ → τ) (p : MvPolynomial σ R) (g : τ → MvPolynomial σ R) : (MvPolynomial.rename k) (MvPolynomial.eval₂ MvPolynomial.C (g ∘ k) p) = MvPolynomial.eval₂ MvPolynomial.C (⇑(MvPolynomial.rename k) ∘ g) ((MvPolynomial.rename k) p)

theorem MvPolynomial.rename_prod_mk_eval₂ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (p : MvPolynomial σ R) (j : τ) (g : σ → MvPolynomial σ R) : (MvPolynomial.rename (Prod.mk j)) (MvPolynomial.eval₂ MvPolynomial.C g p) = MvPolynomial.eval₂ MvPolynomial.C (fun (x : σ) => (MvPolynomial.rename (Prod.mk j)) (g x)) p

theorem MvPolynomial.eval₂_rename_prod_mk {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] (f : R →+* S) (g : σ × τ → S) (i : σ) (p : MvPolynomial τ R) : MvPolynomial.eval₂ f g ((MvPolynomial.rename (Prod.mk i)) 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} [CommSemiring R] (g : σ × τ → R) (i : σ) (p : MvPolynomial τ R) : (MvPolynomial.eval g) ((MvPolynomial.rename (Prod.mk i)) p) = (MvPolynomial.eval fun (j : τ) => g (i, j)) p

theorem MvPolynomial.exists_finset_rename {σ : Type u_1} {R : Type u_4} [CommSemiring R] (p : MvPolynomial σ R) : ∃ (s : Finset σ) (q : MvPolynomial { x : σ // x ∈ s } R), 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} [CommSemiring R] (p₁ : MvPolynomial σ R) (p₂ : MvPolynomial σ R) : ∃ (s : Finset σ) (q₁ : MvPolynomial { x : σ // x ∈ s } R) (q₂ : MvPolynomial { x : σ // x ∈ s } R), 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} [CommSemiring R] (p : MvPolynomial σ R) : ∃ (n : ℕ) (f : Fin n → σ) (_ : Function.Injective f) (q : MvPolynomial (Fin n) R), p = (MvPolynomial.rename f) 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} [CommSemiring R] (f : σ → τ) (c : ℤ →+* R) (g : τ → R) (p : MvPolynomial σ ℤ) : MvPolynomial.eval₂ c (g ∘ f) p = MvPolynomial.eval₂ c g ((MvPolynomial.rename f) p)

@[simp]

theorem MvPolynomial.coeff_rename_mapDomain {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (hf : Function.Injective f) (φ : MvPolynomial σ R) (d : σ →₀ ℕ) : MvPolynomial.coeff (Finsupp.mapDomain f d) ((MvPolynomial.rename f) φ) = MvPolynomial.coeff d φ

@[simp]

theorem MvPolynomial.coeff_rename_embDomain {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ ↪ τ) (φ : MvPolynomial σ R) (d : σ →₀ ℕ) : MvPolynomial.coeff (Finsupp.embDomain f d) ((MvPolynomial.rename ⇑f) φ) = MvPolynomial.coeff d φ

theorem MvPolynomial.coeff_rename_eq_zero {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ) (h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → MvPolynomial.coeff u φ = 0) : MvPolynomial.coeff d ((MvPolynomial.rename f) φ) = 0

theorem MvPolynomial.coeff_rename_ne_zero {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ) (h : MvPolynomial.coeff d ((MvPolynomial.rename f) φ) ≠ 0) : ∃ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d ∧ MvPolynomial.coeff u φ ≠ 0

@[simp]

theorem MvPolynomial.constantCoeff_rename {σ : Type u_1} {R : Type u_4} [CommSemiring R] {τ : Type u_6} (f : σ → τ) (φ : MvPolynomial σ R) : MvPolynomial.constantCoeff ((MvPolynomial.rename f) φ) = MvPolynomial.constantCoeff φ

theorem MvPolynomial.support_rename_of_injective {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {p : MvPolynomial σ R} {f : σ → τ} [DecidableEq τ] (h : Function.Injective f) : ((MvPolynomial.rename f) p).support = Finset.image (Finsupp.mapDomain f) p.support