The Nash inverse function theorem

A map between finite real coordinate spaces whose coordinates are Nash germs and whose Fréchet derivative is invertible admits a local Nash inverse. Both the source and target can be chosen open and semialgebraic, with semialgebraic graphs in both directions, inside any prescribed source neighbourhood. Nashness holds at every point of these domains, not just at the original point. The local inverse supplied by the native inverse function theorem has the same Nash germ.

The analytic inverse function theorem supplies convergence and local bijectivity. The local Nash graph criterion supplies semialgebraic coordinate graphs on a common neighbourhood; exchanging graph coordinates then proves Nashness of the analytic inverse.

References

• J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Springer, 1998, Section 8.1.
• S. G. Krantz, H. R. Parks, A Primer of Real Analytic Functions, second edition, Birkhäuser, 2002, Chapter 2.

theorem TauCeti.exists_openPartialHomeomorph_of_forall_isNashAt {σ : Type u_1} {τ : Type u_2} [Fintype σ] [Fintype τ] {f : (σ → ℝ) → τ → ℝ} {a : σ → ℝ} (hf : ∀ (i : τ), IsNashAt (fun (x : σ → ℝ) => f x i) a) {L : (σ → ℝ) ≃L[ℝ] τ → ℝ} (hL : fderiv ℝ f a = ↑L) {s : Set (σ → ℝ)} (hs : s ∈ nhds a) : ∃ (Θ : OpenPartialHomeomorph (σ → ℝ) (τ → ℝ)), ↑Θ = f ∧ a ∈ Θ.source ∧ Θ.source ⊆ s ∧ IsSemialgebraicOn (↑Θ) Θ.source ∧ IsSemialgebraicOn (↑Θ.symm) Θ.target ∧ (∀ x ∈ Θ.source, ∀ (i : τ), IsNashAt (fun (z : σ → ℝ) => f z i) x) ∧ ∀ y ∈ Θ.target, ∀ (i : σ), IsNashAt (fun (z : τ → ℝ) => ↑Θ.symm z i) y

The Nash inverse function theorem. A map with Nash coordinate germs and invertible Fréchet derivative at a restricts, inside any prescribed neighbourhood, to a local homeomorphism with open semialgebraic source and target and semialgebraic graphs in both directions. Every coordinate of the map and its inverse is Nash throughout those domains. Empty coordinate index types are allowed.

theorem HasStrictFDerivAt.isNashAt_localInverse {σ : Type u_1} {τ : Type u_2} [Fintype σ] [Fintype τ] {f : (σ → ℝ) → τ → ℝ} {a : σ → ℝ} {L : (σ → ℝ) ≃L[ℝ] τ → ℝ} (hL : HasStrictFDerivAt f (↑L) a) (hf : ∀ (i : τ), TauCeti.IsNashAt (fun (x : σ → ℝ) => f x i) a) (i : σ) : TauCeti.IsNashAt (fun (y : τ → ℝ) => localInverse f L a hL y i) (f a)

The native local inverse of a map with Nash coordinate germs has Nash coordinate germs. The invertible strict derivative is the same one used by the native construction.