Translation of multivariate polynomials by a point: originShift a substitutes X j + a j for every variable, moving the point a to the origin. originShiftEquiv a is the same substitution as an algebra automorphism, with inverse the shift by -a.

noncomputable def CCDN.originShift {R : Type u_1} {σ : Type u_2} [CommRing R] (a : σ → R) : MvPolynomial σ R →+* MvPolynomial σ R

The substitution X j ↦ X j + a j, which moves the point a to the origin.

Equations

• CCDN.originShift a = MvPolynomial.eval₂Hom MvPolynomial.C fun (j : σ) => MvPolynomial.X j + MvPolynomial.C (a j)

@[simp]

theorem CCDN.originShift_C {R : Type u_1} {σ : Type u_2} [CommRing R] (a : σ → R) (c : R) : (originShift a) (MvPolynomial.C c) = MvPolynomial.C c

The origin shift fixes constant polynomials.

@[simp]

theorem CCDN.originShift_X {R : Type u_1} {σ : Type u_2} [CommRing R] (a : σ → R) (j : σ) : (originShift a) (MvPolynomial.X j) = MvPolynomial.X j + MvPolynomial.C (a j)

The origin shift by a sends the variable X j to X j + a j.

noncomputable def CCDN.originShiftEquiv {R : Type u_1} {σ : Type u_2} [CommRing R] (a : σ → R) : MvPolynomial σ R ≃ₐ[R] MvPolynomial σ R

The substitution X j ↦ X j + a j as an algebra automorphism, with inverse the substitution X j ↦ X j - a j.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CCDN.originShiftEquiv_apply {R : Type u_1} {σ : Type u_2} [CommRing R] (a : σ → R) (f : MvPolynomial σ R) : (originShiftEquiv a) f = (originShift a) f

The automorphism originShiftEquiv a acts as the origin shift originShift a.

@[simp]

theorem CCDN.originShiftEquiv_symm_apply {R : Type u_1} {σ : Type u_2} [CommRing R] (a : σ → R) (f : MvPolynomial σ R) : (originShiftEquiv a).symm f = (originShift (-a)) f

The inverse of originShiftEquiv a acts as the origin shift by -a.

theorem CCDN.originShift_injective {R : Type u_1} {σ : Type u_2} [CommRing R] (a : σ → R) : Function.Injective ⇑(originShift a)

The origin shift is injective.

theorem CCDN.originShift_ne_zero {R : Type u_1} {σ : Type u_2} [CommRing R] (a : σ → R) {f : MvPolynomial σ R} (hf : f ≠ 0) : (originShift a) f ≠ 0

The origin shift of a nonzero polynomial is nonzero.

theorem CCDN.originShift_map {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommRing R] [CommRing S] (φ : R →+* S) (a : σ → R) (f : MvPolynomial σ R) : (MvPolynomial.map φ) ((originShift a) f) = (originShift fun (j : σ) => φ (a j)) ((MvPolynomial.map φ) f)

The origin shift commutes with coefficient maps: mapping the coefficients of the shift of f by a along φ gives the shift of the mapped polynomial by the mapped point φ ∘ a.

theorem CCDN.eval_sub_originShift {R : Type u_1} {σ : Type u_2} [CommRing R] (a x : σ → R) (f : MvPolynomial σ R) : (MvPolynomial.eval fun (j : σ) => x j - a j) ((originShift a) f) = (MvPolynomial.eval x) f

Evaluating the origin shift of f by a at x - a gives the value of f at x.

theorem CCDN.eval_zero_originShift {R : Type u_1} {σ : Type u_2} [CommRing R] (a : σ → R) (f : MvPolynomial σ R) : (MvPolynomial.eval 0) ((originShift a) f) = (MvPolynomial.eval a) f

The origin shift of f by a takes at the origin the value of f at a.

theorem CCDN.pderiv_originShift {R : Type u_1} {σ : Type u_2} [CommRing R] (a : σ → R) (f : MvPolynomial σ R) (j : σ) : (MvPolynomial.pderiv j) ((originShift a) f) = (originShift a) ((MvPolynomial.pderiv j) f)

The origin shift commutes with partial derivatives.