Documentation

TauCeti.Geometry.RealAlgebraic.Semialgebraic.QuantifierElimination

Quantifier elimination from projection closure #

Let R be a commutative ring with a compatible linear order, regarded as a structure in the first-order language of ordered rings Language.ring.sum Language.order. Suppose that semialgebraic sets are closed under projection: for every semialgebraic s ⊆ R ^ (n + 1), the image Fin.tail '' s ⊆ R ^ n forgetting coordinate 0 is semialgebraic (TauCeti.HasSemialgebraicProjections R). For ℝ this is the Tarski–Seidenberg theorem, an instance proved in TauCeti.Geometry.RealAlgebraic.CAD.Existence, so every result below holds over ℝ unconditionally. This file shows that projection closure gives quantifier elimination in the language of ordered rings, with parameters from R.

The argument is by induction on formulas. Atomic formulas define semialgebraic sets, and so do implications of semialgebraic conditions. An existential quantifier over the last bound variable is a projection of a semialgebraic set; a universal quantifier is the complement of the existential quantifier of the complement. The projection hypothesis concerns R ^ (n + 1) only, but formulas may have infinitely many free variables (the parameters are free variables indexed by R). Since membership in a semialgebraic set depends on only finitely many coordinates (TauCeti.IsSemialgebraic.exists_finset_mem_iff_of_eqOn), projections in arbitrary dimension reduce to the finite-dimensional case.

Main results #

All results but the last assume projection closure, [TauCeti.HasSemialgebraicProjections R].

References #

source
theorem TauCeti.IsSemialgebraic.image_comp_some {R : Type u_1} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] {σ : Type u_2} {s : Set (Option σ → R)} (hs : IsSemialgebraic s) :
IsSemialgebraic ((fun (x : Option σ → R) => x ∘ some) '' s)

Projection in arbitrary dimension. If semialgebraic subsets of R ^ (n + 1) have semialgebraic projections to R ^ n, then for every index type σ the projection of a semialgebraic subset of Option σ → R, forgetting the coordinate none, is semialgebraic.

source
theorem FirstOrder.Language.BoundedFormula.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] [TauCeti.HasSemialgebraicProjections R] {α : Type u_2} {n : ℕ} (φ : (ring.sum Language.order).BoundedFormula α n) :
TauCeti.IsSemialgebraic {x : α ⊕ Fin n → R | φ.Realize (x ∘ Sum.inl) (x ∘ Sum.inr)}

Given projection closure, a formula of ordered rings with free variables α and n bound variables defines a semialgebraic subset of α ⊕ Fin n → R.

source
theorem FirstOrder.Language.Formula.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] [TauCeti.HasSemialgebraicProjections R] {α : Type u_2} (φ : (ring.sum Language.order).Formula α) :
TauCeti.IsSemialgebraic {v : α → R | φ.Realize v}

Given projection closure, a formula of ordered rings with free variables α defines a semialgebraic subset of α → R.

source
theorem FirstOrder.Language.Formula.isSemialgebraic_setOf_realize_sumElim {R : Type u_1} [CommRing R] [Ring.CompatibleRing R] [Language.order.Structure R] [LinearOrder R] [IsOrderedAddMonoid R] [(ring.sum Language.order).OrderedStructure R] [TauCeti.HasSemialgebraicProjections R] {A : Type u_2} {σ : Type u_3} (φ : (ring.sum Language.order).Formula (A ⊕ σ)) (f : A → R) :
TauCeti.IsSemialgebraic {v : σ → R | φ.Realize (Sum.elim f v)}

Given projection closure, a formula of ordered rings with free variables A ⊕ σ defines a semialgebraic subset of σ → R once the variables Sum.inl a are assigned parameters f a.

source
theorem Set.Definable.isSemialgebraic {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] [TauCeti.HasSemialgebraicProjections R] {σ : Type u_2} {A : Set R} {s : Set (σ → R)} (hs : A.Definable (FirstOrder.Language.ring.sum FirstOrder.Language.order) s) :
TauCeti.IsSemialgebraic s

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

source
theorem TauCeti.isSemialgebraic_iff_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] [HasSemialgebraicProjections R] {σ : Type u_2} {s : Set (σ → R)} :
IsSemialgebraic s ↔ Set.univ.Definable (FirstOrder.Language.ring.sum FirstOrder.Language.order) s

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

source
theorem TauCeti.exists_isQF_realize_iff {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] [HasSemialgebraicProjections R] {σ : Type u_2} (φ : (FirstOrder.Language.ring.sum FirstOrder.Language.order).Formula (R ⊕ σ)) :
∃ (ψ : (FirstOrder.Language.ring.sum FirstOrder.Language.order).Formula (R ⊕ σ)), FirstOrder.Language.BoundedFormula.IsQF ψ ∧ ∀ (v : σ → R), φ.Realize (Sum.elim id v) ↔ ψ.Realize (Sum.elim id v)

Quantifier elimination, given projection closure. Every formula of ordered rings whose free variables Sum.inl r are assigned the parameters r ∈ R is equivalent, for every assignment v of the remaining free variables, to a quantifier-free formula with parameters.

source
theorem TauCeti.hasSemialgebraicProjections_iff_forall_definable_isSemialgebraic {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] :
HasSemialgebraicProjections R ↔ ∀ (n : ℕ) (s : Set (Fin n → R)), Set.univ.Definable (FirstOrder.Language.ring.sum FirstOrder.Language.order) s → IsSemialgebraic s

Projection closure is equivalent to quantifier elimination. Semialgebraic subsets of R ^ (n + 1) have semialgebraic projections to R ^ n, for every n, if and only if every subset of every R ^ n definable with parameters in the language of ordered rings is semialgebraic.