The local Nash graph criterion

A continuous real function satisfying one nonzero polynomial relation on an open semialgebraic domain has a semialgebraic graph. Consequently a function is a Nash germ precisely when it is analytic and has a semialgebraic graph on some open semialgebraic neighbourhood. The same holds for a map between finite-dimensional coordinate spaces, read coordinatewise.

On the locus where the specialized polynomial is nonzero, a CAD adapted to its Collins projection and to the domain gives finitely many connected base cells. A continuous root chooses one fixed section over each cell. The native delineation handles repeated roots directly, so no squarefree hypothesis is required. A nonzero coefficient has dense nonvanishing locus; continuity recovers the entire graph, including the nullified fibres, from the closure of the graph over this locus. In particular, no arbitrary values can be assigned on a nullified fibre.

References

• J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Springer, 1998, Section 8.1.
• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapters 10 and 11 (Collins projection and delineability).

theorem TauCeti.isSemialgebraicOn_of_polynomial_relation_of_not_nullified {σ : Type u_1} [Finite σ] {s : Set (σ → ℝ)} {f : (σ → ℝ) → ℝ} (hs : IsSemialgebraic s) (hf : ContinuousOn f s) (P : Polynomial (MvPolynomial σ ℝ)) (hne : ∀ x ∈ s, Polynomial.map (MvPolynomial.eval x) P ≠ 0) (hrel : ∀ x ∈ s, (Polynomial.map (MvPolynomial.eval x) P).IsRoot (f x)) : IsSemialgebraicOn (fun (x : σ → ℝ) (x_1 : Unit) => f x) s

On a semialgebraic domain, a continuous root of a nowhere-nullified polynomial relation has semialgebraic graph. No openness or simplicity of the roots is required.

theorem TauCeti.isSemialgebraicOn_of_polynomial_relation {σ : Type u_1} [Finite σ] {s : Set (σ → ℝ)} {f : (σ → ℝ) → ℝ} (hs : IsSemialgebraic s) (hso : IsOpen s) (hf : ContinuousOn f s) (P : Polynomial (MvPolynomial σ ℝ)) (hP : P ≠ 0) (hrel : ∀ x ∈ s, (Polynomial.map (MvPolynomial.eval x) P).IsRoot (f x)) : IsSemialgebraicOn (fun (x : σ → ℝ) (x_1 : Unit) => f x) s

A continuous function satisfying a single nonzero polynomial relation on an open semialgebraic domain has semialgebraic graph, including over nullified fibres.

theorem TauCeti.isNashAt_iff_exists_isSemialgebraicOn {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ} {x : σ → ℝ} : IsNashAt f x ↔ AnalyticAt ℝ f x ∧ ∃ (U : Set (σ → ℝ)), IsOpen U ∧ x ∈ U ∧ IsSemialgebraic U ∧ IsSemialgebraicOn (fun (y : σ → ℝ) (x : Unit) => f y) U

The local Nash graph criterion. A scalar function is a Nash germ at x exactly when it is analytic there and its graph is semialgebraic on some open semialgebraic neighbourhood.

theorem TauCeti.exists_isSemialgebraicOn_of_forall_isNashAt {σ : Type u_1} {ι : Type u_2} [Fintype σ] [Finite ι] {f : ι → (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : ∀ (i : ι), IsNashAt (f i) x) : ∃ (U : Set (σ → ℝ)), IsOpen U ∧ x ∈ U ∧ IsSemialgebraic U ∧ ∀ (i : ι), IsSemialgebraicOn (fun (y : σ → ℝ) (x : Unit) => f i y) U

Finitely many Nash germs have semialgebraic graphs on one common open semialgebraic neighbourhood. This includes the empty family.

theorem TauCeti.forall_isNashAt_apply_iff_exists_isSemialgebraicOn {σ : Type u_1} {τ : Type u_2} [Fintype σ] [Fintype τ] {g : (σ → ℝ) → τ → ℝ} {x : σ → ℝ} : (∀ (i : τ), IsNashAt (fun (y : σ → ℝ) => g y i) x) ↔ AnalyticAt ℝ g x ∧ ∃ (U : Set (σ → ℝ)), IsOpen U ∧ x ∈ U ∧ IsSemialgebraicOn g U

The local Nash graph criterion for maps. The coordinates of a map between finite-dimensional coordinate spaces are Nash germs at x exactly when the map is analytic at x and its graph is semialgebraic on some open semialgebraic neighbourhood of x.