Smooth maps in Euclidean normal-bundle coordinates #
The smooth structure on the normal bundle agrees with its ambient coordinates: a map into
the normal bundle is C^n exactly when its base component and its ambient normal vector are
C^n. In particular, the ambient fibre inclusion and the normal addition map are C^n.
This lets tubular maps and their inverses be checked without choosing local normal frames.
Install normalFiberBundle locally as in VectorBundle.lean. The results use the same
projected normal-coordinate atlas, with an arbitrary fixed model fibre of the codimension.
No compactness or injectivity of the core immersion is required.
References #
- J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., the construction of the normal bundle and its addition map preceding Theorem 6.24.
theorem
TauCeti.contMDiff_normalBundle_snd
{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 ℕ∞}
[IsManifold I (n + 1) M]
{f : M → V}
(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)
:
ContMDiff (I.prod (modelWithCornersSelf ℝ F)) (modelWithCornersSelf ℝ V) n
fun (p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) => ↑p.snd
The ambient normal-vector component is C^n on the normal bundle of a C^(n+1)
immersion, with the projected normal-coordinate atlas.
theorem
TauCeti.contMDiffWithinAt_normalBundle_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]
{n : WithTop ℕ∞}
[IsManifold I (n + 1) M]
{f : M → V}
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_7}
[TopologicalSpace H']
{J : ModelWithCorners ℝ E' H'}
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace H' N]
(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)
{g : N → Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)}
{s : Set N}
{x : N}
:
ContMDiffWithinAt J (I.prod (modelWithCornersSelf ℝ F)) n g s x ↔ ContMDiffWithinAt J I n (fun (y : N) => (g y).proj) s x ∧ ContMDiffWithinAt J (modelWithCornersSelf ℝ V) n (fun (y : N) => ↑(g y).snd) s x
Smoothness within a set of a normal-bundle-valued map can be tested on its base component and its ambient normal vector.
theorem
TauCeti.contMDiffAt_normalBundle_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]
{n : WithTop ℕ∞}
[IsManifold I (n + 1) M]
{f : M → V}
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_7}
[TopologicalSpace H']
{J : ModelWithCorners ℝ E' H'}
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace H' N]
(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)
{g : N → Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)}
{x : N}
:
ContMDiffAt J (I.prod (modelWithCornersSelf ℝ F)) n g x ↔ ContMDiffAt J I n (fun (y : N) => (g y).proj) x ∧ ContMDiffAt J (modelWithCornersSelf ℝ V) n (fun (y : N) => ↑(g y).snd) x
Smoothness at a point of a normal-bundle-valued map is equivalent to smoothness of its base component and its ambient normal vector.
theorem
TauCeti.contMDiffOn_normalBundle_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]
{n : WithTop ℕ∞}
[IsManifold I (n + 1) M]
{f : M → V}
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_7}
[TopologicalSpace H']
{J : ModelWithCorners ℝ E' H'}
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace H' N]
(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)
{g : N → Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)}
{s : Set N}
:
ContMDiffOn J (I.prod (modelWithCornersSelf ℝ F)) n g s ↔ ContMDiffOn J I n (fun (y : N) => (g y).proj) s ∧ ContMDiffOn J (modelWithCornersSelf ℝ V) n (fun (y : N) => ↑(g y).snd) s
A map into the normal bundle is C^n on a set exactly when both ambient components
are C^n on that set.
theorem
TauCeti.contMDiff_normalBundle_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]
{n : WithTop ℕ∞}
[IsManifold I (n + 1) M]
{f : M → V}
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_7}
[TopologicalSpace H']
{J : ModelWithCorners ℝ E' H'}
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace H' N]
(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)
{g : N → Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)}
:
A map into the normal bundle is C^n exactly when its base component and its ambient
normal vector are C^n.
theorem
TauCeti.contMDiff_normalBundle_add
{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 ℕ∞}
[IsManifold I (n + 1) M]
{f : M → V}
(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)
:
ContMDiff (I.prod (modelWithCornersSelf ℝ F)) (modelWithCornersSelf ℝ V) n
fun (p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) => f p.proj + ↑p.snd
Normal addition is C^n on the entire normal bundle of a C^(n+1) immersion.
Restricting this map to an injective normal tube gives the forward tubular map.