Local inverses to normal addition

A Euclidean immersion admits a smooth local retraction to its source manifold near every image point. The displacement from the retracted point is normal to the immersion. With the projected normal-bundle atlas, the retraction and displacement together give a smooth local right inverse to normal addition, recovering the zero section on the immersed patch. Normal addition is consequently a local diffeomorphism at every zero-section point.

These results transport exists_contDiffOn_normalRetraction through a manifold chart. They apply to individual immersed patches, including self-intersecting immersions; they do not assert a globally defined retraction or nearest-point uniqueness.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24.

theorem TauCeti.exists_contMDiffOn_normalRetraction {E : Type u_1} {V : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) (n + 1) f) (x₀ : M) (himm : Function.Injective ⇑(mfderiv% f x₀)) (hn : 1 ≤ n) : ∃ (U : Set M), IsOpen U ∧ x₀ ∈ U ∧ ∃ (t : Set V), IsOpen t ∧ f x₀ ∈ t ∧ f '' U ⊆ t ∧ ∃ (r : V → M), ContMDiffOn (modelWithCornersSelf ℝ V) I n r t ∧ (∀ x ∈ U, r (f x) = x) ∧ ∀ y ∈ t, r y ∈ U ∧ y - f (r y) ∈ normalSubspace I f (r y)

Near any point of a C^(n+1) Euclidean immersion there is a C^n local retraction to its source, with normal displacement. Its domain contains the image of an open source patch, and the retraction recovers every point of that patch.

theorem TauCeti.exists_contMDiff_normalBundle_add_rightInverse {E : Type u_1} {V : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] {f : M → V} {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (hf : ContMDiff I (modelWithCornersSelf ℝ V) (n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E) (x₀ : M) (hn : 1 ≤ n) : ∃ (U : Set M), IsOpen U ∧ x₀ ∈ U ∧ ∃ (t : TopologicalSpace.Opens V), f '' U ⊆ ↑t ∧ ∃ (R : ↥t → Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)), ContMDiff (modelWithCornersSelf ℝ V) (I.prod (modelWithCornersSelf ℝ F)) n R ∧ (∀ (y : ↥t), (R y).proj ∈ U) ∧ (∀ (y : ↥t), f (R y).proj + ↑(R y).snd = ↑y) ∧ ∀ x ∈ U, ∀ (y : ↥t), ↑y = f x → R y = Bundle.zeroSection F (fun (x : M) => ↥(normalSubspace I f x)) x

Normal addition has a C^n local right inverse near every image point of a C^(n+1) immersion. On a source patch this inverse recovers the zero section. The normal bundle carries its projected atlas, with model fibre F of the codimension.

theorem TauCeti.isLocalDiffeomorphAt_normalBundle_add_zeroSection {E : Type u_1} {V : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] {f : M → V} {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (hf : ContMDiff I (modelWithCornersSelf ℝ V) (n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E) (x₀ : M) (hn : 1 ≤ n) : IsLocalDiffeomorphAt (I.prod (modelWithCornersSelf ℝ F)) (modelWithCornersSelf ℝ V) n (fun (p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) => f p.proj + ↑p.snd) (Bundle.zeroSection F (fun (x : M) => ↥(normalSubspace I f x)) x₀)

Normal addition is a C^n local diffeomorphism at every zero-section point of the normal bundle of a C^(n+1) Euclidean immersion. No global embedding or compactness assumption is needed.