Isotopies of the boundary torus extend over the solid torus

A homeomorphism of the boundary torus S¹ × S¹ of the solid torus V = D² × S¹ which is the final homeomorphism of an ambient isotopy extends to a homeomorphism of V: the isotopy is run along the radial coordinate of the disc factor, in the collar 1 / 2 ≤ ‖w‖ ≤ 1, and the extension is the identity on the core solid torus ‖w‖ ≤ 1 / 2 (TauCeti.AmbientIsotopy.solidTorusHomeomorph). This is the case D × Z = D² × S¹ of TauCeti.AmbientIsotopy.closedBallProdHomeomorph, read through the identification Circle ≃ₜ sphere (0 : ℂ) 1.

Consequently the torus homeomorphisms extending over V are closed under composition with homeomorphisms isotopic to the identity (TauCeti.SolidTorus.exists_homeomorph_boundaryInclusion_comp_final). This is the isotopy step of the classical proof that a Dehn filling depends only on its slope (Rolfsen, Knots and Links, Section 9F): two fillings of a knot exterior whose gluings g, g' differ by a torus homeomorphism g'⁻¹ ∘ g extending over the filling solid torus are homeomorphic, by the identity on the exterior and that extension on the solid torus, so a gluing may be replaced by any gluing isotopic to it. Here the isotopy is absorbed into a collar inside the filling solid torus, so no collar of the exterior is needed.

Since the torus is a compact connected surface, an isotopy of a homeomorphism of S¹ × S¹ in the general sense of TauCeti.Isotopic, through embeddings, is an ambient isotopy (TauCeti.isotopic_iff_ambientIsotopic). So whenever two homeomorphisms g, k of the boundary torus are isotopic, g⁻¹ ∘ k extends over the solid torus (TauCeti.SolidTorus.exists_homeomorph_boundaryInclusion_symm_apply_of_isotopic).

Main definitions

• TauCeti.AmbientIsotopy.solidTorusHomeomorph: the homeomorphism of the solid torus extending the final homeomorphism of an ambient isotopy of its boundary torus.

Main results

• TauCeti.AmbientIsotopy.solidTorusHomeomorph_boundaryInclusion: on the boundary torus it is the final homeomorphism of the isotopy.
• TauCeti.AmbientIsotopy.solidTorusHomeomorph_of_norm_le: it is the identity on the core ‖w‖ ≤ 1 / 2.
• TauCeti.SolidTorus.exists_homeomorph_boundaryInclusion_comp_final: if a homeomorphism h of the boundary torus extends over the solid torus, so does h ∘ Φ₁ for every ambient isotopy Φ of the torus.
• TauCeti.SolidTorus.exists_homeomorph_boundaryInclusion_symm_apply_of_isotopic: if two homeomorphisms g, k of the boundary torus are isotopic, then g⁻¹ ∘ k extends over the solid torus.

References

• D. Rolfsen, Knots and Links, Publish or Perish (1976), Section 9F (the result of a Dehn filling depends only on the isotopy class of the gluing).

noncomputable def TauCeti.AmbientIsotopy.solidTorusHomeomorph (Φ : AmbientIsotopy (Circle × Circle)) : SolidTorus ≃ₜ SolidTorus

The extension of an ambient isotopy of the boundary torus over the solid torus V = D² × S¹: the isotopy Φ of S¹ × S¹ is run along the radial coordinate ‖w‖ ∈ [1 / 2, 1] of the disc factor. It is the identity on the core ‖w‖ ≤ 1 / 2 (solidTorusHomeomorph_of_norm_le) and the final homeomorphism of Φ on the boundary torus (solidTorusHomeomorph_boundaryInclusion).

@[simp]

theorem TauCeti.AmbientIsotopy.solidTorusHomeomorph_boundaryInclusion (Φ : AmbientIsotopy (Circle × Circle)) (q : Circle × Circle) : Φ.solidTorusHomeomorph (SolidTorus.boundaryInclusion q) = SolidTorus.boundaryInclusion (Φ.final q)

On the boundary torus the extension of Φ is the final homeomorphism of Φ.

theorem TauCeti.AmbientIsotopy.solidTorusHomeomorph_of_norm_le (Φ : AmbientIsotopy (Circle × Circle)) {p : SolidTorus} (hp : ‖↑p.1‖ ≤ 1 / 2) : Φ.solidTorusHomeomorph p = p

The extension of Φ over the solid torus is the identity on the core ‖w‖ ≤ 1 / 2.

theorem TauCeti.SolidTorus.exists_homeomorph_boundaryInclusion_comp_final {h : Circle × Circle → Circle × Circle} (ψ : SolidTorus ≃ₜ SolidTorus) (hψ : ∀ (q : Circle × Circle), ψ (boundaryInclusion q) = boundaryInclusion (h q)) (Φ : AmbientIsotopy (Circle × Circle)) : ∃ (ψ' : SolidTorus ≃ₜ SolidTorus), ∀ (q : Circle × Circle), ψ' (boundaryInclusion q) = boundaryInclusion (h (Φ.final q))

Isotopies are absorbed by the solid torus. If a homeomorphism h of the boundary torus extends to a homeomorphism ψ of the solid torus, then so does h ∘ Φ₁ for every ambient isotopy Φ of the torus: so whether a torus homeomorphism extends over the solid torus only depends on it up to isotopy.

theorem TauCeti.SolidTorus.exists_homeomorph_boundaryInclusion_symm_apply_of_isotopic {g k : Circle × Circle ≃ₜ Circle × Circle} (hgk : Isotopic ↑g ↑k) : ∃ (ψ : SolidTorus ≃ₜ SolidTorus), ∀ (q : Circle × Circle), ψ (boundaryInclusion q) = boundaryInclusion (g.symm (k q))

Isotopic torus homeomorphisms differ by a map extending over the solid torus. If two homeomorphisms g, k of the boundary torus S¹ × S¹ are isotopic, then g⁻¹ ∘ k is the restriction of a homeomorphism of the solid torus D² × S¹.