The unknot as a grid link #

The standard unknot grids of all sizes present one grid link, the unknot GridLink.unknot. The standard grid of size n + 3 is the X-stabilization of the standard grid of size n + 2 that splits the X-marking in its first column (GridDiagram.isXStabilization_unknot_succ), so by induction every standard unknot grid is connected to the 2 × 2 grid by grid moves (GridDiagram.toGridLink_unknot). This makes the unknot a well-defined grid link, independent of the grid size used to present it.

Main definitions #

TauCeti.GridLink.unknot: the unknot as a grid link.

Main results #

TauCeti.GridDiagram.unknot_succ_eq_stabilizeX: the explicit stabilization relating consecutive standard unknot grids.
TauCeti.GridDiagram.isXStabilization_unknot_succ: consecutive standard unknot grids are related by an X-stabilization.
TauCeti.GridDiagram.isColumnCommutation_stabilizeX_zero_unknot: the south-west stabilization splitting the first column of a standard unknot grid commutes to the next standard unknot grid.
TauCeti.GridDiagram.toGridLink_unknot: every standard unknot grid presents the unknot.
TauCeti.GridLink.isKnot_unknot: the unknot is a knot.

References #

The grid moves follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

source

theorem TauCeti.GridDiagram.unknot_succ_eq_stabilizeX (n : ℕ) :

unknot (n + 1) = (unknot n).stabilizeX 1 1 0

The standard unknot grid of size n + 3 is the X-stabilization of the standard unknot grid of size n + 2 that splits the X-marking in its first column, with the new O-marking in column 1 and row 1.

source

theorem TauCeti.GridDiagram.isXStabilization_unknot_succ (n : ℕ) :

(unknot n).IsXStabilization (unknot (n + 1))

The standard unknot grid of size n + 3 is the X-stabilization of the standard unknot grid of size n + 2 that splits the X-marking in its first column.

source

theorem TauCeti.GridDiagram.isColumnCommutation_stabilizeX_zero_unknot (n : ℕ) :

((unknot n).stabilizeX 0 1 0).IsColumnCommutation (unknot (n + 1))

The south-west X-stabilization of the standard unknot grid of size n + 2 splitting the X-marking of its first column differs from the standard unknot grid of size n + 3 by exchanging the two columns of the new block.

source

def TauCeti.GridLink.unknot :

GridLink

The unknot as a grid link: the grid link of the 2 × 2 grid diagram. Every standard unknot grid presents it (GridDiagram.toGridLink_unknot).

Instances For

source

@[simp]

theorem TauCeti.GridDiagram.toGridLink_unknot (n : ℕ) :

(unknot n).toGridLink = GridLink.unknot

Every standard unknot grid presents the unknot.

source

@[simp]