Documentation

TauCeti.Topology.Homotopy.Isotopy.Comp

Naturality of isotopy under composition with embeddings #

An isotopy is a homotopy through topological embeddings. This file records that the isotopy relation is natural: composing on either side with a topological embedding carries an isotopy to an isotopy, and so an isotopy relation to an isotopy relation. These are the closure properties the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md) asks the general isotopy notion to carry before specialising to smooth embeddings S¹ ↪ M: they mirror, for TauCeti.Isotopy, the composition lemmas Mathlib provides for IsEmbedding (Topology.IsEmbedding.comp) and for homotopy (ContinuousMap.Homotopy.comp, ContinuousMap.Homotopy.compContinuousMap), which this file reuses for the underlying homotopies.

The two-sided generality (an embedding on either side, not merely a homeomorphism) is what the roadmap's layer-2 closure properties for locally flat embeddings will consume: a submanifold inclusion postcomposes, a chart or open embedding precomposes, and the isotopy survives both.

Main definitions #

Main results #

source
def TauCeti.Isotopy.postcomp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ f₁ : C(X, Y)} (F : Isotopy f₀ f₁) (g : C(Y, Z)) (hg : Topology.IsEmbedding ⇑g) :
Isotopy (g.comp f₀) (g.comp f₁)

Postcompose an isotopy f₀ ≈ f₁ with a topological embedding g : Y ↪ Z to get an isotopy g ∘ f₀ ≈ g ∘ f₁.

Instances For
    source
    @[simp]
    theorem TauCeti.Isotopy.postcomp_apply {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ f₁ : C(X, Y)} (F : Isotopy f₀ f₁) (g : C(Y, Z)) (hg : Topology.IsEmbedding ⇑g) (p : ↑unitInterval × X) :
    (F.postcomp g hg) p = g (F p)
    source
    def TauCeti.Isotopy.precomp {W : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace W] [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (F : Isotopy f₀ f₁) (e : C(W, X)) (he : Topology.IsEmbedding ⇑e) :
    Isotopy (f₀.comp e) (f₁.comp e)

    Precompose an isotopy f₀ ≈ f₁ with a topological embedding e : W ↪ X to get an isotopy f₀ ∘ e ≈ f₁ ∘ e.

    Instances For
      source
      @[simp]
      theorem TauCeti.Isotopy.precomp_apply {W : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace W] [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (F : Isotopy f₀ f₁) (e : C(W, X)) (he : Topology.IsEmbedding ⇑e) (p : ↑unitInterval × W) :
      (F.precomp e he) p = F (p.1, e p.2)
      source
      theorem TauCeti.Isotopic.postcomp {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ f₁ : C(X, Y)} (h : Isotopic f₀ f₁) (g : C(Y, Z)) (hg : Topology.IsEmbedding ⇑g) :
      Isotopic (g.comp f₀) (g.comp f₁)

      Postcompose an isotopy relation with a topological embedding: if f₀ ≈ f₁ and g is an embedding, then g ∘ f₀ ≈ g ∘ f₁.

      source
      theorem TauCeti.Isotopic.precomp {W : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace W] [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (h : Isotopic f₀ f₁) (e : C(W, X)) (he : Topology.IsEmbedding ⇑e) :
      Isotopic (f₀.comp e) (f₁.comp e)

      Precompose an isotopy relation with a topological embedding: if f₀ ≈ f₁ and e is an embedding, then f₀ ∘ e ≈ f₁ ∘ e.

      source
      theorem TauCeti.Isotopic.postcomp_precomp {W : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace W] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ f₁ : C(X, Y)} (h : Isotopic f₀ f₁) (g : C(Y, Z)) (hg : Topology.IsEmbedding ⇑g) (e : C(W, X)) (he : Topology.IsEmbedding ⇑e) :
      Isotopic (g.comp (f₀.comp e)) (g.comp (f₁.comp e))

      The two-sided form: an isotopy relation survives composing with an embedding on each side.

      source
      theorem TauCeti.Isotopic.postcomp_homeomorph {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ f₁ : C(X, Y)} (h : Isotopic f₀ f₁) (e : Y ≃ₜ Z) :
      Isotopic ((↑e).comp f₀) ((↑e).comp f₁)

      Postcomposing an isotopy relation with a homeomorphism of the codomain.

      source
      theorem TauCeti.Isotopic.precomp_homeomorph {W : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace W] [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (h : Isotopic f₀ f₁) (e : W ≃ₜ X) :
      Isotopic (f₀.comp ↑e) (f₁.comp ↑e)

      Precomposing an isotopy relation with a homeomorphism of the source.