The gradings of the center states of an X-stabilization

Let G' = G.stabilizeX s.castSucc (G.X s).castSucc s be the stabilization of a grid diagram G of size n splitting the X-marking of column s. Its center states are the states x' = x.insertPoint s.succ (G.X s).succ obtained from the states x of G by adding the center of the new 2 × 2 block. This file computes the gradings of x' in G' from those of x in G:

M_O(x') = M_O(x) - 1, M_X(x') = M_X(x) and A(x') = A(x) - 1.

All three point sets entering these gradings arise by inserting one point: the O-marking state of G' inserts the new O-marking at (s.castSucc, (G.X s).castSucc), and its X-marking state inserts X₂ at (s.succ, (G.X s).castSucc) (GridState.splitPoint_castSucc_eq_insertPoint). With these column and row offsets, every comparison between two old points is the comparison in G, so each point-pair count in the Maslov gradings of x' (GridDiagram.maslovOℤ_eq_card) is the count for x plus the comparisons involving an inserted point. Those extra comparisons cancel, up to the constant -1 for M_O.

On off-center states the chain map GC⁻(G') ⟶ GC⁻(G) of the stabilization is the component H_I^N of the X₂-homotopy, which sends an off-center state y to the sum of the terms V^{O(r)} · x' over its rectangles r from y to center states x', followed by x' ↦ x and the merging of the two variables of the new block (GridDiagram.map_offCenterInclusion_comp_stabilizeXMap). Combining the grading shift with the grading change across such a rectangle (GridDiagram.alexander_sub_card_OColumns_eq_alexander_sub_one), the term V^{O(r)} · x has the O-Maslov and Alexander gradings of y (GridDiagram.maslovOℤ_stabilizeX_eq_of_isEmpty and GridDiagram.alexander_stabilizeX_eq_of_mem_XHomotopyRectangles). These are the grading facts from which the stabilization map preserves the bigrading.

Since a center state has doubled Alexander grading two below that of the state it comes from, the parity criterion GridDiagram.even_alexanderTwoℤ_iff shows that the stabilization of a diagram with an odd number of components again has an odd number of components (OddComponentGridDiagram.stabilizeX).

Main definitions

• TauCeti.OddComponentGridDiagram.stabilizeX: the stabilization splitting the X-marking of a column, as a grid diagram with an odd number of components.

Main results

• TauCeti.GridDiagram.maslovOℤ_stabilizeX_insertPoint, TauCeti.GridDiagram.maslovXℤ_stabilizeX_insertPoint, TauCeti.GridDiagram.alexanderTwoℤ_stabilizeX_insertPoint and TauCeti.GridDiagram.alexander_stabilizeX_insertPoint: the gradings of a center state.
• TauCeti.GridDiagram.maslovOℤ_stabilizeX_eq_of_isEmpty and TauCeti.GridDiagram.alexander_stabilizeX_eq_of_mem_XHomotopyRectangles: a term V^{O(r)} · x of the X-homotopy into the center states has the bigrading of its source.

References

This is the grading computation in the proof of stabilization invariance in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.2, and Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.2.

Point-pair counts of inserted states

The gradings of the center states

@[simp]

theorem TauCeti.GridDiagram.maslovOℤ_stabilizeX_insertPoint {n : ℕ} (s : Fin n) (x : GridState n) (G : GridDiagram n) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).maslovOℤ (x.insertPoint s.succ (G.X.toPerm s).succ) = G.maslovOℤ x - 1

The O-Maslov grading of a center state. Adding the center of the new block to a state of G gives a state of the stabilization one lower in the O-Maslov grading.

@[simp]

theorem TauCeti.GridDiagram.maslovXℤ_stabilizeX_insertPoint {n : ℕ} (s : Fin n) (x : GridState n) (G : GridDiagram n) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).maslovXℤ (x.insertPoint s.succ (G.X.toPerm s).succ) = G.maslovXℤ x

The X-Maslov grading of a center state. Adding the center of the new block to a state of G gives a state of the stabilization with the same X-Maslov grading.

@[simp]

theorem TauCeti.GridDiagram.alexanderTwoℤ_stabilizeX_insertPoint {n : ℕ} (s : Fin n) (x : GridState n) (G : GridDiagram n) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).alexanderTwoℤ (x.insertPoint s.succ (G.X.toPerm s).succ) = G.alexanderTwoℤ x - 2

The Alexander grading of a center state, in its doubled integer form.

@[simp]

theorem TauCeti.GridDiagram.alexander_stabilizeX_insertPoint {n : ℕ} (s : Fin n) (x : GridState n) (G : GridDiagram n) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).alexander (x.insertPoint s.succ (G.X.toPerm s).succ) = G.alexander x - 1

The Alexander grading of a center state. Adding the center of the new block to a state of G gives a state of the stabilization one lower in the Alexander grading.

The terms of the stabilization map

theorem TauCeti.GridDiagram.maslovOℤ_stabilizeX_eq_of_isEmpty {n : ℕ} (s : Fin n) (x : GridState n) (G : GridDiagram n) {y : GridState (n + 1)} {r : GridRectangleBetween y (x.insertPoint s.succ (G.X.toPerm s).succ)} (hr : r.IsEmpty) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).maslovOℤ y = G.maslovOℤ x - 2 * ↑((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).OColumns r.toGridRectangle).card

An empty rectangle of the stabilization from a state y to a center state x' lowers the O-Maslov grading by one once its weight V^{O(r)} is charged -2 per variable, and x' lies one below x: so the term V^{O(r)} · x has the O-Maslov grading of y.

theorem TauCeti.GridDiagram.alexander_stabilizeX_eq_of_mem_XHomotopyRectangles {n : ℕ} (s : Fin n) (x : GridState n) (G : GridDiagram n) {k : Fin (n + 1)} {y : GridState (n + 1)} {r : GridRectangleBetween y (x.insertPoint s.succ (G.X.toPerm s).succ)} (hr : r ∈ (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).XHomotopyRectangles k y (x.insertPoint s.succ (G.X.toPerm s).succ)) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).alexander y = G.alexander x - ↑((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).OColumns r.toGridRectangle).card

A rectangle of an X-marking homotopy of the stabilization from a state y to a center state x' lowers the Alexander grading by one once its weight V^{O(r)} is charged -1 per variable, and x' lies one below x: so the term V^{O(r)} · x has the Alexander grading of y.

def TauCeti.OddComponentGridDiagram.stabilizeX {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) : OddComponentGridDiagram (n + 1)

The stabilization of a grid diagram with an odd number of components that splits the X-marking of column s, as a grid diagram with an odd number of components. A center state has doubled Alexander grading two below that of the state it comes from, so the parity of the number of components, which is that of the doubled Alexander grading of any state, is unchanged.

@[simp]

theorem TauCeti.OddComponentGridDiagram.val_stabilizeX {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) : ↑(G.stabilizeX s) = (↑G).stabilizeX s.castSucc ((↑G).X.toPerm s).castSucc s

The underlying grid diagram of G.stabilizeX s is the stabilization splitting the X-marking of column s.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bidegree_stabilizeX_insertPoint {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (x : GridState n) : (G.stabilizeX s).bidegree (x.insertPoint s.succ ((↑G).X.toPerm s).succ) = G.bidegree x - (1, 1)

Inserting the center lowers both state gradings by one.