Lazard valuations at points over a base point

Let f be a polynomial in the variables X₀, …, Xₙ over a commutative ring R, and single out the last variable Xₙ, which is the least significant one for the lexicographic order. Moving it into the coefficients (MvPolynomial.optionEquivRight after renaming along finSuccEquivLast) turns f into a polynomial g in the base variables X₀, …, Xₙ₋₁ with coefficients in R[Xₙ]. For a base point α ∈ Rⁿ, Lazard evaluation of g at the constant polynomials C αᵢ divides out the base variables and leaves a univariate polynomial q = g.lazardEval (C ∘ α), the Lazard evaluation of f over α, which is nonzero when f ≠ 0; it records the removed base exponents u = g.lazardExponent (C ∘ α).

This file describes the Lazard invariants of f at a point (α, β) above α. The vector of exponents removed by Lazard evaluation of f, and for f ≠ 0 its Lazard valuation, is u with the root multiplicity of β in q appended as last entry (MvPolynomial.lazardExponent_snoc, MvPolynomial.lazardValuation_snoc). The Lazard evaluation of f at (α, β) is obtained from q by one more step of division: it is the trailing coefficient of the Taylor expansion of q at β (MvPolynomial.lazardEval_snoc); for f ≠ 0 this is its lowest nonzero coefficient, and for f = 0 both sides are 0.

So, for f ≠ 0, at the points of a root section β = θ(α) of the Lazard evaluations q, the Lazard valuation of f is the removed base exponent vector followed by the multiplicity of the root, and in a sector between root sections it is the removed base exponent vector followed by 0. Constancy of the removed base exponents and of the root multiplicities over a base set thus makes the Lazard valuation of a nonzero f constant on each section and sector above it. This is how Lazard's lifting theorem passes valuation-invariance from the base to the cylinder.

Main results

• MvPolynomial.lazardExponent_snoc, MvPolynomial.lazardValuation_snoc: at (α, β) the removed exponents of f, and for f ≠ 0 its Lazard valuation, are the removed exponents of g at α, followed by the root multiplicity of β in the Lazard evaluation of g at α.
• MvPolynomial.lazardEval_snoc: the Lazard evaluation of f at (α, β) is the trailing coefficient of the Taylor expansion at β of the Lazard evaluation of g at α.
• MvPolynomial.lazardEval_optionEquivRight_rename_finSuccEquivLast_eq_map, MvPolynomial.lazardEval_optionEquivRight_rename_finSuccEquivLast_eq_map_iff: the Lazard evaluation over α is the ordinary fibre of f over α exactly when that fibre is nonzero or f = 0.
• MvPolynomial.coeff_lazardEval_optionEquivRight_rename_finSuccEquivLast: the coefficients of the Lazard evaluation of g at α are Taylor coefficients of f at (α, 0).
• MvPolynomial.lazardValuation_map_constantCoeff_eq_iff: 0 is not a root of the Lazard evaluation of g at α exactly when the constant coefficients of g have Lazard valuation at α equal to the removed base exponents.

References

• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), 52–69, Section 2.

theorem MvPolynomial.lazardEval_optionEquivRight_rename_finSuccEquivLast_eq_zero_iff {R : Type u_1} [CommRing R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} (α : Fin n → R) : ((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).lazardEval (⇑Polynomial.C ∘ α) = 0 ↔ f = 0

The Lazard evaluation of f over a base point α, after moving the last variable into the coefficients, vanishes exactly when f does.

theorem MvPolynomial.lazardEval_optionEquivRight_rename_finSuccEquivLast_eq_map {R : Type u_1} [CommRing R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {α : Fin n → R} (h : Polynomial.map (eval α) ((optionEquivLeft R (Fin n)) ((rename ⇑finSuccEquivLast) f)) ≠ 0) : ((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).lazardEval (⇑Polynomial.C ∘ α) = Polynomial.map (eval α) ((optionEquivLeft R (Fin n)) ((rename ⇑finSuccEquivLast) f))

Agreement with ordinary specialization over a base point. Where the ordinary fibre of f over α, the univariate polynomial t ↦ f (Fin.snoc α t), is nonzero, the Lazard evaluation of f over α is that fibre.

theorem MvPolynomial.lazardEval_optionEquivRight_rename_finSuccEquivLast_eq_map_iff {R : Type u_1} [CommRing R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {α : Fin n → R} : ((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).lazardEval (⇑Polynomial.C ∘ α) = Polynomial.map (eval α) ((optionEquivLeft R (Fin n)) ((rename ⇑finSuccEquivLast) f)) ↔ Polynomial.map (eval α) ((optionEquivLeft R (Fin n)) ((rename ⇑finSuccEquivLast) f)) ≠ 0 ∨ f = 0

The Lazard evaluation of f over a base point α is the ordinary fibre of f over α exactly when that fibre is nonzero or f is zero. A nonzero f whose fibre over α vanishes identically has a nonzero Lazard evaluation there.

theorem MvPolynomial.lazardEval_optionEquivRight_rename_finSuccEquivLast_eq_map_of_nullified {R : Type u_1} [CommRing R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {α : Fin n → R} (hnull : Polynomial.map (eval α) ((optionEquivLeft R (Fin n)) ((rename ⇑finSuccEquivLast) f)) = 0 → f = 0) : ((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).lazardEval (⇑Polynomial.C ∘ α) = Polynomial.map (eval α) ((optionEquivLeft R (Fin n)) ((rename ⇑finSuccEquivLast) f))

If the ordinary fibre of f over α vanishes only when f is zero, then the Lazard evaluation of f over α agrees with that fibre.

theorem MvPolynomial.lazardExponent_snoc {R : Type u_1} [CommRing R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) (α : Fin n → R) (β : R) : f.lazardExponent (Fin.snoc α β) = (((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).lazardExponent (⇑Polynomial.C ∘ α)).snoc (Polynomial.rootMultiplicity β (((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).lazardEval (⇑Polynomial.C ∘ α)))

Lazard evaluation at a point over a base point. The exponents removed by Lazard evaluation of f at Fin.snoc α β are those removed over the base point α, after moving the last variable into the coefficients, followed by the multiplicity of β as a root of the resulting Lazard evaluation over α.

theorem MvPolynomial.lazardValuation_snoc {R : Type u_1} [CommRing R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} (hf : f ≠ 0) (α : Fin n → R) (β : R) : f.lazardValuation (Fin.snoc α β) = ↑(toLex ((((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).lazardExponent (⇑Polynomial.C ∘ α)).snoc (Polynomial.rootMultiplicity β (((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).lazardEval (⇑Polynomial.C ∘ α)))))

The Lazard valuation at a point over a base point. For f ≠ 0, the Lazard valuation of f at Fin.snoc α β is the vector of base exponents removed by Lazard evaluation over α, after moving the last variable into the coefficients, with the multiplicity of β as a root of the resulting Lazard evaluation over α appended. In particular it is the removed base exponents followed by 0 when β is not a root.

theorem MvPolynomial.lazardEval_snoc {R : Type u_1} [CommRing R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) (α : Fin n → R) (β : R) : f.lazardEval (Fin.snoc α β) = ((Polynomial.taylor β) (((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).lazardEval (⇑Polynomial.C ∘ α))).trailingCoeff

The Lazard evaluation of f at Fin.snoc α β is the trailing coefficient of the Taylor expansion at β of the Lazard evaluation over the base point α, after moving the last variable into the coefficients. By Polynomial.trailingCoeff_taylor, this is one more step of Lazard's successive division: divide by the largest power of Xₙ - β and evaluate at β.

theorem MvPolynomial.coeff_lazardEval_optionEquivRight_rename_finSuccEquivLast {R : Type u_1} [CommRing R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) (α : Fin n → R) (k : ℕ) : (((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).lazardEval (⇑Polynomial.C ∘ α)).coeff k = ((taylor (Fin.snoc α 0)) f).coeff ((((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).lazardExponent (⇑Polynomial.C ∘ α)).snoc k)

The coefficient of Xₙ ^ k in the Lazard evaluation of f over the base point α, after moving the last variable into the coefficients, is the Taylor coefficient of f at Fin.snoc α 0 whose exponent is the vector of base exponents removed over α followed by k. So over a set of base points where the removed exponents are constant, the coefficients of the Lazard evaluations are polynomial functions of the base point.

theorem MvPolynomial.exists_polynomial_map_eq_lazardEval {R : Type u_1} [CommRing R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) (e : Fin n →₀ ℕ) : ∃ (P : Polynomial (MvPolynomial (Fin n) R)), ∀ (α : Fin n → R), ((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).lazardExponent (⇑Polynomial.C ∘ α) = e → Polynomial.map (eval α) P = ((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).lazardEval (⇑Polynomial.C ∘ α)

On a stratum with fixed removed base exponents, Lazard evaluation in the last variable is specialization of a single polynomial family. Its coefficients are polynomial in the base point, including where the ordinary fiber is nullified. The coefficient ring need not be a domain.

theorem MvPolynomial.coeff_taylor_map_constantCoeff {R : Type u_1} [CommRing R] {n : ℕ} (g : MvPolynomial (Fin n) (Polynomial R)) (α : Fin n → R) (d : Fin n →₀ ℕ) : ((taylor α) ((map Polynomial.constantCoeff) g)).coeff d = (((taylor (⇑Polynomial.C ∘ α)) g).coeff d).coeff 0

The Taylor coefficients of the constant coefficients of g, taken coefficientwise, are the constant coefficients of the Taylor coefficients of g at the corresponding constant polynomials.

theorem MvPolynomial.lazardValuation_map_constantCoeff_eq_iff {R : Type u_1} [CommRing R] {n : ℕ} (g : MvPolynomial (Fin n) (Polynomial R)) (α : Fin n → R) : ((map Polynomial.constantCoeff) g).lazardValuation α = ↑(toLex (g.lazardExponent (⇑Polynomial.C ∘ α))) ↔ ¬(g.lazardEval (⇑Polynomial.C ∘ α)).IsRoot 0

The root 0 of a Lazard evaluation. Let g be a polynomial in the base variables with univariate polynomial coefficients. Its Lazard evaluation over α does not vanish at 0 exactly when the Lazard valuation at α of the polynomial of constant coefficients of g is the vector of base exponents removed by that evaluation. Otherwise this valuation is lexicographically larger.