Lazard delineations of a family from its irreducible basis

Let F be a finite family of polynomials in a distinguished variable over ℝ[X₀, …, Xₙ₋₁], and let B be an irreducible basis of F (Finset.IsIrreducibleBasis): every member of F is its content times a unit times a product of powers of members of B. Read each such polynomial as a real polynomial in n + 1 variables whose last variable is the distinguished one, as in TauCeti.LazardDelineation.

A Lazard delineation of the basis over S ⊆ ℝⁿ induces a Lazard delineation of the family with exactly the same root functions, provided the content of every member of F has constant Lazard valuation on S. For each nonzero member of F, Lazard evaluation is multiplicative, so its Lazard evaluation is a nonzero constant times a product of powers of the Lazard evaluations of the basis members. Hence its roots are basis roots, its root multiplicities are fixed weighted sums of the basis multiplicities, and its removed base exponents are the content exponents plus a fixed weighted sum of the basis exponents. Zero members are allowed; the root-coverage condition for a Lazard delineation applies only to nonzero members. Every section of the basis stack is a root of some nonzero member of F, since each basis member divides one.

No connectedness, analyticity or preservation of ordinary fibre degrees is needed. Nonzero members of F may be nullified at points of S, and their contents may vanish. This is the passage from the basis to the original family in Lazard's lifting: once the basis has a Lazard delineation over a cell on which the Lazard projection is valuation-invariant, every original input is valuation-invariant, hence sign-invariant, on each section and sector above it (TauCeti.LazardDelineation.lazardValuation_snoc_eq_of_mem_sectionSet, TauCeti.LazardDelineation.signInvariant_sectionSet and their sector versions).

Main definitions and results

• TauCeti.LazardDelineation.ofIrreducibleBasis: the Lazard delineation of a family induced by a Lazard delineation of its irreducible basis.
• TauCeti.LazardDelineation.ofIrreducibleBasis_count, TauCeti.LazardDelineation.ofIrreducibleBasis_root: it has the same ordered root functions.

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, Sections 2 and 5.

noncomputable def TauCeti.LazardDelineation.ofIrreducibleBasis {n : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {S : Set (Fin n → ℝ)} (D : LazardDelineation (fun (b : ↥B) => (MvPolynomial.rename ⇑finSuccEquivLast.symm) ((MvPolynomial.optionEquivLeft ℝ (Fin n)).symm ↑b)) S) (hB : F.IsIrreducibleBasis B) (hc : ∀ f ∈ F, ∀ x ∈ S, ∀ y ∈ S, f.content.lazardValuation x = f.content.lazardValuation y) : LazardDelineation (fun (f : ↥F) => (MvPolynomial.rename ⇑finSuccEquivLast.symm) ((MvPolynomial.optionEquivLeft ℝ (Fin n)).symm ↑f)) S

Lazard delineation of a family from its irreducible basis. A Lazard delineation of an irreducible basis B of F over S induces a Lazard delineation of F with the same ordered root functions, provided the content of every member of F has constant Lazard valuation on S. Members of F may be nullified at points of S; no connectedness of S is needed.

@[simp]

theorem TauCeti.LazardDelineation.ofIrreducibleBasis_count {n : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {S : Set (Fin n → ℝ)} (D : LazardDelineation (fun (b : ↥B) => (MvPolynomial.rename ⇑finSuccEquivLast.symm) ((MvPolynomial.optionEquivLeft ℝ (Fin n)).symm ↑b)) S) (hB : F.IsIrreducibleBasis B) (hc : ∀ f ∈ F, ∀ x ∈ S, ∀ y ∈ S, f.content.lazardValuation x = f.content.lazardValuation y) : (D.ofIrreducibleBasis hB hc).count = D.count

Passing from a basis to its family preserves the number of sections.

@[simp]

theorem TauCeti.LazardDelineation.ofIrreducibleBasis_root {n : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {S : Set (Fin n → ℝ)} (D : LazardDelineation (fun (b : ↥B) => (MvPolynomial.rename ⇑finSuccEquivLast.symm) ((MvPolynomial.optionEquivLeft ℝ (Fin n)).symm ↑b)) S) (hB : F.IsIrreducibleBasis B) (hc : ∀ f ∈ F, ∀ x ∈ S, ∀ y ∈ S, f.content.lazardValuation x = f.content.lazardValuation y) (i : Fin (D.ofIrreducibleBasis hB hc).count) (x : ↑S) : (D.ofIrreducibleBasis hB hc).root i x = D.root (Fin.cast ⋯ i) x

Passing from a basis to its family preserves the ordered root functions.