Orientations of Dehn fillings

A Dehn filling Y of the exterior of a knot in an oriented 3-manifold X contains the open exterior, the complement in X of the closed solid torus, as the open complement of the filling solid torus (TauCeti.DehnFilling.range_openExteriorEmbedding). An orientation of Y is compatible with an orientation of X when the two orientations agree on the open exterior: this is how a surgery on a knot in an oriented manifold, such as S³, is itself oriented, and it is the orientation that statements about orientation-preserving homeomorphisms between surgered manifolds refer to (Kirby's problems 1.19 and 1.81).

Orientations are the homological orientations of TauCeti.HomologicalOrientation, since the filled space of a TauCeti.DehnFilling is only a topological space: compatibility (TauCeti.DehnFilling.IsOrientationCompatible) asks that the orientations of X and of Y pull back to the same orientation of the open exterior, along its inclusion in X and along TauCeti.DehnFilling.openExteriorEmbedding. On a connected filled space a compatible orientation is unique when the open exterior is nonempty (TauCeti.DehnFilling.IsOrientationCompatible.unique), so being orientation-preserving is a well-defined property of a homeomorphism between two fillings of knot exteriors in the same oriented manifold.

Main definitions

• TauCeti.DehnFilling.IsOrientationCompatible F o oY: the orientation oY of the filled space agrees with the orientation o of the ambient space on the open exterior.

Main results

• TauCeti.DehnFilling.IsOrientationCompatible.unique: on a connected filled space there is at most one orientation compatible with a given orientation of the ambient space, provided the open exterior is nonempty.
• TauCeti.DehnFilling.isOrientationCompatible_neg_iff: reversing both orientations preserves compatibility.
• TauCeti.DehnFilling.isOrientationCompatible_transHomeomorph_iff: compatibility after transport along a homeomorphism of the filled space.
• TauCeti.IsSolidTorusNeighborhood.isOrientationCompatible_meridianDehnFilling: the trivial filling, the ambient space itself, carries the ambient orientation as a compatible orientation.

References

• D. Rolfsen, Knots and Links, Publish or Perish (1976), Chapter 9 (Dehn surgery on knots in oriented 3-manifolds).
• A. Hatcher, Algebraic Topology, Cambridge University Press (2002), Section 3.3 (orientations as locally consistent local orientations, restricted along open subsets).

def TauCeti.DehnFilling.IsOrientationCompatible {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type} [TopologicalSpace Y] [T2Space Y] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E X] [ChartedSpace E Y] {d : ℕ} (F : DehnFilling h s Y) (o : HomologicalOrientation X E d) (oY : HomologicalOrientation Y E d) : Prop

The orientation oY of the filled space Y of a Dehn filling F is compatible with the orientation o of the ambient space X of the knot when the two agree on the open exterior, the complement of the closed solid torus: they pull back to the same orientation of the open exterior, along TauCeti.DehnFilling.openExteriorEmbedding and along its inclusion in X.

theorem TauCeti.DehnFilling.isOrientationCompatible_iff {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type} [TopologicalSpace Y] [T2Space Y] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E X] [ChartedSpace E Y] {d : ℕ} (F : DehnFilling h s Y) (o : HomologicalOrientation X E d) (oY : HomologicalOrientation Y E d) : F.IsOrientationCompatible o oY ↔ oY.comap ⋯ = o.comap ⋯

theorem TauCeti.DehnFilling.IsOrientationCompatible.apply_openExteriorEmbedding {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type} [TopologicalSpace Y] [T2Space Y] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E X] [ChartedSpace E Y] {d : ℕ} {F : DehnFilling h s Y} {o : HomologicalOrientation X E d} {oY : HomologicalOrientation Y E d} (hF : F.IsOrientationCompatible o oY) (x : ↥h.openExterior) : oY (F.openExteriorEmbedding x) = (⋯.localOrientationEquiv x d) ((⋯.localOrientationEquiv x d).symm (o ↑x))

At a point of the open exterior, a compatible orientation of the filled space is the orientation of the ambient space, carried across by the two identifications of local homology with that of the open exterior.

theorem TauCeti.DehnFilling.IsOrientationCompatible.unique {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type} [TopologicalSpace Y] [T2Space Y] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E X] [ChartedSpace E Y] {d : ℕ} [ConnectedSpace Y] {F : DehnFilling h s Y} {o : HomologicalOrientation X E d} {oY oY' : HomologicalOrientation Y E d} (hF : F.IsOrientationCompatible o oY) (hF' : F.IsOrientationCompatible o oY') (x : ↥h.openExterior) : oY = oY'

Compatible orientations are unique: on a connected filled space, two orientations compatible with the same orientation of the ambient space are equal, provided the open exterior is nonempty.

@[simp]

theorem TauCeti.DehnFilling.isOrientationCompatible_neg_iff {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type} [TopologicalSpace Y] [T2Space Y] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E X] [ChartedSpace E Y] {d : ℕ} (F : DehnFilling h s Y) (o : HomologicalOrientation X E d) (oY : HomologicalOrientation Y E d) : F.IsOrientationCompatible (-o) (-oY) ↔ F.IsOrientationCompatible o oY

Reversing both orientations preserves compatibility.

theorem TauCeti.DehnFilling.isOrientationCompatible_transHomeomorph_iff {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {h : IsSolidTorusNeighborhood f Φ} {s : Slope h.framedBoundaryTorus.H} {Y : Type} [TopologicalSpace Y] [T2Space Y] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E X] [ChartedSpace E Y] {d : ℕ} (F : DehnFilling h s Y) {Y' : Type} [TopologicalSpace Y'] [T2Space Y'] [ChartedSpace E Y'] (e : Y ≃ₜ Y') (o : HomologicalOrientation X E d) (oY' : HomologicalOrientation Y' E d) : (F.transHomeomorph e).IsOrientationCompatible o oY' ↔ F.IsOrientationCompatible o (oY'.comap ⋯)

A Dehn filling transported along a homeomorphism e : Y ≃ₜ Y' carries the orientation oY' of Y' as a compatible orientation exactly when the original filling carries the pullback of oY' along e.

theorem TauCeti.IsSolidTorusNeighborhood.isOrientationCompatible_meridianDehnFilling {X : Type} [TopologicalSpace X] [T2Space X] {f : Circle → X} {Φ : SolidTorus → X} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E X] {d : ℕ} (h : IsSolidTorusNeighborhood f Φ) (o : HomologicalOrientation X E d) : h.meridianDehnFilling.IsOrientationCompatible o o

The trivial filling along the meridian, the ambient space itself (TauCeti.IsSolidTorusNeighborhood.meridianDehnFilling), carries every orientation of the ambient space as a compatible orientation.