Polynomial relations on semialgebraic sets with empty interior

A real semialgebraic set with empty interior is contained in the zero set of a single nonzero polynomial. No boundedness, closedness or regularity assumption is needed. This is the algebraic step that turns semialgebraic graphs into algebraic relations.

In a finite sign presentation, a point where none of the nonzero defining polynomials vanishes is an interior point: all the signs are locally constant there. Consequently the product of the nonzero defining polynomials vanishes on the set. Identically zero polynomials must be omitted from this product. The empty set is included, with the empty product equal to one.

References

• J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Springer, 1998, Section 2.8 (dimension) and Section 8.1 (Nash functions).

theorem TauCeti.IsSemialgebraic.exists_ne_zero_polynomial_of_interior_eq_empty {σ : Type u_1} {s : Set (σ → ℝ)} (hs : IsSemialgebraic s) (hint : interior s = ∅) : ∃ (p : MvPolynomial σ ℝ), p ≠ 0 ∧ ∀ x ∈ s, (MvPolynomial.eval x) p = 0

A real semialgebraic set with empty interior satisfies a nonzero polynomial equation. The index type need not be finite: a semialgebraic presentation uses only finitely many polynomials, each involving only finitely many coordinates.