Graph coordinates over the tangent space

Let F : E → V be a C^n map, 1 ≤ n, from an open subset U of a finite-dimensional real normed space into a real inner product space, and let u₀ ∈ U be a point at which the differential of F is injective. Its image R is the tangent space of F at u₀. The orthogonal projection of F onto R is a local diffeomorphism near u₀, by the inverse function theorem, so near u₀ the map F is a graph over R: in the coordinate given by that projection, F = w + h(w) with h(w) ∈ Rᗮ. This is the normal form of an immersion into an inner product space used to perturb distance functions along immersed submanifolds.

Main results

• ContDiffOn.exists_openPartialHomeomorph_starProjection: a chart Φ of E around u₀, C^n with invertible differential on its source and with C^n inverse, in which the orthogonal projection of F onto its tangent space at u₀ is a fixed linear isomorphism.

References

• V. Guillemin and A. Pollack, Differential Topology, Prentice-Hall, 1974, Chapter 1, §3, for the local immersion theorem.

theorem ContDiffOn.exists_openPartialHomeomorph_starProjection {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {F : E → V} {U : Set E} {n : WithTop ℕ∞} (hF : ContDiffOn ℝ n F U) (hU : IsOpen U) (hn : 1 ≤ n) {u₀ : E} (hu₀ : u₀ ∈ U) (hinj : Function.Injective ⇑(fderiv ℝ F u₀)) : ∃ (e₀ : E ≃L[ℝ] ↥(↑(fderiv ℝ F u₀)).range) (Φ : OpenPartialHomeomorph E E), u₀ ∈ Φ.source ∧ Φ.source ⊆ U ∧ (∀ u ∈ Φ.source, ↑(e₀ (↑Φ u)) = (↑(fderiv ℝ F u₀)).range.starProjection (F u)) ∧ (∀ u ∈ Φ.source, ContDiffAt ℝ n (↑Φ) u ∧ (fderiv ℝ (↑Φ) u).IsInvertible) ∧ ∀ w ∈ Φ.target, ContDiffAt ℝ n (↑Φ.symm) w

Graph coordinates. Near a point u₀ at which its differential is injective, a C^n map F into an inner product space is a graph over its tangent space R at u₀: there is a chart Φ of E around u₀, C^n with invertible differential on its source and with C^n inverse, in which the orthogonal projection of F onto R is a fixed linear isomorphism e₀ : E ≃ R.