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:
-
σ τ α : 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 inMvPolynomial σ Rwhich mathematicians might callX^s -
r : Relements of the coefficient ring -
i : σ, with corresponding monomialX i, often denotedX_iby 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)
Instances For
@[simp]
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)
:
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 { val := i, property := h }) else 0
Instances For
theorem
MvPolynomial.killCompl_comp_rename
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[CommSemiring R]
{f : σ → τ}
(hf : Function.Injective f)
:
AlgHom.comp (MvPolynomial.killCompl hf) (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
- One or more equations did not get rendered due to their size.
Instances For
@[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 : σ ≃ τ)
:
AlgEquiv.symm (MvPolynomial.renameEquiv R f) = 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 : τ ≃ α)
:
AlgEquiv.trans (MvPolynomial.renameEquiv R e) (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)
: