Local frames of the Euclidean normal bundle

For a C^(n+1) immersion into a finite-dimensional real inner product space, orthogonal projection onto the normal space is C^n. Projecting a basis of one normal fibre onto the nearby normal fibres gives a local frame, with the prescribed value at the original point. These ambient-vector-valued frames provide coordinates for constructing the smooth normal bundle before any vector-bundle structure on that family has been installed.

The normal bundle is the one used in the Euclidean tubular-neighbourhood theorem. As in ContDiffAt.starProjection_orthogonal_range, the pointwise normal-projection result allows a complete, possibly infinite-dimensional ambient space. Neither compactness nor injectivity of the underlying map is required.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer (2013), the normal-bundle construction preceding Theorem 6.24.

theorem TauCeti.contMDiffAt_normalSubspace_starProjection {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] {f : M → V} [CompleteSpace V] {x : M} (hf : ContMDiffAt I (modelWithCornersSelf ℝ V) (n + 1) f x) (himm : Function.Injective ⇑(mfderiv% f x)) : ContMDiffAt I (modelWithCornersSelf ℝ (V →L[ℝ] V)) n (fun (y : M) => (normalSubspace I f y).starProjection) x

Orthogonal projection onto the normal fibre of a C^(n+1) map is C^n at every point where its differential is injective.

theorem TauCeti.contMDiff_normalSubspace_starProjection {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] {f : M → V} [CompleteSpace V] (hf : ContMDiff I (modelWithCornersSelf ℝ V) (n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) : ContMDiff I (modelWithCornersSelf ℝ (V →L[ℝ] V)) n fun (x : M) => (normalSubspace I f x).starProjection

For a C^(n+1) immersion, the family of orthogonal normal projections is C^n.

theorem TauCeti.exists_contMDiffOn_normalFrame {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] {f : M → V} [FiniteDimensional ℝ V] {ι : Type u_5} (hf : ContMDiff I (modelWithCornersSelf ℝ V) (n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (x₀ : M) (b : Module.Basis ι ℝ ↥(normalSubspace I f x₀)) : ∃ (U : Set M), IsOpen U ∧ x₀ ∈ U ∧ (∀ (i : ι), ContMDiffOn I (modelWithCornersSelf ℝ V) n (fun (x : M) => (normalSubspace I f x).starProjection ↑(b i)) U) ∧ ∀ x ∈ U, ∃ (bx : Module.Basis ι ℝ ↥(normalSubspace I f x)), ∀ (i : ι), ↑(bx i) = (normalSubspace I f x).starProjection ↑(b i)

Any basis of one normal fibre of a C^(n+1) immersion extends to a C^n local normal frame. The frame vectors are the orthogonal projections of the prescribed basis; their values at the original point are unchanged. At every point of the open neighbourhood they form a basis of the full normal space, including when the codimension is zero.