Local trivializations of the Euclidean normal bundle

The normal fibres of a C^(n+1) immersion into a finite-dimensional real inner product space admit local linear trivializations whose coordinate maps are C^n. The model fibre at a chosen point x₀ is its normal space. Orthogonal projection transports that space to nearby normal spaces; the inverse is obtained by inverting the compression of this projection to the original normal space.

normalTrivialization uses the existing subspace topology on the total normal space. The forward fibre coordinates extend smoothly to all ambient vectors, and the inverse fibre coordinates are smooth as ambient-vector-valued maps. These formulas also give smooth changes of normal coordinates without assuming a smooth bundle structure in advance. No compactness, injectivity of the core map, or choice of basis is needed.

The projection and its regularity are supplied by normalSubspace and contMDiff_normalSubspace_starProjection; the fibrewise inverse identity uses Submodule.starProjection_inverse_apply. The algebraic coordinate operators only require orthogonal projections onto the relevant fibres; their recovery identity only requires the moving normal fibre to be finite-dimensional. Regularity holds in a complete ambient space.

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.

noncomputable def TauCeti.normalCompression {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) (f : M → V) (x₀ x : M) [(normalSubspace I f x₀).HasOrthogonalProjection] [(normalSubspace I f x).HasOrthogonalProjection] : ↥(normalSubspace I f x₀) →L[ℝ] ↥(normalSubspace I f x₀)

The normal projection at x, compressed to the normal space at x₀. Its invertibility specifies the domain of the local normal trivialization at x₀.

theorem TauCeti.normalCompression_def {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → V} (x₀ x : M) [(normalSubspace I f x₀).HasOrthogonalProjection] [(normalSubspace I f x).HasOrthogonalProjection] : normalCompression I f x₀ x = (normalSubspace I f x₀).orthogonalProjectionOnto ∘SL (normalSubspace I f x).starProjection ∘SL (normalSubspace I f x₀).subtypeL

The compression is the moving normal projection sandwiched between inclusion and projection for the reference fibre.

@[simp]

theorem TauCeti.normalCompression_self {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → V} (x₀ : M) [(normalSubspace I f x₀).HasOrthogonalProjection] : normalCompression I f x₀ x₀ = 1

At the reference point the compression is the identity.

noncomputable def TauCeti.normalCoordinateMap {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) (f : M → V) (x₀ x : M) [(normalSubspace I f x₀).HasOrthogonalProjection] [(normalSubspace I f x).HasOrthogonalProjection] : V →L[ℝ] ↥(normalSubspace I f x₀)

Ambient-vector coordinates in the reference normal fibre. These recover a reference vector after projection to the moving normal fibre whenever the compression is invertible.

theorem TauCeti.normalCoordinateMap_def {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → V} (x₀ x : M) [(normalSubspace I f x₀).HasOrthogonalProjection] [(normalSubspace I f x).HasOrthogonalProjection] : normalCoordinateMap I f x₀ x = Ring.inverse (normalCompression I f x₀ x) ∘SL (normalSubspace I f x₀).orthogonalProjectionOnto

The ambient coordinate operator is the inverse compression followed by projection onto the reference normal space.

@[simp]

theorem TauCeti.normalCoordinateMap_starProjection {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → V} (x₀ x : M) [(normalSubspace I f x₀).HasOrthogonalProjection] [(normalSubspace I f x).HasOrthogonalProjection] (hx : IsUnit (normalCompression I f x₀ x)) (w : ↥(normalSubspace I f x₀)) : (normalCoordinateMap I f x₀ x) ((normalSubspace I f x).starProjection ↑w) = w

Coordinates of a projected reference vector recover that vector.

noncomputable def TauCeti.normalCoordinateChange {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) (f : M → V) (x₀ x₁ x : M) [(normalSubspace I f x₁).HasOrthogonalProjection] [(normalSubspace I f x).HasOrthogonalProjection] : ↥(normalSubspace I f x₀) →L[ℝ] ↥(normalSubspace I f x₁)

The continuous-linear change from the reference normal fibre at x₀ to that at x₁. On overlaps it transports coordinates between the corresponding normal trivializations.

@[simp]

theorem TauCeti.normalCoordinateChange_apply {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → V} (x₀ x₁ x : M) [(normalSubspace I f x₁).HasOrthogonalProjection] [(normalSubspace I f x).HasOrthogonalProjection] (w : ↥(normalSubspace I f x₀)) : (normalCoordinateChange I f x₀ x₁ x) w = (normalCoordinateMap I f x₁ x) ((normalSubspace I f x).starProjection ↑w)

A change of normal coordinates projects into the moving fibre and takes its target reference coordinates.

theorem TauCeti.starProjection_normalCoordinateMap {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → V} (x₀ x : M) [FiniteDimensional ℝ ↥(normalSubspace I f x)] [(normalSubspace I f x₀).HasOrthogonalProjection] (hrank : Module.finrank ℝ ↥(normalSubspace I f x₀) = Module.finrank ℝ ↥(normalSubspace I f x)) (hx : IsUnit (normalCompression I f x₀ x)) {v : V} (hv : v ∈ normalSubspace I f x) : (normalSubspace I f x).starProjection ↑((normalCoordinateMap I f x₀ x) v) = v

Projecting the coordinates recovers a normal vector, when the two fibres have the same finite dimension and the compression is invertible.

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

The compression of the normal projection varies C^n along a C^(n+1) immersion.

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

The ambient coordinate operator of a C^(n+1) map is C^n at an immersion point where the compression is invertible.

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

Changes between projected normal-fibre coordinates are C^n wherever the target compression is invertible. On the overlap of two trivializations these are their fibrewise transition operators.

noncomputable def TauCeti.normalTrivialization {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → V} [FiniteDimensional ℝ E] [FiniteDimensional ℝ V] [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] (hf : ContMDiff I (modelWithCornersSelf ℝ V) (n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (x₀ : M) : Bundle.Trivialization (↥(normalSubspace I f x₀)) Bundle.TotalSpace.proj

Local linear trivialization of the normal bundle of a C^(n+1) immersion, with model fibre the normal space at x₀. Its base set is the open neighbourhood on which normalCompression I f x₀ is invertible.

@[simp]

theorem TauCeti.mem_normalTrivialization_baseSet {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → V} [FiniteDimensional ℝ E] [FiniteDimensional ℝ V] [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] (hf : ContMDiff I (modelWithCornersSelf ℝ V) (n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (x₀ x : M) : x ∈ (normalTrivialization hf himm x₀).baseSet ↔ IsUnit (normalCompression I f x₀ x)

The base set of the normal trivialization is characterized by invertibility of its compression.

@[simp]

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

The forward normal trivialization uses the ambient coordinate operator.

theorem TauCeti.normalCoordinateChange_normalTrivialization {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → V} [FiniteDimensional ℝ E] [FiniteDimensional ℝ V] [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] (hf : ContMDiff I (modelWithCornersSelf ℝ V) (n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (x₀ x₁ : M) (p : Bundle.TotalSpace ↥(normalSubspace I f x₀) fun (x : M) => ↥(normalSubspace I f x)) (hp : p.proj ∈ (normalTrivialization hf himm x₀).baseSet) : (normalCoordinateChange I f x₀ x₁ p.proj) (↑(normalTrivialization hf himm x₀) p).2 = (↑(normalTrivialization hf himm x₁) ⟨p.proj, p.snd⟩).2

The transition operator takes source trivialization coordinates to target coordinates. Source base-set membership suffices, so the identity applies in particular on overlaps.

@[simp]

theorem TauCeti.normalTrivialization_symm_apply {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → V} [FiniteDimensional ℝ E] [FiniteDimensional ℝ V] [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] (hf : ContMDiff I (modelWithCornersSelf ℝ V) (n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (x₀ : M) (p : M × ↥(normalSubspace I f x₀)) : ↑(normalTrivialization hf himm x₀).symm p = ⟨p.1, ⟨(normalSubspace I f p.1).starProjection ↑p.2, ⋯⟩⟩

The inverse normal trivialization projects the reference vector into the moving normal fibre, retaining its base point.

instance TauCeti.instIsLinearNormalTrivialization {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → V} [FiniteDimensional ℝ E] [FiniteDimensional ℝ V] [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] (hf : ContMDiff I (modelWithCornersSelf ℝ V) (n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (x₀ : M) : Bundle.Trivialization.IsLinear ℝ (normalTrivialization hf himm x₀)

Normal trivializations are linear on each fibre.

theorem TauCeti.contMDiffOn_normalCoordinates {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → V} [FiniteDimensional ℝ E] [FiniteDimensional ℝ V] [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] (hf : ContMDiff I (modelWithCornersSelf ℝ V) (n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (x₀ : M) : ContMDiffOn (I.prod (modelWithCornersSelf ℝ V)) (modelWithCornersSelf ℝ ↥(normalSubspace I f x₀)) n (fun (p : M × V) => (normalCoordinateMap I f x₀ p.1) p.2) ((normalTrivialization hf himm x₀).baseSet ×ˢ Set.univ)

The forward normal coordinates extend to a C^n map on the ambient product, above the base set of the trivialization.

theorem TauCeti.contMDiff_normalTrivialization_symm_snd {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → V} [FiniteDimensional ℝ E] [FiniteDimensional ℝ V] [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] (hf : ContMDiff I (modelWithCornersSelf ℝ V) (n + 1) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (x₀ : M) : ContMDiff (I.prod (modelWithCornersSelf ℝ ↥(normalSubspace I f x₀))) (modelWithCornersSelf ℝ V) n fun (p : M × ↥(normalSubspace I f x₀)) => ↑(↑(normalTrivialization hf himm x₀).symm p).snd

The inverse normal coordinates, viewed in the ambient vector space, are C^n.