mathlib3 documentation

data.mv_polynomial.rename

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:

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

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 : σ) :
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) :
@[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) :
@[simp]
theorem mv_polynomial.rename_id {σ : Type u_1} {R : Type u_4} [comm_semiring R] (p : mv_polynomial σ R) :
theorem mv_polynomial.rename_monomial {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : σ τ) (d : σ →₀ ) (r : R) :
theorem mv_polynomial.rename_eq {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : σ τ) (p : mv_polynomial σ R) :
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) :

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
@[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) :
@[simp]
theorem mv_polynomial.rename_equiv_apply {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [comm_semiring R] (f : σ τ) (ᾰ : mv_polynomial σ R) :
noncomputable def mv_polynomial.rename_equiv {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [comm_semiring R] (f : σ τ) :

mv_polynomial.rename e is an equivalence when e is.

Equations
@[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 : τ α) :
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) :
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) :
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] :
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) :
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) :
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 σ ) :
@[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 : σ →₀ ) :
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) :
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) :