Isotopies of homeomorphisms of compact manifolds are ambient

An isotopy (TauCeti.Isotopy) only asks every time slice to be a topological embedding, while an ambient isotopy (TauCeti.AmbientIsotopy) is a motion of the whole space by homeomorphisms. Every ambient isotopy Φ of Y moves a homeomorphism f₀ : X ≃ₜ Y by the isotopy t ↦ Φ_t ∘ f₀ (TauCeti.AmbientIsotopy.isotopic). This file proves the converse when Y is a compact connected topological manifold without boundary: every isotopy starting at f₀ is of that form (TauCeti.isotopic_iff_ambientIsotopic). So for self-homeomorphisms of such a manifold, for instance of the torus S¹ × S¹, isotopy in the general sense of TauCeti.Isotopic is isotopy through homeomorphisms.

There are two steps.

• Point-set topology. If Y is compact Hausdorff and every time slice of an isotopy F starting at f₀ is onto, then (t, y) ↦ F (t, f₀⁻¹ y) is an ambient isotopy of Y (TauCeti.AmbientIsotopy.ofIsotopy): its level-preserving total map is a continuous bijection of the compact Hausdorff space [0, 1] × Y, hence a homeomorphism.
• Invariance of domain. If Y is moreover a connected manifold, every time slice is onto (TauCeti.Isotopy.surjective_apply): read through f₀, it is a continuous injection of Y into itself, which is onto by invariance of domain (Continuous.surjective_of_injective).

Main definitions

• TauCeti.AmbientIsotopy.ofIsotopy: the ambient isotopy traced by an isotopy of a homeomorphism onto a compact Hausdorff space whose time slices are onto.

Main results

• TauCeti.AmbientIsotopy.final_ofIsotopy_apply: it moves the initial homeomorphism to the end of the isotopy.
• TauCeti.Isotopy.surjective_apply: an isotopy of a homeomorphism onto a compact connected manifold is onto at every time.
• TauCeti.isotopic_iff_ambientIsotopic: a map is isotopic to a homeomorphism f₀ onto a compact connected manifold exactly when it is ambient isotopic to f₀, that is, it is Φ₁ ∘ f₀ for an ambient isotopy Φ.

References

• M. W. Hirsch, Differential Topology, Graduate Texts in Mathematics 33, Springer (1976), Chapter 8, Section 1 (isotopies and ambient isotopies).

def TauCeti.AmbientIsotopy.ofIsotopy {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] (f₀ : X ≃ₜ Y) {f₁ : C(X, Y)} (F : Isotopy (↑f₀) f₁) (hF : ∀ (t : ↑unitInterval), Function.Surjective fun (x : X) => F (t, x)) : AmbientIsotopy Y

The ambient isotopy traced by an isotopy F starting at a homeomorphism f₀ : X ≃ₜ Y onto a compact Hausdorff space, all of whose time slices are onto: it is (t, y) ↦ F (t, f₀⁻¹ y). Its level-preserving total map is a continuous bijection of the compact Hausdorff space [0, 1] × Y, hence a homeomorphism. It carries f₀ to the end f₁ of the isotopy (TauCeti.AmbientIsotopy.final_ofIsotopy_apply).

@[simp]

theorem TauCeti.AmbientIsotopy.ofIsotopy_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] (f₀ : X ≃ₜ Y) {f₁ : C(X, Y)} (F : Isotopy (↑f₀) f₁) (hF : ∀ (t : ↑unitInterval), Function.Surjective fun (x : X) => F (t, x)) (p : ↑unitInterval × Y) : (ofIsotopy f₀ F hF).toContinuousMap p = F (p.1, f₀.symm p.2)

theorem TauCeti.AmbientIsotopy.final_ofIsotopy_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] (f₀ : X ≃ₜ Y) {f₁ : C(X, Y)} (F : Isotopy (↑f₀) f₁) (hF : ∀ (t : ↑unitInterval), Function.Surjective fun (x : X) => F (t, x)) (x : X) : (ofIsotopy f₀ F hF).final (f₀ x) = f₁ x

The ambient isotopy traced by an isotopy F from f₀ to f₁ carries f₀ to f₁.

theorem TauCeti.Isotopy.surjective_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E Y] [CompactSpace Y] [T2Space Y] [ConnectedSpace Y] (f₀ : X ≃ₜ Y) {f₁ : C(X, Y)} (F : Isotopy (↑f₀) f₁) (t : ↑unitInterval) : Function.Surjective fun (x : X) => F (t, x)

An isotopy of a homeomorphism onto a compact connected manifold is onto at every time. If Y is a compact connected topological manifold without boundary, every time slice of an isotopy starting at a homeomorphism f₀ : X ≃ₜ Y is surjective: composed with f₀⁻¹, it is a continuous injection of Y into itself, which is onto by invariance of domain.

theorem TauCeti.isotopic_iff_ambientIsotopic {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E Y] [CompactSpace Y] [T2Space Y] [ConnectedSpace Y] (f₀ : X ≃ₜ Y) (f₁ : C(X, Y)) : Isotopic (↑f₀) f₁ ↔ AmbientIsotopic (↑f₀) f₁

Isotopy of a homeomorphism of a compact connected manifold is ambient. If Y is a compact connected topological manifold without boundary, a map f₁ : C(X, Y) is isotopic to a homeomorphism f₀ : X ≃ₜ Y exactly when it is ambient isotopic to f₀, that is f₁ = Φ₁ ∘ f₀ for some ambient isotopy Φ of Y.