Documentation

TauCeti.KnotTheory.Grid.SmallGrid.Gradings

The standard two-by-two grid grading computation #

This file records the first explicit grading calculation for the grid-combinatorial lane. There are exactly two grid states in grid size two: the identity graph and the transposition graph. The standard 2 × 2 grid diagram used for the unknot has O markings on the identity graph and X markings on the transposition graph.

The named states are available from StateCardinality and the standard diagram itself from Unknot, where it is the smallest member of the unknot grid family. Here we combine that small-grid API with the integer grading API to compute the two generators' Maslov and Alexander gradings in this concrete diagram, and package the diagram with its odd-component witness.

Main definitions #

Main results #

References #

This supplies a small prerequisite for TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.3, "The complexes and ∂² = 0", and the acceptance criterion that grid homology compute on the 2 × 2 unknot grid with its bigradings. The grid and grading conventions follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapters 3 and 4.

source
@[simp]
theorem TauCeti.GridDiagram.twoByTwo_OSet :
twoByTwo.OSet = {(0, 0), (1, 1)}

The standard two-by-two diagram has O markings at (0,0) and (1,1).

source
@[simp]
theorem TauCeti.GridDiagram.twoByTwo_XSet :
twoByTwo.XSet = {(0, 1), (1, 0)}

The standard two-by-two diagram has X markings at (0,1) and (1,0).

source
theorem TauCeti.GridDiagram.maslovXℤ_O_of_two (G : GridDiagram 2) :
G.maslovXℤ G.O = 0

In a 2 × 2 diagram, the integer X-Maslov grading of the O-marking state vanishes.

source
theorem TauCeti.GridDiagram.maslovOℤ_X_of_two (G : GridDiagram 2) :
G.maslovOℤ G.X = 0

In a 2 × 2 diagram, the integer O-Maslov grading of the X-marking state vanishes.

source
theorem TauCeti.GridDiagram.alexanderTwoℤ_O_of_two (G : GridDiagram 2) :
G.alexanderTwoℤ G.O = -2

Twice the Alexander grading of the O-marking state in a 2 × 2 diagram is -2.

source
theorem TauCeti.GridDiagram.alexanderTwoℤ_X_of_two (G : GridDiagram 2) :
G.alexanderTwoℤ G.X = 0

Twice the Alexander grading of the X-marking state in a 2 × 2 diagram is 0.

source
theorem TauCeti.GridDiagram.alexander_O_of_two (G : GridDiagram 2) :
G.alexander G.O = -1

The Alexander grading of the O-marking state in a 2 × 2 diagram is -1.

source
theorem TauCeti.GridDiagram.alexander_X_of_two (G : GridDiagram 2) :
G.alexander G.X = 0

The Alexander grading of the X-marking state in a 2 × 2 diagram is 0.

source
theorem TauCeti.GridDiagram.maslovOℤ_twoByTwo_twoByTwoId :
twoByTwo.maslovOℤ GridState.twoByTwoId = -1

The integer O-Maslov grading of the identity generator in the standard two-by-two diagram is -1.

source
theorem TauCeti.GridDiagram.maslovXℤ_twoByTwo_twoByTwoId :
twoByTwo.maslovXℤ GridState.twoByTwoId = 0

The integer X-Maslov grading of the identity generator in the standard two-by-two diagram is 0.

source
theorem TauCeti.GridDiagram.alexanderTwoℤ_twoByTwo_twoByTwoId :
twoByTwo.alexanderTwoℤ GridState.twoByTwoId = -2

Twice the Alexander grading of the identity generator in the standard two-by-two diagram is -2.

source
theorem TauCeti.GridDiagram.alexander_twoByTwo_twoByTwoId :
twoByTwo.alexander GridState.twoByTwoId = -1

The Alexander grading of the identity generator in the standard two-by-two diagram is -1.

source
theorem TauCeti.GridDiagram.maslovOℤ_twoByTwo_twoByTwoSwap :
twoByTwo.maslovOℤ GridState.twoByTwoSwap = 0

The integer O-Maslov grading of the transposition generator in the standard two-by-two diagram is 0.

source
theorem TauCeti.GridDiagram.maslovXℤ_twoByTwo_twoByTwoSwap :
twoByTwo.maslovXℤ GridState.twoByTwoSwap = -1

The integer X-Maslov grading of the transposition generator in the standard two-by-two diagram is -1.

source
theorem TauCeti.GridDiagram.alexanderTwoℤ_twoByTwo_twoByTwoSwap :
twoByTwo.alexanderTwoℤ GridState.twoByTwoSwap = 0

Twice the Alexander grading of the transposition generator in the standard two-by-two diagram is 0.

source
theorem TauCeti.GridDiagram.alexander_twoByTwo_twoByTwoSwap :
twoByTwo.alexander GridState.twoByTwoSwap = 0

The Alexander grading of the transposition generator in the standard two-by-two diagram is 0.

source
theorem TauCeti.GridDiagram.alexander_eq_neg_one_or_eq_zero_of_two (G : GridDiagram 2) (x : GridState 2) :
G.alexander x = -1 ∨ G.alexander x = 0

Every generator of an arbitrary 2 × 2 diagram has Alexander grading -1 or 0.

source
theorem TauCeti.GridDiagram.alexander_twoByTwo_eq_neg_one_or_eq_zero (x : GridState 2) :
twoByTwo.alexander x = -1 ∨ twoByTwo.alexander x = 0

Every generator of the standard two-by-two diagram has one of the two computed Alexander gradings.

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

The standard 2 × 2 unknot grid diagram, as an odd-component grid diagram: it presents a knot, so its component count is one.

Instances For
    source
    @[simp]
    theorem TauCeti.OddComponentGridDiagram.bidegree_twoByTwo_twoByTwoId :
    twoByTwo.bidegree GridState.twoByTwoId = (-1, -1)

    The identity generator in the standard two-by-two diagram has bidegree (-1, -1).

    source
    @[simp]
    theorem TauCeti.OddComponentGridDiagram.bidegree_twoByTwo_twoByTwoSwap :
    twoByTwo.bidegree GridState.twoByTwoSwap = (0, 0)

    The transposition generator in the standard two-by-two diagram has bidegree (0, 0).