Rescaling the variables of a multivariate polynomial

For a : σ → R, MvPolynomial.rescale a is the R-algebra endomorphism of MvPolynomial σ R sending each variable X i to a i * X i. It multiplies the coefficient of the monomial X^n by ∏ i, a i ^ n i, so supports can only shrink, and it is the polynomial counterpart of Mathlib's MvPowerSeries.rescale. When every a i is a unit, rescaling by a is an algebra automorphism with inverse the rescaling by the inverses, MvPolynomial.rescaleEquiv; then contracting an ideal along rescale a is the same as extending it along the inverse rescaling.

Such diagonal changes of variables relate algebra maps X i ↦ f i and X i ↦ a i * f i (MvPolynomial.aeval_rescale), for instance a presentation of a subalgebra by generators to the presentation by rescaled generators.

Main declarations

• MvPolynomial.rescale: the endomorphism X i ↦ a i * X i.
• MvPolynomial.coeff_rescale: the coefficient of X^n is multiplied by ∏ i, a i ^ n i.
• MvPolynomial.aeval_rescale: evaluating a rescaled polynomial at x is evaluating it at a i • x i.
• MvPolynomial.rescale_mul: rescalings compose multiplicatively.
• MvPolynomial.rescaleEquiv: for units u, rescaling by u as an algebra automorphism, with inverse MvPolynomial.rescaleEquiv u⁻¹.
• MvPolynomial.comap_rescale: contraction along the rescaling by a is extension along the rescaling by an inverse family b.

noncomputable def MvPolynomial.rescale {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ → R) : MvPolynomial σ R →ₐ[R] MvPolynomial σ R

The R-algebra endomorphism of MvPolynomial σ R rescaling the variables, X i ↦ a i * X i. It sends p(X) to p(a X).

theorem MvPolynomial.rescale_eq_aeval {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ → R) : rescale a = aeval fun (i : σ) => C (a i) * X i

@[simp]

theorem MvPolynomial.rescale_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ → R) (i : σ) : (rescale a) (X i) = C (a i) * X i

theorem MvPolynomial.aeval_rescale {σ : Type u_1} {R : Type u_2} [CommSemiring R] {S : Type u_3} [CommSemiring S] [Algebra R S] (a : σ → R) (x : σ → S) (p : MvPolynomial σ R) : (aeval x) ((rescale a) p) = (aeval fun (i : σ) => a i • x i) p

Evaluating a rescaled polynomial at x is evaluating the polynomial at a i • x i.

@[simp]

theorem MvPolynomial.rescale_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ → R) (n : σ →₀ ℕ) (r : R) : (rescale a) ((monomial n) r) = (monomial n) ((n.prod fun (i : σ) (k : ℕ) => a i ^ k) * r)

Rescaling the monomial r X^n multiplies its coefficient by ∏ i, a i ^ n i.

@[simp]

theorem MvPolynomial.coeff_rescale {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ → R) (p : MvPolynomial σ R) (n : σ →₀ ℕ) : ((rescale a) p).coeff n = (n.prod fun (i : σ) (k : ℕ) => a i ^ k) * p.coeff n

Rescaling multiplies the coefficient of X^n by ∏ i, a i ^ n i.

theorem MvPolynomial.support_rescale_subset {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ → R) (p : MvPolynomial σ R) : ((rescale a) p).support ⊆ p.support

@[simp]

theorem MvPolynomial.rescale_one {σ : Type u_1} {R : Type u_2} [CommSemiring R] : rescale 1 = AlgHom.id R (MvPolynomial σ R)

theorem MvPolynomial.rescale_rescale {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a b : σ → R) (p : MvPolynomial σ R) : (rescale b) ((rescale a) p) = (rescale (a * b)) p

theorem MvPolynomial.rescale_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a b : σ → R) : rescale (a * b) = (rescale b).comp (rescale a)

theorem MvPolynomial.rescale_rescale_of_mul_eq_one {σ : Type u_1} {R : Type u_2} [CommSemiring R] {a b : σ → R} (h : ∀ (i : σ), a i * b i = 1) (p : MvPolynomial σ R) : (rescale b) ((rescale a) p) = p

Rescaling by a and then by b is the identity when a i * b i = 1 for every i.

noncomputable def MvPolynomial.rescaleEquiv {σ : Type u_1} {R : Type u_2} [CommSemiring R] (u : σ → Rˣ) : MvPolynomial σ R ≃ₐ[R] MvPolynomial σ R

Rescaling by a family of units is an algebra automorphism, whose inverse rescales by the inverse units.

@[simp]

theorem MvPolynomial.rescaleEquiv_apply {σ : Type u_1} {R : Type u_2} [CommSemiring R] (u : σ → Rˣ) (p : MvPolynomial σ R) : (rescaleEquiv u) p = (rescale fun (i : σ) => ↑(u i)) p

@[simp]

theorem MvPolynomial.toAlgHom_rescaleEquiv {σ : Type u_1} {R : Type u_2} [CommSemiring R] (u : σ → Rˣ) : ↑(rescaleEquiv u) = rescale fun (i : σ) => ↑(u i)

@[simp]

theorem MvPolynomial.rescaleEquiv_symm {σ : Type u_1} {R : Type u_2} [CommSemiring R] (u : σ → Rˣ) : (rescaleEquiv u).symm = rescaleEquiv u⁻¹

theorem MvPolynomial.comap_rescale {σ : Type u_1} {R : Type u_2} [CommSemiring R] {a b : σ → R} (h : ∀ (i : σ), a i * b i = 1) (I : Ideal (MvPolynomial σ R)) : Ideal.comap (rescale a) I = Ideal.map (rescale b) I

If a i * b i = 1 for every i, then the contraction of an ideal along the rescaling by a is its extension along the rescaling by b.