Smooth ambient isotopy of smooth embeddings

This file specializes TauCeti.SmoothAmbientIsotopic, the smooth ambient-isotopy relation on arbitrary bundled smooth maps, to bundled smooth embeddings. Two embeddings are related when a diffeotopy of the codomain carries the first to the second at time one. This is the smooth equivalence relation needed by geometric knot presentations: unlike SmoothEmbedding.ContinuousAmbientIsotopic, its witness is smooth in both time and the ambient variable and every time slice is a diffeomorphism.

The general relation is defined once for arbitrary C^n maps; this file's relation is its thin specialization along SmoothEmbedding.toContMDiffMap. Smooth knots are obtained by taking the domain to be the circle and the codomain to be the ambient 3-manifold. Forgetting the diffeotopy's smoothness recovers continuous ambient isotopy.

This is the specialization of TauCeti.Diffeotopy requested by Layer 4 of the GeometricTopology roadmap, in the milestone “equivalence in each presentation.”

Main definitions

• TauCeti.SmoothEmbedding.SmoothAmbientIsotopic: smooth ambient isotopy of bundled smooth embeddings.
• TauCeti.SmoothEmbedding.SmoothAmbientIsotopic.setoid: the resulting equivalence relation.

Main results

• SmoothAmbientIsotopic.refl, symm, and trans: smooth ambient isotopy is an equivalence relation.
• SmoothAmbientIsotopic.continuousAmbientIsotopic: smoothly ambient isotopic embeddings are continuously ambient isotopic.

References

• G. Burde and H. Zieschang, Knots, 2nd ed., de Gruyter (2003), Chapter 1, for ambient isotopy as knot equivalence.
• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 8, §8.1, for smooth isotopies.

def TauCeti.SmoothEmbedding.SmoothAmbientIsotopic {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 g : SmoothEmbedding I J n M N) : Prop

Two smooth embeddings are smoothly ambient isotopic when the final diffeomorphism of a C^n diffeotopy of the codomain carries the first embedding to the second.

Equations

• f.SmoothAmbientIsotopic g = TauCeti.SmoothAmbientIsotopic f.toContMDiffMap g.toContMDiffMap

theorem TauCeti.SmoothEmbedding.smoothAmbientIsotopic_iff_toContMDiffMap {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 g : SmoothEmbedding I J n M N} : f.SmoothAmbientIsotopic g ↔ TauCeti.SmoothAmbientIsotopic f.toContMDiffMap g.toContMDiffMap

Smooth ambient isotopy of embeddings is exactly the general relation TauCeti.SmoothAmbientIsotopic on the underlying bundled smooth maps.

theorem TauCeti.SmoothEmbedding.smoothAmbientIsotopic_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 g : SmoothEmbedding I J n M N} : f.SmoothAmbientIsotopic g ↔ ∃ (Φ : Diffeotopy J n N), ∀ (x : M), Φ.final (f x) = g x

Smooth ambient isotopy is witnessed by a diffeotopy whose final diffeomorphism carries the first embedding pointwise to the second.

theorem TauCeti.SmoothEmbedding.SmoothAmbientIsotopic.of_diffeotopy {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 g : SmoothEmbedding I J n M N} (Φ : Diffeotopy J n N) (hΦ : ∀ (x : M), Φ.final (f x) = g x) : f.SmoothAmbientIsotopic g

A diffeotopy carrying f to g witnesses their smooth ambient isotopy.

theorem TauCeti.SmoothEmbedding.SmoothAmbientIsotopic.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 : SmoothEmbedding I J n M N) : f.SmoothAmbientIsotopic f

Smooth ambient isotopy of embeddings is reflexive.

theorem TauCeti.SmoothEmbedding.SmoothAmbientIsotopic.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 g : SmoothEmbedding I J n M N} (hfg : f.SmoothAmbientIsotopic g) : g.SmoothAmbientIsotopic f

Smooth ambient isotopy of embeddings is symmetric.

theorem TauCeti.SmoothEmbedding.SmoothAmbientIsotopic.trans {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 g h : SmoothEmbedding I J n M N} (hfg : f.SmoothAmbientIsotopic g) (hgh : g.SmoothAmbientIsotopic h) : f.SmoothAmbientIsotopic h

Smooth ambient isotopy of embeddings is transitive.

theorem TauCeti.SmoothEmbedding.SmoothAmbientIsotopic.equivalence {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 ℕ∞} : Equivalence SmoothAmbientIsotopic

Smooth ambient isotopy is an equivalence relation on bundled smooth embeddings.

theorem TauCeti.SmoothEmbedding.SmoothAmbientIsotopic.continuousAmbientIsotopic {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 g : SmoothEmbedding I J n M N} (hfg : f.SmoothAmbientIsotopic g) : f.ContinuousAmbientIsotopic g

Smooth ambient isotopy implies continuous ambient isotopy after forgetting the smoothness of the witnessing diffeotopy.

def TauCeti.SmoothEmbedding.SmoothAmbientIsotopic.setoid {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') (n : WithTop ℕ∞) (M : Type u_7) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_8) [TopologicalSpace N] [ChartedSpace H' N] : Setoid (SmoothEmbedding I J n M N)

Smooth ambient isotopy of bundled smooth embeddings, packaged as a setoid.

Equations

• TauCeti.SmoothEmbedding.SmoothAmbientIsotopic.setoid I J n M N = { r := TauCeti.SmoothEmbedding.SmoothAmbientIsotopic, iseqv := ⋯ }

@[simp]

theorem TauCeti.SmoothEmbedding.SmoothAmbientIsotopic.setoid_r_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 g : SmoothEmbedding I J n M N} : (setoid I J n M N) f g ↔ f.SmoothAmbientIsotopic g

The relation of the smooth-ambient-isotopy setoid is smooth ambient isotopy.