Lazard lifting of irreducible bases and families

On a preconnected analytic submanifold, invariance of the Lazard projection gives a common Lazard delineation of any subfamily of an irreducible basis whose members have nonzero formal constant coefficients. The original fibers may be nullified, and the formal projection polynomials may vanish everywhere on the base.

The projection controls the leading coefficient, constant coefficient and discriminant of the subfamily product. Single-polynomial analytic lifting applies to this product, and recovering its factors gives simultaneous root membership, multiplicities and removed base exponents. Pairwise resultants enter through the discriminant of the product; separate delineations of the members would not by themselves supply this common stack.

The excluded irreducible factors are associates of the distinguished coordinate; by pairwise nonassociation there is at most one. Its delineation is the zero section. The trailing coefficients in the projection decide uniformly whether 0 is a root of the Lazard evaluations of the other members, so the zero section can be adjoined to their common stack. This gives a Lazard delineation of the whole basis, and, since the contents lie in the projection, of the original family.

Main results

• TauCeti.nonempty_lazardDelineation_subfamily_of_lazardProjection: a common Lazard delineation of the basis members with nonzero constant coefficient.
• TauCeti.nonempty_lazardDelineation_basis_of_lazardProjection: a Lazard delineation of the whole irreducible basis.
• TauCeti.nonempty_lazardDelineation_of_lazardProjection: a Lazard delineation of the family.

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

theorem TauCeti.nonempty_lazardDelineation_subfamily_of_lazardProjection {n d : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F B A : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {S : Set (Fin n → ℝ)} (hB : F.IsIrreducibleBasis B) (hAB : A ⊆ B) (hconst : ∀ b ∈ A, b.coeff 0 ≠ 0) (hS : IsAnalyticSubmanifold d S) (hconn : IsPreconnected S) (hproj : ∀ q ∈ F.lazardProjection B, ∀ x ∈ S, ∀ y ∈ S, q.lazardValuation x = q.lazardValuation y) : Nonempty (LazardDelineation (fun (b : ↥A) => (MvPolynomial.rename ⇑finSuccEquivLast.symm) ((MvPolynomial.optionEquivLeft ℝ (Fin n)).symm ↑b)) S)

The noncoordinate members of any subfamily of an irreducible basis have a common Lazard delineation over a preconnected analytic submanifold on which the full Lazard projection is valuation-invariant. The hypothesis on constant coefficients concerns formal polynomials, not their values on the base. No nonnullification or preservation of fiber degrees is required.

In particular, take A to be the members of B with nonzero constant coefficient. Basis members outside A, including associates of the distinguished coordinate, are unrestricted.

theorem TauCeti.nonempty_lazardDelineation_basis_of_lazardProjection {n d : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {S : Set (Fin n → ℝ)} (hB : F.IsIrreducibleBasis B) (hS : IsAnalyticSubmanifold d S) (hconn : IsPreconnected S) (hproj : ∀ q ∈ F.lazardProjection B, ∀ x ∈ S, ∀ y ∈ S, q.lazardValuation x = q.lazardValuation y) : Nonempty (LazardDelineation (fun (b : ↥B) => (MvPolynomial.rename ⇑finSuccEquivLast.symm) ((MvPolynomial.optionEquivLeft ℝ (Fin n)).symm ↑b)) S)

Lazard lifting of an irreducible basis. Over a preconnected analytic submanifold on which the Lazard projection is valuation-invariant, an irreducible basis has a Lazard delineation.

The members with nonzero constant coefficient are lifted together through their product. The remaining member, if any, is an associate of the distinguished coordinate; it contributes the zero section. Invariance of the constant coefficients of the other members makes 0 a root of their Lazard evaluations either over every base point or over none.

theorem TauCeti.nonempty_lazardDelineation_of_lazardProjection {n d : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {S : Set (Fin n → ℝ)} (hB : F.IsIrreducibleBasis B) (hS : IsAnalyticSubmanifold d S) (hconn : IsPreconnected S) (hproj : ∀ q ∈ F.lazardProjection B, ∀ x ∈ S, ∀ y ∈ S, q.lazardValuation x = q.lazardValuation y) : Nonempty (LazardDelineation (fun (f : ↥F) => (MvPolynomial.rename ⇑finSuccEquivLast.symm) ((MvPolynomial.optionEquivLeft ℝ (Fin n)).symm ↑f)) S)

Lazard lifting of a family. Over a preconnected analytic submanifold on which the Lazard projection of a family with respect to an irreducible basis is valuation-invariant, the family has a Lazard delineation. Its members may be nullified at points of the base.