Radial compression of Riemannian vector bundles #
A real vector bundle with a smoothly varying fibre inner product admits a smooth radial identification of its entire total space with its open unit ball bundle. The identification preserves the base point and fixes the zero section. Composing with positive smooth scalar rescaling gives variable-radius coordinates, as used in whole-normal-bundle parametrizations of tubular neighbourhoods.
The fibre maps are Mathlib's OpenPartialHomeomorph.univUnitBall, by Yury Kudryashov and
Oliver Nash. Smoothness on the total space uses the smooth fibre inner product; no
orthonormal trivialization or global frame is needed. The rescaling assembly follows
normalBundleRadialPartialDiffeomorphOfRadius, now for arbitrary Riemannian vector bundles.
References #
- M. W. Hirsch, Differential Topology, Chapter 4, Theorem 6.3 (tubular neighbourhoods).
noncomputable def
TauCeti.vectorBundleRadialPartialDiffeomorph
{B : Type u_1}
{V : B → Type u_2}
{F : Type u_3}
[(b : B) → NormedAddCommGroup (V b)]
[(b : B) → InnerProductSpace ℝ (V b)]
[TopologicalSpace B]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[ChartedSpace H B]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle ℝ F V]
{n : WithTop ℕ∞}
[IsContMDiffRiemannianBundle I n F V]
:
PartialDiffeomorph (I.prod (modelWithCornersSelf ℝ F)) (I.prod (modelWithCornersSelf ℝ F)) (Bundle.TotalSpace F V)
(Bundle.TotalSpace F V) n
A smooth fibre metric makes radial compression a partial diffeomorphism from the whole total space onto the open unit ball bundle. The smooth structure is the original bundle structure in both directions.
Instances For
@[simp]
theorem
TauCeti.vectorBundleRadialPartialDiffeomorph_source
{B : Type u_1}
{V : B → Type u_2}
{F : Type u_3}
[(b : B) → NormedAddCommGroup (V b)]
[(b : B) → InnerProductSpace ℝ (V b)]
[TopologicalSpace B]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[ChartedSpace H B]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle ℝ F V]
{n : WithTop ℕ∞}
[IsContMDiffRiemannianBundle I n F V]
:
The source of radial compression is the entire total space.
@[simp]
theorem
TauCeti.vectorBundleRadialPartialDiffeomorph_target
{B : Type u_1}
{V : B → Type u_2}
{F : Type u_3}
[(b : B) → NormedAddCommGroup (V b)]
[(b : B) → InnerProductSpace ℝ (V b)]
[TopologicalSpace B]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[ChartedSpace H B]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle ℝ F V]
{n : WithTop ℕ∞}
[IsContMDiffRiemannianBundle I n F V]
:
The target of radial compression is exactly the open unit ball bundle.
@[simp]
theorem
TauCeti.vectorBundleRadialPartialDiffeomorph_apply
{B : Type u_1}
{V : B → Type u_2}
{F : Type u_3}
[(b : B) → NormedAddCommGroup (V b)]
[(b : B) → InnerProductSpace ℝ (V b)]
[TopologicalSpace B]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[ChartedSpace H B]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle ℝ F V]
{n : WithTop ℕ∞}
[IsContMDiffRiemannianBundle I n F V]
(p : Bundle.TotalSpace F V)
:
The partial diffeomorphism acts by fibrewise radial compression.
@[simp]
theorem
TauCeti.vectorBundleRadialPartialDiffeomorph_symm_apply
{B : Type u_1}
{V : B → Type u_2}
{F : Type u_3}
[(b : B) → NormedAddCommGroup (V b)]
[(b : B) → InnerProductSpace ℝ (V b)]
[TopologicalSpace B]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[ChartedSpace H B]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle ℝ F V]
{n : WithTop ℕ∞}
[IsContMDiffRiemannianBundle I n F V]
(p : Bundle.TotalSpace F V)
:
The inverse partial diffeomorphism acts by fibrewise radial expansion.
noncomputable def
TauCeti.vectorBundleRadialPartialDiffeomorphOfRadius
{B : Type u_1}
{V : B → Type u_2}
{F : Type u_3}
[(b : B) → NormedAddCommGroup (V b)]
[(b : B) → InnerProductSpace ℝ (V b)]
[TopologicalSpace B]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[ChartedSpace H B]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle ℝ F V]
{n : WithTop ℕ∞}
[IsContMDiffRiemannianBundle I n F V]
{r : B → ℝ}
(hr : ContMDiff I (modelWithCornersSelf ℝ ℝ) n r)
(hrpos : ∀ (b : B), 0 < r b)
:
PartialDiffeomorph (I.prod (modelWithCornersSelf ℝ F)) (I.prod (modelWithCornersSelf ℝ F)) (Bundle.TotalSpace F V)
(Bundle.TotalSpace F V) n
Radial compression followed by positive smooth rescaling identifies the entire total space with its variable-radius open ball bundle.
Instances For
@[simp]
theorem
TauCeti.vectorBundleRadialPartialDiffeomorphOfRadius_source
{B : Type u_1}
{V : B → Type u_2}
{F : Type u_3}
[(b : B) → NormedAddCommGroup (V b)]
[(b : B) → InnerProductSpace ℝ (V b)]
[TopologicalSpace B]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[ChartedSpace H B]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle ℝ F V]
{n : WithTop ℕ∞}
[IsContMDiffRiemannianBundle I n F V]
{r : B → ℝ}
(hr : ContMDiff I (modelWithCornersSelf ℝ ℝ) n r)
(hrpos : ∀ (b : B), 0 < r b)
:
Variable-radius compression is defined on the entire total space.
@[simp]
theorem
TauCeti.vectorBundleRadialPartialDiffeomorphOfRadius_target
{B : Type u_1}
{V : B → Type u_2}
{F : Type u_3}
[(b : B) → NormedAddCommGroup (V b)]
[(b : B) → InnerProductSpace ℝ (V b)]
[TopologicalSpace B]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[ChartedSpace H B]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle ℝ F V]
{n : WithTop ℕ∞}
[IsContMDiffRiemannianBundle I n F V]
{r : B → ℝ}
(hr : ContMDiff I (modelWithCornersSelf ℝ ℝ) n r)
(hrpos : ∀ (b : B), 0 < r b)
:
The target consists exactly of vectors shorter than the prescribed positive radius.
@[simp]
theorem
TauCeti.vectorBundleRadialPartialDiffeomorphOfRadius_apply
{B : Type u_1}
{V : B → Type u_2}
{F : Type u_3}
[(b : B) → NormedAddCommGroup (V b)]
[(b : B) → InnerProductSpace ℝ (V b)]
[TopologicalSpace B]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[ChartedSpace H B]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle ℝ F V]
{n : WithTop ℕ∞}
[IsContMDiffRiemannianBundle I n F V]
{r : B → ℝ}
(hr : ContMDiff I (modelWithCornersSelf ℝ ℝ) n r)
(hrpos : ∀ (b : B), 0 < r b)
(p : Bundle.TotalSpace F V)
:
↑(vectorBundleRadialPartialDiffeomorphOfRadius hr hrpos).toPartialEquiv p = (vectorBundleScalarDiffeomorph r hr ⋯) p.radialMap
Variable-radius compression first compresses into the unit ball, then rescales.
@[simp]
theorem
TauCeti.vectorBundleRadialPartialDiffeomorphOfRadius_symm_apply
{B : Type u_1}
{V : B → Type u_2}
{F : Type u_3}
[(b : B) → NormedAddCommGroup (V b)]
[(b : B) → InnerProductSpace ℝ (V b)]
[TopologicalSpace B]
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[ChartedSpace H B]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace (Bundle.TotalSpace F V)]
[FiberBundle F V]
[VectorBundle ℝ F V]
{n : WithTop ℕ∞}
[IsContMDiffRiemannianBundle I n F V]
{r : B → ℝ}
(hr : ContMDiff I (modelWithCornersSelf ℝ ℝ) n r)
(hrpos : ∀ (b : B), 0 < r b)
(p : Bundle.TotalSpace F V)
:
↑(vectorBundleRadialPartialDiffeomorphOfRadius hr hrpos).symm p = ((vectorBundleScalarDiffeomorph r hr ⋯).symm p).radialInverse
The inverse first divides by the radius, then expands the unit ball.