Documentation

TauCeti.LowDimTopology.SolidTorusNeighborhood.Unknot

The exterior of the unknot is a solid torus #

Write ℝ⁴ = ℂ² through (z, w) ↦ (Re z, Im z, Re w, Im w) (TauCeti.complexProdToEuclideanFour). The unknot TauCeti.unknot is the great circle ζ ↦ (ζ, 0) of the unit sphere S³. It has the explicit solid torus neighbourhood (w, ζ) ↦ (ζ, w) / √(1 + ‖w‖ ^ 2) (TauCeti.unknotSolidTorus), whose image is the solid torus ‖w‖ ≤ ‖z‖ of the genus-one Heegaard splitting of S³. Its knot exterior is the complementary solid torus ‖z‖ ≤ ‖w‖ (TauCeti.knotExterior_unknotSolidTorus), which is homeomorphic to D² × S¹ through (z, w) ↦ (z / ‖w‖, w / ‖w‖) (TauCeti.unknotExteriorHomeomorph).

On the common boundary torus this homeomorphism exchanges the two circle factors (TauCeti.unknotExteriorHomeomorph_symm_boundaryInclusion): the point (a, b) of the boundary torus of the exterior is the point (b, a) of the boundary torus of the neighbourhood. So the meridian a ↦ (a, 1) of the exterior solid torus is the longitude a ↦ (1, a) of the unknot, and the longitude of the exterior solid torus is the meridian of the unknot. The preferred (0-) framing of a knot is the one whose longitude is null-homologous in the knot exterior. For the unknot more is true: the longitude of TauCeti.unknotSolidTorus bounds a meridian disc of the exterior, so in particular it is null-homologous there and is the preferred longitude.

This is the geometric input to the surgery descriptions of the unknot: Dehn filling the exterior of the unknot along a slope glues a second solid torus to this one along their boundary tori, which gives S³ for the slope ∞, S¹ × S² for the slope 0, and lens spaces for the other slopes.

Main definitions #

Main results #

References #

The standard solid torus neighbourhood of the unknot #

source
noncomputable def TauCeti.unknotSolidTorus (p : SolidTorus) :
↑(Metric.sphere 0 1)

The standard solid torus neighbourhood of the unknot: (w, ζ) ↦ (ζ, w) / √(1 + ‖w‖ ^ 2) in the coordinates ℝ⁴ = ℂ² of TauCeti.complexProdToEuclideanFour. Its image is the solid torus ‖w‖ ≤ ‖z‖, its meridian discs are w ↦ (ζ, w) / √(1 + ‖w‖ ^ 2) and its longitude is ζ ↦ (ζ, 1) / √2.

Instances For
    source
    @[simp]
    theorem TauCeti.coe_unknotSolidTorus_apply (p : SolidTorus) :
    ↑(unknotSolidTorus p) = complexProdToEuclideanFour (WithLp.toLp 2 ((√(1 + ‖↑p.1‖ ^ 2))⁻¹ • ↑p.2, (√(1 + ‖↑p.1‖ ^ 2))⁻¹ • ↑p.1))
    source
    theorem TauCeti.isSolidTorusNeighborhood_unknotSolidTorus :
    IsSolidTorusNeighborhood (⇑unknot) unknotSolidTorus

    TauCeti.unknotSolidTorus is a solid torus neighbourhood of TauCeti.unknot.

    The exterior of the unknot #

    source
    theorem TauCeti.knotExterior_unknotSolidTorus :
    knotExterior = {x : ↑(Metric.sphere 0 1) | (↑x).ofLp 0 ^ 2 + (↑x).ofLp 1 ^ 2 ≤ (↑x).ofLp 2 ^ 2 + (↑x).ofLp 3 ^ 2}

    The exterior of the unknot for its standard solid torus neighbourhood is the solid torus x₀² + x₁² ≤ x₂² + x₃² of the unit sphere of ℝ⁴.

    source
    noncomputable def TauCeti.unknotExteriorHomeomorph :
    ↑knotExterior ≃ₜ SolidTorus

    The exterior of the unknot is a solid torus. The exterior of the standard solid torus neighbourhood of the unknot, the solid torus ‖z‖ ≤ ‖w‖ in the coordinates ℝ⁴ = ℂ², is homeomorphic to D² × S¹ through (z, w) ↦ (z / ‖w‖, w / ‖w‖).

    Instances For
      source
      @[simp]
      theorem TauCeti.coe_unknotExteriorHomeomorph_apply_fst (x : ↑knotExterior) :
      ↑(unknotExteriorHomeomorph x).1 = ‖(complexProdToEuclideanFour.symm ↑↑x).snd‖⁻¹ • (complexProdToEuclideanFour.symm ↑↑x).fst
      source
      @[simp]
      theorem TauCeti.coe_unknotExteriorHomeomorph_apply_snd (x : ↑knotExterior) :
      ↑(unknotExteriorHomeomorph x).2 = ‖(complexProdToEuclideanFour.symm ↑↑x).snd‖⁻¹ • (complexProdToEuclideanFour.symm ↑↑x).snd
      source
      @[simp]
      theorem TauCeti.coe_unknotExteriorHomeomorph_symm_apply (p : SolidTorus) :
      ↑↑(unknotExteriorHomeomorph.symm p) = complexProdToEuclideanFour (WithLp.toLp 2 ((√(1 + ‖↑p.1‖ ^ 2))⁻¹ • ↑p.1, (√(1 + ‖↑p.1‖ ^ 2))⁻¹ • ↑p.2))
      source
      theorem TauCeti.unknotExteriorHomeomorph_symm_boundaryInclusion (q : Circle × Circle) :
      ↑(unknotExteriorHomeomorph.symm (SolidTorus.boundaryInclusion q)) = unknotSolidTorus (SolidTorus.boundaryInclusion q.swap)

      The exterior of the unknot exchanges meridian and longitude. On the boundary torus, the identification TauCeti.unknotExteriorHomeomorph of the exterior of the unknot with D² × S¹ exchanges the two circle factors: the point (a, b) of the boundary torus of the exterior is the point (b, a) of the boundary torus of TauCeti.unknotSolidTorus. So the boundary a ↦ (a, 1) of the meridian disc w ↦ (w, 1) of the exterior is the longitude a ↦ (1, a) of the unknot, and the longitude b ↦ (1, b) of the exterior is the meridian b ↦ (b, 1) of the unknot.

      source
      @[simp]
      theorem TauCeti.unknotExteriorHomeomorph_exteriorBoundaryInclusion (r : Circle × Circle) :
      unknotExteriorHomeomorph (isSolidTorusNeighborhood_unknotSolidTorus.exteriorBoundaryInclusion r) = SolidTorus.boundaryInclusion r.swap

      On the boundary torus, TauCeti.unknotExteriorHomeomorph sends the exterior boundary point r to SolidTorus.boundaryInclusion r.swap, exchanging the two circle factors. This is the forward counterpart of TauCeti.unknotExteriorHomeomorph_symm_boundaryInclusion.

      source
      theorem TauCeti.unknotExteriorHomeomorph_symm_notMem_range (p : SolidTorus) :
      ↑(unknotExteriorHomeomorph.symm p) ∉ Set.range ⇑unknot

      The exterior of the unknot misses the unknot.