Smooth orthogonal representatives in intrinsic normal bundles

Orthogonal representatives of intrinsic normal classes vary smoothly with both the base point and the normal vector. The metric is the ambient Riemannian metric; no normal framing or compactness assumption is needed. This supplies the map from the normal bundle to the ambient tangent bundle used by the normal exponential.

The construction uses the pullback metric on the embedded manifold. Inverting its flat map recovers the tangential component of an ambient vector from its pairings with tangent vectors. Subtracting this component gives the orthogonal representative, which descends through the smooth normal quotient.

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.contMDiff_normalRepresentative_normalClass {E : Type u_1} {V : Type u_2} {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] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ V G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] {m : WithTop ℕ∞} [IsManifold J 1 N] [IsContMDiffRiemannianBundle J m V fun (y : N) => TangentSpace J y] [IsManifold I (m + 1) M] [IsManifold J (m + 1) N] (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hm : m + 1 ≤ n) : ContMDiff (I.prod (modelWithCornersSelf ℝ V)) (J.prod (modelWithCornersSelf ℝ V)) m fun (p : Bundle.TotalSpace V (⇑f *ᵖ (TangentSpace J))) => ⟨f p.proj, (f.normalRepresentative p.proj hn) ((f.normalClass p.proj hn) p.snd)⟩

Orthogonal normal projection is C^m on the pulled-back ambient tangent bundle for a C^n embedding with m + 1 ≤ n and a C^m ambient metric. Both the base point and the ambient tangent vector may vary.

theorem TauCeti.SmoothEmbedding.contMDiff_normalRepresentative {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] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] {m : WithTop ℕ∞} [IsManifold J 1 N] [IsContMDiffRiemannianBundle J m V fun (y : N) => TangentSpace J y] [IsManifold I (m + 1) M] [IsManifold J (m + 1) N] (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hm : m + 1 ≤ n) (hdim : Module.finrank ℝ P = Module.finrank ℝ V - Module.finrank ℝ E) : ContMDiff (I.prod (modelWithCornersSelf ℝ P)) (J.prod (modelWithCornersSelf ℝ V)) m fun (p : Bundle.TotalSpace P fun (x : M) => f.NormalSpace x hn) => ⟨f p.proj, (f.normalRepresentative p.proj hn) p.snd⟩

The map taking an intrinsic normal vector to its orthogonal representative in the ambient tangent bundle is C^m for a C^n embedding with m + 1 ≤ n and a C^m ambient metric.