Constant Lazard valuation passes to polynomial factors

The lexicographically first nonzero Taylor coefficient stays nonzero near its center. Thus Lazard valuation is locally bounded above by its value at the center. Additivity then implies that a divisor of a nonzero polynomial has locally constant valuation wherever the polynomial does. Over a preconnected parameter set, the divisor's valuation is constant.

The parametrization may be a continuous root section. This allows a common stack for a product to supply constant valuations for its individual factors, including where ordinary fibers are nullified. Nonzeroness of the product is essential: a zero product supplies no information.

References

• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), Propositions 3.2 and 3.4.

The argument follows the ambient-order factor argument in MvPolynomial.eventually_orderAt_eq_of_dvd, with the lexicographic valuation in place of total Taylor order.

theorem MvPolynomial.eventually_lazardValuation_le {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] [T1Space R] (p : MvPolynomial σ R) (a : σ → R) : ∀ᶠ (b : σ → R) in nhds a, p.lazardValuation b ≤ p.lazardValuation a

Near a center, a polynomial's Lazard valuation is at most its valuation at that center. This also includes the zero polynomial, whose valuation is infinite.

theorem MvPolynomial.eventually_lazardValuation_eq_of_dvd {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommRing R] [TopologicalSpace R] [IsTopologicalSemiring R] [NoZeroDivisors R] [T1Space R] {Y : Type u_3} {l : Filter Y} {f : Y → σ → R} {a : σ → R} (p : MvPolynomial σ R) {q : MvPolynomial σ R} (hq : q ≠ 0) (hpq : p ∣ q) (hf : Filter.Tendsto f l (nhds a)) (hval : ∀ᶠ (y : Y) in l, q.lazardValuation (f y) = q.lazardValuation a) : ∀ᶠ (y : Y) in l, p.lazardValuation (f y) = p.lazardValuation a

Along a parametrization tending to a center, a divisor of a nonzero polynomial has eventually constant Lazard valuation if the polynomial does.

theorem MvPolynomial.lazardValuation_eq_of_dvd {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommRing R] [TopologicalSpace R] [IsTopologicalSemiring R] [NoZeroDivisors R] [T1Space R] {Y : Type u_3} {f : Y → σ → R} (p : MvPolynomial σ R) {q : MvPolynomial σ R} (hq : q ≠ 0) (hpq : p ∣ q) [TopologicalSpace Y] {S : Set Y} (hS : IsPreconnected S) (hf : ContinuousOn f S) (hval : ∀ x ∈ S, ∀ y ∈ S, q.lazardValuation (f x) = q.lazardValuation (f y)) {x y : Y} (hx : x ∈ S) (hy : y ∈ S) : p.lazardValuation (f x) = p.lazardValuation (f y)

A divisor of a nonzero polynomial has constant Lazard valuation along a continuous parametrization of a preconnected set whenever the polynomial does.