Smoothly and topologically slice knots #
A knot K ⊆ S³ is smoothly slice if it bounds a smoothly embedded disc in the four-ball
D⁴: a disc D ⊆ D⁴ meeting the boundary sphere exactly along its own boundary circle, with
∂D = K. This file states sliceness on the geometric presentation of a knot, a smooth circle
embedding K : S¹ → Sⁿ (TauCeti.SmoothCircleEmbedding), for the unit sphere of an
(n + 1)-dimensional real inner product space E, so that S³ ⊆ ℝ⁴ is the case n = 3.
A smooth slice disc for K (TauCeti.IsSmoothSliceDisc K Φ) is a map Φ from the closed unit
disc of ℂ to the closed unit ball of E which
- is a smooth embedding in the sense of manifolds with boundary (
Manifold.IsSmoothEmbeddingfor the half-space models ofTauCeti.instChartedSpaceClosedBall); - is properly embedded: the preimage of the manifold boundary of
Dⁿ⁺¹, the unit sphere, is the manifold boundary ofD², the unit circle; and - restricts to
Kon the boundary circle, through the inclusionSet.inclusion Metric.sphere_subset_closedBallof the circle into the disc.
No separate neatness condition is needed. Mathlib's Manifold.IsImmersion is a chart normal form,
not an injectivity condition on the differential: around every point there are half-space charts of
the disc and of the ball in which Φ is the restriction of a linear map u ↦ equiv (u, 0) on the
whole chart target (Manifold.ImmersionAtProp). The boundary coordinate of the ball therefore pulls
back to a linear functional on the model half-plane, nonnegative on the half-plane and, by
preimage_boundary, vanishing exactly on its boundary line; so it is a positive multiple of the
boundary coordinate of the disc. Hence a smooth slice disc is neat: it meets the boundary sphere
transversally, as in the usual notion of a properly embedded smooth slice disc.
K is smoothly slice (TauCeti.IsSmoothlySlice K) when such a disc exists.
A locally flat slice disc (TauCeti.IsTopologicalSliceDisc K Φ) asks only for a locally flat
embedding Φ (TauCeti.IsLocallyFlat) which meets the unit sphere exactly along the unit circle
and restricts to K there. Local flatness is taken with tangential model the half-plane
EuclideanHalfSpace 2 and complementary model ℝⁿ⁻¹: around every point of the disc a chart of the
ball, valued in EuclideanHalfSpace 2 × ℝⁿ⁻¹, carries the disc exactly onto
EuclideanHalfSpace 2 × {0}, so that at the boundary circle the disc is flat up to the boundary
sphere. K is topologically slice (TauCeti.IsTopologicallySlice K) when such a disc exists. The
two notions are kept separate on purpose: the gap between them is the content of Freedman's theorem
that Alexander-polynomial-one knots are topologically slice, and of the existence of topologically
but not smoothly slice knots. In the forward direction a smooth slice disc is a locally flat one
(TauCeti.IsSmoothSliceDisc.isTopologicalSliceDisc): it is a neat smooth embedding of manifolds
with boundary, hence locally flat with complementary model ℝⁿ⁻¹ by
TauCeti.IsLocallyFlat.of_isSmoothEmbedding_of_preimage_boundary_of_sub_eq.
The predicate is exercised on the great circles: a great circle
TauCeti.SmoothCircleEmbedding.greatCircle ι bounds the flat disc ι D², the restriction of the
linear isometry ι to the closed unit balls, which is a smooth embedding of manifolds with boundary
(LinearIsometry.isSmoothEmbedding_unitClosedBallMap). In particular the unknot is smoothly
slice.
Main definitions #
TauCeti.IsSmoothSliceDisc K Φ:Φis a smooth slice disc forK.TauCeti.IsSmoothlySlice K:Kbounds a smooth slice disc.TauCeti.IsTopologicalSliceDisc K Φ:Φis a locally flat slice disc forK.TauCeti.IsTopologicallySlice K:Kbounds a locally flat slice disc.
Both kinds of sliceness are invariant under the two canonical reparametrizations of the circle,
rotation and reversal: each reparametrizes the slice disc by the corresponding linear isometry of
the plane, which is a diffeomorphism of the disc (LinearIsometryEquiv.unitClosedBallDiffeomorph).
In particular sliceness does not depend on the orientation of the knot. More generally a slice disc
can be reparametrized by any diffeomorphism of the disc preserving its boundary circle
(TauCeti.IsSmoothSliceDisc.comp_diffeomorph), so sliceness is invariant under the corresponding
reparametrization of the knot (TauCeti.isSmoothlySlice_congr_diffeomorph); invariance under
diffeomorphisms of the circle given by a lift is derived from this in
TauCeti.KnotTheory.Slice.Reparametrization. Dually, both kinds
of sliceness are invariant under linear isometries e : E ≃ₗᵢ[ℝ] F of the ambient spaces, which
carry a slice disc Φ for K to the slice disc e ∘ Φ for e ∘ K; this is what makes sliceness
invariant under taking mirror images.
Main results #
TauCeti.IsSmoothSliceDisc.norm_eq_one_iff: a slice disc meets the unit sphere exactly along the unit circle.TauCeti.IsSmoothSliceDisc.comp_diffeomorph,TauCeti.IsSmoothSliceDisc.comp_unitClosedBallMap: reparametrizing a slice disc by a diffeomorphism of the disc preserving its boundary circle, for instance a linear isometry of the plane, gives a slice disc for the correspondingly reparametrized knot.TauCeti.isSmoothlySlice_congr_diffeomorph: smooth sliceness is invariant under reparametrization by the boundary values of a diffeomorphism of the disc.TauCeti.isSmoothlySlice_rotate_iff,TauCeti.isSmoothlySlice_reverse_iff: sliceness is invariant under rotation and reversal of the parametrization.TauCeti.IsSmoothSliceDisc.unitClosedBallMap_comp,TauCeti.isSmoothlySlice_congr_linearIsometryEquiv: sliceness is invariant under linear isometries of the ambient spaces.TauCeti.isSmoothSliceDisc_greatCircle_unitClosedBallMap: the flat discι D²is a slice disc for the great circleι S¹.TauCeti.isSmoothlySlice_greatCircle,TauCeti.isSmoothlySlice_unknot: great circles, and in particular the unknot, are smoothly slice.TauCeti.IsSmoothSliceDisc.isTopologicalSliceDisc,TauCeti.IsSmoothlySlice.isTopologicallySlice: smoothly slice knots are topologically slice.TauCeti.IsTopologicalSliceDisc.comp_homeomorph: reparametrizing a locally flat slice disc by a homeomorphism of the disc preserving its boundary circle gives a locally flat slice disc.TauCeti.isTopologicallySlice_congr_homeomorph: topological sliceness is invariant under reparametrization by the boundary values of a homeomorphism of the disc.TauCeti.isTopologicallySlice_rotate_iff,TauCeti.isTopologicallySlice_reverse_iff: topological sliceness is invariant under rotation and reversal of the parametrization.TauCeti.IsTopologicalSliceDisc.unitClosedBallMap_comp,TauCeti.isTopologicallySlice_congr_linearIsometryEquiv: topological sliceness is invariant under linear isometries of the ambient spaces.TauCeti.isTopologicalSliceDisc_greatCircle_unitClosedBallMap: the flat discι D²is a locally flat slice disc for the great circleι S¹.TauCeti.isTopologicallySlice_greatCircle,TauCeti.isTopologicallySlice_unknot: great circles, and in particular the unknot, are topologically slice.
References #
- W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 8, for slice knots.
- C. Livingston, A survey of classical knot concordance, in Handbook of Knot Theory (2005), Section 2, for smooth versus topological sliceness.
- M. Freedman and F. Quinn, Topology of 4-Manifolds, Princeton (1990), Section 11.7, for locally flat slice discs.
A smooth slice disc for a smooth circle embedding K : S¹ → Sⁿ in the unit sphere of E:
a smooth embedding Φ of the closed unit disc of ℂ into the closed unit ball of E, in the sense
of manifolds with boundary, which is properly embedded (the preimage of the boundary sphere is the
boundary circle) and restricts to K on the boundary circle.
- isSmoothEmbedding : Manifold.IsSmoothEmbedding (modelWithCornersEuclideanHalfSpace 2) (modelWithCornersEuclideanHalfSpace (n + 1)) (↑⊤) Φ
The disc is a smooth embedding of manifolds with boundary.
- preimage_boundary : Φ ⁻¹' ModelWithCorners.boundary ↑(Metric.closedBall 0 1) = ModelWithCorners.boundary ↑(Metric.closedBall 0 1)
The disc is properly embedded: it meets the boundary sphere exactly along its boundary circle.
The disc restricts to
Kon its boundary circle.
Instances For
A smooth circle embedding K : S¹ → Sⁿ is smoothly slice if it bounds a smooth slice disc
in the closed unit ball Dⁿ⁺¹.
Instances For
A smoothly slice knot bounds a smooth slice disc.
A knot with a smooth slice disc is smoothly slice.
A smooth slice disc is a smooth map of manifolds with boundary.
A smooth slice disc is a topological embedding.
A smooth slice disc is injective.
A slice disc meets the unit sphere exactly along the unit circle: a point of the disc is sent to a unit vector exactly when it is a unit vector.
The image of the boundary circle under a slice disc for K is the image of K.
Reparametrizing a slice disc for K by a diffeomorphism D of the closed unit disc gives a
slice disc for the reparametrization of K along the circle (a diffeomorphism preserves the
boundary circle automatically): if D is σ : Circle → Circle on the circle and K' = K ∘ σ,
then Φ ∘ D is a slice disc for K'.
Reparametrizing a slice disc for K by a linear isometry e of the plane gives a slice disc
for the reparametrization of K along the circle: if σ : Circle → Circle is e on the circle
and K' = K ∘ σ, then Φ ∘ e is a slice disc for K'.
Transporting a smooth slice disc for K along a linear isometry e : E ≃ₗᵢ[ℝ] F of the
ambient spaces gives a smooth slice disc for the transported knot: if K' = e ∘ K, then e ∘ Φ is
a smooth slice disc for K'.
Smooth sliceness is invariant under reparametrization by a disc diffeomorphism. If a
diffeomorphism D of the closed unit disc is σ on the boundary circle, then K ∘ σ is smoothly
slice exactly when K is.
Invariance under rotation and reversal #
Rotating the parametrization of a smoothly slice knot gives a smoothly slice knot.
Smooth sliceness does not depend on the rotation of the parametrization.
Reversing the orientation of a smoothly slice knot gives a smoothly slice knot.
Smooth sliceness does not depend on the orientation of the knot.
Transporting a smoothly slice knot along a linear isometry of the ambient spaces gives a smoothly slice knot.
Smooth sliceness is invariant under linear isometries of the ambient spaces: if K' = e ∘ K
for a linear isometry e : E ≃ₗᵢ[ℝ] F, then K' is smoothly slice exactly when K is.
The flat disc ι D² is a smooth slice disc for the great circle ι S¹.
Great circles are smoothly slice: they bound flat discs.
The unknot is smoothly slice: it bounds the flat disc of the first coordinate plane.
Topological sliceness #
A locally flat slice disc for a smooth circle embedding K : S¹ → Sⁿ in the unit sphere of
E: a map Φ from the closed unit disc of ℂ to the closed unit ball of E which is a locally
flat embedding, meets the unit sphere exactly along the unit circle, and restricts to K on the
boundary circle.
Local flatness has tangential model the half-plane EuclideanHalfSpace 2 and complementary model
ℝⁿ⁻¹: around every point of the disc there is a chart of the ball, valued in
EuclideanHalfSpace 2 × ℝⁿ⁻¹, carrying the disc exactly onto EuclideanHalfSpace 2 × {0}.
- isLocallyFlat : IsLocallyFlat (EuclideanHalfSpace 2) (EuclideanSpace ℝ (Fin (n - 1))) Φ
The disc is a locally flat embedding, flat up to the boundary sphere.
The disc is properly embedded: a point of the disc is sent to a unit vector exactly when it is a unit vector.
The disc restricts to
Kon its boundary circle.
Instances For
A smooth circle embedding K : S¹ → Sⁿ is topologically slice if it bounds a locally flat
slice disc in the closed unit ball Dⁿ⁺¹.
Instances For
A topologically slice knot bounds a locally flat slice disc.
A knot with a locally flat slice disc is topologically slice.
A locally flat slice disc is continuous.
A locally flat slice disc is a topological embedding.
A locally flat slice disc is injective.
A locally flat slice disc is properly embedded: the preimage of the manifold boundary of the ball, the unit sphere, is the manifold boundary of the disc, the unit circle.
The image of the boundary circle under a locally flat slice disc for K is the image of
K.
Reparametrizing a locally flat slice disc for K by a homeomorphism D of the closed unit
disc which preserves the boundary circle gives a locally flat slice disc for the reparametrization
of K along the circle: if D is σ : Circle → Circle on the circle and K' = K ∘ σ, then
Φ ∘ D is a locally flat slice disc for K'.
Reparametrizing a locally flat slice disc for K by a linear isometry e of the plane gives a
locally flat slice disc for the reparametrization of K along the circle: if σ : Circle → Circle
is e on the circle and K' = K ∘ σ, then Φ ∘ e is a locally flat slice disc for K'.
Transporting a locally flat slice disc for K along a linear isometry e : E ≃ₗᵢ[ℝ] F of the
ambient spaces gives a locally flat slice disc for the transported knot: if K' = e ∘ K, then
e ∘ Φ is a locally flat slice disc for K'.
Topological sliceness is invariant under reparametrization by a disc homeomorphism. If a
homeomorphism D of the closed unit disc preserves the boundary circle and is σ there, then
K ∘ σ is topologically slice exactly when K is.
A smooth slice disc is a locally flat slice disc. A smooth slice disc is a neat smooth
embedding of manifolds with boundary, so it is locally flat with tangential model the half-plane
and complementary model ℝⁿ⁻¹
(TauCeti.IsLocallyFlat.of_isSmoothEmbedding_of_preimage_boundary_of_sub_eq).
Smoothly slice knots are topologically slice.
Rotating the parametrization of a topologically slice knot gives a topologically slice knot.
Topological sliceness does not depend on the rotation of the parametrization.
Reversing the orientation of a topologically slice knot gives a topologically slice knot.
Topological sliceness does not depend on the orientation of the knot.
Transporting a topologically slice knot along a linear isometry of the ambient spaces gives a topologically slice knot.
Topological sliceness is invariant under linear isometries of the ambient spaces: if
K' = e ∘ K for a linear isometry e : E ≃ₗᵢ[ℝ] F, then K' is topologically slice exactly when
K is.
The flat disc ι D² is a locally flat slice disc for the great circle ι S¹.
Great circles are topologically slice: they bound locally flat discs.
The unknot is topologically slice: the flat disc bounding it is locally flat.