Smooth isotopies induced by diffeotopies #
Restrict an ambient diffeotopy to a smooth embedding to obtain a smooth isotopy through embeddings. The motion is jointly smooth, and every slice is the original embedding followed by a diffeomorphism. This connects smooth ambient isotopy to the general smooth isotopy type without assuming an isotopy extension theorem.
References #
- M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 8, §8.1.
The construction uses Tau Ceti's Diffeotopy.timeSlice and the smooth-embedding
invariance theorem isSmoothEmbedding_diffeomorph_comp.
def
TauCeti.Diffeotopy.smoothIsotopy
{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 ℕ∞}
[IsManifold J n N]
(Φ : Diffeotopy J n N)
(f : ContMDiffMap I J M N n)
(hf : Manifold.IsSmoothEmbedding I J n ⇑f)
:
SmoothIsotopy f ((↑Φ.final).comp f)
An ambient diffeotopy restricts to a smooth isotopy of any smooth embedding.
Instances For
@[simp]
theorem
TauCeti.Diffeotopy.smoothIsotopy_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 ℕ∞}
[IsManifold J n N]
(Φ : Diffeotopy J n N)
(f : ContMDiffMap I J M N n)
(hf : Manifold.IsSmoothEmbedding I J n ⇑f)
(p : ↑unitInterval × M)
:
Restricting a diffeotopy evaluates the ambient motion on the embedded point.
theorem
TauCeti.SmoothAmbientIsotopic.smoothIsotopic
{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 ℕ∞}
[IsManifold J n N]
{f g : ContMDiffMap I J M N n}
(h : SmoothAmbientIsotopic f g)
(hf : Manifold.IsSmoothEmbedding I J n ⇑f)
:
SmoothIsotopic f g
Smooth ambient isotopy of an embedding is witnessed by a smooth isotopy through embeddings.