The disc theorem in a manifold

Let M be a boundaryless smooth manifold modelled on a finite-dimensional real normed space E. Two smooth embeddings f g : E → M with the same centre f 0 = g 0, whose derivatives at 0 have the same orientation, are smoothly isotopic through embeddings, relative to the centre (TauCeti.SmoothEmbedding.exists_smoothIsotopy_of_det_chartAt_mul_pos). The orientations are compared in the chart at the centre, by asking that the product of the two derivative determinants be positive.

This is the disc theorem in the form of Hirsch, Chapter 4, Theorem 6.6, for open discs E ≅ ℝⁿ: the condition there, Det (D(g⁻¹ ∘ f)(0)) > 0, is the positivity of the product of determinants above.

The isotopy extension theorem (TauCeti.SmoothIsotopy.exists_diffeotopy_final_apply_eq) turns this into the ambient form of Palais's disc theorem, used to show that connected sums are well defined: on every compact subset of E, g is f followed by the final diffeomorphism of a compactly supported diffeotopy of M (TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_det_chartAt_mul_pos). On a connected oriented manifold the centres can first be made to agree by a compactly supported diffeotopy (TauCeti.exists_diffeotopy_final_apply_eq), which gives the ambient disc theorem for embeddings with different centres (TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_isOrientationPreservingAt).

The Euclidean case is TauCeti.SmoothEmbedding.exists_smoothIsotopy_of_det_mul_pos. To reduce to it, both embeddings are first shrunk by precomposing with a radial contraction of E onto a small Euclidean ball about 0 (TauCeti.SmoothEmbedding.compRadialContractionIsotopy), so that they land in a Euclidean ball B inside the chart at the centre. Read in the chart (TauCeti.SmoothEmbedding.transChart), they are embeddings E → E with values in B, and the Euclidean disc theorem confined to B (TauCeti.SmoothEmbedding.exists_smoothIsotopy_mapsTo_ball) connects them. Since the motion stays in B, the inverse chart carries it back to M (TauCeti.SmoothIsotopy.postcomp).

Main results

• TauCeti.SmoothEmbedding.exists_smoothIsotopy_of_det_chartAt_mul_pos: the disc theorem in a manifold, for embeddings with a common centre.
• TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_det_chartAt_mul_pos: the ambient disc theorem, for embeddings with a common centre, on compact subsets of E.

References

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

theorem TauCeti.SmoothEmbedding.exists_smoothIsotopy_of_det_chartAt_mul_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] (f g : SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) (↑⊤) E M) (hcentre : f 0 = g 0) (hdet : 0 < (fderiv ℝ (↑(chartAt E (f 0)) ∘ ⇑f) 0).det * (fderiv ℝ (↑(chartAt E (f 0)) ∘ ⇑g) 0).det) : ∃ (G : SmoothIsotopy f.toContMDiffMap g.toContMDiffMap), ∀ (t : ↑unitInterval), G (t, 0) = f 0

The disc theorem in a manifold. Two smooth embeddings of E into a boundaryless manifold modelled on E, with the same centre f 0 = g 0 and derivatives at 0 of the same orientation, are smoothly isotopic relative to that centre. The orientations are compared in the chart at the centre: the product of the derivative determinants there is positive. This condition does not depend on the chart, since a change of chart multiplies both determinants by the same nonzero number. For M = E it is the hypothesis of the Euclidean disc theorem TauCeti.SmoothEmbedding.exists_smoothIsotopy_of_det_mul_pos.

theorem TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_det_chartAt_mul_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] [T2Space M] [SigmaCompactSpace M] (f g : SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) (↑⊤) E M) (hcentre : f 0 = g 0) (hdet : 0 < (fderiv ℝ (↑(chartAt E (f 0)) ∘ ⇑f) 0).det * (fderiv ℝ (↑(chartAt E (f 0)) ∘ ⇑g) 0).det) {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 in a manifold. Let f and g be smooth embeddings of E into a Hausdorff, σ-compact boundaryless manifold modelled on E, with the same centre f 0 = g 0 and derivatives at 0 of the same orientation, compared in the chart at the centre. 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.