Continuous ambient isotopy of bundled smooth embeddings

The geometric-topology roadmap treats geometric knot presentations as smooth embeddings, and asks that isotopy and ambient isotopy be defined generally before being specialised. TauCeti.AmbientIsotopic already gives the point-set ambient-isotopy relation for continuous maps. This file connects that relation to the bundled smooth embeddings of TauCeti.Geometry.Manifold.SmoothEmbedding.Basic.

The relation here does not assert that the ambient isotopy is smooth in time or in the ambient variable. It is the continuous ambient-isotopy relation on the underlying maps of two bundled smooth embeddings, which is the topological relation later smooth-knot and concordance files can specialise further when they need differentiable isotopies. Because the smooth and topological ambient-isotopy relations genuinely differ in high dimensions, the name says Continuous: this is not a smooth ambient isotopy of the embeddings, only continuous ambient isotopy of their underlying maps.

Main definitions

• TauCeti.SmoothEmbedding.ContinuousAmbientIsotopic: two bundled smooth embeddings are continuously ambient isotopic when their underlying continuous maps are ambient isotopic.
• TauCeti.SmoothEmbedding.ContinuousAmbientIsotopic.setoid: continuous ambient isotopy as a setoid on bundled smooth embeddings.

The source for the topological ambient-isotopy notion is Burde--Zieschang, Knots, Chapter 1, Definition 1.2, via the existing TauCeti.Topology.Homotopy.Isotopy.Basic and TauCeti.Topology.Homotopy.AmbientIsotopic.Basic files.

def TauCeti.SmoothEmbedding.ContinuousAmbientIsotopic {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (f g : SmoothEmbedding I J n M N) : Prop

Two bundled smooth embeddings are continuously ambient isotopic when their underlying continuous maps are ambient isotopic. This is the continuous topological relation, not a smooth ambient isotopy.

Equations

• f.ContinuousAmbientIsotopic g = TauCeti.AmbientIsotopic f.toContinuousMap g.toContinuousMap

theorem TauCeti.SmoothEmbedding.continuousAmbientIsotopic_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f g : SmoothEmbedding I J n M N} : f.ContinuousAmbientIsotopic g ↔ ∃ (Φ : AmbientIsotopy N), Φ.final.comp f.toContinuousMap = g.toContinuousMap

Continuous ambient isotopy of bundled smooth embeddings is witnessed by an ambient isotopy whose final homeomorphism postcomposes the first underlying continuous map to the second.

theorem TauCeti.SmoothEmbedding.ContinuousAmbientIsotopic.of_ambientIsotopy {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f g : SmoothEmbedding I J n M N} (Φ : AmbientIsotopy N) (hΦ : Φ.final.comp f.toContinuousMap = g.toContinuousMap) : f.ContinuousAmbientIsotopic g

An ambient isotopy whose final map carries f to g witnesses continuous ambient isotopy of the two bundled smooth embeddings.

theorem TauCeti.SmoothEmbedding.ContinuousAmbientIsotopic.of_eq_final_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f g : SmoothEmbedding I J n M N} (Φ : AmbientIsotopy N) (hΦ : g.toContinuousMap = Φ.final.comp f.toContinuousMap) : f.ContinuousAmbientIsotopic g

A symmetric form of SmoothEmbedding.ContinuousAmbientIsotopic.of_ambientIsotopy, useful when the endpoint equation is oriented as g = Φ.final ∘ f.

theorem TauCeti.SmoothEmbedding.ContinuousAmbientIsotopic.refl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) : f.ContinuousAmbientIsotopic f

Continuous ambient isotopy of bundled smooth embeddings is reflexive.

theorem TauCeti.SmoothEmbedding.ContinuousAmbientIsotopic.symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f g : SmoothEmbedding I J n M N} (hfg : f.ContinuousAmbientIsotopic g) : g.ContinuousAmbientIsotopic f

Continuous ambient isotopy of bundled smooth embeddings is symmetric.

theorem TauCeti.SmoothEmbedding.ContinuousAmbientIsotopic.trans {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f g h : SmoothEmbedding I J n M N} (hfg : f.ContinuousAmbientIsotopic g) (hgh : g.ContinuousAmbientIsotopic h) : f.ContinuousAmbientIsotopic h

Continuous ambient isotopy of bundled smooth embeddings is transitive.

theorem TauCeti.SmoothEmbedding.ContinuousAmbientIsotopic.isotopic {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f g : SmoothEmbedding I J n M N} (hfg : f.ContinuousAmbientIsotopic g) : Isotopic f.toContinuousMap g.toContinuousMap

Continuously ambient isotopic bundled smooth embeddings have isotopic underlying continuous maps.

theorem TauCeti.SmoothEmbedding.ContinuousAmbientIsotopic.equivalence {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} : Equivalence ContinuousAmbientIsotopic

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

def TauCeti.SmoothEmbedding.ContinuousAmbientIsotopic.setoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 E' H') (n : WithTop ℕ∞) (M : Type u_8) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_9) [TopologicalSpace N] [ChartedSpace H' N] : Setoid (SmoothEmbedding I J n M N)

The continuous-ambient-isotopy equivalence relation on bundled smooth embeddings, packaged as a Setoid.

Equations

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

@[simp]

theorem TauCeti.SmoothEmbedding.ContinuousAmbientIsotopic.setoid_r_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f g : SmoothEmbedding I J n M N} : (setoid I J n M N) f g ↔ f.ContinuousAmbientIsotopic g