Extending diffeotopies by the identity

A diffeotopy of N which fixes every point outside a compact set at all times extends along a smooth open embedding χ : N → M into a Hausdorff manifold: the extension moves χ z as the original motion moves z, and fixes every point outside the image of the compact set (TauCeti.Diffeotopy.exists_extend_of_isCompact). For the inclusion of an open subset this transplants a motion built inside the open subset to the ambient manifold, keeping all of its moving points inside the subset.

The total level-preserving diffeomorphism of I × N is extended along Prod.map id χ by IsLocalDiffeomorph.exists_diffeomorph_extend_of_isCompact; the extension preserves the time coordinate and starts at the identity because it either agrees with the original motion or is the identity.

References

• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 8, §8.1, for diffeotopies with compact support.

theorem TauCeti.Diffeotopy.exists_extend_of_isCompact {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_4} [TopologicalSpace H'] {J' : ModelWithCorners ℝ E' H'} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H' M] {N : Type u_6} [TopologicalSpace N] [ChartedSpace H N] {n : WithTop ℕ∞} [T2Space M] {χ : N → M} (hχ : IsLocalDiffeomorph J J' n χ) (hχo : Topology.IsOpenEmbedding χ) (Λ : Diffeotopy J n N) {K : Set N} (hK : IsCompact K) (hΛ : ∀ (t : ↑unitInterval), ∀ z ∉ K, (fun (p : ↑unitInterval × N) => (Λ.toDiffeomorph p).2) (t, z) = z) : ∃ (Φ : Diffeotopy J' n M), (∀ (t : ↑unitInterval) (z : N), (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) (t, χ z) = χ ((fun (p : ↑unitInterval × N) => (Λ.toDiffeomorph p).2) (t, z))) ∧ ∀ (t : ↑unitInterval), ∀ y ∉ χ '' K, (fun (p : ↑unitInterval × M) => (Φ.toDiffeomorph p).2) (t, y) = y

A diffeotopy of N fixing every point outside a compact set K at all times extends along a smooth open embedding χ : N → M into a Hausdorff manifold. The extension moves χ z as the original motion moves z, and fixes every point outside χ '' K at all times.