Solid torus neighbourhoods of knots

A solid torus neighbourhood of a loop f : S¹ → X is an embedding Φ of the closed solid torus D² × S¹ into X whose core {0} × S¹ traces f and which maps the open solid torus onto an open subset of X. In Rolfsen's terminology Φ is a framing of the solid torus it parametrizes, with meridians w ↦ Φ (w, z) and longitude z ↦ Φ (1, z); it need not be the preferred framing. Removing the image of the open solid torus from X leaves the exterior of the knot, a closed set whose frontier is the torus Φ (S¹ × S¹) when X is Hausdorff. This is the input to Dehn surgery, which glues a solid torus back onto this boundary torus along a homeomorphism specified by a slope on it.

The main theorem is that every C² embedded circle in ℝ³ has solid torus neighbourhoods, inside any prescribed neighbourhood of the circle. By the tubular neighbourhood theorem TauCeti.exists_isOpenEmbedding_normalTube, the normal vectors of length less than some ε embed openly into ℝ³ by (z, v) ↦ f z + v. It remains to trivialize the normal bundle, that is, to choose a continuous orthonormal frame (n₁ z, n₂ z) of the normal plane at every z. The tangent lines of the circle form the image of a C¹ map from a plane, which has dense complement in ℝ³, so some vector a is tangent to the circle nowhere; n₁ z is the normalized projection of a onto the normal plane, and n₂ z is the cross product of the unit tangent with n₁ z. Then Φ (w, z) = f z + r • (re w • n₁ z + im w • n₂ z) for a small r > 0.

This Φ is differentiable at its core point (0, 1) when read as (u, t) ↦ Φ (u, exp (t i)) (TauCeti.SolidTorus.coreReading), with injective derivative (u, t) ↦ t • τ + r • (re u • n₁ 1 + im u • n₂ 1) for the velocity τ of f at 1, although the frame is only continuous: the frame is multiplied by u, which vanishes on the core. This is what lets the orientation of a solid torus neighbourhood be read off its derivative at the core.

Main definitions

• TauCeti.IsSolidTorusNeighborhood f Φ: Φ : D² × S¹ → X is a solid torus neighbourhood of the loop f.
• TauCeti.SolidTorus.boundaryInclusion: the inclusion of the boundary torus S¹ × S¹ into the solid torus.
• TauCeti.SolidTorus.twist: the meridian-disc twist (w, z) ↦ (w zⁿ, z).
• TauCeti.SolidTorus.coreReading Φ: a map Φ from the solid torus read near the core point (0, 1) as (u, t) ↦ Φ (u, exp (t i)) on ℂ × ℝ.
• TauCeti.SolidTorus.conjDisc: the reflection (u, w) ↦ (conj u, w) of the solid torus.

Main results

• TauCeti.SolidTorus.extendsDisjointOpens_boundaryInclusion: the inclusion of the boundary torus into the solid torus extends disjoint open sets, through open collars.
• TauCeti.IsSolidTorusNeighborhood.frontier_image: the frontier of the image of the open solid torus, which is also the frontier of the knot exterior, is the image of the boundary torus when the ambient space is Hausdorff.
• TauCeti.IsSolidTorusNeighborhood.isEmbedding_comp_boundaryInclusion: the boundary torus S¹ × S¹ embeds.
• TauCeti.IsSolidTorusNeighborhood.comp: solid torus neighbourhoods are carried along open embeddings of the ambient space.
• TauCeti.IsSolidTorusNeighborhood.comp_prodMap: and along reparametrizations of the loop by homeomorphisms of the circle.
• TauCeti.IsSolidTorusNeighborhood.apply_mem_range_iff: a point of the solid torus lies on the knot exactly when it lies on the core.
• TauCeti.IsSolidTorusNeighborhood.frontier_subset_compl_range: the boundary torus of the exterior misses the knot.
• TauCeti.IsSolidTorusNeighborhood.exteriorFrontierHomeomorph: the framing identifies the torus with the frontier of the exterior.
• TauCeti.IsSolidTorusNeighborhood.comp_conjDisc: reflecting the disc of a solid torus neighbourhood gives a solid torus neighbourhood of the same loop.
• TauCeti.exists_isSolidTorusNeighborhood: a C² embedded circle in ℝ³ has a solid torus neighbourhood inside any neighbourhood of its image.
• TauCeti.exists_isSolidTorusNeighborhood_hasFDerivAt_coreReading: such a neighbourhood can be chosen with an injective derivative at its core point.

References

• D. Rolfsen, Knots and Links, Publish or Perish (1976), Section 2E (solid tori, framings, meridians and longitudes) and Section 9F (Dehn surgery along tubular neighbourhoods).
• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer (2013), Theorem 6.24 (tubular neighbourhoods).

Solid torus neighbourhoods

def TauCeti.SolidTorus.boundaryInclusion (q : Circle × Circle) : SolidTorus

The inclusion of the boundary torus S¹ × S¹ = ∂D² × S¹ into the solid torus D² × S¹.

@[simp]

theorem TauCeti.SolidTorus.coe_boundaryInclusion_fst (q : Circle × Circle) : ↑(boundaryInclusion q).1 = ↑q.1

@[simp]

theorem TauCeti.SolidTorus.boundaryInclusion_snd (q : Circle × Circle) : (boundaryInclusion q).2 = q.2

theorem TauCeti.SolidTorus.isEmbedding_boundaryInclusion : Topology.IsEmbedding boundaryInclusion

The boundary torus is embedded in the solid torus.

theorem TauCeti.SolidTorus.extendsDisjointOpens_boundaryInclusion : TopCat.extendsDisjointOpens (TopCat.ofHom { toFun := boundaryInclusion, continuous_toFun := ⋯ })

The inclusion of the boundary torus into the solid torus extends disjoint open sets: an open subset U of S¹ × S¹ is the trace of the open collar of points (w, z) with 1 / 2 < ‖w‖ and (w / ‖w‖, z) ∈ U, and the collars over disjoint sets are disjoint (TauCeti.TopCat.extendsDisjointOpens_of_continuousOn with the radial projection).

theorem TauCeti.SolidTorus.range_boundaryInclusion : Set.range boundaryInclusion = {p : SolidTorus | ‖↑p.1‖ = 1}

The boundary torus is the set of points (w, z) of the solid torus with ‖w‖ = 1.

noncomputable def TauCeti.SolidTorus.twist (n : ℤ) : SolidTorus ≃ₜ SolidTorus

The twist (w, z) ↦ (w zⁿ, z) of the solid torus D² × S¹ along its meridian discs.

@[simp]

theorem TauCeti.SolidTorus.coe_twist_apply_fst (n : ℤ) (p : SolidTorus) : ↑((twist n) p).1 = ↑p.1 * ↑(p.2 ^ n)

The meridian-disc twist multiplies the disc coordinate by zⁿ.

@[simp]

theorem TauCeti.SolidTorus.twist_apply_snd (n : ℤ) (p : SolidTorus) : ((twist n) p).2 = p.2

The meridian-disc twist preserves the circle coordinate.

@[simp]

theorem TauCeti.SolidTorus.twist_zero : twist 0 = Homeomorph.refl SolidTorus

The zero twist is the identity homeomorphism.

theorem TauCeti.SolidTorus.twist_add (m n : ℤ) : twist (m + n) = (twist m).trans (twist n)

Successive meridian-disc twists add their twisting numbers.

@[simp]

theorem TauCeti.SolidTorus.twist_symm (n : ℤ) : (twist n).symm = twist (-n)

The inverse meridian-disc twist has the opposite twisting number.

@[simp]

theorem TauCeti.SolidTorus.twist_boundaryInclusion (n : ℤ) (q : Circle × Circle) : (twist n) (boundaryInclusion q) = boundaryInclusion (q.1 * q.2 ^ n, q.2)

The twist restricts on the boundary torus to (a, b) ↦ (a bⁿ, b).

theorem TauCeti.SolidTorus.closure_setOf_norm_lt_one : closure {p : SolidTorus | ‖↑p.1‖ < 1} = Set.univ

The open solid torus is dense in the closed solid torus.

noncomputable def TauCeti.SolidTorus.coreReading {F : Type u_1} [Zero F] (Φ : SolidTorus → F) (v : ℂ × ℝ) : F

A map Φ from the solid torus, read near the point (0, 1) of its core as the map (u, t) ↦ Φ (u, exp (t i)) on ℂ × ℝ. It is extended by 0 off the closed unit disc, which does not affect its germ at the origin; so the derivative of this reading at the origin is the derivative of Φ at the core point (0, 1) in the coordinates (u, t).

theorem TauCeti.SolidTorus.coreReading_of_norm_le {F : Type u_1} [Zero F] (Φ : SolidTorus → F) {v : ℂ × ℝ} (hv : ‖v.1‖ ≤ 1) : coreReading Φ v = Φ (⟨v.1, ⋯⟩, Circle.exp v.2)

On the closed unit disc the reading of Φ is (u, t) ↦ Φ (u, exp (t i)).

theorem TauCeti.SolidTorus.coreReading_of_not_norm_le {F : Type u_1} [Zero F] (Φ : SolidTorus → F) {v : ℂ × ℝ} (hv : ¬‖v.1‖ ≤ 1) : coreReading Φ v = 0

Off the closed unit disc the reading of Φ is 0.

@[simp]

theorem TauCeti.SolidTorus.coreReading_zero {F : Type u_1} [Zero F] (Φ : SolidTorus → F) : coreReading Φ 0 = Φ (0, 1)

At the origin the reading of Φ is the core point Φ (0, 1).

theorem TauCeti.SolidTorus.eventually_coreReading_eq {F : Type u_1} [Zero F] (Φ : SolidTorus → F) : ∀ᶠ (v : ℂ × ℝ) in nhds 0, ∃ (hv : ‖v.1‖ ≤ 1), coreReading Φ v = Φ (⟨v.1, ⋯⟩, Circle.exp v.2)

Near the origin the reading of Φ is (u, t) ↦ Φ (u, exp (t i)).

theorem TauCeti.SolidTorus.coreReading_comp_eventuallyEq {F : Type u_1} [Zero F] {F' : Type u_2} [Zero F'] (g : F → F') (Φ : SolidTorus → F) : coreReading (g ∘ Φ) =ᶠ[nhds 0] g ∘ coreReading Φ

Near the origin the reading of g ∘ Φ is g composed with the reading of Φ.

structure TauCeti.IsSolidTorusNeighborhood {X : Type u_1} [TopologicalSpace X] (f : Circle → X) (Φ : SolidTorus → X) : Prop

Φ : D² × S¹ → X is a solid torus neighbourhood of the loop f : S¹ → X when it is an embedding whose core {0} × S¹ traces f, and which maps the open solid torus {w | ‖w‖ < 1} × S¹ onto an open subset of X. The complement of that open subset is the exterior of the knot f, and when X is Hausdorff its frontier is the boundary torus (TauCeti.IsSolidTorusNeighborhood.frontier_image).

• isEmbedding : Topology.IsEmbedding Φ

  The solid torus is embedded.

• apply_zero (z : Circle) : Φ (0, z) = f z

  The core circle of the solid torus traces the loop.

• isOpen_image : IsOpen (Φ '' {p : SolidTorus | ‖↑p.1‖ < 1})

  The open solid torus is mapped onto an open set.

theorem TauCeti.IsSolidTorusNeighborhood.range_subset_image {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : Set.range f ⊆ Φ '' {p : SolidTorus | ‖↑p.1‖ < 1}

The loop runs inside the image of the open solid torus.

theorem TauCeti.IsSolidTorusNeighborhood.range_mem_nhdsSet {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : Set.range Φ ∈ nhdsSet (Set.range f)

The solid torus is a neighbourhood of the loop.

theorem TauCeti.IsSolidTorusNeighborhood.apply_mem_range_iff {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) (p : SolidTorus) : Φ p ∈ Set.range f ↔ ↑p.1 = 0

A point of the solid torus lies on the knot exactly when it lies on the core {0} × S¹.

theorem TauCeti.IsSolidTorusNeighborhood.isClosedEmbedding {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h : IsSolidTorusNeighborhood f Φ) : Topology.IsClosedEmbedding Φ

A solid torus neighbourhood in a Hausdorff space is a closed embedding.

theorem TauCeti.IsSolidTorusNeighborhood.isCompact_range {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : IsCompact (Set.range f)

A loop with a solid torus neighbourhood has compact image, the image of the core circle.

theorem TauCeti.IsSolidTorusNeighborhood.isClosed_range {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h : IsSolidTorusNeighborhood f Φ) : IsClosed (Set.range f)

A loop with a solid torus neighbourhood in a Hausdorff space has closed image.

theorem TauCeti.IsSolidTorusNeighborhood.comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Circle → X} {Φ : SolidTorus → X} {e : X → Y} (he : Topology.IsOpenEmbedding e) (h : IsSolidTorusNeighborhood f Φ) : IsSolidTorusNeighborhood (e ∘ f) (e ∘ Φ)

A solid torus neighbourhood is carried along an open embedding of the ambient space, such as the inclusion of an open subset or a homeomorphism.

theorem TauCeti.IsSolidTorusNeighborhood.comp_prodMap {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) (g : Circle ≃ₜ Circle) : IsSolidTorusNeighborhood (f ∘ ⇑g) (Φ ∘ Prod.map id ⇑g)

A solid torus neighbourhood is carried along a reparametrization of the loop by a homeomorphism g of the circle: (w, z) ↦ Φ (w, g z) is a solid torus neighbourhood of f ∘ g.

theorem TauCeti.IsSolidTorusNeighborhood.frontier_image {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h : IsSolidTorusNeighborhood f Φ) : frontier (Φ '' {p : SolidTorus | ‖↑p.1‖ < 1}) = Set.range (Φ ∘ SolidTorus.boundaryInclusion)

In a Hausdorff ambient space, the frontier of the image of the open solid torus is the image of the boundary torus {w | ‖w‖ = 1} × S¹. This set is also the frontier of the exterior of the knot, the complement of the image of the open solid torus.

theorem TauCeti.IsSolidTorusNeighborhood.isEmbedding_comp_boundaryInclusion {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : Topology.IsEmbedding (Φ ∘ SolidTorus.boundaryInclusion)

The boundary torus of a solid torus neighbourhood is embedded: by TauCeti.IsSolidTorusNeighborhood.frontier_image, the frontier of the knot exterior is a torus when the ambient space is Hausdorff.

theorem TauCeti.IsSolidTorusNeighborhood.frontier_subset_compl_range {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : frontier (Φ '' {p : SolidTorus | ‖↑p.1‖ < 1})ᶜ ⊆ (Set.range f)ᶜ

The boundary torus of the knot exterior is disjoint from the knot.

noncomputable def TauCeti.IsSolidTorusNeighborhood.exteriorFrontierHomeomorph {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h : IsSolidTorusNeighborhood f Φ) : Circle × Circle ≃ₜ ↑(frontier (Φ '' {p : SolidTorus | ‖↑p.1‖ < 1})ᶜ)

The framing identifies the boundary torus with the frontier of the knot exterior, the complement of the image of the open solid torus.

@[simp]

theorem TauCeti.IsSolidTorusNeighborhood.coe_exteriorFrontierHomeomorph_apply {X : Type u_1} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h : IsSolidTorusNeighborhood f Φ) (q : Circle × Circle) : ↑(h.exteriorFrontierHomeomorph q) = Φ (SolidTorus.boundaryInclusion q)

The frontier parametrization is the restriction of the solid torus framing.

Reflecting the disc

noncomputable def TauCeti.SolidTorus.conjDisc : SolidTorus ≃ₜ SolidTorus

The reflection (u, w) ↦ (conj u, w) of the solid torus. Precomposing a solid torus with it reverses its orientation at the core point, see SolidTorusNeighborhood/Orientation.lean.

@[simp]

theorem TauCeti.SolidTorus.coe_conjDisc_fst (p : SolidTorus) : ↑(conjDisc p).1 = (starRingEnd ℂ) ↑p.1

The reflection conjugates the disc coordinate.

@[simp]

theorem TauCeti.SolidTorus.conjDisc_snd (p : SolidTorus) : (conjDisc p).2 = p.2

The reflection keeps the circle coordinate.

@[simp]

theorem TauCeti.SolidTorus.conjDisc_conjDisc (p : SolidTorus) : conjDisc (conjDisc p) = p

The reflection is an involution.

@[simp]

theorem TauCeti.SolidTorus.conjDisc_zero (z : Circle) : conjDisc (0, z) = (0, z)

The reflection fixes the core circle.

theorem TauCeti.IsSolidTorusNeighborhood.comp_conjDisc {X : Type u_3} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : IsSolidTorusNeighborhood f (Φ ∘ ⇑SolidTorus.conjDisc)

Precomposing a solid torus neighbourhood with the reflection (u, w) ↦ (conj u, w) gives a solid torus neighbourhood of the same loop.

Existence for embedded circles in ℝ³

theorem TauCeti.exists_isSolidTorusNeighborhood_hasFDerivAt_coreReading {f : Circle → EuclideanSpace ℝ (Fin 3)} (hf : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3))) 2 f) (himm : ∀ (z : Circle), Function.Injective ⇑(mfderiv% f z)) (hinj : Function.Injective f) {U : Set (EuclideanSpace ℝ (Fin 3))} (hU : U ∈ nhdsSet (Set.range f)) : ∃ (Φ : SolidTorus → EuclideanSpace ℝ (Fin 3)), IsSolidTorusNeighborhood f Φ ∧ Set.range Φ ⊆ U ∧ ∃ (L : ℂ × ℝ →L[ℝ] EuclideanSpace ℝ (Fin 3)), HasFDerivAt (SolidTorus.coreReading Φ) L 0 ∧ Function.Injective ⇑L

Solid torus neighbourhoods of knots in ℝ³, with their derivative at the core. A C² embedded circle f in ℝ³ has a solid torus neighbourhood Φ inside any neighbourhood of its image, whose reading (u, t) ↦ Φ (u, exp (t i)) at the core point (0, 1) (TauCeti.SolidTorus.coreReading) is differentiable at the origin with injective derivative.

theorem TauCeti.exists_isSolidTorusNeighborhood {f : Circle → EuclideanSpace ℝ (Fin 3)} (hf : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3))) 2 f) (himm : ∀ (z : Circle), Function.Injective ⇑(mfderiv% f z)) (hinj : Function.Injective f) {U : Set (EuclideanSpace ℝ (Fin 3))} (hU : U ∈ nhdsSet (Set.range f)) : ∃ (Φ : SolidTorus → EuclideanSpace ℝ (Fin 3)), IsSolidTorusNeighborhood f Φ ∧ Set.range Φ ⊆ U

Solid torus neighbourhoods of knots in ℝ³. A C² embedded circle in ℝ³ has a solid torus neighbourhood inside any neighbourhood of its image.