Images and composition of semialgebraic functions

Let R be a commutative ring with a compatible linear order, and 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 develops the parts of the theory of semialgebraic sets and functions that need projection.

Eliminating one coordinate at a time, the projection of a semialgebraic subset of σ ⊕ τ → R onto the coordinates τ is semialgebraic whenever σ is finite. Since the graph of a function f : (σ → R) → (τ → R) is encoded as a subset of σ ⊕ τ → R (TauCeti.IsSemialgebraicOn), this gives the following consequences.

• The image of a semialgebraic set under a semialgebraic function with finitely many input coordinates is semialgebraic, and so is the inverse image of a semialgebraic set under a semialgebraic function with finitely many output coordinates.
• The domain of a function with finitely many output coordinates and semialgebraic graph is the projection of that graph, so it is semialgebraic: the domain hypothesis in TauCeti.IsSemialgebraicOn becomes redundant.
• Semialgebraic functions compose when the intermediate space has finitely many coordinates: the graph of g ∘ f is obtained from the graphs of f and g by eliminating the intermediate coordinates.
• Composing the pair of two semialgebraic functions with a polynomial map shows that pointwise sums, products, and differences of semialgebraic functions with finitely many output coordinates are semialgebraic, and that the loci where two of them agree, or are ordered, are semialgebraic.

Main results

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

• TauCeti.IsSemialgebraic.image_comp_inr, TauCeti.IsSemialgebraic.image_comp_inl: projections of semialgebraic sets that forget finitely many coordinates are semialgebraic.
• TauCeti.IsSemialgebraic.setOf_exists_sumElim, TauCeti.IsSemialgebraic.setOf_forall_sumElim: quantification over finitely many coordinates.
• TauCeti.IsSemialgebraicOn.isSemialgebraic_image, TauCeti.IsSemialgebraicMap.isSemialgebraic_image: images under semialgebraic functions with finitely many input coordinates; TauCeti.IsSemialgebraic.image_eval: images under polynomial maps with finitely many input and output coordinates; TauCeti.IsSemialgebraic.image_comp: images under changes of coordinates, such as coordinate projections.
• TauCeti.IsSemialgebraicOn.isSemialgebraic_inter_preimage, TauCeti.IsSemialgebraicMap.isSemialgebraic_preimage: inverse images under semialgebraic functions with finitely many output coordinates.
• TauCeti.isSemialgebraicOn_iff_graph: a function with finitely many output coordinates is semialgebraic on s exactly when its graph over s is semialgebraic.
• TauCeti.IsSemialgebraicOn.comp, TauCeti.IsSemialgebraicMap.comp: composition, when the intermediate space has finitely many coordinates.
• TauCeti.IsSemialgebraicOn.eval_comp: applying a polynomial map to the values; TauCeti.isSemialgebraicOn_sumElim_iff: a pair is semialgebraic exactly when its components are, and TauCeti.isSemialgebraicOn_pi_iff: so is a function with finitely many output coordinates; TauCeti.IsSemialgebraicOn.add, TauCeti.IsSemialgebraicOn.mul, TauCeti.IsSemialgebraicOn.sub: pointwise arithmetic. Negation needs no projection and is proved in TauCeti.Geometry.RealAlgebraic.Semialgebraic.Function.
• TauCeti.IsSemialgebraicOn.isSemialgebraic_inter_setOf_eq, TauCeti.IsSemialgebraicOn.isSemialgebraic_inter_setOf_le: the loci where two semialgebraic functions agree, or where one is bounded above by the other, are semialgebraic.

References

• S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 2.
• J. Bochnak, M. Coste, and M.-F. Roy, Real Algebraic Geometry, Ergebnisse der Mathematik und ihrer Grenzgebiete 36, Springer (1998), Section 2.2.

theorem TauCeti.IsSemialgebraic.image_comp_inr {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] [Finite σ] {s : Set (σ ⊕ τ → R)} (hs : IsSemialgebraic s) : IsSemialgebraic ((fun (z : σ ⊕ τ → R) => z ∘ Sum.inr) '' s)

Given projection closure, the projection of a semialgebraic subset of σ ⊕ τ → R that forgets the finitely many coordinates σ is semialgebraic.

theorem TauCeti.IsSemialgebraic.image_comp_inl {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] [Finite τ] {s : Set (σ ⊕ τ → R)} (hs : IsSemialgebraic s) : IsSemialgebraic ((fun (z : σ ⊕ τ → R) => z ∘ Sum.inl) '' s)

Given projection closure, the projection of a semialgebraic subset of σ ⊕ τ → R that forgets the finitely many coordinates τ is semialgebraic.

theorem TauCeti.IsSemialgebraic.setOf_exists_sumElim {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] [Finite τ] {s : Set (σ ⊕ τ → R)} (hs : IsSemialgebraic s) : IsSemialgebraic {x : σ → R | ∃ (y : τ → R), Sum.elim x y ∈ s}

Existential quantification over finitely many coordinates preserves semialgebraicity.

theorem TauCeti.IsSemialgebraic.setOf_forall_sumElim {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] [Finite τ] {s : Set (σ ⊕ τ → R)} (hs : IsSemialgebraic s) : IsSemialgebraic {x : σ → R | ∀ (y : τ → R), Sum.elim x y ∈ s}

Universal quantification over finitely many coordinates preserves semialgebraicity.

theorem TauCeti.IsSemialgebraicOn.isSemialgebraic_image {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] [Finite σ] {f : (σ → R) → τ → R} {s : Set (σ → R)} (hf : IsSemialgebraicOn f s) : IsSemialgebraic (f '' s)

Given projection closure, the image of the domain of a semialgebraic function with finitely many input coordinates is semialgebraic.

theorem TauCeti.IsSemialgebraicMap.isSemialgebraic_image {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] [Finite σ] {f : (σ → R) → τ → R} (hf : IsSemialgebraicMap f) {s : Set (σ → R)} (hs : IsSemialgebraic s) : IsSemialgebraic (f '' s)

Given projection closure, the image of a semialgebraic set under a semialgebraic map with finitely many input coordinates is semialgebraic.

theorem TauCeti.IsSemialgebraic.image_eval {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] [Finite σ] [Finite τ] {s : Set (σ → R)} (hs : IsSemialgebraic s) (p : τ → MvPolynomial σ R) : IsSemialgebraic ((fun (x : σ → R) (i : τ) => (MvPolynomial.eval x) (p i)) '' s)

Given projection closure, the image of a semialgebraic set under a polynomial map with finitely many input coordinates and finitely many output coordinates is semialgebraic.

theorem TauCeti.IsSemialgebraic.image_comp {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] [Finite σ] [Finite τ] {s : Set (σ → R)} (hs : IsSemialgebraic s) (f : τ → σ) : IsSemialgebraic ((fun (x : σ → R) => x ∘ f) '' s)

Given projection closure, the image of a semialgebraic set under a change of coordinates x ↦ x ∘ f, such as a coordinate projection, is semialgebraic.

theorem TauCeti.IsSemialgebraicOn.isSemialgebraic_inter_preimage {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] [Finite τ] {f : (σ → R) → τ → R} {s : Set (σ → R)} (hf : IsSemialgebraicOn f s) {t : Set (τ → R)} (ht : IsSemialgebraic t) : IsSemialgebraic (s ∩ f ⁻¹' t)

Given projection closure, the points of the domain of a semialgebraic function with finitely many output coordinates at which it takes values in a semialgebraic set form a semialgebraic set.

theorem TauCeti.IsSemialgebraicMap.isSemialgebraic_preimage {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] [Finite τ] {f : (σ → R) → τ → R} (hf : IsSemialgebraicMap f) {t : Set (τ → R)} (ht : IsSemialgebraic t) : IsSemialgebraic (f ⁻¹' t)

Given projection closure, the inverse image of a semialgebraic set under a semialgebraic map with finitely many output coordinates is semialgebraic.

theorem TauCeti.isSemialgebraicOn_iff_graph {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] [Finite τ] {f : (σ → R) → τ → R} {s : Set (σ → R)} : IsSemialgebraicOn f s ↔ IsSemialgebraic (⇑(Equiv.sumArrowEquivProdArrow σ τ R) ⁻¹' Set.graphOn f s)

Given projection closure, a function with finitely many output coordinates is semialgebraic on s if and only if its graph over s is semialgebraic: the domain s is the projection of the graph.

theorem TauCeti.IsSemialgebraicOn.comp {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] [Finite τ] {g : (τ → R) → υ → R} {f : (σ → R) → τ → R} {s : Set (σ → R)} {t : Set (τ → R)} (hg : IsSemialgebraicOn g t) (hf : IsSemialgebraicOn f s) (hst : Set.MapsTo f s t) : IsSemialgebraicOn (g ∘ f) s

Given projection closure, the composition of semialgebraic functions is semialgebraic: if f is semialgebraic on s and maps it into t, and g is semialgebraic on t, then g ∘ f is semialgebraic on s. The intermediate space has finitely many coordinates.

theorem TauCeti.IsSemialgebraicMap.comp {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] [Finite τ] {g : (τ → R) → υ → R} {f : (σ → R) → τ → R} (hg : IsSemialgebraicMap g) (hf : IsSemialgebraicMap f) : IsSemialgebraicMap (g ∘ f)

Given projection closure, the composition of semialgebraic maps is semialgebraic when the intermediate space has finitely many coordinates.

Polynomial operations on semialgebraic functions

theorem TauCeti.IsSemialgebraicOn.eval_comp {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] {f : (σ → R) → τ → R} {s : Set (σ → R)} [Finite τ] [Finite υ] (hf : IsSemialgebraicOn f s) (p : υ → MvPolynomial τ R) : IsSemialgebraicOn (fun (x : σ → R) (i : υ) => (MvPolynomial.eval (f x)) (p i)) s

Given projection closure, applying a polynomial map to the values of a semialgebraic function with finitely many output coordinates gives a semialgebraic function.

@[simp]

theorem TauCeti.isSemialgebraicOn_sumElim_iff {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] {τ' : Type u_5} {f : (σ → R) → τ → R} {s : Set (σ → R)} [Finite τ] [Finite τ'] {g : (σ → R) → τ' → R} : IsSemialgebraicOn (fun (x : σ → R) => Sum.elim (f x) (g x)) s ↔ IsSemialgebraicOn f s ∧ IsSemialgebraicOn g s

Given projection closure, a pair of functions with finitely many output coordinates is semialgebraic exactly when both of its components are.

theorem TauCeti.isSemialgebraicOn_pi_iff {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] {f : (σ → R) → τ → R} {s : Set (σ → R)} [Finite τ] : IsSemialgebraicOn f s ↔ IsSemialgebraic s ∧ ∀ (i : τ), IsSemialgebraicOn (fun (x : σ → R) (x_1 : Unit) => f x i) s

Given projection closure, a function with finitely many output coordinates is semialgebraic on s exactly when s is semialgebraic and each coordinate of the function is semialgebraic on s.

theorem TauCeti.IsSemialgebraicOn.add {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] {f : (σ → R) → τ → R} {s : Set (σ → R)} [Finite τ] {g : (σ → R) → τ → R} (hf : IsSemialgebraicOn f s) (hg : IsSemialgebraicOn g s) : IsSemialgebraicOn (f + g) s

Given projection closure, the pointwise sum of semialgebraic functions is semialgebraic.

theorem TauCeti.IsSemialgebraicOn.mul {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] {f : (σ → R) → τ → R} {s : Set (σ → R)} [Finite τ] {g : (σ → R) → τ → R} (hf : IsSemialgebraicOn f s) (hg : IsSemialgebraicOn g s) : IsSemialgebraicOn (f * g) s

Given projection closure, the pointwise product of semialgebraic functions is semialgebraic.

theorem TauCeti.IsSemialgebraicOn.sub {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] {f : (σ → R) → τ → R} {s : Set (σ → R)} [Finite τ] {g : (σ → R) → τ → R} (hf : IsSemialgebraicOn f s) (hg : IsSemialgebraicOn g s) : IsSemialgebraicOn (f - g) s

Given projection closure, the pointwise difference of semialgebraic functions is semialgebraic.

theorem TauCeti.IsSemialgebraicMap.add {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] {f : (σ → R) → τ → R} [Finite τ] {g : (σ → R) → τ → R} (hf : IsSemialgebraicMap f) (hg : IsSemialgebraicMap g) : IsSemialgebraicMap (f + g)

Given projection closure, the pointwise sum of semialgebraic maps is semialgebraic.

theorem TauCeti.IsSemialgebraicMap.mul {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] {f : (σ → R) → τ → R} [Finite τ] {g : (σ → R) → τ → R} (hf : IsSemialgebraicMap f) (hg : IsSemialgebraicMap g) : IsSemialgebraicMap (f * g)

Given projection closure, the pointwise product of semialgebraic maps is semialgebraic.

theorem TauCeti.IsSemialgebraicMap.sub {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] {f : (σ → R) → τ → R} [Finite τ] {g : (σ → R) → τ → R} (hf : IsSemialgebraicMap f) (hg : IsSemialgebraicMap g) : IsSemialgebraicMap (f - g)

Given projection closure, the pointwise difference of semialgebraic maps is semialgebraic.

theorem TauCeti.IsSemialgebraicOn.isSemialgebraic_inter_setOf_eq {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] {f : (σ → R) → τ → R} {s : Set (σ → R)} [Finite τ] {g : (σ → R) → τ → R} (hf : IsSemialgebraicOn f s) (hg : IsSemialgebraicOn g s) : IsSemialgebraic (s ∩ {x : σ → R | f x = g x})

Given projection closure, the points of the common domain at which two semialgebraic functions agree form a semialgebraic set.

theorem TauCeti.IsSemialgebraicOn.isSemialgebraic_inter_setOf_le {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommRing R] [LinearOrder R] [HasSemialgebraicProjections R] {f : (σ → R) → τ → R} {s : Set (σ → R)} [Finite τ] {g : (σ → R) → τ → R} [IsOrderedAddMonoid R] (hf : IsSemialgebraicOn f s) (hg : IsSemialgebraicOn g s) : IsSemialgebraic (s ∩ {x : σ → R | f x ≤ g x})

Given projection closure, the points of the common domain at which one semialgebraic function is bounded above by another, coordinatewise, form a semialgebraic set.