Semialgebraic sets are the quantifier-free definable sets

Let R be a commutative ring with a linear order compatible with addition, regarded as a structure in the first-order language of ordered rings Language.ring.sum Language.order, with the ring symbols and ≤ interpreted as usual. This file identifies the semialgebraic subsets of σ → R, defined intrinsically as finite Boolean combinations of polynomial zero sets and positivity sets (TauCeti.IsSemialgebraic), with the sets defined by quantifier-free formulas with parameters from R.

• FirstOrder.Language.BoundedFormula.IsQF.isSemialgebraic_setOf_realize and FirstOrder.Language.BoundedFormula.IsQF.isSemialgebraic_setOf_formula_realize: a quantifier-free formula without parameters defines a semialgebraic set, since it is a sign condition on finitely many integer polynomials (FirstOrder.Language.BoundedFormula.IsQF.exists_realize_iff_sign).
• TauCeti.isSemialgebraic_iff_exists_isQF: a set is semialgebraic if and only if it is defined by a quantifier-free formula whose extra variables Sum.inl r are assigned the parameters r ∈ R. The strict inequality 0 < p is expressed as the negation ¬ p ≤ 0.
• TauCeti.IsSemialgebraic.definable: hence every semialgebraic set is definable with parameters, in the sense of Mathlib's Set.Definable.

The converse of the last statement, that every definable set is semialgebraic, is quantifier elimination; over a real closed field it is the Tarski–Seidenberg theorem. TauCeti.Geometry.RealAlgebraic.Semialgebraic.QuantifierElimination derives it from closure of semialgebraic sets under projection.

To apply these results to a concrete ordered field such as ℝ, install the structures FirstOrder.Ring.compatibleRingOfRing ℝ and FirstOrder.Language.orderStructure ℝ; the OrderedStructure hypothesis is then found by the instances FirstOrder.Language.orderedStructure_orderStructure and FirstOrder.Language.orderedStructure_sum of TauCeti.ModelTheory.Order.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 2, for semi-algebraic sets as the realizations of quantifier-free formulas.

theorem FirstOrder.Language.BoundedFormula.IsQF.isSemialgebraic_setOf_realize {R : Type u_1} [CommRing R] [Ring.CompatibleRing R] [Language.order.Structure R] [LinearOrder R] [IsOrderedAddMonoid R] [(ring.sum Language.order).OrderedStructure R] {α : Type u_2} {n : ℕ} {φ : (ring.sum Language.order).BoundedFormula α n} (hφ : φ.IsQF) : TauCeti.IsSemialgebraic {x : α ⊕ Fin n → R | φ.Realize (x ∘ Sum.inl) (x ∘ Sum.inr)}

A quantifier-free formula of ordered rings, with free variables α and n bound variables, defines a semialgebraic subset of α ⊕ Fin n → R.

theorem FirstOrder.Language.BoundedFormula.IsQF.isSemialgebraic_setOf_formula_realize {R : Type u_1} [CommRing R] [Ring.CompatibleRing R] [Language.order.Structure R] [LinearOrder R] [IsOrderedAddMonoid R] [(ring.sum Language.order).OrderedStructure R] {α : Type u_2} {φ : (ring.sum Language.order).Formula α} (hφ : IsQF φ) : TauCeti.IsSemialgebraic {v : α → R | φ.Realize v}

A quantifier-free formula of ordered rings with free variables α defines a semialgebraic subset of α → R.

theorem TauCeti.isSemialgebraic_iff_exists_isQF {R : Type u_1} [CommRing R] [FirstOrder.Ring.CompatibleRing R] [FirstOrder.Language.order.Structure R] [LinearOrder R] [IsOrderedAddMonoid R] [(FirstOrder.Language.ring.sum FirstOrder.Language.order).OrderedStructure R] {σ : Type u_2} {s : Set (σ → R)} : IsSemialgebraic s ↔ ∃ (φ : (FirstOrder.Language.ring.sum FirstOrder.Language.order).Formula (R ⊕ σ)), FirstOrder.Language.BoundedFormula.IsQF φ ∧ s = {v : σ → R | φ.Realize (Sum.elim id v)}

A subset of σ → R is semialgebraic if and only if it is defined by a quantifier-free formula of ordered rings with parameters from R: the formula has free variables R ⊕ σ, and each variable Sum.inl r is assigned the value r.

theorem TauCeti.IsSemialgebraic.definable {R : Type u_1} [CommRing R] [FirstOrder.Ring.CompatibleRing R] [FirstOrder.Language.order.Structure R] [LinearOrder R] [IsOrderedAddMonoid R] [(FirstOrder.Language.ring.sum FirstOrder.Language.order).OrderedStructure R] {σ : Type u_2} {s : Set (σ → R)} (hs : IsSemialgebraic s) : Set.univ.Definable (FirstOrder.Language.ring.sum FirstOrder.Language.order) s

A semialgebraic subset of σ → R is definable in the language of ordered rings with parameters from R.