The standard torus link grid diagrams

This file builds the standard grid diagram of the (p + 1, q + 1) torus link: on a grid of size (p + 1) + (q + 1) the O markings sit on the diagonal and the X markings sit on the diagonal shifted up by q + 1 rows. Following the markings alternately horizontally and vertically shifts the column down by q + 1 each time, so the component permutation is the inverse of the (q + 1)-st power of the cyclic shift finRotate. The smallest members are the standard unknot grids (q = 0), the 4 × 4 grid with p = q = 1, and the 5 × 5 grid with p = 1, q = 2.

The cycle decomposition of the component permutation is computed from Equiv.Perm.IsCycle.cycleType_pow_of_not_dvd: the diagram has exactly gcd (p + 1) (q + 1) link components, all of them carrying the same number ((p + 1) + (q + 1)) / gcd (p + 1) (q + 1) of markings, and it represents a knot exactly when p + 1 and q + 1 are coprime. That is all that is proved here.

Everything else in the name "torus link" is informal motivation and is not established by this file: that the staircase traversal is the closure of the (p + 1)-strand braid winding q + 1 times around, hence the (p + 1, q + 1) torus link — of which the classical component count is indeed gcd (p + 1) (q + 1), matching the count proved here — and, in the same vein, the readings of the members above as the unknot, the Hopf link, and the trefoil. As the roadmap's standing convention has it, a link is a grid diagram modulo grid moves at this stage, and the comparison with other presentations of a link belongs to the separate reconciliation lane; until that lane runs, the classical names are labels for these diagrams, not theorems about them.

Main definitions

• TauCeti.GridDiagram.torusLink: the standard grid diagram of the (p + 1, q + 1) torus link, of grid number (p + 1) + (q + 1).

Main results

• TauCeti.GridDiagram.torusLink_X_val_of_le and TauCeti.GridDiagram.torusLink_X_val_of_lt: the X marking in column c sits in row c + (q + 1) for c ≤ p and in row c - (p + 1) for c > p.
• TauCeti.GridDiagram.torusLink_zero_right: with q = 0 this is the standard unknot grid.
• TauCeti.GridDiagram.transpose_torusLink: the diagonal reflection of the (p + 1, q + 1) grid is the (q + 1, p + 1) grid, transported to the same grid number.
• TauCeti.GridDiagram.componentPerm_torusLink: the component permutation is the inverse of the (q + 1)-st power of the cyclic shift.
• TauCeti.GridDiagram.componentCycleType_torusLink and TauCeti.GridDiagram.componentCount_torusLink: there are gcd (p + 1) (q + 1) components, of equal size.
• TauCeti.GridDiagram.isKnot_torusLink_iff: the diagram represents a knot exactly when p + 1 and q + 1 are coprime.

References

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.1, "Grid diagrams and grid states", and supplies the family of diagrams that Lane G.7 needs for τ(T_{p,q}) and the Milnor conjecture, together with the 5 × 5 trefoil grid named in the acceptance criteria. The diagram follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

The cyclic shift of a torus link grid

The diagram

def TauCeti.GridDiagram.torusLink (p q : ℕ) : GridDiagram (p + 1 + (q + 1))

The standard grid diagram of the (p + 1, q + 1) torus link, of grid number (p + 1) + (q + 1).

The O markings occupy the diagonal squares and the X markings the diagonal shifted up by q + 1 rows. Following the markings alternately horizontally and vertically traverses staircases that wind q + 1 times around the torus in one direction and p + 1 times in the other.

@[simp]

theorem TauCeti.GridDiagram.torusLink_O_toPerm (p q : ℕ) : (torusLink p q).O.toPerm = 1

The O markings of a standard torus link grid are the identity permutation graph.

@[simp]

theorem TauCeti.GridDiagram.torusLink_X_toPerm (p q : ℕ) : (torusLink p q).X.toPerm = finRotate (p + 1 + (q + 1)) ^ (q + 1)

The X markings of a standard torus link grid are the (q + 1)-st power of the cyclic shift permutation graph.

theorem TauCeti.GridDiagram.torusLink_O_apply (p q : ℕ) (c : Fin (p + 1 + (q + 1))) : (torusLink p q).O.toPerm c = c

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

theorem TauCeti.GridDiagram.torusLink_X_apply (p q : ℕ) (c : Fin (p + 1 + (q + 1))) : (torusLink p q).X.toPerm c = (finRotate (p + 1 + (q + 1)) ^ (q + 1)) c

The X marking of a standard torus link grid in a column is q + 1 rows above the diagonal.

theorem TauCeti.GridDiagram.torusLink_X_val (p q : ℕ) (c : Fin (p + 1 + (q + 1))) : ↑((torusLink p q).X.toPerm c) = (↑c + (q + 1)) % (p + 1 + (q + 1))

The row of the X-marking of a torus link grid in a column c, as a natural number: the column index shifted by q + 1 modulo the grid number.

theorem TauCeti.GridDiagram.torusLink_X_val_of_le (p q : ℕ) {c : Fin (p + 1 + (q + 1))} (hc : ↑c ≤ p) : ↑((torusLink p q).X.toPerm c) = ↑c + (q + 1)

In the first p + 1 columns of a torus link grid the X-marking sits q + 1 rows above the diagonal.

theorem TauCeti.GridDiagram.torusLink_X_val_of_lt (p q : ℕ) {c : Fin (p + 1 + (q + 1))} (hc : p < ↑c) : ↑((torusLink p q).X.toPerm c) = ↑c - (p + 1)

In the last q + 1 columns of a torus link grid the X-marking sits p + 1 rows below the diagonal.

theorem TauCeti.GridDiagram.torusLink_zero_right (p : ℕ) : torusLink p 0 = unknot p

With q = 0 the standard torus link grid is the standard unknot grid: the (p + 1, 1) torus link is the unknot.

theorem TauCeti.GridDiagram.relabelRows_relabelColumns_torusLink (p q : ℕ) : relabelColumns (finRotate (p + 1 + (q + 1))) (relabelRows (finRotate (p + 1 + (q + 1))) (torusLink p q)) = torusLink p q

A standard torus link grid is invariant under shifting all rows and all columns by one at the same time: the shift commutes with its own power.

theorem TauCeti.GridDiagram.transpose_torusLink (p q : ℕ) : (torusLink p q).transpose = cast ⋯ (torusLink q p)

The diagonal reflection of the standard (p + 1, q + 1) torus link grid is the standard (q + 1, p + 1) torus link grid, transported to the same grid number: the inverse of the shift by q + 1 is the shift by p + 1 on a grid of size (p + 1) + (q + 1).

The represented link and its components

theorem TauCeti.GridDiagram.componentPerm_torusLink (p q : ℕ) : (torusLink p q).componentPerm = (finRotate (p + 1 + (q + 1)) ^ (q + 1))⁻¹

Traversing a standard torus link 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 q + 1.

theorem TauCeti.GridDiagram.componentCycleType_torusLink (p q : ℕ) : (torusLink p q).componentCycleType = Multiset.replicate ((p + 1).gcd (q + 1)) ((p + 1 + (q + 1)) / (p + 1).gcd (q + 1))

The components of a standard torus link grid all carry the same number of markings, and there are gcd (p + 1) (q + 1) of them: exactly the number of components of the (p + 1, q + 1) torus link.

theorem TauCeti.GridDiagram.componentCount_torusLink (p q : ℕ) : (torusLink p q).componentCount = (p + 1).gcd (q + 1)

A standard torus link grid represents a link with gcd (p + 1) (q + 1) components.

theorem TauCeti.GridDiagram.isKnot_torusLink_iff (p q : ℕ) : (torusLink p q).IsKnot ↔ (p + 1).Coprime (q + 1)

A standard torus link grid represents a knot exactly when its two winding numbers are coprime.

The smallest members

theorem TauCeti.GridDiagram.isKnot_torusLink_one_two : (torusLink 1 2).IsKnot

The 5 × 5 grid diagram torusLink 1 2 of the (2, 3) torus knot, the trefoil, represents a knot.

theorem TauCeti.GridDiagram.componentCount_torusLink_one_one : (torusLink 1 1).componentCount = 2

The 4 × 4 grid diagram torusLink 1 1 of the (2, 2) torus link, the Hopf link, represents a two-component link.

theorem TauCeti.GridDiagram.not_isKnot_torusLink_one_one : ¬(torusLink 1 1).IsKnot

The 4 × 4 Hopf link grid does not represent a knot, so the family really does produce links of more than one component.

theorem TauCeti.GridDiagram.componentCycleType_torusLink_two_two : (torusLink 2 2).componentCycleType = {2, 2, 2}

The 6 × 6 grid diagram torusLink 2 2 of the (3, 3) torus link has three components, each carrying two of its six markings.