Solid torus neighbourhoods of knots in the three-sphere

A C² embedded circle in the unit three-sphere has a solid torus neighbourhood inside any prescribed neighbourhood of its image. Stereographic projection from a point omitted by the circle reduces the construction to the Euclidean tubular-neighbourhood theorem. The closed solid torus is transported back by inverse stereographic projection.

Removing its open image gives a compact exterior with torus frontier. The neighbourhood carries an explicit framing; no preferred longitude is selected.

Read in the ambient space at its core point (TauCeti.SolidTorus.coreReading), the neighbourhood is differentiable with injective derivative, valued in the tangent space of the sphere: the Euclidean neighbourhood is, and the inverse stereographic projection is smooth with injective derivative. This is the input for choosing the neighbourhood to preserve orientation.

Main results

• TauCeti.exists_isSolidTorusNeighborhood_sphere_hasFDerivAt_coreReading: a C² embedded circle in S³ has solid torus neighbourhoods, inside any neighbourhood of its image, with an injective derivative at the core point.
• TauCeti.exists_isSolidTorusNeighborhood_sphere: the same without the derivative.

References

• D. Rolfsen, Knots and Links (1976), Sections 2E and 9F.
• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013), Theorem 6.24.

theorem TauCeti.exists_isSolidTorusNeighborhood_sphere_hasFDerivAt_coreReading {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3 + 1)] {f : Circle → ↑(Metric.sphere 0 1)} (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 ↑(Metric.sphere 0 1)} (hU : U ∈ nhdsSet (Set.range f)) : ∃ (Φ : SolidTorus → ↑(Metric.sphere 0 1)), IsSolidTorusNeighborhood f Φ ∧ Set.range Φ ⊆ U ∧ ∃ (L : ℂ × ℝ →L[ℝ] E), HasFDerivAt (SolidTorus.coreReading fun (q : SolidTorus) => ↑(Φ q)) L 0 ∧ Function.Injective ⇑L ∧ ∀ (v : ℂ × ℝ), inner ℝ (↑(Φ (0, 1))) (L v) = 0

Solid torus neighbourhoods of knots in the three-sphere, with their derivative at the core. Every C² embedded circle f in a unit three-sphere has a solid torus neighbourhood Φ inside any prescribed neighbourhood of its image, whose reading (u, t) ↦ Φ (u, exp (t i)) at the core point (0, 1) (TauCeti.SolidTorus.coreReading), taken in the ambient space, is differentiable at the origin with injective derivative valued in the tangent space (ℝ ∙ Φ (0, 1))ᗮ of the sphere.

theorem TauCeti.exists_isSolidTorusNeighborhood_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3 + 1)] {f : Circle → ↑(Metric.sphere 0 1)} (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 ↑(Metric.sphere 0 1)} (hU : U ∈ nhdsSet (Set.range f)) : ∃ (Φ : SolidTorus → ↑(Metric.sphere 0 1)), IsSolidTorusNeighborhood f Φ ∧ Set.range Φ ⊆ U

Every C² embedded circle in a unit three-sphere has a solid torus neighbourhood inside any prescribed neighbourhood of its image.