Documentation

TauCeti.KnotTheory.Grid.Unknot.Basic

The standard unknot grid diagram of arbitrary grid number #

This file builds the standard unknot grid diagram of every grid number n + 2: the O markings sit on the diagonal and the X markings sit on the diagonal shifted up by one row, so the represented link is the staircase closing up once around the torus in each direction, that is, the unknot. Its smallest member, the 2 × 2 diagram TauCeti.GridDiagram.twoByTwo, is defined here too and identified with the n = 0 member of the family; the two-by-two grading computations that use it live downstream in TauCeti.KnotTheory.Grid.SmallGrid.Gradings.

Two things are proved about the family. First it really is a knot diagram: its component permutation is (finRotate (n + 2))⁻¹, a single (n + 2)-cycle, so all n + 2 markings lie on one component. Second, the bigradings of its two marking states are computed. Writing N = n + 2 for the grid number, the general lemmas maslovOℤ_O and maslovXℤ_X give M_O(O) = M_X(X) = 1 - N, while the two crossed Maslov gradings are computed here to be M_X(O) = M_O(X) = 0. Hence

(M_O, A) is (1 - N, -(N - 1)) at the O-state and (0, 0) at the X-state.

Both gradings therefore differ by N - 1 between the two marking states, which is the spread expected of the fully blocked grid homology of an N-grid unknot: that homology is predicted to be W^{⊗(N-1)} with W = 𝔽 ⊕ 𝔽 in bigradings (0, 0) and (-1, -1), and the two computed bigradings are exactly the two extreme bigradings of that tensor power. Nothing about the homology is proved here, and the gradings of the remaining grid states are not compared with these two: only the two marking states are graded.

The Maslov computation reduces to counts of pairs of columns. Only the state-to-marking direction uses weak comparisons against the centers of the marked squares; the marking-to-state direction and both self-pairings remain strict. Each of the three strict crossed counts differs from the plain count #{(c, c') | c < c'} by exactly N - 1 — the missing pairs are the ones ending in the last column, respectively the ones with consecutive columns — and each of the two weak crossed counts exceeds it by exactly 1. The five count comparisons are the private lemmas below, and the plain count itself never has to be evaluated.

Main definitions #

Main results #

References #

The diagram and the grading conventions follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapters 3 and 4.

source
def TauCeti.GridDiagram.unknot (n : ℕ) :
GridDiagram (n + 2)

The standard grid diagram for the unknot with grid number n + 2.

The O markings occupy the diagonal squares and the X markings the diagonal shifted up by one row. Following the markings alternately horizontally and vertically traverses a single staircase that winds once around the torus in each direction, so the represented link is the unknot.

Instances For
    source
    @[simp]
    theorem TauCeti.GridDiagram.unknot_O_toPerm (n : ℕ) :
    (unknot n).O.toPerm = 1

    The O markings of the standard unknot grid are the identity permutation graph.

    source
    @[simp]
    theorem TauCeti.GridDiagram.unknot_X_toPerm (n : ℕ) :
    (unknot n).X.toPerm = finRotate (n + 2)

    The X markings of the standard unknot grid are the cyclic shift permutation graph.

    source
    theorem TauCeti.GridDiagram.unknot_O_apply (n : ℕ) (c : Fin (n + 2)) :
    (unknot n).O.toPerm c = c

    The O marking of the standard unknot grid in a column is in the diagonal row.

    source
    theorem TauCeti.GridDiagram.unknot_X_apply (n : ℕ) (c : Fin (n + 2)) :
    (unknot n).X.toPerm c = (finRotate (n + 2)) c

    The X marking of the standard unknot grid in a column is one row above the diagonal.

    source
    theorem TauCeti.GridDiagram.unknot_X_apply_eq_add_one (n : ℕ) (c : Fin (n + 2)) :
    (unknot n).X.toPerm c = c + 1

    The X markings of the standard unknot grid form the shifted diagonal.

    The smallest member, in grid number two #

    source
    @[reducible, inline]
    abbrev TauCeti.GridDiagram.twoByTwo :
    GridDiagram 2

    The standard 2 × 2 grid diagram with O markings on the identity state and X markings on the transposition state. This is the usual smallest grid diagram for the unknot.

    Instances For
      source
      @[simp]
      theorem TauCeti.GridDiagram.twoByTwo_O :
      twoByTwo.O = GridState.twoByTwoId

      The O-marking state of the standard two-by-two diagram is the identity state.

      source
      @[simp]
      theorem TauCeti.GridDiagram.twoByTwo_X :
      twoByTwo.X = GridState.twoByTwoSwap

      The X-marking state of the standard two-by-two diagram is the transposition state.

      source
      theorem TauCeti.GridDiagram.unknot_zero :
      unknot 0 = twoByTwo

      In grid number two the standard unknot grid is the 2 × 2 diagram twoByTwo.

      source
      theorem TauCeti.GridDiagram.componentPerm_unknot (n : ℕ) :
      (unknot n).componentPerm = (finRotate (n + 2))⁻¹

      Traversing the standard unknot grid from an O marking to the X marking in its row and back down to the next O marking shifts the column down by one.

      source
      theorem TauCeti.GridDiagram.isKnot_unknot (n : ℕ) :
      (unknot n).IsKnot

      The standard unknot grid diagram represents a knot: its component permutation is a single cycle through all n + 2 markings.

      source
      theorem TauCeti.GridDiagram.componentCycleType_unknot (n : ℕ) :
      (unknot n).componentCycleType = {n + 2}

      The sole component of the standard unknot grid diagram carries all n + 2 markings.

      source
      theorem TauCeti.GridDiagram.relabelRows_relabelColumns_unknot (n : ℕ) :
      relabelColumns (finRotate (n + 2)) (relabelRows (finRotate (n + 2)) (unknot n)) = unknot n

      The standard unknot grid diagram is invariant under shifting all rows and all columns by one at the same time.

      Column-pair counts for the Maslov gradings #

      The bigradings of the two marking states #

      source
      theorem TauCeti.GridDiagram.maslovXℤ_unknot_O (n : ℕ) :
      (unknot n).maslovXℤ (unknot n).O = 0

      The X-Maslov grading of the O-marking state of the standard unknot grid vanishes.

      source
      theorem TauCeti.GridDiagram.maslovOℤ_unknot_X (n : ℕ) :
      (unknot n).maslovOℤ (unknot n).X = 0

      The O-Maslov grading of the X-marking state of the standard unknot grid vanishes.

      source
      theorem TauCeti.GridDiagram.alexanderTwoℤ_unknot_X (n : ℕ) :
      (unknot n).alexanderTwoℤ (unknot n).X = 0

      Twice the Alexander grading of the X-marking state of the standard unknot grid vanishes.

      source
      theorem TauCeti.GridDiagram.alexanderTwoℤ_unknot_O (n : ℕ) :
      (unknot n).alexanderTwoℤ (unknot n).O = -2 * (↑n + 1)

      Twice the Alexander grading of the O-marking state of the standard unknot grid is -2 (n + 1).

      source
      theorem TauCeti.GridDiagram.alexander_unknot_X (n : ℕ) :
      (unknot n).alexander (unknot n).X = 0

      The Alexander grading of the X-marking state of the standard unknot grid is zero.

      source
      theorem TauCeti.GridDiagram.alexander_unknot_O (n : ℕ) :
      (unknot n).alexander (unknot n).O = -(↑n + 1)

      The Alexander grading of the O-marking state of the standard unknot grid is -(n + 1), one less than the negated grid number.