Surgery on the unknot

The standard solid torus neighbourhood TauCeti.unknotSolidTorus of the unknot in S³ has the complementary solid torus as exterior (TauCeti.unknotExteriorHomeomorph), and on the common boundary torus the two framings exchange meridian and longitude. This file computes the surgeries on the unknot with coefficients ∞, 0 and -1 / n, which pin the slope convention of Dehn filling against the preferred framing.

• The framing is the preferred one. The longitude z ↦ Φ (1, z) of Φ = unknotSolidTorus is the boundary of a meridian disc of the exterior solid torus, so it is null-homologous in the knot complement: the framing number of Φ is 0 (TauCeti.framingNumber_unknotSolidTorus), and the preferred framing of the boundary torus is the framing by Φ (TauCeti.preferredFramedBoundaryTorus_unknotSolidTorus). So slope values read in the framing of Φ are the surgery coefficients.
• ∞-surgery gives S³. This is the trivial filling of any knot, TauCeti.IsSolidTorusNeighborhood.meridianDehnFilling.
• 0-surgery gives S¹ × S² (TauCeti.unknotZeroDehnFilling). Write S² ⊆ ℝ³ as the union of its closed upper and lower hemispheres, each a disc D² through (x₀, x₁, x₂) ↦ x₀ + i x₁ (TauCeti.hemisphereGraph). Then S¹ × S² is the union of the solid tori S¹ × D²₊ and S¹ × D²₋, glued along S¹ × S¹ by the identity. The first is the exterior of the unknot, through TauCeti.unknotExteriorHomeomorph; since that identification exchanges the two circle factors on the boundary, the meridian of the second solid torus is glued to the longitude of Φ, the slope 0.
• -1 / n-surgery gives S³ (TauCeti.unknotInvIntDehnFilling). Twisting the exterior solid torus n times along its meridian discs is a homeomorphism of the exterior. Embedding the exterior through it and gluing Φ back exhibits S³ as the filling in which the meridian of Φ is glued to the (1, -n) curve, the slope -1 / n.

Main definitions

• TauCeti.unknotZeroDehnFilling: S¹ × S² as the Dehn filling of the exterior of the unknot along the longitude, the 0-surgery on the unknot.
• TauCeti.unknotInvIntDehnFilling: S³ as the Dehn filling of the exterior of the unknot along the slope of the (1, -n) curve, the -1 / n-surgery on the unknot.

Main results

• TauCeti.framingNumber_unknotSolidTorus: the standard solid torus neighbourhood of the unknot has framing number 0.
• TauCeti.preferredFramedBoundaryTorus_unknotSolidTorus: its framing is the preferred framing.
• TauCeti.preferredFramedBoundaryTorus_unknotSolidTorus_longitude: the longitude of the preferred framing is the longitude of TauCeti.unknotSolidTorus.
• TauCeti.nonempty_dehnFilling_preferredFramedBoundaryTorus_longitude_unknotSolidTorus: the 0-surgery on the unknot, read in the preferred framing, is S¹ × S².
• TauCeti.DehnFilling.nonempty_homeomorph_circle_prod_sphere_of_unknot_longitude: every filling along the longitude whose gluing is isotopic to a matrix gluing is homeomorphic to S¹ × S².

References

• D. Rolfsen, Knots and Links, Publish or Perish (1976), Section 2E (the preferred framing, whose longitude is null-homologous in the exterior) and Chapter 9, Example 9G1 (surgery on the unknot: ∞- and ±1 / n-surgery give S³, 0-surgery gives S¹ × S², and p / q-surgery gives the lens space L(p, q)).

The preferred framing of the unknot

theorem TauCeti.framingNumber_unknotSolidTorus (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧↑(Metric.sphere 0 1))) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧↑(Metric.sphere 0 1))) : IsSolidTorusNeighborhood.framingNumber h₁ h₂ isSolidTorusNeighborhood_unknotSolidTorus = 0

The standard framing of the unknot is the preferred framing. The longitude z ↦ Φ (1, z) of Φ = TauCeti.unknotSolidTorus bounds the meridian disc w ↦ (w, 1) of the exterior solid torus, so it is null-homologous in the complement of the unknot, and the framing number of Φ is 0.

theorem TauCeti.preferredFramedBoundaryTorus_unknotSolidTorus (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧↑(Metric.sphere 0 1))) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧↑(Metric.sphere 0 1))) : IsSolidTorusNeighborhood.preferredFramedBoundaryTorus h₁ h₂ isSolidTorusNeighborhood_unknotSolidTorus = isSolidTorusNeighborhood_unknotSolidTorus.framedBoundaryTorus

The preferred framing of the boundary torus of the exterior of the unknot is its framing by the standard solid torus neighbourhood TauCeti.unknotSolidTorus.

theorem TauCeti.preferredFramedBoundaryTorus_unknotSolidTorus_longitude (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧↑(Metric.sphere 0 1))) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧↑(Metric.sphere 0 1))) : (IsSolidTorusNeighborhood.preferredFramedBoundaryTorus h₁ h₂ isSolidTorusNeighborhood_unknotSolidTorus).longitude = isSolidTorusNeighborhood_unknotSolidTorus.framedBoundaryTorus.longitude

The longitude of the preferred framing of the standard solid torus neighbourhood of the unknot is its longitude: the framing number is 0.

0-surgery on the unknot

noncomputable def TauCeti.unknotZeroDehnFilling : DehnFilling isSolidTorusNeighborhood_unknotSolidTorus isSolidTorusNeighborhood_unknotSolidTorus.framedBoundaryTorus.longitude (Circle × ↑(Metric.sphere 0 1))

0-surgery on the unknot is S¹ × S². The product S¹ × S² is the Dehn filling of the exterior of the unknot along the longitude of its standard solid torus neighbourhood, the slope 0 in the preferred framing (TauCeti.preferredFramedBoundaryTorus_unknotSolidTorus, TauCeti.FramedBoundaryTorus.value_longitude). The exterior is the solid torus S¹ × D²₊ over the upper hemisphere and the filling solid torus is S¹ × D²₋ over the lower one.

@[simp]

theorem TauCeti.unknotZeroDehnFilling_exteriorEmbedding_apply (x : ↑knotExterior) : unknotZeroDehnFilling.exteriorEmbedding x = ((unknotExteriorHomeomorph x).2, hemisphereGraph ⋯ (unknotExteriorHomeomorph x).1)

The 0-surgery on the unknot embeds its exterior as the solid torus S¹ × D²₊ over the upper hemisphere, through TauCeti.unknotExteriorHomeomorph.

@[simp]

theorem TauCeti.unknotZeroDehnFilling_solidTorusEmbedding_apply (p : SolidTorus) : unknotZeroDehnFilling.solidTorusEmbedding p = (p.2, hemisphereGraph unknotZeroDehnFilling_solidTorusEmbedding_apply._proof_1 p.1)

The filling solid torus of the 0-surgery on the unknot is the solid torus S¹ × D²₋ over the lower hemisphere.

@[simp]

theorem TauCeti.unknotZeroDehnFilling_gluing : unknotZeroDehnFilling.gluing = Homeomorph.prodComm Circle Circle

The 0-surgery on the unknot glues the boundary tori by exchanging the circle factors.

theorem TauCeti.nonempty_dehnFilling_preferredFramedBoundaryTorus_longitude_unknotSolidTorus (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧↑(Metric.sphere 0 1))) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧↑(Metric.sphere 0 1))) : Nonempty (DehnFilling isSolidTorusNeighborhood_unknotSolidTorus (IsSolidTorusNeighborhood.preferredFramedBoundaryTorus h₁ h₂ isSolidTorusNeighborhood_unknotSolidTorus).longitude (Circle × ↑(Metric.sphere 0 1)))

The 0-surgery on the unknot is S¹ × S², read in the preferred framing: the Dehn filling TauCeti.unknotZeroDehnFilling is along the longitude of TauCeti.unknotSolidTorus, which is the preferred longitude (TauCeti.preferredFramedBoundaryTorus_unknotSolidTorus_longitude).

-1 / n-surgery on the unknot

noncomputable def TauCeti.unknotInvIntDehnFilling (n : ℤ) : DehnFilling isSolidTorusNeighborhood_unknotSolidTorus (Slope.mk (FramedBoundaryTorus.torusCurveClass isSolidTorusNeighborhood_unknotSolidTorus.exteriorFrontierHomeomorph 1 (-n)) ⋯) ↑(Metric.sphere 0 1)

-1 / n-surgery on the unknot is S³. The 3-sphere is the Dehn filling of the exterior of the unknot along the slope of the (1, -n) curve t ↦ Φ (exp (2πit), exp (-2πint)) of Φ = TauCeti.unknotSolidTorus, of value -1 / n in the preferred framing (TauCeti.preferredFramedBoundaryTorus_unknotSolidTorus). The filling solid torus is Φ itself, glued by the shear (a, b) ↦ (a, b a⁻ⁿ) of the boundary tori, and the exterior is embedded after a twist along its meridian discs. For n = 0 this is the trivial filling.

@[simp]

theorem TauCeti.unknotInvIntDehnFilling_exteriorEmbedding_apply (n : ℤ) (x : ↑knotExterior) : (unknotInvIntDehnFilling n).exteriorEmbedding x = ↑(unknotExteriorHomeomorph.symm ((SolidTorus.twist n) (unknotExteriorHomeomorph x)))

The exterior embedding of the -1 / n-surgery on the unknot is the meridian-disc twist, read through the solid torus coordinates of the exterior.

theorem TauCeti.range_unknotInvIntDehnFilling_exteriorEmbedding (n : ℤ) : Set.range (unknotInvIntDehnFilling n).exteriorEmbedding = knotExterior

The -1 / n-surgery on the unknot embeds its exterior onto the exterior itself.

@[simp]

theorem TauCeti.unknotInvIntDehnFilling_solidTorusEmbedding (n : ℤ) : (unknotInvIntDehnFilling n).solidTorusEmbedding = unknotSolidTorus

The filling solid torus of the -1 / n-surgery on the unknot is TauCeti.unknotSolidTorus.

@[simp]

theorem TauCeti.unknotInvIntDehnFilling_gluing (n : ℤ) : (unknotInvIntDehnFilling n).gluing = (Matrix.GeneralLinearGroup.transvection 1 0 unknotInvIntDehnFilling_gluing._proof_1 (-n)).torusHomeomorph

The -1 / n-surgery on the unknot glues the boundary tori by the shear (a, b) ↦ (a, b a⁻ⁿ).

theorem TauCeti.DehnFilling.nonempty_homeomorph_circle_prod_sphere_of_unknot_longitude {Y : Type u_1} [TopologicalSpace Y] (F : DehnFilling isSolidTorusNeighborhood_unknotSolidTorus isSolidTorusNeighborhood_unknotSolidTorus.framedBoundaryTorus.longitude Y) {A : GL (Fin 2) ℤ} (hA : Isotopic ↑F.gluing ↑A.torusHomeomorph) : Nonempty (Y ≃ₜ Circle × ↑(Metric.sphere 0 1))

0-surgery on the unknot. A Dehn filling of the exterior of the unknot along the longitude of its standard solid torus neighbourhood, the slope 0 in the preferred framing, whose gluing is isotopic to a homeomorphism induced by an invertible integral matrix, is homeomorphic to S¹ × S².