Shrinking smooth embeddings near their centre

Positive dilations of the source give a smooth isotopy of an embedding of a real normed space, fixing the image of the origin. A bounded part of the source can consequently be moved inside any neighbourhood of that image. For a star-convex source subset, the motion stays inside its original image throughout the isotopy.

This is the shrinking step used to compare ball embeddings in a common ambient chart. It gives an isotopy through embeddings; extending it to an ambient isotopy is a separate assertion. Neither finite dimensionality nor compactness of the source is required.

A dilation moves only bounded parts of the source into a neighbourhood of the centre. When the source is finite-dimensional, the radial contractions TauCeti.radialContraction move all of it: precomposing with them gives a smooth isotopy from an embedding of E to one whose image lies in any prescribed neighbourhood of the centre (compRadialContractionIsotopy). Postcomposing an embedding into E with them gives a smooth isotopy into a Euclidean ball which never leaves a Euclidean ball about the centre containing the original image (transRadialContractionIsotopy).

Main definitions

• TauCeti.SmoothEmbedding.shrinkingIsotopy: shrinking by positive dilations of the source.
• TauCeti.SmoothEmbedding.compRadialContractionIsotopy: shrinking by radial contractions of a finite-dimensional source.
• TauCeti.SmoothEmbedding.transRadialContractionIsotopy: radial contraction of the target of an embedding into a finite-dimensional space.

Reference: M. Hirsch, Differential Topology, GTM 33, Chapter 4, §6, Theorem 6.6. The bounded-set shrinking argument uses Mathlib's von Neumann boundedness and small-sets API.

noncomputable def TauCeti.SmoothEmbedding.shrinkingIsotopy {E : Type u_1} {F : Type u_2} {H : Type u_3} {N : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] {J : ModelWithCorners ℝ F H} [TopologicalSpace N] [ChartedSpace H N] {n : WithTop ℕ∞} (f : SmoothEmbedding (modelWithCornersSelf ℝ E) J n E N) {c : ℝ} (hc : 0 < c) : SmoothIsotopy f.toContMDiffMap (f.toContMDiffMap.comp (c • ContMDiffMap.id))

Reparametrize an embedding by positive source dilations, from scale one to scale c. The image of the origin remains fixed, and every time slice is an embedding.

@[simp]

theorem TauCeti.SmoothEmbedding.shrinkingIsotopy_apply {E : Type u_1} {F : Type u_2} {H : Type u_3} {N : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] {J : ModelWithCorners ℝ F H} [TopologicalSpace N] [ChartedSpace H N] {n : WithTop ℕ∞} (f : SmoothEmbedding (modelWithCornersSelf ℝ E) J n E N) {c : ℝ} (hc : 0 < c) (p : ↑unitInterval × E) : (f.shrinkingIsotopy hc) p = f ((1 - ↑p.1 + ↑p.1 * c) • p.2)

The shrinking motion interpolates linearly between its positive dilation factors.

theorem TauCeti.SmoothEmbedding.shrinkingIsotopy_mapsTo_image {E : Type u_1} {F : Type u_2} {H : Type u_3} {N : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] {J : ModelWithCorners ℝ F H} [TopologicalSpace N] [ChartedSpace H N] {n : WithTop ℕ∞} (f : SmoothEmbedding (modelWithCornersSelf ℝ E) J n E N) {c : ℝ} (hc : 0 < c) (hc₁ : c ≤ 1) {s : Set E} (hs : StarConvex ℝ 0 s) (t : ↑unitInterval) : Set.MapsTo (fun (x : E) => (f.shrinkingIsotopy hc) (t, x)) s (⇑f '' s)

Shrinking a star-convex subset never leaves its original embedded image.

theorem TauCeti.SmoothEmbedding.exists_shrinkingIsotopy_mapsTo {E : Type u_1} {F : Type u_2} {H : Type u_3} {N : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] {J : ModelWithCorners ℝ F H} [TopologicalSpace N] [ChartedSpace H N] {n : WithTop ℕ∞} (f : SmoothEmbedding (modelWithCornersSelf ℝ E) J n E N) {s : Set E} (hs : Bornology.IsBounded s) {U : Set N} (hU : U ∈ nhds (f 0)) : ∃ (c : ℝ) (hc : 0 < c), c ≤ 1 ∧ Set.MapsTo (fun (x : E) => (f.shrinkingIsotopy hc) (1, x)) s U

A bounded part of a smooth embedding can be mapped into any neighbourhood of its centre at the endpoint of a shrinking isotopy. For a star-convex source subset, shrinkingIsotopy_mapsTo_image gives containment in its original image throughout the motion.

Radial contractions

noncomputable def TauCeti.SmoothEmbedding.compRadialContractionIsotopy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {F : Type u_2} {H : Type u_3} {N : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] {J : ModelWithCorners ℝ F H} [TopologicalSpace N] [ChartedSpace H N] (f : SmoothEmbedding (modelWithCornersSelf ℝ E) J n E N) (hn : n ≤ ↑⊤) {κ : ℝ} (hκ : 0 ≤ κ) : SmoothIsotopy f.toContMDiffMap (f.compRadialContraction hn hκ).toContMDiffMap

The source contraction t ↦ f ∘ radialContraction 0 (t κ), a smooth isotopy from f to f.compRadialContraction hn hκ fixing the image of 0, preserving regularity n ≤ ∞.

@[simp]

theorem TauCeti.SmoothEmbedding.compRadialContractionIsotopy_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {F : Type u_2} {H : Type u_3} {N : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] {J : ModelWithCorners ℝ F H} [TopologicalSpace N] [ChartedSpace H N] (f : SmoothEmbedding (modelWithCornersSelf ℝ E) J n E N) (hn : n ≤ ↑⊤) {κ : ℝ} (hκ : 0 ≤ κ) (p : ↑unitInterval × E) : (f.compRadialContractionIsotopy hn hκ) p = f (radialContraction 0 (↑p.1 * κ) p.2)

noncomputable def TauCeti.SmoothEmbedding.transRadialContractionIsotopy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {E₀ : Type u_5} {H₀ : Type u_6} {M : Type u_7} [NormedAddCommGroup E₀] [NormedSpace ℝ E₀] [TopologicalSpace H₀] {I : ModelWithCorners ℝ E₀ H₀} [TopologicalSpace M] [ChartedSpace H₀ M] (f : SmoothEmbedding I (modelWithCornersSelf ℝ E) n M E) (c : E) (hn : n ≤ ↑⊤) {κ : ℝ} (hκ : 0 ≤ κ) : SmoothIsotopy f.toContMDiffMap (f.transRadialContraction c hn hκ).toContMDiffMap

The target contraction t ↦ radialContraction c (t κ) ∘ f, a smooth isotopy from f to f.transRadialContraction c hn hκ, preserving regularity n ≤ ∞.

@[simp]

theorem TauCeti.SmoothEmbedding.transRadialContractionIsotopy_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {E₀ : Type u_5} {H₀ : Type u_6} {M : Type u_7} [NormedAddCommGroup E₀] [NormedSpace ℝ E₀] [TopologicalSpace H₀] {I : ModelWithCorners ℝ E₀ H₀} [TopologicalSpace M] [ChartedSpace H₀ M] (f : SmoothEmbedding I (modelWithCornersSelf ℝ E) n M E) (c : E) (hn : n ≤ ↑⊤) {κ : ℝ} (hκ : 0 ≤ κ) (p : ↑unitInterval × M) : (f.transRadialContractionIsotopy c hn hκ) p = radialContraction c (↑p.1 * κ) (f p.2)

theorem TauCeti.SmoothEmbedding.transRadialContractionIsotopy_mem_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {E₀ : Type u_5} {H₀ : Type u_6} {M : Type u_7} [NormedAddCommGroup E₀] [NormedSpace ℝ E₀] [TopologicalSpace H₀] {I : ModelWithCorners ℝ E₀ H₀} [TopologicalSpace M] [ChartedSpace H₀ M] (f : SmoothEmbedding I (modelWithCornersSelf ℝ E) n M E) (hn : n ≤ ↑⊤) {c : E} {r κ : ℝ} (hκ : 0 ≤ κ) (hf : ∀ (x : M), f x ∈ Euclidean.ball c r) (p : ↑unitInterval × M) : (f.transRadialContractionIsotopy c hn hκ) p ∈ Euclidean.ball c r

The target contraction never leaves a Euclidean ball about its centre containing the original image.