Slice knots

TheoremThe Conway knot is topologically slice#●ready to prove

Let \(K\) be the PL knot traced by the braid closure on \(4\) strands of the braid word \(\sigma_1^{-2} \sigma_2 \sigma_1^{-1} \sigma_2 \sigma_1^{-1} \sigma_3 \sigma_2^{-2} \sigma_3^2\) for the Conway knot 11n34. Then \(K\) is topologically slice: there is a smooth knot \(J\) whose image is unoriented topologically ambient isotopic in \(\mathbb{R}^3\) to the image of \(K\), and \(J\) is topologically slice.

This follows from Freedman's theorem that every knot with trivial Alexander polynomial is topologically slice, since the Conway knot has \(\Delta_K(t) = 1\).

public theorem_wanted conway_knot_topologically_slice : conwayKnot.TopologicallySlice

Sources

• Freedman, The topology of four-dimensional manifolds, J. Diff. Geom. 17 (1982). See also Freedman-Quinn, Topology of 4-Manifolds, Princeton 1990. Problem conway_knot_topologically_slice of the lean-eval benchmark.

Uses 2

Statement usesTopologically slice (PL knot version) · The Conway knot

TheoremThe Conway knot polyline is a simple closed curve#●ready to prove

Let \(K\) be the Conway knot \(11n34\), realized as a closed polyline in \(\mathbb{R}^3\) (the braid closure of a 4-strand braid word for it), and let \(N\) be its number of vertices. The periodic piecewise-linear parametrization of \(K\), which traverses each edge in unit time, is injective on the interval \([0, N)\).

Equivalently, the vertices of \(K\) are distinct, non-adjacent edges are disjoint, and adjacent edges meet only at their shared vertex.

public theorem_wanted conwayKnot_isSimple : conwayKnot.IsSimple

Sources

• https://arxiv.org/abs/1808.02923. Problem conway_knot_not_smoothly_slice of the lean-eval benchmark.

Uses 2

Statement usesSimple PL knot · The Conway knot

TheoremThe Conway knot is not smoothly slice (Piccirillo)#●ready to prove

Let \(K\) be the Conway knot \(11n34\), realized as a closed polyline in \(\mathbb{R}^3\). There is no smooth knot \(J\), that is, a smooth \(2\pi\)-periodic map \(\mathbb{R} \to \mathbb{R}^3\) with nowhere vanishing derivative that is injective on \([0, 2\pi)\), with both of the following properties: some topological ambient isotopy of \(\mathbb{R}^3\) carries the image of \(J\) onto the image of \(K\); and there is a smooth map \(D \colon \mathbb{R}^2 \to \mathbb{R}^3 \times \mathbb{R}\) that is injective with injective derivative on the closed unit disk \(\overline{\mathbb{D}}\), takes \(\overline{\mathbb{D}}\) into the half-space \(\mathbb{R}^3 \times [0, \infty)\), takes a point of \(\overline{\mathbb{D}}\) to height \(0\) exactly when it lies on the unit circle, and whose \(\mathbb{R}^3\)-component maps the unit circle onto the image of \(J\).

public theorem_wanted conway_knot_not_smoothly_slice : ¬ conwayKnot.SmoothlySlice

Sources

• https://arxiv.org/abs/1808.02923. Problem conway_knot_not_smoothly_slice of the lean-eval benchmark.

Uses 2

Statement usesSmoothly slice (PL knot version) · The Conway knot

TheoremA topologically slice knot that is not smoothly slice#●ready to prove

There is a PL knot \(K\) (a closed polyline in \(\mathbb{R}^3\) with at least three vertices, not required to be simple) that is topologically slice but not smoothly slice. Here \(K\) is smoothly (respectively topologically) slice when some smooth knot whose image is topologically ambient isotopic to the image of \(K\) bounds a smooth (respectively locally flat) properly embedded \(2\)-disk in \(\mathbb{R}^3 \times [0, \infty)\).

public theorem_wanted exists_topologically_slice_not_smoothly_slice :
    ∃ K : PLKnot, K.TopologicallySlice ∧ ¬ K.SmoothlySlice

Sources

• Casson, 1980s (unpublished); Akbulut-Matveyev, A convex decomposition theorem for 4-manifolds, IMRN 1998. See also Hedden-Kirk-Livingston, Non-slice linear combinations of algebraic knots, J. Eur. Math. Soc. 14 (2012). Problem exists_topologically_slice_not_smoothly_slice of the lean-eval benchmark.

Uses 3

Statement usesPL knot (closed polyline) · Smoothly slice (PL knot version) · Topologically slice (PL knot version)

4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.