Isotopy and ambient isotopy

An isotopy between two continuous maps is a homotopy whose every time slice is a topological embedding, and an ambient isotopy of a space Y is a homotopy from the identity of Y whose level-preserving total map I × Y → I × Y is a homeomorphism. These are the point-set foundations that the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology) asks for once, in full generality, before specialising. Isotopy deliberately uses the slice-wise, homotopy-through-embeddings convention. Burde--Zieschang, Knots, Chapter 1, Definition 1.1 instead requires the associated level-preserving map I × X → I × Y to be an embedding. The two conditions agree when X is compact and Y is Hausdorff, but the slice-wise condition is weaker for the arbitrary spaces allowed here. AmbientIsotopy follows their Definition 1.2, generalized to this continuous topological setting. The non-ambient relation is a general point-set notion of isotopy; later knot-equivalence foundations should use ambient isotopy, specialized as needed to smooth embeddings S¹ ↪ M. Later geometric-topology foundations specialize these notions as appropriate for locally flat isotopy, diffeotopies, and concordance.

A warning: non-ambient isotopy is degenerate for knots

The non-ambient relation Isotopy/Isotopic is not the right equivalence for classical knot theory. It records a moving embedded image, but it need not extend to a motion of the ambient space and therefore need not preserve knot complements. Ambient isotopy is the relation with knot-theoretic content: an ambient isotopy induces a homeomorphism of complements, so knot invariants must be built on AmbientIsotopy and the AmbientIsotopic equivalence from TauCeti.Topology.Homotopy.AmbientIsotopic.Basic, not on Isotopy/Isotopic. See Burde--Zieschang, Knots, Chapter 1 §A, where ambient isotopy (Definition 1.2) is introduced after their stronger level-preserving notion of non-ambient isotopy (Definition 1.1).

Main definitions

• TauCeti.Isotopy f₀ f₁: a homotopy from f₀ to f₁ through topological embeddings.
• TauCeti.Isotopic f₀ f₁: the proposition that such an isotopy exists. This is the reusable general non-ambient relation; knot-equivalence layers should instead use AmbientIsotopic from TauCeti.Topology.Homotopy.AmbientIsotopic.Basic.
• TauCeti.AmbientIsotopy Y: a homotopy of Y from the identity whose total level-preserving map is a homeomorphism.
• TauCeti.AmbientIsotopy.reparamHomeomorph: the level-preserving self-homeomorphism (y, s) ↦ (Φ (ρ s, y), s) of Y × T obtained by reparametrising an ambient isotopy along a continuous map ρ : T → I.
• TauCeti.AmbientIsotopy.trans / TauCeti.AmbientIsotopy.symm: the composition and inverse of ambient isotopies, the closure operations that make ambient isotopy an equivalence relation.

Main results

• TauCeti.Isotopy.isEmbedding_left / isEmbedding_right: the endpoints of an isotopy are embeddings.
• TauCeti.Isotopic.refl / TauCeti.Isotopic.symm / TauCeti.Isotopic.trans: isotopy is reflexive on embeddings, symmetric, and transitive.
• TauCeti.Isotopic.homotopic: isotopic maps are homotopic.
• TauCeti.AmbientIsotopy.isotopy / TauCeti.AmbientIsotopy.isotopic: an ambient isotopy carries any embedding f to the isotopic embedding Φ.final ∘ f. This is the "ambient isotopy implies isotopy" direction.
• TauCeti.AmbientIsotopy.final_trans / TauCeti.AmbientIsotopy.symm_final_final / TauCeti.AmbientIsotopy.final_symm_final: the final maps of the composite and inverse ambient isotopies, and that the inverse final map undoes the original on both sides.

@[reducible, inline]

abbrev TauCeti.Isotopy {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f₀ f₁ : C(X, Y)) : Type (max u_2 u_1)

An isotopy between f₀ f₁ : C(X, Y) is a homotopy for which every time slice x ↦ F(t, x) is a topological embedding.

As an equivalence this non-ambient relation is too coarse for classical knot theory: it need not extend to a motion of the ambient space and therefore need not preserve knot complements. Use AmbientIsotopy/AmbientIsotopic for knot equivalence; see the module docstring and the comparison with the Burde--Zieschang definition there.

Equations

• TauCeti.Isotopy f₀ f₁ = f₀.HomotopyWith f₁ fun (g : C(X, Y)) => Topology.IsEmbedding ⇑g

theorem TauCeti.Isotopy.isEmbedding_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (F : Isotopy f₀ f₁) (t : ↑unitInterval) : Topology.IsEmbedding fun (x : X) => F (t, x)

Every time-slice of an isotopy is a topological embedding.

theorem TauCeti.Isotopy.isEmbedding_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (F : Isotopy f₀ f₁) : Topology.IsEmbedding ⇑f₀

The map an isotopy starts at is a topological embedding.

theorem TauCeti.Isotopy.isEmbedding_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (F : Isotopy f₀ f₁) : Topology.IsEmbedding ⇑f₁

The map an isotopy ends at is a topological embedding.

def TauCeti.Isotopic {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f₀ f₁ : C(X, Y)) : Prop

Two maps f₀ f₁ : C(X, Y) are isotopic if there is an isotopy between them.

Warning: for classical knot theory this non-ambient relation is too coarse: it need not preserve knot complements, so knot invariants must be built on AmbientIsotopic, not on Isotopic.

Equations

• TauCeti.Isotopic f₀ f₁ = Nonempty (TauCeti.Isotopy f₀ f₁)

theorem TauCeti.isotopic_def {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} : Isotopic f₀ f₁ ↔ Nonempty (Isotopy f₀ f₁)

Two maps are isotopic exactly when there is an isotopy between them.

theorem TauCeti.Isotopic.of_isotopy {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (F : Isotopy f₀ f₁) : Isotopic f₀ f₁

An isotopy witnesses that its endpoints are isotopic.

theorem TauCeti.Isotopic.refl {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (hf : Topology.IsEmbedding ⇑f) : Isotopic f f

Isotopy is reflexive on embeddings.

theorem TauCeti.Isotopic.symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (h : Isotopic f₀ f₁) : Isotopic f₁ f₀

Isotopy is symmetric.

theorem TauCeti.Isotopic.trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ f₂ : C(X, Y)} (h₀₁ : Isotopic f₀ f₁) (h₁₂ : Isotopic f₁ f₂) : Isotopic f₀ f₂

Isotopy is transitive.

theorem TauCeti.Isotopic.isEmbedding_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (h : Isotopic f₀ f₁) : Topology.IsEmbedding ⇑f₀

The left endpoint of an isotopy relation is an embedding.

theorem TauCeti.Isotopic.isEmbedding_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (h : Isotopic f₀ f₁) : Topology.IsEmbedding ⇑f₁

The right endpoint of an isotopy relation is an embedding.

theorem TauCeti.Isotopic.homotopic {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (h : Isotopic f₀ f₁) : f₀.Homotopic f₁

Isotopic maps are homotopic.

theorem TauCeti.Isotopic.homotopicWith {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (h : Isotopic f₀ f₁) : f₀.HomotopicWith f₁ fun (g : C(X, Y)) => Topology.IsEmbedding ⇑g

Isotopic maps are homotopic through embeddings in Mathlib's generic API.

structure TauCeti.AmbientIsotopy (Y : Type u_3) [TopologicalSpace Y] extends C(↑unitInterval × Y, Y) : Type u_3

An ambient isotopy of Y is a homotopy from the identity map of Y whose level-preserving total map is a homeomorphism. The time-1 map Φ.final is the resulting homeomorphism.

• toFun : ↑unitInterval × Y → Y
• continuous_toFun : Continuous self.toFun
• isHomeomorph_total' : IsHomeomorph fun (p : ↑unitInterval × Y) => (p.1, self.toFun p)

  the level-preserving total map of the ambient isotopy is a homeomorphism

• map_zero_left' (y : Y) : self.toFun (0, y) = y

  the ambient isotopy starts at the identity of Y

theorem TauCeti.AmbientIsotopy.ext {Y : Type u_2} [TopologicalSpace Y] {Φ Ψ : AmbientIsotopy Y} (h : ∀ (p : ↑unitInterval × Y), Φ.toContinuousMap p = Ψ.toContinuousMap p) : Φ = Ψ

Two ambient isotopies are equal when their underlying continuous maps agree pointwise.

theorem TauCeti.AmbientIsotopy.ext_iff {Y : Type u_2} [TopologicalSpace Y] {Φ Ψ : AmbientIsotopy Y} : Φ = Ψ ↔ ∀ (p : ↑unitInterval × Y), Φ.toContinuousMap p = Ψ.toContinuousMap p

def TauCeti.AmbientIsotopy.totalMap {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) : C(↑unitInterval × Y, ↑unitInterval × Y)

The level-preserving total map of an ambient isotopy.

Equations

• Φ.totalMap = { toFun := fun (p : ↑unitInterval × Y) => (p.1, Φ.toContinuousMap p), continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.AmbientIsotopy.totalMap_apply {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (p : ↑unitInterval × Y) : Φ.totalMap p = (p.1, Φ.toContinuousMap p)

theorem TauCeti.AmbientIsotopy.isHomeomorph_total {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) : IsHomeomorph ⇑Φ.totalMap

The level-preserving total map of an ambient isotopy is a homeomorphism.

theorem TauCeti.AmbientIsotopy.isHomeomorph_apply {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (t : ↑unitInterval) : IsHomeomorph fun (y : Y) => Φ.toContinuousMap (t, y)

Every time-slice of an ambient isotopy is a self-homeomorphism of Y.

@[simp]

theorem TauCeti.AmbientIsotopy.map_zero_left {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (y : Y) : Φ.toContinuousMap (0, y) = y

The ambient isotopy starts at the identity of Y.

def TauCeti.AmbientIsotopy.final {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) : C(Y, Y)

The time-1 homeomorphism produced by an ambient isotopy, as a continuous map.

Equations

• Φ.final = { toFun := fun (y : Y) => Φ.toContinuousMap (1, y), continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.AmbientIsotopy.final_apply {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (y : Y) : Φ.final y = Φ.toContinuousMap (1, y)

theorem TauCeti.AmbientIsotopy.isHomeomorph_final {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) : IsHomeomorph ⇑Φ.final

The final map produced by an ambient isotopy is a homeomorphism.

noncomputable def TauCeti.AmbientIsotopy.homeomorph {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (t : ↑unitInterval) : Y ≃ₜ Y

The time-t self-homeomorphism bundled as a Homeomorph.

Equations

• Φ.homeomorph t = IsHomeomorph.homeomorph (fun (y : Y) => Φ.toContinuousMap (t, y)) ⋯

@[simp]

theorem TauCeti.AmbientIsotopy.homeomorph_apply {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (t : ↑unitInterval) (y : Y) : (Φ.homeomorph t) y = Φ.toContinuousMap (t, y)

noncomputable def TauCeti.AmbientIsotopy.finalHomeomorph {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) : Y ≃ₜ Y

The time-1 homeomorphism produced by an ambient isotopy.

Equations

• Φ.finalHomeomorph = Φ.homeomorph 1

@[simp]

theorem TauCeti.AmbientIsotopy.finalHomeomorph_apply {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (y : Y) : Φ.finalHomeomorph y = Φ.final y

def TauCeti.AmbientIsotopy.refl (Y : Type u_3) [TopologicalSpace Y] : AmbientIsotopy Y

The constant ambient isotopy at the identity.

Equations

• TauCeti.AmbientIsotopy.refl Y = { toFun := fun (p : ↑unitInterval × Y) => p.2, continuous_toFun := ⋯, isHomeomorph_total' := ⋯, map_zero_left' := ⋯ }

@[simp]

theorem TauCeti.AmbientIsotopy.final_refl {Y : Type u_2} [TopologicalSpace Y] (y : Y) : (refl Y).final y = y

The final map of the constant ambient isotopy is the identity.

@[simp]

theorem TauCeti.AmbientIsotopy.homeomorph_refl {Y : Type u_2} [TopologicalSpace Y] (t : ↑unitInterval) : (refl Y).homeomorph t = Homeomorph.refl Y

Every time slice of the constant ambient isotopy is the identity homeomorphism.

@[simp]

theorem TauCeti.AmbientIsotopy.finalHomeomorph_refl {Y : Type u_2} [TopologicalSpace Y] : (refl Y).finalHomeomorph = Homeomorph.refl Y

The final homeomorphism of the constant ambient isotopy is the identity.

@[instance_reducible]

instance TauCeti.AmbientIsotopy.instInhabited {Y : Type u_2} [TopologicalSpace Y] : Inhabited (AmbientIsotopy Y)

Equations

• TauCeti.AmbientIsotopy.instInhabited = { default := TauCeti.AmbientIsotopy.refl Y }

def TauCeti.AmbientIsotopy.isotopy {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (Φ : AmbientIsotopy Y) {f : C(X, Y)} (hf : Topology.IsEmbedding ⇑f) : Isotopy f (Φ.final.comp f)

An ambient isotopy carries any embedding f to the embedding Φ.final ∘ f through an explicit isotopy: at time t the embedding is the homeomorphism Φ t postcomposed with f.

Equations

• Φ.isotopy hf = { toFun := fun (p : ↑unitInterval × X) => Φ.toContinuousMap (p.1, f p.2), continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯, prop' := ⋯ }

@[simp]

theorem TauCeti.AmbientIsotopy.isotopy_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (Φ : AmbientIsotopy Y) {f : C(X, Y)} (hf : Topology.IsEmbedding ⇑f) (t : ↑unitInterval) (x : X) : (Φ.isotopy hf) (t, x) = Φ.toContinuousMap (t, f x)

theorem TauCeti.AmbientIsotopy.isotopic {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (Φ : AmbientIsotopy Y) {f : C(X, Y)} (hf : Topology.IsEmbedding ⇑f) : Isotopic f (Φ.final.comp f)

Ambient isotopy implies isotopy: an ambient isotopy of Y carries any embedding f into Y to the isotopic embedding Φ.final ∘ f.

noncomputable def TauCeti.AmbientIsotopy.totalHomeomorph {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) : ↑unitInterval × Y ≃ₜ ↑unitInterval × Y

The level-preserving total map of an ambient isotopy, bundled as a self-homeomorphism of I × Y.

Equations

• Φ.totalHomeomorph = IsHomeomorph.homeomorph ⇑Φ.totalMap ⋯

@[simp]

theorem TauCeti.AmbientIsotopy.totalHomeomorph_apply {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (p : ↑unitInterval × Y) : Φ.totalHomeomorph p = (p.1, Φ.toContinuousMap p)

@[simp]

theorem TauCeti.AmbientIsotopy.totalHomeomorph_symm_fst {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (p : ↑unitInterval × Y) : (Φ.totalHomeomorph.symm p).1 = p.1

The inverse total homeomorphism preserves the time coordinate.

noncomputable def TauCeti.AmbientIsotopy.reparamHomeomorph {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) {T : Type u_3} [TopologicalSpace T] (ρ : C(T, ↑unitInterval)) : Y × T ≃ₜ Y × T

Reparametrising the ambient isotopy Φ by a continuous map ρ : T → I gives the level-preserving self-homeomorphism (y, s) ↦ (Φ (ρ s, y), s) of Y × T. With T = ℝ and ρ a clamp which is 0 near -∞ and 1 near +∞, composing it with f × id for an embedding f gives the trace of Φ along f, a concordance from f to Φ.final ∘ f.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AmbientIsotopy.reparamHomeomorph_apply {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) {T : Type u_3} [TopologicalSpace T] (ρ : C(T, ↑unitInterval)) (p : Y × T) : (Φ.reparamHomeomorph ρ) p = (Φ.toContinuousMap (ρ p.2, p.1), p.2)

def TauCeti.AmbientIsotopy.trans {Y : Type u_2} [TopologicalSpace Y] (Φ Ψ : AmbientIsotopy Y) : AmbientIsotopy Y

Composition of ambient isotopies: follow Φ_t then Ψ_t at each time t.

Equations

• Φ.trans Ψ = { toFun := fun (p : ↑unitInterval × Y) => Ψ.toContinuousMap (p.1, Φ.toContinuousMap p), continuous_toFun := ⋯, isHomeomorph_total' := ⋯, map_zero_left' := ⋯ }

@[simp]

theorem TauCeti.AmbientIsotopy.trans_apply {Y : Type u_2} [TopologicalSpace Y] (Φ Ψ : AmbientIsotopy Y) (p : ↑unitInterval × Y) : (Φ.trans Ψ).toContinuousMap p = Ψ.toContinuousMap (p.1, Φ.toContinuousMap p)

@[simp]

theorem TauCeti.AmbientIsotopy.final_trans {Y : Type u_2} [TopologicalSpace Y] (Φ Ψ : AmbientIsotopy Y) (y : Y) : (Φ.trans Ψ).final y = Ψ.final (Φ.final y)

The final map of the composite ambient isotopy Φ.trans Ψ is the composition of the final maps of Φ and Ψ: at the endpoint it is Ψ.final ∘ Φ.final.

@[simp]

theorem TauCeti.AmbientIsotopy.homeomorph_trans {Y : Type u_2} [TopologicalSpace Y] (Φ Ψ : AmbientIsotopy Y) (t : ↑unitInterval) : (Φ.trans Ψ).homeomorph t = (Φ.homeomorph t).trans (Ψ.homeomorph t)

Every time slice of a composite ambient isotopy is the composite of the corresponding time slices.

@[simp]

theorem TauCeti.AmbientIsotopy.finalHomeomorph_trans {Y : Type u_2} [TopologicalSpace Y] (Φ Ψ : AmbientIsotopy Y) : (Φ.trans Ψ).finalHomeomorph = Φ.finalHomeomorph.trans Ψ.finalHomeomorph

The final homeomorphism of a composite ambient isotopy is the composite of the final homeomorphisms.

noncomputable def TauCeti.AmbientIsotopy.symm {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) : AmbientIsotopy Y

Inverse of an ambient isotopy: undo Φ_t at each time t.

Equations

• Φ.symm = { toFun := fun (p : ↑unitInterval × Y) => (Φ.totalHomeomorph.symm p).2, continuous_toFun := ⋯, isHomeomorph_total' := ⋯, map_zero_left' := ⋯ }

@[simp]

theorem TauCeti.AmbientIsotopy.symm_apply {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (p : ↑unitInterval × Y) : Φ.symm.toContinuousMap p = (Φ.totalHomeomorph.symm p).2

@[simp]

theorem TauCeti.AmbientIsotopy.symm_final_final {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (y : Y) : Φ.symm.final (Φ.final y) = y

The inverse ambient isotopy undoes the original: its final map is a left inverse of the original final map.

@[simp]

theorem TauCeti.AmbientIsotopy.final_symm_final {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (y : Y) : Φ.final (Φ.symm.final y) = y

The original ambient isotopy undoes its inverse: the original final map is a left inverse of the inverse final map.

@[simp]

theorem TauCeti.AmbientIsotopy.homeomorph_symm {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (t : ↑unitInterval) : Φ.symm.homeomorph t = (Φ.homeomorph t).symm

Every time slice of the inverse ambient isotopy is the inverse of the corresponding time slice.

@[simp]

theorem TauCeti.AmbientIsotopy.finalHomeomorph_symm {Y : Type u_2} [TopologicalSpace Y] (Φ : AmbientIsotopy Y) : Φ.symm.finalHomeomorph = Φ.finalHomeomorph.symm

The final homeomorphism of the inverse ambient isotopy is the inverse final homeomorphism.