Postcomposing smooth isotopies with local diffeomorphisms

A smooth isotopy whose motion stays in a set s, postcomposed with a map which is a local diffeomorphism at every point of s and a topological embedding on s, is again a smooth isotopy. The map need not be defined smoothly, or injective, away from s, so this applies to the inverse of a chart on a motion confined to the chart's target, and to radial contractions of a model space.

This is the smooth counterpart of TauCeti.Isotopy.postcomp, where any topological embedding may be applied; here the time slices must remain smooth embeddings, which TauCeti.isSmoothEmbedding_isLocalDiffeomorphAt_comp provides.

Main definitions

• TauCeti.SmoothIsotopy.postcomp: postcompose a smooth isotopy confined to s with a map which is a local diffeomorphism along s and a topological embedding on s.

def TauCeti.SmoothIsotopy.postcomp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H : Type u_3} [TopologicalSpace H] {H' : Type u_4} [TopologicalSpace H'] {I : ModelWithCorners ℝ E 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 ℕ∞} {P : Type u_7} [TopologicalSpace P] [ChartedSpace H' P] [IsManifold J n P] {f₀ f₁ : ContMDiffMap I J M N n} (K : SmoothIsotopy f₀ f₁) (k : N → P) {s : Set N} (hKs : ∀ (p : ↑unitInterval × M), K p ∈ s) (hk : ∀ y ∈ s, IsLocalDiffeomorphAt J J n k y) (hks : Topology.IsEmbedding (s.domRestrict k)) (g₀ g₁ : ContMDiffMap I J M P n) (hg₀ : ∀ (x : M), g₀ x = k (f₀ x)) (hg₁ : ∀ (x : M), g₁ x = k (f₁ x)) : SmoothIsotopy g₀ g₁

Postcompose a smooth isotopy with a map k which is a local diffeomorphism at every point of a set s containing the motion, and a topological embedding on s. The endpoints g₀ and g₁ are supplied as bundled maps agreeing with k ∘ f₀ and k ∘ f₁, since k itself need not be smooth away from s.

@[simp]

theorem TauCeti.SmoothIsotopy.postcomp_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H : Type u_3} [TopologicalSpace H] {H' : Type u_4} [TopologicalSpace H'] {I : ModelWithCorners ℝ E 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 ℕ∞} {P : Type u_7} [TopologicalSpace P] [ChartedSpace H' P] [IsManifold J n P] {f₀ f₁ : ContMDiffMap I J M N n} (K : SmoothIsotopy f₀ f₁) (k : N → P) {s : Set N} (hKs : ∀ (p : ↑unitInterval × M), K p ∈ s) (hk : ∀ y ∈ s, IsLocalDiffeomorphAt J J n k y) (hks : Topology.IsEmbedding (s.domRestrict k)) (g₀ g₁ : ContMDiffMap I J M P n) (hg₀ : ∀ (x : M), g₀ x = k (f₀ x)) (hg₁ : ∀ (x : M), g₁ x = k (f₁ x)) (p : ↑unitInterval × M) : (K.postcomp k hKs hk hks g₀ g₁ hg₀ hg₁) p = k (K p)