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^sr : Relements of the coefficient ringi : σ, with corresponding monomialX i, often denotedX_iby mathematiciansp : MvPolynomial σ α
Rename all the variables in a multivariable polynomial.
Equations
theorem
MvPolynomial.rename_C
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[CommSemiring R]
(f : σ → τ)
(r : 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_apply
{σ : 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)
:
Function.Injective ⇑(rename f)
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)
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)
theorem
MvPolynomial.rename_surjective
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[CommSemiring R]
(f : σ → τ)
(hf : Function.Surjective 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
- 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)
:
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)
:
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
- 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_apply
{σ : Type u_1}
{τ : Type u_2}
(R : Type u_4)
[CommSemiring R]
(f : σ ≃ τ)
(a : MvPolynomial σ R)
:
@[simp]
@[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.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]
:
theorem
MvPolynomial.rename_eval₂
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_4}
[CommSemiring R]
(k : σ → τ)
(p : MvPolynomial σ R)
(g : τ → MvPolynomial σ R)
:
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)
:
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)
:
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.
theorem
MvPolynomial.exists_finset_rename₂
{σ : Type u_1}
{R : Type u_4}
[CommSemiring R]
(p₁ p₂ : MvPolynomial σ R)
:
∃ (s : Finset σ) (q₁ : MvPolynomial { x : σ // x ∈ s } R) (q₂ : MvPolynomial { x : σ // x ∈ 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.
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.
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 = d → 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 : coeff d ((rename f) φ) ≠ 0)
:
@[simp]
theorem
MvPolynomial.constantCoeff_rename
{σ : Type u_1}
{R : Type u_4}
[CommSemiring R]
{τ : Type u_6}
(f : σ → τ)
(φ : MvPolynomial σ R)
:
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)
: