Lazard valuations of discriminants of polynomial products

For a finite family of positive-degree polynomials with multivariate coefficients, constancy of the Lazard valuations of the individual discriminants and pairwise resultants implies constancy of the valuation of the product discriminant. Neither the factors nor the projection polynomials need have nonzero values at the base points. This algebraic reduction supplies the discriminant condition when applying a single-polynomial Lazard lifting theorem to a product.

As with ambient order, the proof specializes Finset.map_discr_prod_eq using the multiplicativity of MvPolynomial.lazardValuation.

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 5.

theorem Finset.lazardValuation_discr_prod_eq {σ : Type u_1} {R : Type u_2} {ι : Type u_3} [LinearOrder σ] [WellFoundedGT σ] [CommRing R] [IsDomain R] (s : Finset ι) (f : ι → Polynomial (MvPolynomial σ R)) (hdeg : ∀ i ∈ s, 0 < (f i).natDegree) (a b : σ → R) (hdiscr : ∀ i ∈ s, (f i).discr.lazardValuation a = (f i).discr.lazardValuation b) (hres : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → ((f i).resultant (f j)).lazardValuation a = ((f i).resultant (f j)).lazardValuation b) : (∏ i ∈ s, f i).discr.lazardValuation a = (∏ i ∈ s, f i).discr.lazardValuation b

If individual discriminants and pairwise resultants have the same Lazard valuations at a and b, so does the discriminant of the product. The factors need not be monic and may specialize to zero at either point. Empty products are included.