Semialgebraic sets are the sets definable in the field language

Over a real closed field the order is definable from the ring operations: x is positive exactly when x * z ^ 2 = 1 for some z. Consequently every semialgebraic subset of σ → R is already definable with parameters in the first-order language of rings Language.ring, without the order symbol. When semialgebraic sets are closed under projection, as they are over ℝ by the Tarski–Seidenberg theorem, the converse holds as well. Then the semialgebraic sets, the sets definable in the language of rings and the sets definable in the language of ordered rings all coincide.

Following Mathlib, statements about first-order structures on a concrete ring take the structures as instance hypotheses, since FirstOrder.Ring.compatibleRingOfRing and FirstOrder.Language.orderStructure are not global instances. With these two structures installed on R, the instances of TauCeti.ModelTheory.Order make the sum-language structure an ordered structure, so the results of TauCeti.Geometry.RealAlgebraic.Semialgebraic.QuantifierElimination apply. The theorems TauCeti.isSemialgebraic_iff_definable_ring_real and TauCeti.isSemialgebraic_iff_definable_real install them on ℝ and state the identification there with no hypothesis.

Main results

• TauCeti.IsSemialgebraic.definable_ring: over a real closed field, a semialgebraic set is definable with parameters in the language of rings.
• TauCeti.isSemialgebraic_iff_definable_ring: given projection closure, a subset of σ → R is semialgebraic if and only if it is definable with parameters in the language of rings.
• TauCeti.definable_ring_iff_definable: given projection closure, the order symbol adds no definable sets.
• TauCeti.isSemialgebraic_iff_definable_ring_real, TauCeti.isSemialgebraic_iff_definable_real: the semialgebraic subsets of σ → ℝ are the sets definable with parameters in the field ℝ, and in the ordered field ℝ.

References

• S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Sections 2.3 and 2.4.
• D. Marker, Model Theory: An Introduction, Graduate Texts in Mathematics 217, Springer (2002), Section 3.3.

theorem Set.Definable.isSemialgebraic_of_ring {R : Type u_1} [CommRing R] [FirstOrder.Ring.CompatibleRing R] [LinearOrder R] [IsOrderedAddMonoid R] [TauCeti.HasSemialgebraicProjections R] {σ : Type u_2} {A : Set R} {s : Set (σ → R)} (hs : A.Definable FirstOrder.Language.ring s) : TauCeti.IsSemialgebraic s

Given projection closure, a subset of σ → R definable with parameters in the language of rings is semialgebraic.

theorem TauCeti.IsSemialgebraic.definable_ring {R : Type u_1} [Field R] [FirstOrder.Ring.CompatibleRing R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {σ : Type u_2} {s : Set (σ → R)} (hs : IsSemialgebraic s) : Set.univ.Definable FirstOrder.Language.ring s

The order of a real closed field is definable from its ring operations. A semialgebraic subset of σ → R is definable with parameters from R in the language of rings. Zero sets are definable by equations, and the positivity set of p is the projection of the zero set of p * z ^ 2 - 1, since the positive elements of R are its nonzero squares.

theorem TauCeti.isSemialgebraic_iff_definable_ring {R : Type u_1} [Field R] [FirstOrder.Ring.CompatibleRing R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {σ : Type u_2} [HasSemialgebraicProjections R] {s : Set (σ → R)} : IsSemialgebraic s ↔ Set.univ.Definable FirstOrder.Language.ring s

Tarski's theorem in the field language. Given projection closure, a subset of σ → R is semialgebraic if and only if it is definable in the language of rings with parameters from R.

theorem TauCeti.definable_ring_iff_definable {R : Type u_1} [Field R] [FirstOrder.Ring.CompatibleRing R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {σ : Type u_2} [HasSemialgebraicProjections R] [FirstOrder.Language.order.Structure R] [(FirstOrder.Language.ring.sum FirstOrder.Language.order).OrderedStructure R] {s : Set (σ → R)} : Set.univ.Definable FirstOrder.Language.ring s ↔ Set.univ.Definable (FirstOrder.Language.ring.sum FirstOrder.Language.order) s

Given projection closure, a subset of σ → R is definable with parameters in the language of rings if and only if it is definable with parameters in the language of ordered rings, for any structure on R interpreting ≤ as the order of R.

theorem TauCeti.isSemialgebraic_iff_definable_ring_real {σ : Type u_2} {s : Set (σ → ℝ)} : IsSemialgebraic s ↔ Set.univ.Definable FirstOrder.Language.ring s

Tarski's theorem for the real field. A subset of σ → ℝ is semialgebraic if and only if it is definable with parameters in the field ℝ, that is, in the language of rings with its usual interpretation.

theorem TauCeti.isSemialgebraic_iff_definable_real {σ : Type u_2} {s : Set (σ → ℝ)} : IsSemialgebraic s ↔ Set.univ.Definable (FirstOrder.Language.ring.sum FirstOrder.Language.order) s

A subset of σ → ℝ is semialgebraic if and only if it is definable with parameters in the ordered field ℝ, that is, in the language of ordered rings with its usual interpretation.