Semialgebraicity of polynomial delineations

Every delineation of a finite polynomial family over a semialgebraic base is a semialgebraic stack. No closure under differentiation is needed. The sections and sectors are described by membership in the shared distinct root set and the number of shared roots strictly below the height, using the uniform formulas of Finset.isSemialgebraic_setOf_mem_biUnion_roots_card_lt and Finset.isSemialgebraic_setOf_notMem_biUnion_roots_card_lt.

Coefficients may come from any commutative ring equipped with a homomorphism to ℝ. Nullified fibers contribute no roots to the finite shared root set; they do not contribute their entire zero set. Repeated roots and roots shared by several members are counted once. The empty family and a stack with no sections are included.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapters 10 and 11 (uniform shared-root descriptions and semialgebraic stacks).

theorem TauCeti.Delineation.isSemialgebraicStack {A : Type u_1} [CommRing A] {n : ℕ} {φ : A →+* ℝ} {F : Finset (Polynomial (MvPolynomial (Fin n) A))} {C : Set (Fin n → ℝ)} (hC : IsSemialgebraic C) (D : Delineation fun (p : ↥F) (x : ↑C) => Polynomial.map (MvPolynomial.eval₂Hom φ ↑x) ↑p) : IsSemialgebraicStack C D.root

A delineation of a finite polynomial family over a semialgebraic base is a semialgebraic stack. The family need not be closed under differentiation. Nullified members are allowed.