Roots of Lazard evaluations from an irreducible basis

Move the distinguished polynomial variable into the coefficient ring using MvPolynomial.optionEquivLeft and MvPolynomial.optionEquivRight. Multiplicative Lazard evaluation preserves the factorization into irreducible basis members, including where ordinary specialization is nullified. Since every member of an irreducible basis divides a nonzero input, the roots of the Lazard evaluations of the nonzero inputs are exactly the roots of the Lazard evaluations of the basis members. So a complete stack for the basis is a complete stack for the input family, and every one of its sections is used by an input.

The transfer of root multiplicities, which needs only a squarefree basis, is Finset.IsSquarefreeBasis.rootMultiplicity_lazardEval_eq.

References

S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), Sections 2 and 5. The multiplicity reconstruction is Finset.IsSquarefreeBasis.exists_rootMultiplicity_lazardEval_eq_sum; the multiplicative evaluation is MvPolynomial.lazardEvalHom.

theorem Finset.IsIrreducibleBasis.exists_isRoot_lazardEval_iff {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} {F B : Finset (Polynomial (MvPolynomial (Fin n) R))} (hB : F.IsIrreducibleBasis B) (a : Fin n → R) (t : R) : (∃ f ∈ F, f ≠ 0 ∧ ((((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) f).lazardEval (⇑Polynomial.C ∘ a)).IsRoot t) ↔ ∃ b ∈ B, ((((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) b).lazardEval (⇑Polynomial.C ∘ a)).IsRoot t

The union of the roots in R of the nonzero inputs' Lazard evaluations is exactly the roots of the basis evaluations. Thus a complete basis stack also covers the input family, and every basis section is used by an input.