Semialgebraic sets

A subset of σ → R, for a commutative ring R with a chosen linear order, is semialgebraic when it is a finite Boolean combination of polynomial zero sets {x | p(x) = 0} and positivity sets {x | 0 < p(x)}. We define TauCeti.IsSemialgebraic as membership in the algebra of sets (MeasureTheory.generateSetAlgebra) generated by these basic sets. This is the intrinsic, quantifier-free definition. When R is a real closed field, closure under coordinate projection is the Tarski–Seidenberg theorem, a consequence of cylindrical algebraic decomposition; projection closure is not built into the definition.

Every closure property proved here follows directly from the definition:

• the Boolean operations, including finite unions and intersections;
• every polynomial sign condition, such as {x | p(x) ≤ q(x)} or {x | sign p(x) = ε};
• any condition on the signs of finitely many polynomials (TauCeti.isSemialgebraic_setOf_sign_eval), in particular a prescribed permanences minus variations of their values (TauCeti.isSemialgebraic_setOf_permanencesMinusVariations_eval);
• the vanishing of a prescribed set of coefficients of a polynomial family P : Polynomial (MvPolynomial σ R) (TauCeti.isSemialgebraic_setOf_forall_coeff_eq_zero);
• inverse images under polynomial maps (TauCeti.IsSemialgebraic.preimage_eval), and hence under changes of coordinates, in particular coordinate permutations;
• products, in the form σ ⊕ τ → R and in the form Fin (m + n) → R;
• the sections {x : Fin n → R | Fin.cons t x ∈ s} and {y : Fin 1 → R | Fin.cons (y 0) x ∈ s} of a subset of Fin (n + 1) → R, which are the horizontal and vertical slices of a cylinder over Fin n → R with distinguished coordinate 0; the vertical slice is a subset of Fin 1 → R, the one-coordinate space of the definition.

Conversely, every semialgebraic set is described by a condition on the signs of finitely many polynomials (TauCeti.IsSemialgebraic.exists_eq_setOf_sign_eval), and so membership in it depends on only finitely many coordinates (TauCeti.IsSemialgebraic.exists_finset_mem_iff_of_eqOn).

Closure under projection is recorded as the property TauCeti.HasSemialgebraicProjections R of the ordered ring R, with field TauCeti.HasSemialgebraicProjections.isSemialgebraic_image_tail. Its consequences, such as quantifier elimination and the image and composition laws of semialgebraic functions, are stated under this assumption.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 2, for semi-algebraic sets.

The generated algebra of sets is Mathlib's MeasureTheory.generateSetAlgebra, from Mathlib/MeasureTheory/SetAlgebra.lean by Etienne Marion.

def TauCeti.IsSemialgebraic {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] (s : Set (σ → R)) : Prop

A set s ⊆ σ → R is semialgebraic if it belongs to the algebra of sets (closed under complements and finite unions) generated by the polynomial zero sets {x | p(x) = 0} and the positivity sets {x | 0 < p(x)}, for p : MvPolynomial σ R.

theorem TauCeti.isSemialgebraic_def {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {s : Set (σ → R)} : IsSemialgebraic s ↔ s ∈ MeasureTheory.generateSetAlgebra ((Set.range fun (p : MvPolynomial σ R) => {x : σ → R | (MvPolynomial.eval x) p = 0}) ∪ Set.range fun (p : MvPolynomial σ R) => {x : σ → R | 0 < (MvPolynomial.eval x) p})

A set is semialgebraic if and only if it belongs to the algebra of sets generated by the polynomial zero sets and the polynomial positivity sets.

theorem TauCeti.isSemialgebraic_eval_eq_zero {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] (p : MvPolynomial σ R) : IsSemialgebraic {x : σ → R | (MvPolynomial.eval x) p = 0}

The zero set of a polynomial is semialgebraic.

theorem TauCeti.isSemialgebraic_eval_pos {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] (p : MvPolynomial σ R) : IsSemialgebraic {x : σ → R | 0 < (MvPolynomial.eval x) p}

The positivity set of a polynomial is semialgebraic.

theorem TauCeti.isSetAlgebra_setOf_isSemialgebraic {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] : MeasureTheory.IsSetAlgebra {s : Set (σ → R) | IsSemialgebraic s}

The semialgebraic sets form an algebra of sets.

theorem TauCeti.setOf_isSemialgebraic_subset {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {ℬ : Set (Set (σ → R))} (hℬ : MeasureTheory.IsSetAlgebra ℬ) (eq_zero : ∀ (p : MvPolynomial σ R), {x : σ → R | (MvPolynomial.eval x) p = 0} ∈ ℬ) (pos : ∀ (p : MvPolynomial σ R), {x : σ → R | 0 < (MvPolynomial.eval x) p} ∈ ℬ) : {s : Set (σ → R) | IsSemialgebraic s} ⊆ ℬ

The semialgebraic sets form the smallest algebra of sets containing every polynomial zero set and every polynomial positivity set.

theorem TauCeti.IsSemialgebraic.induction {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {motive : Set (σ → R) → Prop} (eq_zero : ∀ (p : MvPolynomial σ R), motive {x : σ → R | (MvPolynomial.eval x) p = 0}) (pos : ∀ (p : MvPolynomial σ R), motive {x : σ → R | 0 < (MvPolynomial.eval x) p}) (compl : ∀ (s : Set (σ → R)), IsSemialgebraic s → motive s → motive sᶜ) (union : ∀ (s t : Set (σ → R)), IsSemialgebraic s → IsSemialgebraic t → motive s → motive t → motive (s ∪ t)) {s : Set (σ → R)} (hs : IsSemialgebraic s) : motive s

Induction principle for semialgebraic sets: a property of sets that holds for polynomial zero sets and polynomial positivity sets, and is preserved by complements and binary unions, holds for every semialgebraic set.

Boolean operations

@[simp]

theorem TauCeti.isSemialgebraic_empty {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] : IsSemialgebraic ∅

The empty set is semialgebraic.

@[simp]

theorem TauCeti.isSemialgebraic_univ {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] : IsSemialgebraic Set.univ

The whole space is semialgebraic.

theorem TauCeti.IsSemialgebraic.compl {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {s : Set (σ → R)} (hs : IsSemialgebraic s) : IsSemialgebraic sᶜ

The complement of a semialgebraic set is semialgebraic.

theorem TauCeti.IsSemialgebraic.of_compl {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {s : Set (σ → R)} (hs : IsSemialgebraic sᶜ) : IsSemialgebraic s

A set whose complement is semialgebraic is semialgebraic.

@[simp]

theorem TauCeti.isSemialgebraic_compl_iff {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {s : Set (σ → R)} : IsSemialgebraic sᶜ ↔ IsSemialgebraic s

The complement of a set is semialgebraic if and only if the set is.

theorem TauCeti.IsSemialgebraic.union {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {s t : Set (σ → R)} (hs : IsSemialgebraic s) (ht : IsSemialgebraic t) : IsSemialgebraic (s ∪ t)

The union of two semialgebraic sets is semialgebraic.

theorem TauCeti.IsSemialgebraic.inter {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {s t : Set (σ → R)} (hs : IsSemialgebraic s) (ht : IsSemialgebraic t) : IsSemialgebraic (s ∩ t)

The intersection of two semialgebraic sets is semialgebraic.

theorem TauCeti.IsSemialgebraic.sdiff {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {s t : Set (σ → R)} (hs : IsSemialgebraic s) (ht : IsSemialgebraic t) : IsSemialgebraic (s \ t)

The difference of two semialgebraic sets is semialgebraic.

theorem TauCeti.IsSemialgebraic.biUnion {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {ι : Type u_4} {S : Set ι} (hS : S.Finite) {s : ι → Set (σ → R)} (hs : ∀ i ∈ S, IsSemialgebraic (s i)) : IsSemialgebraic (⋃ i ∈ S, s i)

A finite union of semialgebraic sets is semialgebraic.

theorem TauCeti.IsSemialgebraic.biInter {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {ι : Type u_4} {S : Set ι} (hS : S.Finite) {s : ι → Set (σ → R)} (hs : ∀ i ∈ S, IsSemialgebraic (s i)) : IsSemialgebraic (⋂ i ∈ S, s i)

A finite intersection of semialgebraic sets is semialgebraic.

theorem TauCeti.IsSemialgebraic.iUnion {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {ι : Type u_4} [Finite ι] {s : ι → Set (σ → R)} (hs : ∀ (i : ι), IsSemialgebraic (s i)) : IsSemialgebraic (⋃ (i : ι), s i)

A union of finitely many semialgebraic sets is semialgebraic.

theorem TauCeti.IsSemialgebraic.iInter {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {ι : Type u_4} [Finite ι] {s : ι → Set (σ → R)} (hs : ∀ (i : ι), IsSemialgebraic (s i)) : IsSemialgebraic (⋂ (i : ι), s i)

An intersection of finitely many semialgebraic sets is semialgebraic.

Polynomial sign conditions

theorem TauCeti.isSemialgebraic_eval_ne_zero {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] (p : MvPolynomial σ R) : IsSemialgebraic {x : σ → R | (MvPolynomial.eval x) p ≠ 0}

The set where a polynomial does not vanish is semialgebraic.

theorem TauCeti.isSemialgebraic_eval_eq {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] (p q : MvPolynomial σ R) : IsSemialgebraic {x : σ → R | (MvPolynomial.eval x) p = (MvPolynomial.eval x) q}

The set where two polynomials agree is semialgebraic.

theorem TauCeti.isSemialgebraic_eval_nonpos {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] (p : MvPolynomial σ R) : IsSemialgebraic {x : σ → R | (MvPolynomial.eval x) p ≤ 0}

The set where a polynomial is nonpositive is semialgebraic.

theorem TauCeti.isSemialgebraic_eval_neg {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] (p : MvPolynomial σ R) : IsSemialgebraic {x : σ → R | (MvPolynomial.eval x) p < 0}

The set where a polynomial is negative is semialgebraic.

theorem TauCeti.isSemialgebraic_eval_nonneg {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] (p : MvPolynomial σ R) : IsSemialgebraic {x : σ → R | 0 ≤ (MvPolynomial.eval x) p}

The set where a polynomial is nonnegative is semialgebraic.

theorem TauCeti.isSemialgebraic_eval_lt {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] [IsOrderedAddMonoid R] (p q : MvPolynomial σ R) : IsSemialgebraic {x : σ → R | (MvPolynomial.eval x) p < (MvPolynomial.eval x) q}

The set where one polynomial is less than another is semialgebraic.

theorem TauCeti.isSemialgebraic_eval_le {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] [IsOrderedAddMonoid R] (p q : MvPolynomial σ R) : IsSemialgebraic {x : σ → R | (MvPolynomial.eval x) p ≤ (MvPolynomial.eval x) q}

The set where one polynomial is at most another is semialgebraic.

theorem TauCeti.isSemialgebraic_sign_eval_eq {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] (p : MvPolynomial σ R) (ε : SignType) : IsSemialgebraic {x : σ → R | SignType.sign ((MvPolynomial.eval x) p) = ε}

The set where a polynomial has a prescribed sign is semialgebraic.

theorem TauCeti.isSemialgebraic_setOf_sign_eval {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {ι : Type u_4} [Finite ι] (p : ι → MvPolynomial σ R) (Φ : (ι → SignType) → Prop) : IsSemialgebraic {x : σ → R | Φ fun (i : ι) => SignType.sign ((MvPolynomial.eval x) (p i))}

A sign condition on finitely many polynomials defines a semialgebraic set: membership may depend in any way on the signs of their values.

theorem TauCeti.isSemialgebraic_setOf_permanencesMinusVariations_eval {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] (l : List (MvPolynomial σ R)) (c : ℤ) : IsSemialgebraic {x : σ → R | (List.map (⇑(MvPolynomial.eval x)) l).permanencesMinusVariations = c}

A condition on the permanences minus variations of the values of finitely many polynomials defines a semialgebraic set, since the statistic depends only on the signs of the values.

theorem TauCeti.isSemialgebraic_setOf_forall_coeff_eq_zero {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] (P : Polynomial (MvPolynomial σ R)) (s : Set ℕ) : IsSemialgebraic {x : σ → R | ∀ n ∈ s, (MvPolynomial.eval x) (P.coeff n) = 0}

The parameters at which the coefficients of P of index in s all vanish form a semialgebraic set.

Finite sets

theorem TauCeti.isSemialgebraic_singleton {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] [Finite σ] (a : σ → R) : IsSemialgebraic {a}

In finitely many coordinates, a point is semialgebraic.

theorem Set.Finite.isSemialgebraic {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] [Finite σ] {s : Set (σ → R)} (hs : s.Finite) : TauCeti.IsSemialgebraic s

In finitely many coordinates, a finite set is semialgebraic.

Inverse images and products

theorem TauCeti.IsSemialgebraic.preimage_eval {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {s : Set (τ → R)} (hs : IsSemialgebraic s) (f : τ → MvPolynomial σ R) : IsSemialgebraic ((fun (x : σ → R) (i : τ) => (MvPolynomial.eval x) (f i)) ⁻¹' s)

The inverse image of a semialgebraic set under a polynomial map is semialgebraic.

theorem TauCeti.IsSemialgebraic.preimage_comp {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {s : Set (τ → R)} (hs : IsSemialgebraic s) (f : τ → σ) : IsSemialgebraic ((fun (x : σ → R) => x ∘ f) ⁻¹' s)

The inverse image of a semialgebraic set under a change of coordinates x ↦ x ∘ f is semialgebraic.

@[simp]

theorem TauCeti.isSemialgebraic_preimage_comp_equiv {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {s : Set (τ → R)} (e : τ ≃ σ) : IsSemialgebraic ((fun (x : σ → R) => x ∘ ⇑e) ⁻¹' s) ↔ IsSemialgebraic s

Semialgebraicity is invariant under a bijective change of coordinates, such as a coordinate permutation.

theorem TauCeti.IsSemialgebraic.preimage_sumArrowEquivProdArrow_prod {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {s : Set (σ → R)} {t : Set (τ → R)} (hs : IsSemialgebraic s) (ht : IsSemialgebraic t) : IsSemialgebraic (⇑(Equiv.sumArrowEquivProdArrow σ τ R) ⁻¹' s ×ˢ t)

The product of semialgebraic sets, as a subset of σ ⊕ τ → R, is semialgebraic.

theorem TauCeti.IsSemialgebraic.image_appendEquiv_prod {R : Type u_3} [CommRing R] [LinearOrder R] {m n : ℕ} {s : Set (Fin m → R)} {t : Set (Fin n → R)} (hs : IsSemialgebraic s) (ht : IsSemialgebraic t) : IsSemialgebraic (⇑(Fin.appendEquiv m n) '' s ×ˢ t)

The product of semialgebraic sets, as a subset of Fin (m + n) → R, is semialgebraic.

theorem TauCeti.IsSemialgebraic.preimage_tail {R : Type u_3} [CommRing R] [LinearOrder R] {n : ℕ} {s : Set (Fin n → R)} (hs : IsSemialgebraic s) : IsSemialgebraic (Fin.tail ⁻¹' s)

The cylinder Fin.tail ⁻¹' s over a semialgebraic subset s of Fin n → R, with distinguished coordinate 0, is semialgebraic.

theorem TauCeti.IsSemialgebraic.preimage_cons_left {R : Type u_3} [CommRing R] [LinearOrder R] {n : ℕ} {s : Set (Fin (n + 1) → R)} (hs : IsSemialgebraic s) (t : R) : IsSemialgebraic {x : Fin n → R | Fin.cons t x ∈ s}

The horizontal section at height t of a semialgebraic subset of Fin (n + 1) → R, whose distinguished coordinate is 0, is semialgebraic.

theorem TauCeti.IsSemialgebraic.preimage_cons_right {R : Type u_3} [CommRing R] [LinearOrder R] {n : ℕ} {s : Set (Fin (n + 1) → R)} (hs : IsSemialgebraic s) (x : Fin n → R) : IsSemialgebraic {y : Fin 1 → R | Fin.cons (y 0) x ∈ s}

The vertical section over a base point x of a semialgebraic subset of Fin (n + 1) → R, whose distinguished coordinate is 0, is semialgebraic as a subset of Fin 1 → R.

Sign-condition normal form

theorem TauCeti.IsSemialgebraic.exists_eq_setOf_sign_eval {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {s : Set (σ → R)} (hs : IsSemialgebraic s) : ∃ (m : ℕ) (p : Fin m → MvPolynomial σ R) (Φ : (Fin m → SignType) → Prop), s = {x : σ → R | Φ fun (i : Fin m) => SignType.sign ((MvPolynomial.eval x) (p i))}

Sign-condition normal form. Every semialgebraic set is described by a condition on the signs of finitely many polynomials.

theorem TauCeti.IsSemialgebraic.exists_finset_mem_iff_of_eqOn {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] {s : Set (σ → R)} (hs : IsSemialgebraic s) : ∃ (F : Finset σ), ∀ (x y : σ → R), Set.EqOn x y ↑F → (x ∈ s ↔ y ∈ s)

Finitely many coordinates. Membership in a semialgebraic set depends on only finitely many coordinates: those of the variables of the polynomials describing it.

Projection closure

class TauCeti.HasSemialgebraicProjections (R : Type u_3) [CommRing R] [LinearOrder R] : Prop

Semialgebraic subsets of the coordinate spaces over R have semialgebraic projections if, for every n, forgetting the coordinate 0 (Fin.tail) maps semialgebraic subsets of Fin (n + 1) → R to semialgebraic subsets of Fin n → R. For R = ℝ this is the Tarski–Seidenberg theorem, proved by cylindrical algebraic decomposition in TauCeti.Geometry.RealAlgebraic.CAD.Existence. It fails for some ordered fields: over ℚ, forgetting t maps the parabola {(t, x) | t ^ 2 = x} to the set of rational squares, which is dense and codense in the positive rationals and so is not semialgebraic.

• isSemialgebraic_image_tail {n : ℕ} {s : Set (Fin (n + 1) → R)} : IsSemialgebraic s → IsSemialgebraic (Fin.tail '' s)

  Forgetting the coordinate 0 maps semialgebraic sets to semialgebraic sets.