The ambient-isotopy equivalence relation

Building on TauCeti.AmbientIsotopy (an ambient isotopy of a space Y: a homotopy from the identity whose level-preserving total map I × Y → I × Y is a homeomorphism), this file makes ambient isotopy a relation between maps and shows it is an equivalence relation. Two maps f g : C(X, Y) are ambient isotopic when some ambient isotopy Φ of Y carries f to g, meaning its final homeomorphism postcomposes f to g. This is the continuous topological relation the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology, encoding conventions) intends to specialise to smooth embeddings S¹ ↪ M to underlie knot equivalence: "isotopy is defined generally, then specialised".

The reflexivity, symmetry, and transitivity of the relation are powered by three closure operations on ambient isotopies themselves, which live beside the AmbientIsotopy structure in TauCeti.Topology.Homotopy.Isotopy.Basic: the constant ambient isotopy AmbientIsotopy.refl, the pointwise composition AmbientIsotopy.trans, and the pointwise inverse AmbientIsotopy.symm. Because each of their total maps is a composition or inverse of homeomorphisms, none of the closure operations needs a separate gluing argument. This is a continuous topological generalization of the point-set ambient-isotopy condition in Burde--Zieschang, Knots, Chapter 1, Definition 1.2, intended for later specialization to embeddings such as knots.

Main definitions

• TauCeti.AmbientIsotopic f g: the proposition that some ambient isotopy of Y carries f to g.
• TauCeti.AmbientIsotopic.setoid: the equivalence relation packaged as a Setoid.

Main results

• TauCeti.AmbientIsotopic.refl / symm / trans and TauCeti.AmbientIsotopic.equivalence: ambient isotopy is an equivalence relation on C(X, Y).
• TauCeti.AmbientIsotopic.isotopic: ambient isotopic embeddings are isotopic, specialising the ambient relation to the general isotopy relation of Isotopy.lean.

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

Two maps f g : C(X, Y) are ambient isotopic if some ambient isotopy of the codomain Y carries f to g, that is, its final homeomorphism postcomposes f to g. This is the continuous topological ambient-isotopy relation intended to underlie later knot-equivalence specialisations (ambient isotopy of smooth embeddings S¹ ↪ M); it does not itself encode the smooth or PL structure those specialisations add.

Equations

• TauCeti.AmbientIsotopic f g = ∃ (Φ : TauCeti.AmbientIsotopy Y), Φ.final.comp f = g

theorem TauCeti.ambientIsotopic_def {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} : AmbientIsotopic f g ↔ ∃ (Φ : AmbientIsotopy Y), Φ.final.comp f = g

f and g are ambient isotopic exactly when some ambient isotopy's final homeomorphism postcomposes f to g; this restates the definition without unfolding it.

theorem TauCeti.AmbientIsotopic.of_ambientIsotopy {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (Φ : AmbientIsotopy Y) {f : C(X, Y)} : AmbientIsotopic f (Φ.final.comp f)

An ambient isotopy carrying f to g witnesses that f and g are ambient isotopic.

theorem TauCeti.AmbientIsotopic.refl {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : AmbientIsotopic f f

Ambient isotopy is reflexive: the constant ambient isotopy fixes every map.

theorem TauCeti.AmbientIsotopic.symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (hfg : AmbientIsotopic f g) : AmbientIsotopic g f

Ambient isotopy is symmetric, via the inverse ambient isotopy.

theorem TauCeti.AmbientIsotopic.trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g h : C(X, Y)} (hfg : AmbientIsotopic f g) (hgh : AmbientIsotopic g h) : AmbientIsotopic f h

Ambient isotopy is transitive, via the composite ambient isotopy.

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

Ambient isotopic embeddings are isotopic: this specialises the ambient relation to the general isotopy relation, the "ambient isotopy implies isotopy" direction at the level of maps.

theorem TauCeti.AmbientIsotopic.equivalence {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : Equivalence AmbientIsotopic

Ambient isotopy is an equivalence relation on C(X, Y).

def TauCeti.AmbientIsotopic.setoid (X : Type u_3) (Y : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] : Setoid C(X, Y)

The ambient-isotopy equivalence relation on C(X, Y), packaged as a Setoid.

Equations

• TauCeti.AmbientIsotopic.setoid X Y = { r := TauCeti.AmbientIsotopic, iseqv := ⋯ }

@[simp]

theorem TauCeti.AmbientIsotopic.setoid_r_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} : (setoid X Y) f g ↔ AmbientIsotopic f g