Ambient order of discriminants of polynomial products

For a finite family of positive-degree polynomials with multivariate coefficients, the ambient order of the discriminant of their product is determined by the orders of the individual discriminants and pairwise resultants. Thus constancy of those projection data implies constancy of the product discriminant's order, even when they vanish on the base set. No condition is placed on the specialized degrees or leading coefficients.

This is the algebraic reduction from a family of polynomial root sections to the roots of its product. It specializes Finset.map_discr_prod_eq using the multiplicativity of MvPolynomial.orderAt.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), Section 2.

theorem Finset.orderAt_discr_prod_eq {σ : Type u_1} {R : Type u_2} {ι : Type u_3} [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.orderAt a = (f i).discr.orderAt b) (hres : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → ((f i).resultant (f j)).orderAt a = ((f i).resultant (f j)).orderAt b) : (∏ i ∈ s, f i).discr.orderAt a = (∏ i ∈ s, f i).discr.orderAt b

If individual discriminants and pairwise resultants have the same ambient orders 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.