Collins delineability

Let F be a finite family of polynomials in one distinguished variable over a commutative ring R, and let φ x : R →+* ℝ be a family of specializations parametrized by a preconnected space X. If the elements of the Collins projection F.collinsProjection depend continuously on x after specialization, and the set of those that vanish does not depend on x, then the specialized family p.map (φ x), p ∈ F, has a delineation over X: a common stack of continuous, strictly ordered root functions on whose sections and sectors every member is sign-invariant (TauCeti.Delineation).

The main case is R = MvPolynomial (Fin n) A for a coefficient map φ : A →+* ℝ, specialized at the points x of a preconnected set S ⊆ ℝⁿ by MvPolynomial.eval₂Hom φ x. This is Collins' delineability theorem: if every element of the projection is sign-invariant on S, the family is delineable over S. Taking A = ℝ and φ = RingHom.id ℝ gives real families; taking A = ℤ and φ = Int.castRingHom ℝ gives integer families whose projection is computed over ℤ. Nothing is assumed about the formal leading coefficients, which may vanish on S, nor are nullified members excluded: the reducta in the projection account for both. No semialgebraicity of S is needed. Only the zero pattern of the projection is used, not its signs.

Main results

• TauCeti.nonempty_delineation_of_collinsProjection: a family of specializations along which the Collins projection is continuous and has a constant zero pattern delineates the family.
• TauCeti.nonempty_delineation_of_signInvariant_collinsProjection: Collins delineability over a preconnected subset of ℝⁿ on which the projection is sign-invariant.
• TauCeti.nonempty_delineation_image_finSuccEquiv_map_of_signInvariant_collinsProjection: delineability after mapping the coefficients of a multivariate family injectively into ℝ.

References

• G. E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Lecture Notes in Computer Science 33 (1975), 134–183.
• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Section 5.1 (Theorem 5.16) and Chapter 11.
• D. Jovanović, Solving Non-Linear Arithmetic, dissertation, New York University, 2012, Definition 2.5 and Theorem 2.6.

theorem TauCeti.nonempty_delineation_of_collinsProjection {R : Type u_1} {X : Type u_2} [CommRing R] [TopologicalSpace X] [PreconnectedSpace X] {F : Finset (Polynomial R)} (φ : X → R →+* ℝ) (hcont : ∀ a ∈ F.collinsProjection, Continuous fun (x : X) => (φ x) a) (hzero : ∀ a ∈ F.collinsProjection, ∀ (x y : X), (φ x) a = 0 ↔ (φ y) a = 0) : Nonempty (Delineation fun (p : ↥F) (x : X) => Polynomial.map (φ x) ↑p)

Delineability from the Collins projection. Let φ x : R →+* ℝ be specializations parametrized by a preconnected space X. If every element of the Collins projection of F specializes continuously in x, and whether it specializes to zero does not depend on x, then the specialized family p.map (φ x), p ∈ F, has a delineation over X.

theorem TauCeti.nonempty_delineation_of_signInvariant_collinsProjection {A : Type u_1} [CommRing A] {n : ℕ} {φ : A →+* ℝ} {F : Finset (Polynomial (MvPolynomial (Fin n) A))} {S : Set (Fin n → ℝ)} (hS : IsPreconnected S) (h : ∀ q ∈ F.collinsProjection, SignInvariant (fun (x : Fin n → ℝ) => MvPolynomial.eval₂ φ x q) S) : Nonempty (Delineation fun (p : ↥F) (x : ↑S) => Polynomial.map (MvPolynomial.eval₂Hom φ ↑x) ↑p)

Collins delineability. Let F be a finite family of polynomials in one distinguished variable whose coefficients are polynomials over A in the base coordinates, and let φ : A →+* ℝ. If every element of the Collins projection of F is sign-invariant, after evaluation along φ, on a preconnected set S ⊆ ℝⁿ, then the family of fibers p.map (MvPolynomial.eval₂Hom φ x), p ∈ F, x ∈ S, has a delineation over S.

Only the zero pattern of the projection on S is used; see TauCeti.nonempty_delineation_of_collinsProjection.

theorem TauCeti.nonempty_delineation_image_finSuccEquiv_map_of_signInvariant_collinsProjection {A : Type u_1} [CommRing A] {n : ℕ} {φ : A →+* ℝ} {S : Set (Fin n → ℝ)} [DecidableEq (Polynomial (MvPolynomial (Fin n) A))] [DecidableEq (Polynomial (MvPolynomial (Fin n) ℝ))] (hφ : Function.Injective ⇑φ) {P : Finset (MvPolynomial (Fin (n + 1)) A)} (hS : IsPreconnected S) (h : ∀ q ∈ (Finset.image (⇑(MvPolynomial.finSuccEquiv A n)) P).collinsProjection, SignInvariant (fun (x : Fin n → ℝ) => MvPolynomial.eval₂ φ x q) S) : Nonempty (Delineation fun (p : ↥(Finset.image (fun (f : MvPolynomial (Fin (n + 1)) A) => (MvPolynomial.finSuccEquiv ℝ n) ((MvPolynomial.map φ) f)) P)) (x : ↑S) => Polynomial.map (MvPolynomial.eval₂Hom (RingHom.id ℝ) ↑x) ↑p)

Delineability of families mapped to ℝ. Let P be a finite family of polynomials in the variables X 0, …, X n over A, and let φ : A →+* ℝ be injective. If every element of the Collins projection computed over A, with X 0 singled out, is sign-invariant after evaluation along φ on a preconnected set S ⊆ ℝⁿ, then the family obtained by mapping P to ℝ and singling out X 0 has a delineation over S.