The Euclidean disc theorem

Two smooth embeddings between real normed spaces, with finite-dimensional source, that have the same value at the origin and derivative equivalences with positive relative determinant are smoothly isotopic, fixing that value throughout. For self-embeddings, agreement in orientation is expressed by positivity of the product of their derivative determinants, so both determinants may be negative.

Translate the common centre to zero, linearize both embeddings by rescaling, and connect the two linear maps through their orientation-preserving relative map. Smooth concatenation and translation back give the relative isotopy. This is the Euclidean ambient-space case of the disc theorem, for the open-disc source ℝⁿ. It provides the comparison of embeddings in Euclidean coordinates; it does not assert an ambient isotopy or compare embeddings into a general manifold.

For self-embeddings with values in a Euclidean ball about the common centre, the isotopy can be confined to that ball (exists_smoothIsotopy_mapsTo_ball): the motion is followed by a radial contraction onto the ball, and its ends are joined to the two embeddings by radial contractions, which keep the ball in place. This is the form in which a chart carries the theorem to a manifold.

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.

The construction uses linearizationIsotopy, ContinuousLinearEquiv.exists_smoothIsotopy, and SmoothIsotopy.trans.

theorem TauCeti.SmoothEmbedding.exists_smoothIsotopy_of_det_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f g : SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ F) (↑⊤) E F) (hcentre : f 0 = g 0) (Lf Lg : E ≃L[ℝ] F) (hLf : HasFDerivAt (⇑f) (↑Lf) 0) (hLg : HasFDerivAt (⇑g) (↑Lg) 0) (hrelative : 0 < (↑(Lf.trans Lg.symm)).det) : ∃ (G : SmoothIsotopy f.toContMDiffMap g.toContMDiffMap), ∀ (t : ↑unitInterval), G (t, 0) = f 0

Euclidean disc theorem. Smooth embeddings with a common centre and derivative equivalences with positive relative determinant are smoothly isotopic relative to that centre. The source is finite-dimensional; the target needs neither an orientation nor a completeness instance.

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

Euclidean disc theorem. Smooth self-embeddings with a common centre and the same derivative orientation there are smoothly isotopic relative to that centre. The determinant condition permits either common orientation and includes dimension zero.

theorem TauCeti.SmoothEmbedding.exists_smoothIsotopy_mapsTo_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {c : E} {r : ℝ} (f g : SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) (↑⊤) E E) (hf0 : f 0 = c) (hg0 : g 0 = c) (hf : ∀ (x : E), f x ∈ Euclidean.ball c r) (hg : ∀ (x : E), g x ∈ Euclidean.ball c r) (hdet : 0 < (fderiv ℝ (⇑f) 0).det * (fderiv ℝ (⇑g) 0).det) : ∃ (L : SmoothIsotopy f.toContMDiffMap g.toContMDiffMap), (∀ (q : ↑unitInterval × E), L q ∈ Euclidean.ball c r) ∧ ∀ (t : ↑unitInterval), L (t, 0) = c

The disc theorem in a ball. Smooth self-embeddings with values in a Euclidean ball, centred at its centre, with the same derivative orientation there, are smoothly isotopic relative to the centre through embeddings with values in the ball.