Smooth local normal coordinates

For a map g : E → V into a finite-dimensional real inner product space, fix the normal space at u₀. The map normalParametrization g u₀ sends (u, w) to g u plus the orthogonal projection of w onto the normal space at u. For a C^(n+1) immersion this map is C^n, and near (u₀, 0) it is a partial diffeomorphism with a C^n inverse. These are the local coordinates of the addition map on the normal bundle, used to upgrade a topological tubular neighbourhood to a smooth one. No compactness or global injectivity of the immersion is required.

The derivative at the zero section is (du, dw) ↦ Dg du + dw. Mathlib's product decomposition for complementary subspaces identifies it as an isomorphism, and the inverse function theorem supplies regularity on the whole inverse chart.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), the normal-bundle addition map and proof of Theorem 6.24.

noncomputable def TauCeti.normalParametrization {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (g : E → V) (u₀ : E) : E × ↥(↑(fderiv ℝ g u₀)).rangeᗮ → V

The normal-bundle addition map in projected coordinates from the normal space at u₀.

@[simp]

theorem TauCeti.normalParametrization_apply {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (g : E → V) (u₀ : E) (p : E × ↥(↑(fderiv ℝ g u₀)).rangeᗮ) : normalParametrization g u₀ p = g p.1 + (↑(fderiv ℝ g p.1)).rangeᗮ.starProjection ↑p.2

The parametrization adds the projected reference normal vector to the core map.

theorem TauCeti.contDiffAt_normalParametrization {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {g : E → V} (u₀ : E) {n : WithTop ℕ∞} {p : E × ↥(↑(fderiv ℝ g u₀)).rangeᗮ} (hg : ContDiffAt ℝ (n + 1) g p.1) (hinj : Function.Injective ⇑(fderiv ℝ g p.1)) : ContDiffAt ℝ n (normalParametrization g u₀) p

Normal parametrizations lose one derivative, just as the normal projection does. Only injectivity of the differential at the base point of p is needed.

theorem TauCeti.hasFDerivAt_normalParametrization {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {g : E → V} {u₀ : E} (hg : ContDiffAt ℝ 2 g u₀) (hinj : Function.Injective ⇑(fderiv ℝ g u₀)) : HasFDerivAt (normalParametrization g u₀) ((fderiv ℝ g u₀).coprod (↑(fderiv ℝ g u₀)).rangeᗮ.subtypeL) (u₀, 0)

At the zero section the derivative adds a tangent vector and a normal vector. The derivative of the moving projection contributes zero there.

theorem TauCeti.exists_partialDiffeomorph_normalParametrization {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {g : E → V} {s : Set E} {u₀ : E} {n : WithTop ℕ∞} (hg : ContDiffOn ℝ (n + 1) g s) (hs : IsOpen s) (hu₀ : u₀ ∈ s) (hinj : Function.Injective ⇑(fderiv ℝ g u₀)) (hn : 1 ≤ n) : ∃ (Φ : PartialDiffeomorph (modelWithCornersSelf ℝ (E × ↥(↑(fderiv ℝ g u₀)).rangeᗮ)) (modelWithCornersSelf ℝ V) (E × ↥(↑(fderiv ℝ g u₀)).rangeᗮ) V n), ↑Φ.toPartialEquiv = normalParametrization g u₀ ∧ (u₀, 0) ∈ Φ.source ∧ ∀ p ∈ Φ.source, p.1 ∈ s ∧ Function.Injective ⇑(fderiv ℝ g p.1)

A C^(n+1) map on an open set with injective differential at u₀ admits C^n local normal coordinates there. The source lies over the given open set and consists of immersion points. Both the parametrization and its inverse are smooth on their entire domains; n = ∞ and n = ω are allowed.

theorem TauCeti.exists_contDiffOn_normalRetraction {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {g : E → V} {s : Set E} {u₀ : E} {n : WithTop ℕ∞} (hg : ContDiffOn ℝ (n + 1) g s) (hs : IsOpen s) (hu₀ : u₀ ∈ s) (hinj : Function.Injective ⇑(fderiv ℝ g u₀)) (hn : 1 ≤ n) : ∃ (U : Set E), IsOpen U ∧ u₀ ∈ U ∧ U ⊆ s ∧ ∃ (t : Set V), IsOpen t ∧ g u₀ ∈ t ∧ g '' U ⊆ t ∧ ∃ (r : V → E), ContDiffOn ℝ n r t ∧ (∀ u ∈ U, r (g u) = u) ∧ ∀ y ∈ t, r y ∈ U ∧ y - g (r y) ∈ (↑(fderiv ℝ g (r y))).rangeᗮ

The inverse normal coordinates give a smooth local retraction in parameter space. Near g u₀, every point is a normal displacement from g (r y), and r recovers the parameter on a neighbourhood of u₀. This is a local statement about one immersed patch; it does not assert a global retraction for a self-intersecting immersion.