Smooth radial coordinates on the normal bundle #
Radial compression identifies the entire normal bundle of a Euclidean immersion with the open bundle of normal balls of any positive fixed radius. This identification is a partial diffeomorphism on the total space, with source the whole bundle. It fixes the zero section and preserves base points. Composing it with smooth tubular coordinates therefore gives tubular coordinates parametrized by the whole normal bundle.
Install normalFiberBundle locally as in SmoothMap.lean; its projected normal-coordinate
atlas is used in both directions. No compactness,
injectivity of the core map, or normal framing is required. A C^(n+1) immersion gives
C^n radial coordinates, including n = ∞.
The fibre maps reuse Mathlib's OpenPartialHomeomorph.univUnitBall and its smoothness
theorems, by Yury Kudryashov and Oliver Nash.
This construction adapts the radial fibre formula of Tau Ceti's prior topological
formalization TauCeti.normalBundleHomeomorphTube in
TauCeti/Geometry/Manifold/TubularNeighborhood/WholeBundle.lean to the smooth normal bundle.
Reference: J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Theorem 6.24 (tubular neighbourhoods).
noncomputable def
TauCeti.normalBundleRadialMap
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
(f : M → V)
(ε : ℝ)
(p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))
:
Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)
Scale the unit-ball radial compression in each normal fibre by ε, keeping its base point.
When 0 < ε, its image in each fibre is the open ball of radius ε, and the inverse on
that ball is normalBundleRadialInverse.
Instances For
noncomputable def
TauCeti.normalBundleRadialInverse
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
(f : M → V)
(ε : ℝ)
(p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))
:
Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)
Radial expansion in each normal fibre. Compression undoes this expansion on the
open normal ball of positive radius ε.
Instances For
@[simp]
theorem
TauCeti.normalBundleRadialMap_proj
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
(f : M → V)
(ε : ℝ)
(p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))
:
Radial compression preserves the base point.
@[simp]
theorem
TauCeti.normalBundleRadialInverse_proj
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
(f : M → V)
(ε : ℝ)
(p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))
:
Radial expansion preserves the base point.
@[simp]
theorem
TauCeti.normalBundleRadialMap_snd
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
(f : M → V)
(ε : ℝ)
(p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))
:
Compression in ambient normal-vector coordinates.
@[simp]
theorem
TauCeti.normalBundleRadialInverse_snd
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
(f : M → V)
(ε : ℝ)
(p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))
:
Expansion in ambient normal-vector coordinates.
@[simp]
theorem
TauCeti.normalBundleRadialMap_zeroSection
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
(f : M → V)
(ε : ℝ)
(x : M)
:
normalBundleRadialMap f ε (Bundle.zeroSection F (fun (x : M) => ↥(normalSubspace I f x)) x) = Bundle.zeroSection F (fun (x : M) => ↥(normalSubspace I f x)) x
Compression fixes the zero section.
@[simp]
theorem
TauCeti.normalBundleRadialInverse_zeroSection
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
(f : M → V)
(ε : ℝ)
(x : M)
:
normalBundleRadialInverse f ε (Bundle.zeroSection F (fun (x : M) => ↥(normalSubspace I f x)) x) = Bundle.zeroSection F (fun (x : M) => ↥(normalSubspace I f x)) x
Expansion fixes the zero section.
@[simp]
theorem
TauCeti.normalBundleRadialInverse_map
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
(f : M → V)
{ε : ℝ}
(hε : ε ≠ 0)
(p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))
:
Expansion undoes compression everywhere for a nonzero radius.
@[simp]
theorem
TauCeti.normalBundleRadialMap_inverse
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
(f : M → V)
{ε : ℝ}
(hε : 0 < ε)
(p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))
(hp : ‖↑p.snd‖ < ε)
:
Compression undoes expansion on the open normal ball of positive radius.
theorem
TauCeti.contMDiff_normalBundleRadialMap
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
[I.Boundaryless]
{n : ℕ∞}
[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)) (I.prod (modelWithCornersSelf ℝ F)) (↑n) (normalBundleRadialMap f ε)
Radial compression is C^n on the entire smooth normal bundle.
theorem
TauCeti.contMDiffOn_normalBundleRadialInverse
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
[I.Boundaryless]
{n : ℕ∞}
[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)
{ε : ℝ}
(hε : 0 < ε)
:
ContMDiffOn (I.prod (modelWithCornersSelf ℝ F)) (I.prod (modelWithCornersSelf ℝ F)) (↑n) (normalBundleRadialInverse f ε)
{p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x) | ‖↑p.snd‖ < ε}
Radial expansion is C^n on the open normal ball bundle of positive radius.
noncomputable def
TauCeti.normalBundleRadialPartialDiffeomorph
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
[I.Boundaryless]
{n : ℕ∞}
[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)
{ε : ℝ}
(hε : 0 < ε)
:
PartialDiffeomorph (I.prod (modelWithCornersSelf ℝ F)) (I.prod (modelWithCornersSelf ℝ F))
(Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))
(Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) ↑n
The whole smooth normal bundle is diffeomorphic, by radial compression, to its open ball bundle of any positive fixed radius. The source is the entire total space.
Instances For
@[simp]
theorem
TauCeti.normalBundleRadialPartialDiffeomorph_source
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
[I.Boundaryless]
{n : ℕ∞}
[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)
{ε : ℝ}
(hε : 0 < ε)
:
The radial diffeomorphism is defined on the entire normal bundle.
@[simp]
theorem
TauCeti.normalBundleRadialPartialDiffeomorph_target
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
[I.Boundaryless]
{n : ℕ∞}
[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)
{ε : ℝ}
(hε : 0 < ε)
:
(normalBundleRadialPartialDiffeomorph hf himm hdim hε).target = {p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x) | ‖↑p.snd‖ < ε}
The target consists exactly of normal vectors of norm less than the radius.
@[simp]
theorem
TauCeti.normalBundleRadialPartialDiffeomorph_apply
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
[I.Boundaryless]
{n : ℕ∞}
[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)
{ε : ℝ}
(hε : 0 < ε)
(p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))
:
↑(normalBundleRadialPartialDiffeomorph hf himm hdim hε).toPartialEquiv p = normalBundleRadialMap f ε p
The radial diffeomorphism acts by fibrewise compression.
@[simp]
theorem
TauCeti.normalBundleRadialPartialDiffeomorph_symm_apply
{V : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
{F : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ V]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
[I.Boundaryless]
{n : ℕ∞}
[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)
{ε : ℝ}
(hε : 0 < ε)
(p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))
:
The inverse radial diffeomorphism acts by fibrewise expansion.