The unblocked complex of a stabilized grid

Let G be a grid diagram of size n, let s be a column, and let G' = G.stabilizeX s.castSucc (G.X s).castSucc s be the stabilization that splits the X-marking of column s by inserting a new column immediately before s and a new row immediately below that marking. In G' the new 2 × 2 block is centred at the grid point c = (s.succ, (G.X s).succ): its two X-markings lie in the squares northwest and southeast of c, the new O-marking in the square southwest of c, and the square northeast of c is empty.

The grid states of G' split into those that contain c, denoted I, and the others, denoted N. This file proves two coefficient-level facts about the unblocked differential ∂⁻ of G'. They are the ingredients of the presentation of GC⁻(G') as the mapping cone of the component I → N of ∂⁻ in TauCeti.KnotTheory.Grid.Stabilization.Cone, with the I block identified with GC⁻(G) over one more variable; this is the form in which Ozsváth, Stipsicz and Szabó compare the stabilized complex with GC⁻(G).

• The N-to-I coefficient block vanishes. A rectangle from a state outside I to a state in I has c as a corner, so it covers one of the two X-marked squares of the block. Hence ∂⁻ has no matrix coefficient from N to I (unblockedCoefficient_stabilizeX_eq_zero).
• The I coefficient block agrees with GC⁻(G) over one more variable. Every state of I is obtained from a unique state of G by inserting c (GridState.insertPoint), and inserting c identifies the rectangles counted by ∂⁻ between states in I with those counted by ∂⁻ on GC⁻(G). The two X-markings of the block cover exactly the squares that the X-marking of column s covers in G, and a rectangle avoiding them never covers c or the new O-marking. So the matrix coefficients agree after renaming the variables of G into those of G'; the variable of the new O-marking never occurs (unblockedCoefficient_stabilizeX_insertPoint).

Main results

• TauCeti.GridDiagram.unblockedCoefficient_stabilizeX_insertPoint: the matrix coefficients of ∂⁻ between states containing c are the renamed coefficients of ∂⁻ for G.
• TauCeti.GridDiagram.unblockedCoefficient_stabilizeX_eq_zero: ∂⁻ has no matrix coefficient from a state not containing c to a state containing it.

References

These coefficient identities are part of the stabilization-invariance argument in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.2, where the complex of the stabilized diagram is identified with a mapping cone built from the complex of G.

theorem TauCeti.GridDiagram.disjoint_XSet_stabilizeX_insertPoint {n : ℕ} (G : GridDiagram n) {s : Fin n} {x y : GridState n} (R : GridRectangleBetween x y) : Disjoint (R.insertPoint s.succ (G.X.toPerm s).succ).toGridRectangle.coveredSquares (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).XSet ↔ Disjoint R.toGridRectangle.coveredSquares G.XSet

A rectangle between states containing the centre c = (s.succ, (G.X s).succ) of the new block avoids the X-markings of the stabilization exactly when the rectangle it is transported from avoids the X-markings of G.

@[simp]

theorem TauCeti.GridDiagram.OColumns_stabilizeX_insertPoint {n : ℕ} (G : GridDiagram n) {s : Fin n} {x y : GridState n} {R : GridRectangleBetween x y} (hXs : (s, G.X.toPerm s) ∉ R.toGridRectangle.coveredSquares) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).OColumns (R.insertPoint s.succ (G.X.toPerm s).succ).toGridRectangle = Finset.map s.castSucc.succAboveEmb (G.OColumns R.toGridRectangle)

If a transported rectangle avoids the split X-square, it covers the O-markings of the old columns of the stabilization that the original rectangle covers in G, and never the new O-marking.

@[simp]

theorem TauCeti.GridDiagram.OMonomial_stabilizeX_insertPoint {n : ℕ} (G : GridDiagram n) {s : Fin n} (R : Type u_1) [CommSemiring R] {x y : GridState n} {r : GridRectangleBetween x y} (hXs : (s, G.X.toPerm s) ∉ r.toGridRectangle.coveredSquares) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).OMonomial R (r.insertPoint s.succ (G.X.toPerm s).succ).toGridRectangle = (MvPolynomial.rename s.castSucc.succAbove) (G.OMonomial R r.toGridRectangle)

If a transported rectangle avoids the split X-square, its weight is the weight of the original rectangle with the variables renamed into those of the stabilization.

theorem TauCeti.GridDiagram.mem_unblockedRectangles_stabilizeX_insertPoint {n : ℕ} (G : GridDiagram n) {s : Fin n} {x y : GridState n} (r : GridRectangleBetween x y) : r.insertPoint s.succ (G.X.toPerm s).succ ∈ (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedRectangles (x.insertPoint s.succ (G.X.toPerm s).succ) (y.insertPoint s.succ (G.X.toPerm s).succ) ↔ r ∈ G.unblockedRectangles x y

Transporting along the insertion of the centre c = (s.succ, (G.X s).succ) identifies the rectangles counted by the unblocked differential of G with those counted by the unblocked differential of the stabilization between states containing c.

@[simp]

theorem TauCeti.GridDiagram.unblockedCoefficient_stabilizeX_insertPoint {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (x y : GridState n) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedCoefficient R (x.insertPoint s.succ (G.X.toPerm s).succ) (y.insertPoint s.succ (G.X.toPerm s).succ) = (MvPolynomial.rename s.castSucc.succAbove) (G.unblockedCoefficient R x y)

The I coefficient block of the stabilized complex. Between grid states containing the centre c = (s.succ, (G.X s).succ) of the new block, the matrix coefficients of the unblocked differential of the stabilization are those of G, with the variable of each column renamed to the variable of the corresponding old column. The variable of the new O-marking does not occur.

@[simp]

theorem TauCeti.GridDiagram.unblockedCoefficient_stabilizeX_eq_zero {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] {y z : GridState (n + 1)} (hy : y.toPerm s.succ ≠ (G.X.toPerm s).succ) (hz : z.toPerm s.succ = (G.X.toPerm s).succ) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedCoefficient R y z = 0

The N-to-I coefficient block vanishes. The unblocked differential of the stabilization has no matrix coefficient from a grid state not containing the centre c = (s.succ, (G.X s).succ) of the new block to one containing it: such a rectangle has c as a corner and covers one of the two X-marked squares of the block.