The smooth ambient-isotopy equivalence relation #
This file defines smooth ambient isotopy for arbitrary bundled smooth maps between real manifolds. Two maps are smoothly ambient isotopic when the final diffeomorphism of a diffeotopy of the codomain carries the first map to the second.
The relation is defined generally before its specialization to bundled smooth embeddings in
TauCeti.Geometry.Manifold.SmoothEmbedding.SmoothAmbientIsotopy.Basic, following the
GeometricTopology roadmap's encoding convention. Forgetting smoothness recovers
TauCeti.AmbientIsotopic.
Main definitions #
TauCeti.SmoothAmbientIsotopic: smooth ambient isotopy of arbitrary bundled smooth maps.TauCeti.SmoothAmbientIsotopic.setoid: the resulting equivalence relation.
Main results #
TauCeti.SmoothAmbientIsotopic.refl,symm, andtrans: smooth ambient isotopy is an equivalence relation.TauCeti.SmoothAmbientIsotopic.final_comp: a map is smoothly ambient isotopic to its postcomposition with the time-one map of a diffeotopy.TauCeti.SmoothAmbientIsotopic.precomp: smooth ambient isotopy is preserved by precomposing both maps with a fixed smooth map.TauCeti.SmoothAmbientIsotopic.ambientIsotopic: smooth ambient isotopy implies continuous ambient isotopy.
References #
- G. Burde and H. Zieschang, Knots, 2nd ed., de Gruyter (2003), Chapter 1, for ambient isotopy of knots.
- M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 8, §8.1, for smooth isotopies and diffeotopies.
def
TauCeti.SmoothAmbientIsotopic
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{J : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{J' : ModelWithCorners ℝ E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
(f g : ContMDiffMap J J' M N n)
:
Two bundled smooth maps are smoothly ambient isotopic when the final diffeomorphism of a
C^n diffeotopy of the codomain carries the first map to the second.
Equations
- TauCeti.SmoothAmbientIsotopic f g = ∃ (Φ : TauCeti.Diffeotopy J' n N), (↑Φ.final).comp f = g
Instances For
theorem
TauCeti.smoothAmbientIsotopic_def
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{J : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{J' : ModelWithCorners ℝ E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{f g : ContMDiffMap J J' M N n}
:
Smooth ambient isotopy is witnessed by a diffeotopy whose final diffeomorphism postcomposes the first smooth map to the second.
theorem
TauCeti.SmoothAmbientIsotopic.of_diffeotopy
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{J : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{J' : ModelWithCorners ℝ E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{f g : ContMDiffMap J J' M N n}
(Φ : Diffeotopy J' n N)
(hΦ : (↑Φ.final).comp f = g)
:
A diffeotopy carrying f to g witnesses their smooth ambient isotopy.
theorem
TauCeti.SmoothAmbientIsotopic.final_comp
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{J : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{J' : ModelWithCorners ℝ E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
(f : ContMDiffMap J J' M N n)
(Φ : Diffeotopy J' n N)
:
SmoothAmbientIsotopic f ((↑Φ.final).comp f)
Transport along a diffeotopy is an ambient isotopy. A smooth map and its postcomposition with the time-one map of a diffeotopy of the codomain are smoothly ambient isotopic: the diffeotopy itself is the witness.
theorem
TauCeti.SmoothAmbientIsotopic.refl
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{J : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{J' : ModelWithCorners ℝ E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
(f : ContMDiffMap J J' M N n)
:
Smooth ambient isotopy of smooth maps is reflexive.
theorem
TauCeti.SmoothAmbientIsotopic.symm
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{J : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{J' : ModelWithCorners ℝ E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{f g : ContMDiffMap J J' M N n}
(hfg : SmoothAmbientIsotopic f g)
:
Smooth ambient isotopy of smooth maps is symmetric.
theorem
TauCeti.SmoothAmbientIsotopic.trans
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{J : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{J' : ModelWithCorners ℝ E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{f g h : ContMDiffMap J J' M N n}
(hfg : SmoothAmbientIsotopic f g)
(hgh : SmoothAmbientIsotopic g h)
:
Smooth ambient isotopy of smooth maps is transitive.
theorem
TauCeti.SmoothAmbientIsotopic.precomp
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{J : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{J' : ModelWithCorners ℝ E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{f g : ContMDiffMap J J' M N n}
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace ℝ E'']
{H'' : Type u_8}
[TopologicalSpace H'']
{J'' : ModelWithCorners ℝ E'' H''}
{M'' : Type u_9}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
(hfg : SmoothAmbientIsotopic f g)
(k : ContMDiffMap J'' J M'' M n)
:
SmoothAmbientIsotopic (f.comp k) (g.comp k)
Precomposing two smoothly ambient-isotopic maps with the same smooth map preserves the relation: the witnessing diffeotopy of the codomain is unchanged.
theorem
TauCeti.SmoothAmbientIsotopic.ambientIsotopic
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{J : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{J' : ModelWithCorners ℝ E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{f g : ContMDiffMap J J' M N n}
(hfg : SmoothAmbientIsotopic f g)
:
AmbientIsotopic ↑f ↑g
Smooth ambient isotopy implies continuous ambient isotopy after forgetting smoothness.
theorem
TauCeti.SmoothAmbientIsotopic.equivalence
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{J : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{J' : ModelWithCorners ℝ E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
:
Smooth ambient isotopy is an equivalence relation on bundled smooth maps.
def
TauCeti.SmoothAmbientIsotopic.setoid
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
(J : ModelWithCorners ℝ E H)
(J' : ModelWithCorners ℝ E' H')
(n : WithTop ℕ∞)
(M : Type u_7)
[TopologicalSpace M]
[ChartedSpace H M]
(N : Type u_8)
[TopologicalSpace N]
[ChartedSpace H' N]
:
Setoid (ContMDiffMap J J' M N n)
The smooth-ambient-isotopy equivalence relation on bundled smooth maps.
Equations
- TauCeti.SmoothAmbientIsotopic.setoid J J' n M N = { r := TauCeti.SmoothAmbientIsotopic, iseqv := ⋯ }
Instances For
@[simp]
theorem
TauCeti.SmoothAmbientIsotopic.setoid_r_iff
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{J : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{J' : ModelWithCorners ℝ E' H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
{f g : ContMDiffMap J J' M N n}
:
The relation of the smooth-ambient-isotopy setoid is smooth ambient isotopy.