The smooth Euclidean normal bundle #
The normal spaces of a C^(n+1) immersion into a finite-dimensional real inner product space
form a C^n vector bundle. Its total space keeps the subspace topology inherited from M × V.
A C¹ immersion already gives a continuous vector bundle.
In particular, bundle constructions and the Euclidean tubular map use the same topology.
The local normal trivializations use different reference fibres. Here each reference fibre is
identified with one fixed normed space F of the codimension. These identifications are constant
within each trivialization; no regularity of their dependence on the reference point is needed.
The resulting transition operators are the already established normal-coordinate changes,
conjugated by those fixed identifications.
For a C¹ immersion, install normalFiberBundle hf himm hdim and
normalVectorBundle hf himm hdim with letI. A C^(n+1) immersion supplies the C¹
hypotheses via IsManifold.of_le and hf.of_le le_add_self; its smooth structure is
normalContMDiffVectorBundle hf himm hdim. The model fibre can, for example, be
EuclideanSpace ℝ (Fin (Module.finrank ℝ V - Module.finrank ℝ E)).
Neither compactness nor injectivity of the immersion 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.
noncomputable def
TauCeti.normalFiberEquiv
{E : Type u_1}
{V : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{f : M → V}
(hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E)
(x : M)
(himm : Function.Injective ⇑(mfderiv% f x))
:
A fixed linear identification of a normal fibre with a model of the codimension.
Instances For
noncomputable def
TauCeti.normalBundleTrivialization
{E : Type u_1}
{V : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[I.Boundaryless]
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
{f : M → V}
(hf : ContMDiff I (modelWithCornersSelf ℝ V) 1 f)
(himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x))
(hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E)
(x₀ : M)
:
A local normal trivialization with a single fixed model fibre. Its base set is the invertibility locus of the normal compression at the reference point.
Instances For
@[simp]
theorem
TauCeti.mem_normalBundleTrivialization_baseSet
{E : Type u_1}
{V : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[I.Boundaryless]
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
{f : M → V}
(hf : ContMDiff I (modelWithCornersSelf ℝ V) 1 f)
(himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x))
(hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E)
(x₀ x : M)
:
The base set is unchanged by choosing a fixed model fibre.
@[simp]
theorem
TauCeti.normalBundleTrivialization_apply
{E : Type u_1}
{V : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[I.Boundaryless]
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
{f : M → V}
(hf : ContMDiff I (modelWithCornersSelf ℝ V) 1 f)
(himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x))
(hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E)
(x₀ : M)
(p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))
:
↑(normalBundleTrivialization hf himm hdim x₀) p = (p.proj, (normalFiberEquiv hdim x₀ ⋯) ((normalCoordinateMap I f x₀ p.proj) ↑p.snd))
Fixed-model normal coordinates are the original coordinates followed by the reference fibre identification.
@[simp]
theorem
TauCeti.normalBundleTrivialization_symm_apply
{E : Type u_1}
{V : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[I.Boundaryless]
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
{f : M → V}
(hf : ContMDiff I (modelWithCornersSelf ℝ V) 1 f)
(himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x))
(hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E)
(x₀ : M)
(p : M × F)
:
↑(normalBundleTrivialization hf himm hdim x₀).symm p = ⟨p.1, ⟨(normalSubspace I f p.1).starProjection ↑((normalFiberEquiv hdim x₀ ⋯).symm p.2), ⋯⟩⟩
Inverse fixed-model coordinates project the reference normal vector to the moving fibre.
instance
TauCeti.instIsLinearNormalBundleTrivialization
{E : Type u_1}
{V : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[I.Boundaryless]
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
{f : M → V}
(hf : ContMDiff I (modelWithCornersSelf ℝ V) 1 f)
(himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x))
(hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E)
(x₀ : M)
:
Bundle.Trivialization.IsLinear ℝ (normalBundleTrivialization hf himm hdim x₀)
Fixed-model normal trivializations are fibrewise linear.
theorem
TauCeti.normalBundleTrivialization_coordChangeL
{E : Type u_1}
{V : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[I.Boundaryless]
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
{f : M → V}
(hf : ContMDiff I (modelWithCornersSelf ℝ V) 1 f)
(himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x))
(hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E)
(x₀ x₁ : M)
{x : M}
(hx : x ∈ (normalBundleTrivialization hf himm hdim x₀).baseSet ∩ (normalBundleTrivialization hf himm hdim x₁).baseSet)
:
↑(Bundle.Trivialization.coordChangeL ℝ (normalBundleTrivialization hf himm hdim x₀)
(normalBundleTrivialization hf himm hdim x₁) x) = ↑(normalFiberEquiv hdim x₁ ⋯) ∘SL normalCoordinateChange I f x₀ x₁ x ∘SL ↑(normalFiberEquiv hdim x₀ ⋯).symm
On overlaps, transition operators are the normal-coordinate changes conjugated by the two fixed reference-fibre identifications.
theorem
TauCeti.contMDiffOn_normalBundleTrivialization_coordChangeL
{E : Type u_1}
{V : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[I.Boundaryless]
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{f : M → V}
[IsManifold I (n + 1) M]
(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₀ x₁ : M)
:
ContMDiffOn I (modelWithCornersSelf ℝ (F →L[ℝ] F)) n
(fun (x : M) =>
↑(Bundle.Trivialization.coordChangeL ℝ (normalBundleTrivialization ⋯ himm hdim x₀)
(normalBundleTrivialization ⋯ himm hdim x₁) x))
((normalBundleTrivialization ⋯ himm hdim x₀).baseSet ∩ (normalBundleTrivialization ⋯ himm hdim x₁).baseSet)
The fixed-model normal transition operators vary C^n on overlaps.
@[instance_reducible]
noncomputable def
TauCeti.normalFiberBundle
{E : Type u_1}
{V : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[I.Boundaryless]
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
{f : M → V}
(hf : ContMDiff I (modelWithCornersSelf ℝ V) 1 f)
(himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x))
(hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E)
:
FiberBundle F fun (x : M) => ↥(normalSubspace I f x)
The normal fibres form a fibre bundle with the topology inherited from M × V.
Use this definition as a local instance to choose its projected normal-coordinate atlas.
Instances For
@[simp]
theorem
TauCeti.normalFiberBundle_trivializationAt
{E : Type u_1}
{V : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[I.Boundaryless]
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
{f : M → V}
(hf : ContMDiff I (modelWithCornersSelf ℝ V) 1 f)
(himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x))
(hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E)
(x : M)
:
have this := normalFiberBundle hf himm hdim;
trivializationAt F (fun (x : M) => ↥(normalSubspace I f x)) x = normalBundleTrivialization hf himm hdim x
The preferred normal-bundle trivialization is the fixed-model projected trivialization at the same point.
@[simp]
theorem
TauCeti.mem_normalFiberBundle_trivializationAtlas_iff
{E : Type u_1}
{V : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[I.Boundaryless]
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
{f : M → V}
(hf : ContMDiff I (modelWithCornersSelf ℝ V) 1 f)
(himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x))
(hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E)
(e : Bundle.Trivialization F Bundle.TotalSpace.proj)
:
have this := normalFiberBundle hf himm hdim;
(e ∈ trivializationAtlas F fun (x : M) => ↥(normalSubspace I f x)) ↔ ∃ (x : M), normalBundleTrivialization hf himm hdim x = e
The normal-bundle atlas consists exactly of the projected normal trivializations.
theorem
TauCeti.normalVectorBundle
{E : Type u_1}
{V : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[I.Boundaryless]
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
{f : M → V}
(hf : ContMDiff I (modelWithCornersSelf ℝ V) 1 f)
(himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x))
(hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E)
:
have this := normalFiberBundle hf himm hdim;
VectorBundle ℝ F fun (x : M) => ↥(normalSubspace I f x)
The normal fibre bundle is a real vector bundle: its atlas is linear and its transition operators are continuous in operator norm.
theorem
TauCeti.normalContMDiffVectorBundle
{E : Type u_1}
{V : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H : Type u_4}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[I.Boundaryless]
{M : Type u_5}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{f : M → V}
[IsManifold I (n + 1) M]
(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)
:
let this := normalFiberBundle ⋯ himm hdim;
have this_1 := ⋯;
ContMDiffVectorBundle n F (fun (x : M) => ↥(normalSubspace I f x)) I
The normal bundle of a C^(n+1) immersion is a C^n vector bundle, with the existing
subspace topology on its total space.