Documentation

Mathlib.Algebra.MvPolynomial.Rename

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:

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

Rename all the variables in a multivariable polynomial.

Equations
Instances For
    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 : σ) :
    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) :
    @[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) :
    @[simp]
    theorem MvPolynomial.rename_id {σ : Type u_1} {R : Type u_4} [CommSemiring R] (p : MvPolynomial σ R) :
    theorem MvPolynomial.rename_monomial {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : στ) (d : σ →₀ ) (r : R) :
    theorem MvPolynomial.rename_eq {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : στ) (p : MvPolynomial σ R) :
    theorem MvPolynomial.rename_injective {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : στ) (hf : Function.Injective f) :
    def MvPolynomial.killCompl {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {f : στ} (hf : Function.Injective f) :

    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
    Instances For
      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) :
      @[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) :
      @[simp]
      theorem MvPolynomial.renameEquiv_apply {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [CommSemiring R] (f : σ τ) (a : MvPolynomial σ R) :
      def MvPolynomial.renameEquiv {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [CommSemiring R] (f : σ τ) :

      MvPolynomial.rename e is an equivalence when e is.

      Equations
      Instances For
        @[simp]
        theorem MvPolynomial.renameEquiv_refl {σ : Type u_1} (R : Type u_4) [CommSemiring R] :
        @[simp]
        theorem MvPolynomial.renameEquiv_symm {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [CommSemiring R] (f : σ τ) :
        @[simp]
        theorem MvPolynomial.renameEquiv_trans {σ : Type u_1} {τ : Type u_2} {α : Type u_3} (R : Type u_4) [CommSemiring R] (e : σ τ) (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) :
        theorem MvPolynomial.eval_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (k : στ) (g : τR) (p : MvPolynomial σ R) :
        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) :
        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] :
        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 σ ) :
        @[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 : σ →₀ ) :
        @[simp]
        theorem MvPolynomial.coeff_rename_embDomain {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ τ) (φ : MvPolynomial σ R) (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 = dMvPolynomial.coeff u φ = 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) :
        @[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