# 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 σ α`

source
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)

Instances For

source
theorem MvPolynomial.rename_C {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (r : R) :
(rename f) (C r) = C r
source
@[simp]
theorem MvPolynomial.rename_X {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (i : σ) :
(rename f) (X i) = X (f i)
source
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) :
(map f) ((rename g) p) = (rename g) ((map f) p)
source
theorem MvPolynomial.map_comp_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] (f : R →+* S) (g : σ → τ) :
(map f).comp (rename g).toRingHom = (rename g).comp (map f)
source
@[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) :
(rename g) ((rename f) p) = (rename (g ∘ f)) p
source
theorem MvPolynomial.rename_comp_rename {σ : Type u_1} {τ : Type u_2} {α : Type u_3} {R : Type u_4} [CommSemiring R] (f : σ → τ) (g : τ → α) :
(rename g).comp (rename f) = rename (g ∘ f)
source
@[simp]
theorem MvPolynomial.rename_id {σ : Type u_1} {R : Type u_4} [CommSemiring R] :
rename id = AlgHom.id R (MvPolynomial σ R)
source
theorem MvPolynomial.rename_id_apply {σ : Type u_1} {R : Type u_4} [CommSemiring R] (p : MvPolynomial σ R) :
(rename id) p = p
source
theorem MvPolynomial.rename_monomial {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (d : σ →₀ ℕ) (r : R) :
(rename f) ((monomial d) r) = (monomial (Finsupp.mapDomain f d)) r
source
theorem MvPolynomial.rename_eq {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (p : MvPolynomial σ R) :
(rename f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
source
theorem MvPolynomial.rename_injective {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (hf : Function.Injective f) :
Function.Injective ⇑(rename f)
source
theorem MvPolynomial.rename_leftInverse {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {f : σ → τ} {g : τ → σ} (hf : Function.LeftInverse f g) :
Function.LeftInverse ⇑(rename f) ⇑(rename g)
source
theorem MvPolynomial.rename_rightInverse {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {f : σ → τ} {g : τ → σ} (hf : Function.RightInverse f g) :
Function.RightInverse ⇑(rename f) ⇑(rename g)
source
theorem MvPolynomial.rename_surjective {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (hf : Function.Surjective f) :
Function.Surjective ⇑(rename f)
source
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

Instances For

source
theorem MvPolynomial.killCompl_C {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {f : σ → τ} (hf : Function.Injective f) (r : R) :
(killCompl hf) (C r) = C r
source
theorem MvPolynomial.killCompl_comp_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {f : σ → τ} (hf : Function.Injective f) :
(killCompl hf).comp (rename f) = AlgHom.id R (MvPolynomial σ R)
source
@[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) :
(killCompl hf) ((rename f) p) = p
source
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' := ⋯ }

Instances For

source
@[simp]
theorem MvPolynomial.renameEquiv_apply {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [CommSemiring R] (f : σ ≃ τ) (a : MvPolynomial σ R) :
(renameEquiv R f) a = (rename ⇑f) a
source
@[simp]
theorem MvPolynomial.renameEquiv_refl {σ : Type u_1} (R : Type u_4) [CommSemiring R] :
renameEquiv R (Equiv.refl σ) = AlgEquiv.refl
source
@[simp]
theorem MvPolynomial.renameEquiv_symm {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [CommSemiring R] (f : σ ≃ τ) :
(renameEquiv R f).symm = renameEquiv R f.symm
source
@[simp]
theorem MvPolynomial.renameEquiv_trans {σ : Type u_1} {τ : Type u_2} {α : Type u_3} (R : Type u_4) [CommSemiring R] (e : σ ≃ τ) (f : τ ≃ α) :
(renameEquiv R e).trans (renameEquiv R f) = renameEquiv R (e.trans f)
source
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) :
eval₂ f g ((rename k) p) = eval₂ f (g ∘ k) p
source
theorem MvPolynomial.eval_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (k : σ → τ) (g : τ → R) (p : MvPolynomial σ R) :
(eval g) ((rename k) p) = (eval (g ∘ k)) p
source
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) :
(eval₂Hom f g) ((rename k) p) = (eval₂Hom f (g ∘ k)) p
source
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] :
(aeval g) ((rename k) p) = (aeval (g ∘ k)) p
source
theorem MvPolynomial.aeval_comp_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] (k : σ → τ) (g : τ → S) [Algebra R S] :
(aeval g).comp (rename k) = aeval (g ∘ k)
source
theorem MvPolynomial.rename_eval₂ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (k : σ → τ) (p : MvPolynomial σ R) (g : τ → MvPolynomial σ R) :
(rename k) (eval₂ C (g ∘ k) p) = eval₂ C (⇑(rename k) ∘ g) ((rename k) p)
source
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) :
(rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun (x : σ) => (rename (Prod.mk j)) (g x)) p
source
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) :
eval₂ f g ((rename (Prod.mk i)) p) = eval₂ f (fun (j : τ) => g (i, j)) p
source
theorem MvPolynomial.eval_rename_prod_mk {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (g : σ × τ → R) (i : σ) (p : MvPolynomial τ R) :
(eval g) ((rename (Prod.mk i)) p) = (eval fun (j : τ) => g (i, j)) p
source
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 = (rename Subtype.val) q

Every polynomial is a polynomial in finitely many variables.

source
theorem MvPolynomial.exists_finset_rename₂ {σ : Type u_1} {R : Type u_4} [CommSemiring R] (p₁ p₂ : MvPolynomial σ R) :
∃ (s : Finset σ) (q₁ : MvPolynomial (↥s) R) (q₂ : MvPolynomial (↥s) R), p₁ = (rename Subtype.val) q₁ ∧ p₂ = (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.

source
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 = (rename f) q

Every polynomial is a polynomial in finitely many variables.

source
theorem MvPolynomial.eval₂_cast_comp {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (c : ℤ →+* R) (g : τ → R) (p : MvPolynomial σ ℤ) :
eval₂ c (g ∘ f) p = eval₂ c g ((rename f) p)
source
@[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 : σ →₀ ℕ) :
coeff (Finsupp.mapDomain f d) ((rename f) φ) = coeff d φ
source
@[simp]
theorem MvPolynomial.coeff_rename_embDomain {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ ↪ τ) (φ : MvPolynomial σ R) (d : σ →₀ ℕ) :
coeff (Finsupp.embDomain f d) ((rename ⇑f) φ) = coeff d φ
source
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 → coeff u φ = 0) :
coeff d ((rename f) φ) = 0
source
theorem MvPolynomial.coeff_rename_ne_zero {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ) (h : coeff d ((rename f) φ) ≠ 0) :
∃ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d ∧ coeff u φ ≠ 0
source
@[simp]
theorem MvPolynomial.constantCoeff_rename {σ : Type u_1} {R : Type u_4} [CommSemiring R] {τ : Type u_6} (f : σ → τ) (φ : MvPolynomial σ R) :
constantCoeff ((rename f) φ) = constantCoeff φ
source
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) :
((rename f) p).support = Finset.image (Finsupp.mapDomain f) p.support