Transport of Lazard evaluation

An injective coefficient map preserves the first nonzero Taylor coefficient, hence both the removed exponents and Lazard evaluation. In particular, mapping coefficients to constant univariate polynomials lets a content factor be Lazard-evaluated in the base variables while the distinguished variable is retained.

A Taylor shift translates the point at which both invariants are computed. Renaming the variables along a strictly monotone map of indices relabels the removed exponents and keeps the Lazard evaluation: the variables are eliminated in the same relative order, and the new variables do not occur.

theorem MvPolynomial.lazardExponent_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : ℕ} (φ : R →+* S) (hφ : Function.Injective ⇑φ) (p : MvPolynomial (Fin n) R) (a : Fin n → R) : ((map φ) p).lazardExponent (⇑φ ∘ a) = p.lazardExponent a

An injective coefficient map preserves the exponents removed by Lazard evaluation. Injectivity prevents a surviving Taylor coefficient from disappearing.

theorem MvPolynomial.lazardEval_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : ℕ} (φ : R →+* S) (hφ : Function.Injective ⇑φ) (p : MvPolynomial (Fin n) R) (a : Fin n → R) : ((map φ) p).lazardEval (⇑φ ∘ a) = φ (p.lazardEval a)

Lazard evaluation commutes with an injective coefficient map, including for zero inputs.

@[simp]

theorem MvPolynomial.lazardExponent_taylor {R : Type u_1} [CommRing R] {n : ℕ} (p : MvPolynomial (Fin n) R) (a b : Fin n → R) : ((taylor a) p).lazardExponent b = p.lazardExponent (b + a)

A Taylor shift translates the point at which Lazard evaluation removes its exponents.

@[simp]

theorem MvPolynomial.lazardEval_taylor {R : Type u_1} [CommRing R] {n : ℕ} (p : MvPolynomial (Fin n) R) (a b : Fin n → R) : ((taylor a) p).lazardEval b = p.lazardEval (b + a)

The Lazard evaluation of a Taylor shift is the Lazard evaluation at the translated point.

theorem MvPolynomial.lazardExponent_rename {R : Type u_1} [CommRing R] {n m : ℕ} {f : Fin n → Fin m} (hf : StrictMono f) (p : MvPolynomial (Fin n) R) (b : Fin m → R) : ((rename f) p).lazardExponent b = Finsupp.mapDomain f (p.lazardExponent (b ∘ f))

Renaming the variables along a strictly monotone map relabels the exponents removed by Lazard evaluation.

theorem MvPolynomial.lazardEval_rename {R : Type u_1} [CommRing R] {n m : ℕ} {f : Fin n → Fin m} (hf : StrictMono f) (p : MvPolynomial (Fin n) R) (b : Fin m → R) : ((rename f) p).lazardEval b = p.lazardEval (b ∘ f)

Renaming the variables along a strictly monotone map does not change the Lazard evaluation, at the pulled back point.