The disc theorem for oriented embeddings

Two orientation-preserving smooth embeddings of a real normed space into an oriented manifold of the same dimension, with the same centre, are smoothly isotopic relative to that centre. Only orientation preservation at the centre is needed. Giving the target the opposite orientation also covers two orientation-reversing embeddings.

This connects the intrinsic tangent-orientation condition to the chart determinant condition in SmoothEmbedding.exists_smoothIsotopy_of_det_chartAt_mul_pos.

On a connected manifold the centres need not agree: this is the ambient disc theorem of Palais (TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_isOrientationPreservingAt). On every compact subset of E, one orientation-preserving embedding is the other followed by the final diffeomorphism of a compactly supported diffeotopy. The homogeneity lemma (TauCeti.exists_diffeotopy_final_apply_eq) first moves the centre of the first embedding to the centre of the second by a compactly supported diffeotopy, whose final diffeomorphism preserves the orientation (TauCeti.Diffeotopy.isOrientationPreservingAt_final); the ambient disc theorem at a common centre (TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_det_chartAt_mul_pos) then finishes. That argument needs a σ-compact manifold. The relative form runs it in the open submanifold covered by the images of the two embeddings, which is σ-compact, and extends the result by the identity; taking U to be the whole manifold removes the σ-compactness assumption. This is what makes a connected sum independent of its balls.

Main results

• TauCeti.SmoothEmbedding.exists_smoothIsotopy_of_isOrientationPreservingAt: two orientation-preserving embeddings with a common centre are isotopic relative to the centre.
• TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_isOrientationPreservingAt: on a connected manifold, two orientation-preserving embeddings agree on any compact set after an ambient compactly supported diffeotopy.
• TauCeti.SmoothEmbedding.exists_diffeomorph_comp_eventuallyEq: on a connected manifold, two orientation-preserving embeddings agree near the origin after a diffeomorphism.
• TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_isOrientationPreservingAt_of_range_subset: the relative form, for two embeddings with images in a preconnected open set U; the diffeotopy fixes every point outside a compact subset of U.

References

• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 4, §6, Theorem 6.6.
• R. Palais, Extending diffeomorphisms, Proc. Amer. Math. Soc. 11 (1960), 274–277.

theorem TauCeti.SmoothEmbedding.exists_smoothIsotopy_of_isOrientationPreservingAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_3} [Fintype ι] (f g : SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) (↑⊤) E M) (hcentre : f 0 = g 0) (o : Manifold.Orientation (modelWithCornersSelf ℝ E) E ι) (oM : Manifold.Orientation (modelWithCornersSelf ℝ E) M ι) (hf : o.IsOrientationPreservingAt oM (⇑f) 0) (hg : o.IsOrientationPreservingAt oM (⇑g) 0) : ∃ (G : SmoothIsotopy f.toContMDiffMap g.toContMDiffMap), ∀ (t : ↑unitInterval), G (t, 0) = f 0

The oriented common-centre disc theorem. Two smooth embeddings that preserve the chosen orientations at the origin and have the same centre are smoothly isotopic relative to that centre. No orientation condition away from the origin is required.

theorem TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_isOrientationPreservingAt_of_range_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_3} [Fintype ι] [T2Space M] {U : Set M} (hU : IsOpen U) (hUc : IsPreconnected U) (f g : SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) (↑⊤) E M) (hfU : Set.range ⇑f ⊆ U) (hgU : Set.range ⇑g ⊆ U) (o : Manifold.Orientation (modelWithCornersSelf ℝ E) E ι) (oM : Manifold.Orientation (modelWithCornersSelf ℝ E) M ι) (hf : o.IsOrientationPreservingAt oM (⇑f) 0) (hg : o.IsOrientationPreservingAt oM (⇑g) 0) {A : Set E} (hA : IsCompact A) : ∃ (Φ : Diffeotopy (modelWithCornersSelf ℝ E) (↑⊤) M) (K : Set M), IsCompact K ∧ K ⊆ U ∧ (∀ (t : ↑unitInterval), ∀ y ∉ K, (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) (t, y) = y) ∧ Set.EqOn (⇑Φ.final ∘ ⇑f) (⇑g) A

The relative ambient disc theorem. Let f and g be smooth embeddings of E into a Hausdorff boundaryless manifold M modelled on E, preserving the orientations o of E and oM of M at the origin, with images in a preconnected open set U. On every compact subset A of E, g is f followed by the final diffeomorphism of a smooth diffeotopy of M fixing every point outside a compact subset of U. Points outside U, for instance protected discs and collars, are not moved.

theorem TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_isOrientationPreservingAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_3} [Fintype ι] [T2Space M] [PreconnectedSpace M] (f g : SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) (↑⊤) E M) (o : Manifold.Orientation (modelWithCornersSelf ℝ E) E ι) (oM : Manifold.Orientation (modelWithCornersSelf ℝ E) M ι) (hf : o.IsOrientationPreservingAt oM (⇑f) 0) (hg : o.IsOrientationPreservingAt oM (⇑g) 0) {A : Set E} (hA : IsCompact A) : ∃ (Φ : Diffeotopy (modelWithCornersSelf ℝ E) (↑⊤) M) (K : Set M), IsCompact K ∧ (∀ (t : ↑unitInterval), ∀ y ∉ K, (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) (t, y) = y) ∧ Set.EqOn (⇑Φ.final ∘ ⇑f) (⇑g) A

The ambient disc theorem for oriented embeddings (Palais). Let f and g be smooth embeddings of E into a connected Hausdorff boundaryless manifold M modelled on E, which preserve the orientations o of E and oM of M at the origin; their centres f 0 and g 0 may differ. On every compact subset A of E, g is f followed by the final diffeomorphism of a smooth diffeotopy of M fixing every point outside a compact set.

theorem TauCeti.SmoothEmbedding.exists_diffeomorph_comp_eventuallyEq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] {ι : Type u_3} [Fintype ι] [T2Space M] [PreconnectedSpace M] (f g : SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) (↑⊤) E M) (o : Manifold.Orientation (modelWithCornersSelf ℝ E) E ι) (oM : Manifold.Orientation (modelWithCornersSelf ℝ E) M ι) (hf : o.IsOrientationPreservingAt oM (⇑f) 0) (hg : o.IsOrientationPreservingAt oM (⇑g) 0) : ∃ (φ : Diffeomorph (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) M M ↑⊤), ⇑φ ∘ ⇑f =ᶠ[nhds 0] ⇑g

On a connected oriented manifold, two smooth embeddings of E which preserve the orientations o of E and oM of M at the origin agree near the origin after a diffeomorphism of M.