Documentation

TauCeti.KnotTheory.Grid.Move.Components

The number of components of a grid link #

Cyclic permutations of the rows or columns, commutations and stabilizations all preserve the number of components of the link a grid diagram represents. The number of components is therefore an invariant of grid links, GridLink.componentCount, and so is the property of being a knot, GridLink.IsKnot. The diagrams presenting a knot in this sense are exactly the knot grid diagrams, on which invariants such as τ are defined.

As a first application, the 4 × 4 grid of the Hopf link and the standard unknot grids present different grid links: no sequence of grid moves connects them.

Main definitions #

Main results #

References #

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

source
def TauCeti.GridLink.componentCount :
GridLink → ℕ

The number of components of a grid link, read off any grid diagram presenting it.

Instances For
    source
    def TauCeti.GridLink.IsKnot (L : GridLink) :
    Prop

    A grid link is a knot when it has exactly one component.

    Instances For
      source
      theorem TauCeti.GridLink.isKnot_def (L : GridLink) :
      L.IsKnot ↔ L.componentCount = 1

      A grid link is a knot exactly when it has one component.

      source
      theorem TauCeti.GridDiagram.MovesTo.componentCount_eq {n m : ℕ} {G : GridDiagram n} {G' : GridDiagram m} (h : G.MovesTo G') :
      G'.componentCount = G.componentCount

      Grid moves preserve the number of represented link components.

      source
      theorem TauCeti.GridDiagram.MovesTo.isKnot_iff {n m : ℕ} {G : GridDiagram n} {G' : GridDiagram m} (h : G.MovesTo G') :
      G'.IsKnot ↔ G.IsKnot

      Grid moves preserve whether a grid diagram represents a knot.