Ambient isotopy preserves the complement of the range

The point of ambient isotopy, as opposed to the naive isotopy of TauCeti.Topology.Homotopy.Isotopy.Basic, is that it moves the whole ambient space, not just an embedded image. Consequently an ambient isotopy carrying a map f to a map g induces a homeomorphism of their complements (range f)ᶜ ≃ₜ (range g)ᶜ. This is exactly why the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md, layer 4, "knot theory") insists that knot invariants be built on ambient isotopy: the complement of a knot is the basic invariant, and it is a homeomorphism invariant of the ambient-isotopy class precisely because of the theorem in this file. The module docstring of TauCeti.Topology.Homotopy.Isotopy.Basic states this fact in prose ("an ambient isotopy induces a homeomorphism of complements"); here it is proved.

Everything is stated for arbitrary continuous maps f : C(X, Y), since the range and its complement make sense without an embedding hypothesis; the embedded case (knots) is the intended specialisation. Both witnessing homeomorphisms are restrictions of the ambient isotopy's final homeomorphism Φ.finalHomeomorph: their underlying-value maps are Φ.finalHomeomorph itself and their inverses are Φ.finalHomeomorph.symm, as recorded by the coe_…_apply lemmas below.

Main definitions

• TauCeti.AmbientIsotopy.rangeHomeomorph: the homeomorphism range f ≃ₜ range (Φ.final.comp f) induced on ranges by an ambient isotopy Φ.
• TauCeti.AmbientIsotopy.complementHomeomorph: the homeomorphism (range f)ᶜ ≃ₜ (range (Φ.final.comp f))ᶜ induced on complements.

Main results

• TauCeti.AmbientIsotopy.range_final_comp: the final homeomorphism carries range f onto the range of the moved map Φ.final.comp f.
• TauCeti.AmbientIsotopic.nonempty_rangeHomeomorph / TauCeti.AmbientIsotopic.nonempty_complementHomeomorph: ambient isotopic maps have homeomorphic ranges and homeomorphic complements. The complement statement is the knot-invariance fact.

theorem TauCeti.AmbientIsotopy.range_final_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (f : C(X, Y)) : Set.range ⇑(Φ.final.comp f) = ⇑Φ.finalHomeomorph '' Set.range ⇑f

The final homeomorphism of an ambient isotopy carries range f onto the range of the moved map Φ.final.comp f: the image Φ.finalHomeomorph '' range f is range (Φ.final.comp f).

theorem TauCeti.AmbientIsotopy.mem_range_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (f : C(X, Y)) (y : Y) : y ∈ Set.range ⇑f ↔ Φ.finalHomeomorph y ∈ Set.range ⇑(Φ.final.comp f)

A point lies in range f exactly when its image under the final homeomorphism lies in the range of the moved map. This is the compatibility that lets the final homeomorphism restrict to the ranges (and, negated, to the complements).

theorem TauCeti.AmbientIsotopy.notMem_range_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (f : C(X, Y)) (y : Y) : y ∉ Set.range ⇑f ↔ Φ.finalHomeomorph y ∉ Set.range ⇑(Φ.final.comp f)

A point misses range f exactly when its image under the final homeomorphism misses the range of the moved map. This is the compatibility that lets the final homeomorphism restrict to the complements.

noncomputable def TauCeti.AmbientIsotopy.rangeHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (f : C(X, Y)) : ↑(Set.range ⇑f) ≃ₜ ↑(Set.range ⇑(Φ.final.comp f))

The homeomorphism of ranges induced by an ambient isotopy: Φ.finalHomeomorph restricts to a homeomorphism from range f onto the range of the moved map Φ.final.comp f.

Equations

• Φ.rangeHomeomorph f = Φ.finalHomeomorph.subtype ⋯

theorem TauCeti.AmbientIsotopy.coe_rangeHomeomorph_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (f : C(X, Y)) (y : ↑(Set.range ⇑f)) : ↑((Φ.rangeHomeomorph f) y) = Φ.finalHomeomorph ↑y

theorem TauCeti.AmbientIsotopy.coe_rangeHomeomorph_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (f : C(X, Y)) (y : ↑(Set.range ⇑(Φ.final.comp f))) : ↑((Φ.rangeHomeomorph f).symm y) = Φ.finalHomeomorph.symm ↑y

noncomputable def TauCeti.AmbientIsotopy.complementHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (f : C(X, Y)) : ↑(Set.range ⇑f)ᶜ ≃ₜ ↑(Set.range ⇑(Φ.final.comp f))ᶜ

The homeomorphism of complements induced by an ambient isotopy: Φ.finalHomeomorph restricts to a homeomorphism from (range f)ᶜ onto (range (Φ.final.comp f))ᶜ. This is the point-set core of knot-complement invariance under ambient isotopy.

Equations

• Φ.complementHomeomorph f = Φ.finalHomeomorph.subtype ⋯

theorem TauCeti.AmbientIsotopy.coe_complementHomeomorph_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (f : C(X, Y)) (y : ↑(Set.range ⇑f)ᶜ) : ↑((Φ.complementHomeomorph f) y) = Φ.finalHomeomorph ↑y

theorem TauCeti.AmbientIsotopy.coe_complementHomeomorph_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (Φ : AmbientIsotopy Y) (f : C(X, Y)) (y : ↑(Set.range ⇑(Φ.final.comp f))ᶜ) : ↑((Φ.complementHomeomorph f).symm y) = Φ.finalHomeomorph.symm ↑y

theorem TauCeti.AmbientIsotopic.nonempty_rangeHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (hfg : AmbientIsotopic f g) : Nonempty (↑(Set.range ⇑f) ≃ₜ ↑(Set.range ⇑g))

Ambient isotopy preserves ranges up to homeomorphism. If f and g are ambient isotopic, their ranges (the embedded images, for embeddings) are homeomorphic.

theorem TauCeti.AmbientIsotopic.nonempty_complementHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (hfg : AmbientIsotopic f g) : Nonempty (↑(Set.range ⇑f)ᶜ ≃ₜ ↑(Set.range ⇑g)ᶜ)

Ambient isotopy preserves complements up to homeomorphism. If f and g are ambient isotopic, the complements (range f)ᶜ and (range g)ᶜ are homeomorphic. For knots (embeddings S¹ ↪ M) this is the invariance of the knot complement, the reason knot invariants are built on ambient isotopy rather than on the naive isotopy relation.