The differential of the normal exponential at zero

Under the canonical splitting of the tangent space along the zero section of the intrinsic normal bundle, the differential of the normal exponential sends (u, v) to df u + v, where the normal class v is read as its orthogonal representative. The total differential is therefore invertible at every zero normal vector. These statements supply the linear input to the inverse function theorem, without asserting injectivity away from the zero section.

References

• J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24.
• M. W. Hirsch, Differential Topology, Chapter 4, Theorem 6.3.

theorem TauCeti.SmoothEmbedding.mfderiv_normalExp_zeroSection_apply {E : Type u_1} {V : Type u_2} {P : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ V G} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (1 + 1) M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J (↑⊤) N] [J.Boundaryless] [T2Space N] {n : WithTop ℕ∞} [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y] (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (h2 : 1 + 1 ≤ n) (hdim : Module.finrank ℝ P = Module.finrank ℝ V - Module.finrank ℝ E) (x : M) (u : TangentSpace I x) (v : f.NormalSpace x hn) : (mfderiv% (f.normalExp hn) (Bundle.zeroSection P (fun (x : M) => f.NormalSpace x hn) x)) ((Bundle.zeroSectionTangentEquiv x).symm (u, v)) = (mfderiv% ⇑f x) u + (f.normalRepresentative x hn) v

The total differential of the normal exponential at zero is the sum of the embedded tangent vector and the orthogonal representative of the normal class.

theorem TauCeti.SmoothEmbedding.isInvertible_mfderiv_normalExp_zeroSection {E : Type u_1} {V : Type u_2} {P : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ V G} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (1 + 1) M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J (↑⊤) N] [J.Boundaryless] [T2Space N] {n : WithTop ℕ∞} [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y] (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (h2 : 1 + 1 ≤ n) (hdim : Module.finrank ℝ P = Module.finrank ℝ V - Module.finrank ℝ E) (x : M) : (mfderiv% (f.normalExp hn) (Bundle.zeroSection P (fun (x : M) => f.NormalSpace x hn) x)).IsInvertible

The total differential of the normal exponential at every zero normal vector is invertible. This does not require compactness or a global normal framing.