Dehn fillings of knot exteriors

Let Φ : D² × S¹ → X be a solid torus neighbourhood of a knot f in a Hausdorff space X, with knot exterior E (TauCeti.knotExterior) and boundary torus ∂E, parametrized through Φ by S¹ × S¹. A Dehn filling of E glues a solid torus V = D² × S¹ to E along a homeomorphism of the boundary tori. Up to homeomorphism the result depends only on the slope of the gluing, the class in H₁(∂E; ℤ) modulo sign of the image of the meridian ∂D² × {1} of V (Rolfsen, Knots and Links, Chapter 9); this slope is the datum of the filling.

Here a filling is recorded inside the filled space, without a gluing construction, in the same way as TauCeti.HeegaardSplitting: a TauCeti.DehnFilling h s Y consists of closed embeddings of E and of V into Y whose images cover Y and meet only along the boundary torus of V, which is glued to ∂E by a homeomorphism g of S¹ × S¹ read in the two framings, and whose filling slope (TauCeti.IsSolidTorusNeighborhood.fillingSlope) is s. The two pieces being closed, Y is then homeomorphic to the space obtained from E and V by gluing along g. That the homeomorphism type of such a Y depends only on s is the classical well-definedness of Dehn filling, through the mapping class group of the torus; it is not formalized here. For gluings isotopic to gluings induced by integral matrices it is TauCeti.DehnFilling.exists_homeomorph_of_isotopic_torusHomeomorph. The filling slope itself only depends on the gluing up to homotopy (TauCeti.IsSolidTorusNeighborhood.fillingSlope_eq_of_homotopic).

The slope of the gluing is computed from where g sends the meridian curve (TauCeti.IsSolidTorusNeighborhood.fillingSlope_eq_of_apply_torusCurve): the identity gives the meridian of Φ and the exchange of the two circle factors gives its longitude. Every knot exterior has the trivial filling along the meridian, the ambient space itself with V the solid torus neighbourhood (TauCeti.IsSolidTorusNeighborhood.meridianDehnFilling); since the framing of Φ and the preferred framing share the meridian, this is the ∞-surgery on the knot.

Main definitions

• TauCeti.IsSolidTorusNeighborhood.fillingSlope: the slope on ∂E of the meridian of a solid torus glued along a homeomorphism g of S¹ × S¹.
• TauCeti.DehnFilling h s Y: a Dehn filling of the exterior along the slope s, inside Y.
• TauCeti.DehnFilling.desc: the continuous map on the filled space glued from compatible continuous maps on the two pieces.
• TauCeti.DehnFilling.homeomorphOfSolidTorus: the homeomorphism between two fillings whose gluings differ by the boundary values of a homeomorphism of the solid torus.
• TauCeti.DehnFilling.transHomeomorph: transport of a filling along a homeomorphism.
• TauCeti.DehnFilling.openExteriorEmbedding: the open embedding of the exterior without its boundary torus into the filled space.
• TauCeti.IsSolidTorusNeighborhood.meridianDehnFilling: the trivial filling along the meridian.

Main results

• TauCeti.IsSolidTorusNeighborhood.fillingSlope_refl, TauCeti.IsSolidTorusNeighborhood.fillingSlope_prodComm: gluing by the identity has the meridian as slope, and gluing by the exchange of factors has the longitude.
• TauCeti.DehnFilling.ext: a filling is determined by its two embeddings.
• TauCeti.DehnFilling.range_inter_range: the two pieces meet exactly in the boundary torus of the filling solid torus.
• TauCeti.DehnFilling.hom_ext, TauCeti.DehnFilling.desc_unique: a continuous map on the filled space is determined by its restrictions to the two pieces, so the filled space is their gluing.
• TauCeti.DehnFilling.range_openExteriorEmbedding: the open exterior fills the complement of the filling solid torus.

References

• D. Rolfsen, Knots and Links, Publish or Perish (1976), Chapter 9, Section 9F (Dehn surgery along a solid torus: the filled manifold depends only on the curve to which the meridian of the filling solid torus is sent).

noncomputable def TauCeti.IsSolidTorusNeighborhood.fillingSlope {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) (g : Circle × Circle ≃ₜ Circle × Circle) : Slope h.framedBoundaryTorus.H

The filling slope of a gluing g of a solid torus V = D² × S¹ to the knot exterior, the point q of the boundary torus of V being glued to the point g q of the boundary torus of the exterior, both parametrized by S¹ × S¹: the slope on the boundary torus of the exterior of the image t ↦ Φ (g (exp (2πit), 1)) of the meridian of V.

theorem TauCeti.IsSolidTorusNeighborhood.fillingSlope_eq_of_apply_torusCurve {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) {g : Circle × Circle ≃ₜ Circle × Circle} {p q : ℤ} (hpq : IsCoprime p q) (hg : ∀ (t : ↑unitInterval), g ((torusCurve 1 0) t) = (torusCurve p q) t) : h.fillingSlope g = Slope.mk (FramedBoundaryTorus.torusCurveClass h.exteriorFrontierHomeomorph p q) ⋯

The filling slope from the image of the meridian. If the gluing g carries the meridian curve t ↦ (exp (2πit), 1) of the filling solid torus to the (p, q) curve of S¹ × S¹, then the filling slope is the slope of the (p, q) curve on the boundary torus of the exterior, of value p / q in the framing of Φ (TauCeti.FramedBoundaryTorus.value_mk_torusCurveClass).

theorem TauCeti.IsSolidTorusNeighborhood.fillingSlope_eq_of_homotopic {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) {g g' : Circle × Circle ≃ₜ Circle × Circle} (hgg' : (↑g).Homotopic ↑g') : h.fillingSlope g = h.fillingSlope g'

The filling slope only depends on the gluing up to homotopy. Homotopic gluings carry the meridian of the filling solid torus to homologous curves on the boundary torus of the exterior, so they have the same filling slope.

@[simp]

theorem TauCeti.IsSolidTorusNeighborhood.fillingSlope_refl {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : h.fillingSlope (Homeomorph.refl (Circle × Circle)) = h.framedBoundaryTorus.meridian

Gluing by the identity has the meridian of Φ as filling slope.

@[simp]

theorem TauCeti.IsSolidTorusNeighborhood.fillingSlope_prodComm {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : h.fillingSlope (Homeomorph.prodComm Circle Circle) = h.framedBoundaryTorus.longitude

Gluing by the exchange of the two circle factors has the longitude of Φ as filling slope.

structure TauCeti.DehnFilling {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) (s : Slope h.framedBoundaryTorus.H) (Y : Type u_1) [TopologicalSpace Y] : Type u_1

A Dehn filling of the exterior E of a knot along the slope s, recorded inside the filled space Y: closed embeddings of E and of the filling solid torus V = D² × S¹ into Y, whose images cover Y and meet only along the boundary torus of V, glued to the boundary torus of E by a homeomorphism gluing of S¹ × S¹ whose filling slope is s. The two images being closed, Y is homeomorphic to the space obtained by gluing V to E along gluing.

• exteriorEmbedding : ↑knotExterior → Y

  The embedding of the knot exterior into the filled space.

• isClosedEmbedding_exteriorEmbedding : Topology.IsClosedEmbedding self.exteriorEmbedding
• solidTorusEmbedding : SolidTorus → Y

  The embedding of the filling solid torus into the filled space.

• isClosedEmbedding_solidTorusEmbedding : Topology.IsClosedEmbedding self.solidTorusEmbedding
• gluing : Circle × Circle ≃ₜ Circle × Circle

  The gluing of the two boundary tori, both parametrized by S¹ × S¹: the point q of the boundary torus of the filling solid torus is the point gluing q of the boundary torus of the exterior.

• exteriorEmbedding_exteriorBoundaryInclusion (q : Circle × Circle) : self.exteriorEmbedding (h.exteriorBoundaryInclusion (self.gluing q)) = self.solidTorusEmbedding (SolidTorus.boundaryInclusion q)
• range_union_range : Set.range self.exteriorEmbedding ∪ Set.range self.solidTorusEmbedding = Set.univ
• range_inter_range_subset : Set.range self.exteriorEmbedding ∩ Set.range self.solidTorusEmbedding ⊆ Set.range (self.solidTorusEmbedding ∘ SolidTorus.boundaryInclusion)
• fillingSlope_gluing : h.fillingSlope self.gluing = s

theorem TauCeti.DehnFilling.ext {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] {F G : DehnFilling h s Y} (hext : F.exteriorEmbedding = G.exteriorEmbedding) (hsol : F.solidTorusEmbedding = G.solidTorusEmbedding) : F = G

A Dehn filling is determined by its two embeddings: the gluing is the identification of the boundary tori they induce.

theorem TauCeti.DehnFilling.ext_iff {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] {F G : DehnFilling h s Y} : F = G ↔ F.exteriorEmbedding = G.exteriorEmbedding ∧ F.solidTorusEmbedding = G.solidTorusEmbedding

theorem TauCeti.DehnFilling.range_inter_range {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] (F : DehnFilling h s Y) : Set.range F.exteriorEmbedding ∩ Set.range F.solidTorusEmbedding = Set.range (F.solidTorusEmbedding ∘ SolidTorus.boundaryInclusion)

The two pieces of a Dehn filling meet in the boundary torus of the filling solid torus, which is the image of the boundary torus of the exterior.

theorem TauCeti.DehnFilling.exteriorEmbedding_eq_solidTorusEmbedding_iff {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] {F : DehnFilling h s Y} {x : ↑knotExterior} {p : SolidTorus} : F.exteriorEmbedding x = F.solidTorusEmbedding p ↔ ∃ (q : Circle × Circle), p = SolidTorus.boundaryInclusion q ∧ x = h.exteriorBoundaryInclusion (F.gluing q)

A point of the exterior is sent into the filling solid torus only on the boundary torus.

noncomputable def TauCeti.DehnFilling.desc {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] {Z : Type u_2} [TopologicalSpace Z] (F : DehnFilling h s Y) (a : C(↑knotExterior, Z)) (b : C(SolidTorus, Z)) (hab : ∀ (q : Circle × Circle), a (h.exteriorBoundaryInclusion (F.gluing q)) = b (SolidTorus.boundaryInclusion q)) : C(Y, Z)

Maps out of a Dehn filling. Continuous maps a on the knot exterior and b on the filling solid torus that agree along the gluing of the boundary tori descend to a continuous map on the filled space, which is the gluing of its two closed pieces (TauCeti.DehnFilling.desc_unique).

@[simp]

theorem TauCeti.DehnFilling.desc_exteriorEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] {Z : Type u_2} [TopologicalSpace Z] (F : DehnFilling h s Y) (a : C(↑knotExterior, Z)) (b : C(SolidTorus, Z)) (hab : ∀ (q : Circle × Circle), a (h.exteriorBoundaryInclusion (F.gluing q)) = b (SolidTorus.boundaryInclusion q)) (x : ↑knotExterior) : (F.desc a b hab) (F.exteriorEmbedding x) = a x

The map descended from a and b restricts to a on the knot exterior.

@[simp]

theorem TauCeti.DehnFilling.desc_solidTorusEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] {Z : Type u_2} [TopologicalSpace Z] (F : DehnFilling h s Y) (a : C(↑knotExterior, Z)) (b : C(SolidTorus, Z)) (hab : ∀ (q : Circle × Circle), a (h.exteriorBoundaryInclusion (F.gluing q)) = b (SolidTorus.boundaryInclusion q)) (p : SolidTorus) : (F.desc a b hab) (F.solidTorusEmbedding p) = b p

The map descended from a and b restricts to b on the filling solid torus.

theorem TauCeti.DehnFilling.hom_ext {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] {Z : Type u_2} [TopologicalSpace Z] (F : DehnFilling h s Y) {φ ψ : C(Y, Z)} (hE : ∀ (x : ↑knotExterior), φ (F.exteriorEmbedding x) = ψ (F.exteriorEmbedding x)) (hS : ∀ (p : SolidTorus), φ (F.solidTorusEmbedding p) = ψ (F.solidTorusEmbedding p)) : φ = ψ

Maps out of a Dehn filling are determined by their restrictions to the two pieces.

theorem TauCeti.DehnFilling.desc_unique {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] {Z : Type u_2} [TopologicalSpace Z] (F : DehnFilling h s Y) {a : C(↑knotExterior, Z)} {b : C(SolidTorus, Z)} (hab : ∀ (q : Circle × Circle), a (h.exteriorBoundaryInclusion (F.gluing q)) = b (SolidTorus.boundaryInclusion q)) {φ : C(Y, Z)} (hE : ∀ (x : ↑knotExterior), φ (F.exteriorEmbedding x) = a x) (hS : ∀ (p : SolidTorus), φ (F.solidTorusEmbedding p) = b p) : φ = F.desc a b hab

Uniqueness of the descended map: a continuous map on the filled space restricting to a on the exterior and to b on the filling solid torus is TauCeti.DehnFilling.desc.

noncomputable def TauCeti.DehnFilling.homeomorphOfSolidTorus {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] {s' : Slope h.framedBoundaryTorus.H} {Y' : Type u_2} [TopologicalSpace Y'] (F : DehnFilling h s Y) (F' : DehnFilling h s' Y') (ψ : SolidTorus ≃ₜ SolidTorus) (hψ : ∀ (q : Circle × Circle), ψ (SolidTorus.boundaryInclusion q) = SolidTorus.boundaryInclusion (F'.gluing.symm (F.gluing q))) : Y ≃ₜ Y'

Fillings with gluings related over the solid torus are homeomorphic. If the torus map g'⁻¹ ∘ g between the gluings g, g' of two Dehn fillings Y, Y' of the same knot exterior is the restriction of a homeomorphism ψ of the solid torus to its boundary, then Y and Y' are homeomorphic, by the identity on the exterior and by ψ on the filling solid torus.

@[simp]

theorem TauCeti.DehnFilling.homeomorphOfSolidTorus_exteriorEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] {s' : Slope h.framedBoundaryTorus.H} {Y' : Type u_2} [TopologicalSpace Y'] (F : DehnFilling h s Y) (F' : DehnFilling h s' Y') (ψ : SolidTorus ≃ₜ SolidTorus) (hψ : ∀ (q : Circle × Circle), ψ (SolidTorus.boundaryInclusion q) = SolidTorus.boundaryInclusion (F'.gluing.symm (F.gluing q))) (x : ↑knotExterior) : (F.homeomorphOfSolidTorus F' ψ hψ) (F.exteriorEmbedding x) = F'.exteriorEmbedding x

The homeomorphism between fillings is the identity on the knot exterior.

@[simp]

theorem TauCeti.DehnFilling.homeomorphOfSolidTorus_solidTorusEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] {s' : Slope h.framedBoundaryTorus.H} {Y' : Type u_2} [TopologicalSpace Y'] (F : DehnFilling h s Y) (F' : DehnFilling h s' Y') (ψ : SolidTorus ≃ₜ SolidTorus) (hψ : ∀ (q : Circle × Circle), ψ (SolidTorus.boundaryInclusion q) = SolidTorus.boundaryInclusion (F'.gluing.symm (F.gluing q))) (p : SolidTorus) : (F.homeomorphOfSolidTorus F' ψ hψ) (F.solidTorusEmbedding p) = F'.solidTorusEmbedding (ψ p)

The homeomorphism between fillings is ψ on the filling solid torus.

def TauCeti.DehnFilling.transHomeomorph {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] (F : DehnFilling h s Y) {Y' : Type u_2} [TopologicalSpace Y'] (e : Y ≃ₜ Y') : DehnFilling h s Y'

A Dehn filling is carried along a homeomorphism of the filled space.

@[simp]

theorem TauCeti.DehnFilling.transHomeomorph_exteriorEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] (F : DehnFilling h s Y) {Y' : Type u_2} [TopologicalSpace Y'] (e : Y ≃ₜ Y') : (F.transHomeomorph e).exteriorEmbedding = ⇑e ∘ F.exteriorEmbedding

The exterior embedding of a transported filling is the composite with the homeomorphism.

@[simp]

theorem TauCeti.DehnFilling.transHomeomorph_solidTorusEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] (F : DehnFilling h s Y) {Y' : Type u_2} [TopologicalSpace Y'] (e : Y ≃ₜ Y') : (F.transHomeomorph e).solidTorusEmbedding = ⇑e ∘ F.solidTorusEmbedding

The solid torus embedding of a transported filling is the composite with the homeomorphism.

@[simp]

theorem TauCeti.DehnFilling.transHomeomorph_gluing {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] (F : DehnFilling h s Y) {Y' : Type u_2} [TopologicalSpace Y'] (e : Y ≃ₜ Y') : (F.transHomeomorph e).gluing = F.gluing

Transport along a homeomorphism of the filled space keeps the gluing.

The open exterior in the filled space

def TauCeti.DehnFilling.openExteriorEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] (F : DehnFilling h s Y) : ↥h.openExterior → Y

The open exterior in the filled space: the restriction of the exterior embedding to the open exterior TauCeti.IsSolidTorusNeighborhood.openExterior, the complement of the closed solid torus. It is an open embedding onto the complement of the filling solid torus (TauCeti.DehnFilling.range_openExteriorEmbedding), through which the filled space and the ambient space of the knot can be compared locally, for instance their orientations.

@[simp]

theorem TauCeti.DehnFilling.openExteriorEmbedding_apply {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] (F : DehnFilling h s Y) (x : ↥h.openExterior) : F.openExteriorEmbedding x = F.exteriorEmbedding ⟨↑x, ⋯⟩

theorem TauCeti.DehnFilling.range_openExteriorEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] (F : DehnFilling h s Y) : Set.range F.openExteriorEmbedding = (Set.range F.solidTorusEmbedding)ᶜ

The open exterior is the complement of the filling solid torus in the filled space.

theorem TauCeti.DehnFilling.isOpenEmbedding_openExteriorEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] (F : DehnFilling h s Y) : Topology.IsOpenEmbedding F.openExteriorEmbedding

The open exterior is openly embedded in the filled space.

@[simp]

theorem TauCeti.DehnFilling.transHomeomorph_openExteriorEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type u_1} [TopologicalSpace Y] (F : DehnFilling h s Y) {Y' : Type u_2} [TopologicalSpace Y'] (e : Y ≃ₜ Y') : (F.transHomeomorph e).openExteriorEmbedding = ⇑e ∘ F.openExteriorEmbedding

The open exterior in a transported filling is the composite with the homeomorphism.

noncomputable def TauCeti.IsSolidTorusNeighborhood.meridianDehnFilling {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : DehnFilling h h.framedBoundaryTorus.meridian X

The trivial Dehn filling. Gluing the solid torus neighbourhood Φ back into the exterior by the identity recovers the ambient space: X is the Dehn filling of the knot exterior along the meridian slope of Φ, the ∞-surgery on the knot.

@[simp]

theorem TauCeti.IsSolidTorusNeighborhood.meridianDehnFilling_exteriorEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : h.meridianDehnFilling.exteriorEmbedding = Subtype.val

The trivial filling embeds the exterior by its inclusion.

@[simp]

theorem TauCeti.IsSolidTorusNeighborhood.meridianDehnFilling_solidTorusEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : h.meridianDehnFilling.solidTorusEmbedding = Φ

The filling solid torus of the trivial filling is the solid torus neighbourhood.

@[simp]

theorem TauCeti.IsSolidTorusNeighborhood.meridianDehnFilling_gluing {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : h.meridianDehnFilling.gluing = Homeomorph.refl (Circle × Circle)

The trivial filling glues the boundary tori by the identity.

@[simp]

theorem TauCeti.IsSolidTorusNeighborhood.meridianDehnFilling_openExteriorEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} (h : IsSolidTorusNeighborhood f Φ) : h.meridianDehnFilling.openExteriorEmbedding = Subtype.val

In the trivial filling the open exterior is embedded by its inclusion.