Smooth isotopies through embeddings #
A SmoothIsotopy f₀ f₁ is a jointly C^n map on unitInterval × M from f₀ to
f₁ whose time slices are smooth embeddings. The endpoints are arbitrary bundled
smooth maps; existence of an isotopy forces them to be embeddings.
The time interval carries Mathlib's manifold-with-boundary structure. Forgetting
smoothness produces the existing continuous TauCeti.Isotopy, with exactly the
same time slices. Constant isotopies, smooth changes of time, and time reversal
are provided here, as is the isotopy SmoothIsotopy.ofContDiff given by a C^n map on
ℝ × E between normed spaces. Smooth concatenation is provided in SmoothIsotopy.Trans;
isotopy extension is a separate result.
This slice-wise convention does not impose properness on a noncompact source. Ambient isotopy remains the relation used for knot equivalence; a smooth isotopy is the input to an isotopy extension theorem, rather than an assertion that such an extension exists.
References #
- M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 8, §8.1.
The continuous forgetful construction follows Mathlib's ContinuousMap.HomotopyWith
and Tau Ceti's Isotopy.
structure
TauCeti.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 ℕ∞}
(f₀ f₁ : ContMDiffMap I J M N n)
:
Type (max u_5 u_6)
A jointly C^n homotopy through smooth embeddings, with prescribed endpoints.
The source and target may have boundary or corners.
- toContMDiffMap : ContMDiffMap ((modelWithCornersEuclideanHalfSpace 1).prod I) J (↑unitInterval × M) N n
The motion, smooth in both time and the source variable.
The motion starts at
f₀.The motion ends at
f₁.- isSmoothEmbedding (t : ↑unitInterval) : Manifold.IsSmoothEmbedding I J n fun (x : M) => self.toContMDiffMap (t, x)
Every time slice is a smooth embedding.
Instances For
@[instance_reducible]
instance
TauCeti.SmoothIsotopy.instFunLikeProdElemRealUnitInterval
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
:
FunLike (SmoothIsotopy f₀ f₁) (↑unitInterval × M) N
Evaluate a smooth isotopy at a time and a source point.
@[simp]
theorem
TauCeti.SmoothIsotopy.toContMDiffMap_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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
(p : ↑unitInterval × M)
:
The underlying smooth map evaluates to the motion.
@[simp]
theorem
TauCeti.SmoothIsotopy.apply_zero
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
(x : M)
:
The motion starts at its initial endpoint.
@[simp]
theorem
TauCeti.SmoothIsotopy.apply_one
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
(x : M)
:
The motion ends at its final endpoint.
theorem
TauCeti.SmoothIsotopy.ext
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
{F G : SmoothIsotopy f₀ f₁}
(h : ∀ (p : ↑unitInterval × M), F p = G p)
:
Two smooth isotopies agree when their motions agree pointwise.
theorem
TauCeti.SmoothIsotopy.ext_iff
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
{F G : SmoothIsotopy f₀ f₁}
:
theorem
TauCeti.SmoothIsotopy.contMDiff
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
:
ContMDiff ((modelWithCornersEuclideanHalfSpace 1).prod I) J n ⇑F
A smooth isotopy is jointly smooth in time and space.
noncomputable def
TauCeti.SmoothIsotopy.timeSlice
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
(t : ↑unitInterval)
:
SmoothEmbedding I J n M N
The time-t slice, bundled as a smooth embedding.
Instances For
@[simp]
theorem
TauCeti.SmoothIsotopy.timeSlice_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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
(t : ↑unitInterval)
(x : M)
:
Evaluating a time slice is evaluating the isotopy at that time.
theorem
TauCeti.SmoothIsotopy.isSmoothEmbedding_left
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
:
Manifold.IsSmoothEmbedding I J n ⇑f₀
The initial endpoint of a smooth isotopy is a smooth embedding.
theorem
TauCeti.SmoothIsotopy.isSmoothEmbedding_right
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
:
Manifold.IsSmoothEmbedding I J n ⇑f₁
The final endpoint of a smooth isotopy is a smooth embedding.
def
TauCeti.SmoothIsotopy.toIsotopy
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
:
Isotopy ↑f₀ ↑f₁
Forgetting smoothness gives a continuous isotopy through embeddings.
Instances For
@[simp]
theorem
TauCeti.SmoothIsotopy.toIsotopy_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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
(p : ↑unitInterval × M)
:
Forgetting smoothness preserves the motion.
theorem
TauCeti.SmoothIsotopy.isotopic
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
:
Isotopic ↑f₀ ↑f₁
Smooth isotopy implies the existing continuous isotopy relation.
def
ContMDiffMap.smoothIsotopyRefl
{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 ℕ∞}
(f : ContMDiffMap I J M N n)
(hf : Manifold.IsSmoothEmbedding I J n ⇑f)
:
The constant smooth isotopy at a smooth embedding.
Instances For
@[simp]
theorem
ContMDiffMap.smoothIsotopyRefl_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 ℕ∞}
(f : ContMDiffMap I J M N n)
(hf : Manifold.IsSmoothEmbedding I J n ⇑f)
(p : ↑unitInterval × M)
:
A constant isotopy keeps its source points stationary.
def
TauCeti.SmoothIsotopy.reparam
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
(ρ :
ContMDiffMap (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersEuclideanHalfSpace 1) (↑unitInterval)
(↑unitInterval) n)
(h₀ : ρ 0 = 0)
(h₁ : ρ 1 = 1)
:
SmoothIsotopy f₀ f₁
Change time by a smooth map of the unit interval fixing its endpoints. The time map need not be injective or monotone.
Instances For
@[simp]
theorem
TauCeti.SmoothIsotopy.reparam_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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
(ρ :
ContMDiffMap (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersEuclideanHalfSpace 1) (↑unitInterval)
(↑unitInterval) n)
(h₀ : ρ 0 = 0)
(h₁ : ρ 1 = 1)
(p : ↑unitInterval × M)
:
A time change evaluates the original isotopy at the new time.
def
TauCeti.SmoothIsotopy.symm
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
:
SmoothIsotopy f₁ f₀
Reverse a smooth isotopy in time.
Instances For
@[simp]
theorem
TauCeti.SmoothIsotopy.symm_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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
(p : ↑unitInterval × M)
:
Time reversal evaluates the original isotopy at 1 - t.
@[simp]
theorem
TauCeti.SmoothIsotopy.symm_symm
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(F : SmoothIsotopy f₀ f₁)
:
Reversing time twice recovers the original smooth isotopy.
def
TauCeti.SmoothIsotopy.ofContDiff
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{n : WithTop ℕ∞}
{f₀ f₁ : ContMDiffMap (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E') E E' n}
(G : ℝ × E → E')
(hG : ContDiff ℝ n G)
(h₀ : ∀ (x : E), G (0, x) = f₀ x)
(h₁ : ∀ (x : E), G (1, x) = f₁ x)
(hemb :
∀ u ∈ Set.Icc 0 1,
Manifold.IsSmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E') n fun (x : E) => G (u, x))
:
SmoothIsotopy f₀ f₁
The smooth isotopy given by a C^n map G on ℝ × E, read on [0, 1] × E, which starts at
f₀, ends at f₁, and whose time slices over [0, 1] are smooth embeddings.
Instances For
@[simp]
theorem
TauCeti.SmoothIsotopy.ofContDiff_apply
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{n : WithTop ℕ∞}
{f₀ f₁ : ContMDiffMap (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E') E E' n}
(G : ℝ × E → E')
(hG : ContDiff ℝ n G)
(h₀ : ∀ (x : E), G (0, x) = f₀ x)
(h₁ : ∀ (x : E), G (1, x) = f₁ x)
(hemb :
∀ u ∈ Set.Icc 0 1,
Manifold.IsSmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E') n fun (x : E) => G (u, x))
(q : ↑unitInterval × E)
:
The isotopy given by a C^n map on ℝ × E evaluates to that map.
def
TauCeti.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 ℕ∞}
(f₀ f₁ : ContMDiffMap I J M N n)
:
Two bundled smooth maps are smoothly isotopic when a jointly smooth homotopy through smooth embeddings connects them. This does not assert ambient isotopy.
Instances For
theorem
TauCeti.smoothIsotopic_def
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
:
Smooth isotopy is witnessed by a smooth isotopy through embeddings.
theorem
ContMDiffMap.smoothIsotopic_refl
{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 ℕ∞}
(f : ContMDiffMap I J M N n)
(hf : Manifold.IsSmoothEmbedding I J n ⇑f)
:
A smooth embedding is smoothly isotopic to itself.
theorem
TauCeti.SmoothIsotopic.symm
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(h : SmoothIsotopic f₀ f₁)
:
SmoothIsotopic f₁ f₀
Smooth isotopy is symmetric.
theorem
TauCeti.SmoothIsotopic.isotopic
{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 ℕ∞}
{f₀ f₁ : ContMDiffMap I J M N n}
(h : SmoothIsotopic f₀ f₁)
:
Isotopic ↑f₀ ↑f₁
Smoothly isotopic maps are isotopic after forgetting smoothness.