Semialgebraic functions

A function between coordinate spaces is semialgebraic on a set when its domain and graph are semialgebraic. The graph is regarded as a subset of the coordinate space indexed by the disjoint union of the input and output coordinates. Requiring the specified domain to be semialgebraic is useful before projection closure is available: semialgebraicity of a graph alone does not yet let us recover its projection onto the input coordinates.

This file gives the graph predicate its basic API. It proves restriction, congruence, and piecewise-gluing laws and shows that polynomial maps, and more generally functions whose graph over a semialgebraic domain is cut out by polynomial equations (TauCeti.isSemialgebraicOn_of_forall_eq_iff), are semialgebraic. It also proves the operations whose graphs are inverse images of the given graphs, so that no coordinate has to be eliminated: pairing two functions on the same domain (TauCeti.IsSemialgebraicOn.sumElim), assembling a function from its coordinates (TauCeti.IsSemialgebraicOn.pi), precomposition with a polynomial map (TauCeti.IsSemialgebraicOn.comp_eval), pointwise negation (TauCeti.IsSemialgebraicOn.neg), and bijective changes of the input or output coordinates (TauCeti.isSemialgebraicOn_preimage_comp_equiv_iff, TauCeti.isSemialgebraicOn_comp_equiv_iff). It deliberately does not assert closure under arbitrary composition, whose graph generally requires eliminating the intermediate coordinates; images, inverse images, composition, and pointwise sums, products, and differences are derived from projection closure in TauCeti.Geometry.RealAlgebraic.Semialgebraic.Image.

References

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

TauCeti.isSemialgebraicOn_of_forall_eq_iff is adapted from its complex-coordinate counterpart TauCeti.isSemialgebraicOn_complexToRealPi_of_forall_eq_iff in TauCeti.Geometry.RealAlgebraic.Semialgebraic.Complex.

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

A function f : (σ → R) → (τ → R) is semialgebraic on s if s is semialgebraic and the graph of f over s, encoded in the coordinate space σ ⊕ τ → R, is semialgebraic.

def TauCeti.IsSemialgebraicMap {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] (f : (σ → R) → τ → R) : Prop

A function between coordinate spaces is semialgebraic if its graph over the whole input space is semialgebraic.

@[simp]

theorem TauCeti.isSemialgebraicOn_univ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {f : (σ → R) → τ → R} : IsSemialgebraicOn f Set.univ ↔ IsSemialgebraicMap f

Semialgebraicity on the whole domain is semialgebraicity as a map.

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

Characterization of a function being semialgebraic on a specified domain.

theorem TauCeti.isSemialgebraicMap_def {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {f : (σ → R) → τ → R} : IsSemialgebraicMap f ↔ IsSemialgebraic (⇑(Equiv.sumArrowEquivProdArrow σ τ R) ⁻¹' Set.graphOn f Set.univ)

Characterization of a semialgebraic map by its graph.

theorem TauCeti.mem_preimage_sumArrowEquivProdArrow_graphOn {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {f : (σ → R) → τ → R} {s : Set (σ → R)} {z : σ ⊕ τ → R} : z ∈ ⇑(Equiv.sumArrowEquivProdArrow σ τ R) ⁻¹' Set.graphOn f s ↔ z ∘ Sum.inl ∈ s ∧ f (z ∘ Sum.inl) = z ∘ Sum.inr

A point of σ ⊕ τ → R lies on the encoded graph of f over s exactly when its input coordinates lie in s and f sends them to its output coordinates.

theorem TauCeti.mem_preimage_sumArrowEquivProdArrow_scalar_graphOn {σ : Type u_1} {R : Type u_3} {f : (σ → R) → R} {s : Set (σ → R)} {z : σ ⊕ Unit → R} : z ∈ ⇑(Equiv.sumArrowEquivProdArrow σ Unit R) ⁻¹' Set.graphOn (fun (x : σ → R) (x_1 : Unit) => f x) s ↔ z ∘ Sum.inl ∈ s ∧ f (z ∘ Sum.inl) = z (Sum.inr ())

Membership in a scalar graph encoded using Unit output coordinates is given by the input-domain condition and equality of the scalar output coordinate.

theorem TauCeti.IsSemialgebraicOn.isSemialgebraic {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {f : (σ → R) → τ → R} {s : Set (σ → R)} (hf : IsSemialgebraicOn f s) : IsSemialgebraic s

The domain of a function semialgebraic on a set is semialgebraic.

theorem TauCeti.IsSemialgebraicOn.graph {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {f : (σ → R) → τ → R} {s : Set (σ → R)} (hf : IsSemialgebraicOn f s) : IsSemialgebraic (⇑(Equiv.sumArrowEquivProdArrow σ τ R) ⁻¹' Set.graphOn f s)

The graph of a function semialgebraic on a set is semialgebraic.

theorem TauCeti.IsSemialgebraicOn.mono {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {f : (σ → R) → τ → R} {s t : Set (σ → R)} (hf : IsSemialgebraicOn f s) (ht : IsSemialgebraic t) (h : t ⊆ s) : IsSemialgebraicOn f t

Restricting a semialgebraic function to a semialgebraic subset preserves semialgebraicity.

theorem TauCeti.IsSemialgebraicMap.isSemialgebraicOn {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {f : (σ → R) → τ → R} (hf : IsSemialgebraicMap f) {s : Set (σ → R)} (hs : IsSemialgebraic s) : IsSemialgebraicOn f s

A semialgebraic map is semialgebraic on every semialgebraic domain.

theorem TauCeti.IsSemialgebraicOn.congr {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {f g : (σ → R) → τ → R} {s : Set (σ → R)} (hf : IsSemialgebraicOn f s) (h : Set.EqOn f g s) : IsSemialgebraicOn g s

Semialgebraicity on a set depends only on the values of the function on that set.

@[simp]

theorem TauCeti.isSemialgebraicOn_empty {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] (f : (σ → R) → τ → R) : IsSemialgebraicOn f ∅

Every function is semialgebraic on the empty set.

theorem TauCeti.IsSemialgebraicOn.glue {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {f g h : (σ → R) → τ → R} {s t : Set (σ → R)} (hf : IsSemialgebraicOn f (s ∩ t)) (hg : IsSemialgebraicOn g (s \ t)) (hft : Set.EqOn h f (s ∩ t)) (hgt : Set.EqOn h g (s \ t)) : IsSemialgebraicOn h s

Semialgebraic functions on two semialgebraic pieces glue to a semialgebraic function.

theorem TauCeti.isSemialgebraicOn_of_forall_eq_iff {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {ι : Type u_4} [Finite ι] {f : (σ → R) → τ → R} {s : Set (σ → R)} (hs : IsSemialgebraic s) (p : ι → MvPolynomial (σ ⊕ τ) R) (hp : ∀ x ∈ s, ∀ (y : τ → R), f x = y ↔ ∀ (k : ι), (MvPolynomial.eval (Sum.elim x y)) (p k) = 0) : IsSemialgebraicOn f s

A function is semialgebraic on a semialgebraic domain s when its graph over s is cut out by finitely many polynomial equations in the input and output coordinates: for x ∈ s, f x = y exactly when every p k vanishes at Sum.elim x y.

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

A map whose output coordinates are polynomials in the input coordinates is semialgebraic on every semialgebraic domain.

theorem TauCeti.isSemialgebraicMap_eval {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] [Finite τ] (p : τ → MvPolynomial σ R) : IsSemialgebraicMap fun (x : σ → R) (i : τ) => (MvPolynomial.eval x) (p i)

A polynomial map between coordinate spaces is semialgebraic.

theorem TauCeti.isSemialgebraicOn_const {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] [Finite τ] (c : τ → R) {s : Set (σ → R)} (hs : IsSemialgebraic s) : IsSemialgebraicOn (fun (x : σ → R) => c) s

A constant map into a finite-dimensional coordinate space is semialgebraic on every semialgebraic domain.

@[simp]

theorem TauCeti.isSemialgebraicMap_const {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] [Finite τ] (c : τ → R) : IsSemialgebraicMap fun (x : σ → R) => c

A constant map into a finite-dimensional coordinate space is semialgebraic.

@[simp]

theorem TauCeti.isSemialgebraicMap_id {σ : Type u_1} {R : Type u_3} [CommRing R] [LinearOrder R] [Finite σ] : IsSemialgebraicMap id

The identity map on a finite-dimensional coordinate space is semialgebraic.

theorem TauCeti.IsSemialgebraicOn.sumElim {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {τ' : Type u_5} {f : (σ → R) → τ → R} {g : (σ → R) → τ' → R} {s : Set (σ → R)} (hf : IsSemialgebraicOn f s) (hg : IsSemialgebraicOn g s) : IsSemialgebraicOn (fun (x : σ → R) => Sum.elim (f x) (g x)) s

Pairing two semialgebraic functions on the same domain gives a semialgebraic function into the coordinate space indexed by the disjoint union of their output coordinates. No projection is needed: the graph of the pair is the intersection of the inverse images of the two graphs.

theorem TauCeti.IsSemialgebraicMap.sumElim {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {τ' : Type u_5} {f : (σ → R) → τ → R} {g : (σ → R) → τ' → R} (hf : IsSemialgebraicMap f) (hg : IsSemialgebraicMap g) : IsSemialgebraicMap fun (x : σ → R) => Sum.elim (f x) (g x)

Pairing two semialgebraic maps gives a semialgebraic map.

theorem TauCeti.IsSemialgebraicOn.pi {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] [Finite τ] {f : (σ → R) → τ → R} {s : Set (σ → R)} (hs : IsSemialgebraic s) (hf : ∀ (i : τ), IsSemialgebraicOn (fun (x : σ → R) (x_1 : Unit) => f x i) s) : IsSemialgebraicOn f s

A function with finitely many output coordinates is semialgebraic on a semialgebraic domain if each of its coordinates is. No projection is needed: the graph is the intersection of the inverse images of the graphs of the coordinates.

theorem TauCeti.IsSemialgebraicOn.comp_eval {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {σ' : Type u_4} {f : (σ → R) → τ → R} {s : Set (σ → R)} (hf : IsSemialgebraicOn f s) (p : σ → MvPolynomial σ' R) : IsSemialgebraicOn (f ∘ fun (x : σ' → R) (i : σ) => (MvPolynomial.eval x) (p i)) ((fun (x : σ' → R) (i : σ) => (MvPolynomial.eval x) (p i)) ⁻¹' s)

Precomposing a semialgebraic function with a polynomial map gives a semialgebraic function on the inverse image of its domain. No projection is needed: the new graph is the inverse image of the old one under a polynomial map.

theorem TauCeti.IsSemialgebraicMap.comp_eval {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {σ' : Type u_4} {f : (σ → R) → τ → R} (hf : IsSemialgebraicMap f) (p : σ → MvPolynomial σ' R) : IsSemialgebraicMap (f ∘ fun (x : σ' → R) (i : σ) => (MvPolynomial.eval x) (p i))

Precomposing a semialgebraic map with a polynomial map gives a semialgebraic map.

theorem TauCeti.IsSemialgebraicOn.neg {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {f : (σ → R) → τ → R} {s : Set (σ → R)} (hf : IsSemialgebraicOn f s) : IsSemialgebraicOn (-f) s

The pointwise negation of a semialgebraic function is semialgebraic. No projection is needed: the new graph is the inverse image of the old one under negation of the output coordinates.

theorem TauCeti.IsSemialgebraicMap.neg {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [LinearOrder R] {f : (σ → R) → τ → R} (hf : IsSemialgebraicMap f) : IsSemialgebraicMap (-f)

The pointwise negation of a semialgebraic map is semialgebraic.

@[simp]

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

Semialgebraicity of a function is invariant under a bijective change of input coordinates, such as a permutation, applied to both the function and its domain.

@[simp]

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

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