Lazard content and multiplicity reconstruction from squarefree bases

Moving the distinguished polynomial variable into the coefficient ring preserves the squarefree-basis reconstruction under multiplicative Lazard evaluation. The scalar factor contains the evaluated content and a unit, and the removed base exponents are the content exponents plus a weighted sum of the basis exponents. The weights do not depend on the base point, so invariant content and basis exponents give invariant input exponents.

Likewise the root multiplicities of a nonzero input's Lazard evaluation are weighted sums of the basis multiplicities, with weights independent of the base point, including where ordinary specialization is nullified. So invariant basis multiplicities give invariant input multiplicities; zero inputs have multiplicity zero.

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 factorizations are Finset.IsSquarefreeBasis.exists_eq_C_content_mul_unit_mul_prod and Finset.IsSquarefreeBasis.exists_rootMultiplicity_eq_sum; the multiplicative evaluation is MvPolynomial.lazardEvalHom.

theorem Finset.IsSquarefreeBasis.exists_lazardEval_eq_C_mul_prod {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} {F B : Finset (Polynomial (MvPolynomial (Fin n) R))} [NormalizedGCDMonoid (MvPolynomial (Fin n) R)] (hB : F.IsSquarefreeBasis B) {f : Polynomial (MvPolynomial (Fin n) R)} (hf : f ∈ F) : ∃ (u : (MvPolynomial (Fin n) R)ˣ) (e : Polynomial (MvPolynomial (Fin n) R) → ℕ), ∀ (a : Fin n → R), (((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) f).lazardEval (⇑Polynomial.C ∘ a) = Polynomial.C (f.content.lazardEval a * (↑u).lazardEval a) * ∏ b ∈ B, (((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) b).lazardEval (⇑Polynomial.C ∘ a) ^ e b

The Lazard evaluation of each input is a scalar times the product of powers of the Lazard evaluations of its basis factors. The scalar contains the Lazard-evaluated content and a unit, and the same factorization works at every base point.

theorem Finset.IsSquarefreeBasis.exists_lazardExponent_eq_content_add_sum {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} {F B : Finset (Polynomial (MvPolynomial (Fin n) R))} [NormalizedGCDMonoid (MvPolynomial (Fin n) R)] (hB : F.IsSquarefreeBasis B) {f : Polynomial (MvPolynomial (Fin n) R)} (hf : f ∈ F) (hf0 : f ≠ 0) : ∃ (e : Polynomial (MvPolynomial (Fin n) R) → ℕ), ∀ (a : Fin n → R), (((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) f).lazardExponent (⇑Polynomial.C ∘ a) = f.content.lazardExponent a + ∑ b ∈ B, e b • (((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) b).lazardExponent (⇑Polynomial.C ∘ a)

For a nonzero input, the removed base exponents are the content exponents plus the weighted sum of the basis exponents. The weights do not depend on the base point.

theorem Finset.IsSquarefreeBasis.lazardExponent_eq {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} {F B : Finset (Polynomial (MvPolynomial (Fin n) R))} [NormalizedGCDMonoid (MvPolynomial (Fin n) R)] (hB : F.IsSquarefreeBasis B) {f : Polynomial (MvPolynomial (Fin n) R)} (hf : f ∈ F) {a a' : Fin n → R} (hc : f.content.lazardExponent a = f.content.lazardExponent a') (hb : ∀ b ∈ B, (((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) b).lazardExponent (⇑Polynomial.C ∘ a) = (((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) b).lazardExponent (⇑Polynomial.C ∘ a')) : (((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) f).lazardExponent (⇑Polynomial.C ∘ a) = (((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) f).lazardExponent (⇑Polynomial.C ∘ a')

Invariant content and basis exponents give invariant input exponents, including zero inputs. No connectedness or nonnullification hypothesis is required.

theorem Finset.IsSquarefreeBasis.exists_rootMultiplicity_lazardEval_eq_sum {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} {F B : Finset (Polynomial (MvPolynomial (Fin n) R))} (hB : F.IsSquarefreeBasis B) {f : Polynomial (MvPolynomial (Fin n) R)} (hf : f ∈ F) (hf0 : f ≠ 0) : ∃ (e : Polynomial (MvPolynomial (Fin n) R) → ℕ), ∀ (a : Fin n → R) (t : R), Polynomial.rootMultiplicity t ((((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) f).lazardEval (⇑Polynomial.C ∘ a)) = ∑ b ∈ B, e b * Polynomial.rootMultiplicity t ((((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) b).lazardEval (⇑Polynomial.C ∘ a))

The multiplicities in a nonzero input's Lazard evaluation are fixed weighted sums of the multiplicities in the basis evaluations, even on nullified ordinary fibers.

theorem Finset.IsSquarefreeBasis.rootMultiplicity_lazardEval_eq {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} {F B : Finset (Polynomial (MvPolynomial (Fin n) R))} (hB : F.IsSquarefreeBasis B) {f : Polynomial (MvPolynomial (Fin n) R)} (hf : f ∈ F) {a a' : Fin n → R} {t t' : R} (hb : ∀ b ∈ B, Polynomial.rootMultiplicity t ((((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) b).lazardEval (⇑Polynomial.C ∘ a)) = Polynomial.rootMultiplicity t' ((((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) b).lazardEval (⇑Polynomial.C ∘ a'))) : Polynomial.rootMultiplicity t ((((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) f).lazardEval (⇑Polynomial.C ∘ a)) = Polynomial.rootMultiplicity t' ((((MvPolynomial.optionEquivLeft R (Fin n)).symm.trans (MvPolynomial.optionEquivRight R (Fin n))) f).lazardEval (⇑Polynomial.C ∘ a'))

Equal basis root multiplicities imply equal input root multiplicities after Lazard evaluation. The base points and root coordinates may both differ.