A filtration level for the X-stabilization

Let G' = G.stabilizeX s.castSucc (G.X s).castSucc s be the stabilization of a grid diagram G splitting the X-marking of column s, with new O-marking O_new = (κ, ρ) for κ = s.castSucc and ρ = (G.X s).castSucc. Call the squares off the row ρ and off the column κ the outer squares of the stabilization. This file attaches to every grid state y of G' a rational level that measures, across any rectangle carrying no O-marking, the number of outer squares the rectangle covers: the level of the source minus the level of the target is that number (GridDiagram.stabilizeXLevel_sub_stabilizeXLevel).

The level is the pairing (GridState.JWeight) of y against the integer weight on squares that is 1 on the outer squares, is lowered by n on the O-markings of G' and raised by n on O_new. Every row and every column of that weight sums to zero, because each row and column of G' carries exactly one O-marking and the outer squares fill n squares of every row but ρ and every column but κ. So GridRectangleBetween.JWeight_sub_JWeight_eq_sum computes the change of the level across a rectangle as the covered weight, which on rectangles avoiding the O-markings is the number of covered outer squares.

A rectangle covering no outer square lies in the cross formed by row ρ and column κ, so it is a single row or a single column of squares (GridDiagram.coveredRows_eq_or_coveredColumns_eq_of_disjoint_stabilizeXOuterSquares).

Main definitions

• TauCeti.GridDiagram.stabilizeXOuterSquares: the squares off the row and the column of O_new.
• TauCeti.GridDiagram.stabilizeXWeight: the balanced weight on squares.
• TauCeti.GridDiagram.stabilizeXLevel: the level of a grid state of the stabilization.
• TauCeti.GridDiagram.stabilizeXRowSwapRectangle: the thin rectangle in the row ρ from a state to the state with the row ρ and the following row swapped.

Main results

• TauCeti.GridDiagram.stabilizeXLevel_sub_stabilizeXLevel: across a rectangle avoiding the O-markings the level drops by the number of covered outer squares.
• TauCeti.GridDiagram.stabilizeXLevel_lt_or_disjoint: across such a rectangle the level strictly drops unless the rectangle covers no outer square.
• TauCeti.GridDiagram.coveredRows_eq_or_coveredColumns_eq_of_disjoint_stabilizeXOuterSquares: a rectangle covering no outer square covers the single row ρ or the single column κ.
• TauCeti.GridDiagram.coveredRows_stabilizeXRowSwapRectangle: the row swap rectangle covers only the row ρ.
• TauCeti.GridDiagram.isEmpty_stabilizeXRowSwapRectangle: the row swap rectangle is empty.
• TauCeti.GridDiagram.stabilizeXLevel_swapRows: the level is unchanged by swapping the row ρ with the following row.

References

This is the filtration of Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Geom. Topol. 11 (2007), Section 3.2 (the Q-filtration in the proof of stabilization invariance), and of Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.2, specialised to the fully blocked comparison of TauCeti.KnotTheory.Grid.Stabilization.Reduction.

def TauCeti.GridDiagram.stabilizeXOuterSquares {n : ℕ} (G : GridDiagram n) (s : Fin n) : Finset (Fin (n + 1) × Fin (n + 1))

The outer squares of the stabilization splitting the X-marking of column s: the squares off the row and off the column of its new O-marking (s.castSucc, (G.X s).castSucc).

@[simp]

theorem TauCeti.GridDiagram.mem_stabilizeXOuterSquares {n : ℕ} (G : GridDiagram n) (s : Fin n) (q : Fin (n + 1) × Fin (n + 1)) : q ∈ G.stabilizeXOuterSquares s ↔ q.1 ≠ s.castSucc ∧ q.2 ≠ (G.X.toPerm s).castSucc

def TauCeti.GridDiagram.stabilizeXWeight {n : ℕ} (G : GridDiagram n) (s : Fin n) (q : Fin (n + 1) × Fin (n + 1)) : ℤ

The balanced weight on the squares of the stabilization: 1 on the outer squares, lowered by n on the O-markings of the stabilization and raised by n on its new O-marking.

theorem TauCeti.GridDiagram.stabilizeXWeight_def {n : ℕ} (G : GridDiagram n) (s : Fin n) (q : Fin (n + 1) × Fin (n + 1)) : G.stabilizeXWeight s q = ((if q ∈ G.stabilizeXOuterSquares s then 1 else 0) - ↑n * if q ∈ (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).OSet then 1 else 0) + ↑n * if q = (s.castSucc, (G.X.toPerm s).castSucc) then 1 else 0

The balanced weight as its three contributions on each square.

theorem TauCeti.GridDiagram.sum_stabilizeXWeight_column {n : ℕ} (G : GridDiagram n) (s : Fin n) (c : Fin (n + 1)) : ∑ r : Fin (n + 1), G.stabilizeXWeight s (c, r) = 0

Every column of the balanced weight sums to zero.

theorem TauCeti.GridDiagram.sum_stabilizeXWeight_row {n : ℕ} (G : GridDiagram n) (s : Fin n) (r : Fin (n + 1)) : ∑ c : Fin (n + 1), G.stabilizeXWeight s (c, r) = 0

Every row of the balanced weight sums to zero.

noncomputable def TauCeti.GridDiagram.stabilizeXLevel {n : ℕ} (G : GridDiagram n) (s : Fin n) (y : GridState (n + 1)) : ℚ

The level of a grid state of the stabilization: its pairing against the balanced weight.

theorem TauCeti.GridDiagram.stabilizeXLevel_def {n : ℕ} (G : GridDiagram n) (s : Fin n) (y : GridState (n + 1)) : G.stabilizeXLevel s y = GridState.JWeight (G.stabilizeXWeight s) y

The stabilization level is the weighted pairing of the state.

theorem TauCeti.GridDiagram.stabilizeXLevel_sub_stabilizeXLevel {n : ℕ} (G : GridDiagram n) (s : Fin n) {y z : GridState (n + 1)} (R : GridRectangleBetween y z) (hO : Disjoint R.toGridRectangle.coveredSquares (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).OSet) : G.stabilizeXLevel s y - G.stabilizeXLevel s z = ↑(R.toGridRectangle.coveredSquares ∩ G.stabilizeXOuterSquares s).card

The level counts outer squares. Across a rectangle of the stabilization covering no O-marking, the level of the source minus the level of the target is the number of outer squares the rectangle covers.

theorem TauCeti.GridDiagram.stabilizeXLevel_lt_or_disjoint {n : ℕ} (G : GridDiagram n) (s : Fin n) {y z : GridState (n + 1)} (R : GridRectangleBetween y z) (hO : Disjoint R.toGridRectangle.coveredSquares (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).OSet) : G.stabilizeXLevel s z < G.stabilizeXLevel s y ∨ Disjoint R.toGridRectangle.coveredSquares (G.stabilizeXOuterSquares s)

The level drops across rectangles covering outer squares. Across a rectangle of the stabilization covering no O-marking, the level strictly drops, unless the rectangle covers no outer square.

theorem TauCeti.GridDiagram.stabilizeXLevel_eq_of_disjoint {n : ℕ} (G : GridDiagram n) (s : Fin n) {y z : GridState (n + 1)} (R : GridRectangleBetween y z) (h : Disjoint R.toGridRectangle.coveredSquares (G.stabilizeXOuterSquares s)) : G.stabilizeXLevel s y = G.stabilizeXLevel s z

Across a rectangle all of whose covered squares lie in the row or the column of the new O-marking, the level does not change: the balanced weight vanishes on that cross.

theorem TauCeti.GridDiagram.coveredRows_eq_or_coveredColumns_eq_of_disjoint_stabilizeXOuterSquares {n : ℕ} (G : GridDiagram n) (s : Fin n) {y z : GridState (n + 1)} (R : GridRectangleBetween y z) (h : Disjoint R.toGridRectangle.coveredSquares (G.stabilizeXOuterSquares s)) : R.toGridRectangle.coveredRows = {(G.X.toPerm s).castSucc} ∨ R.toGridRectangle.coveredColumns = {s.castSucc}

Rectangles covering no outer square. A rectangle of the stabilization that covers no outer square covers only the row (G.X s).castSucc of the new O-marking, or only its column s.castSucc.

The row swap rectangle

def TauCeti.GridDiagram.stabilizeXRowSwapRectangle {n : ℕ} (G : GridDiagram n) (s : Fin n) (y : GridState (n + 1)) : GridRectangleBetween y (GridState.swapRows (G.X.toPerm s).castSucc (G.X.toPerm s).succ y)

The row swap rectangle of a state of the stabilization: the thin rectangle in the row (G.X s).castSucc from the state to the state with the two stabilization rows (G.X s).castSucc and (G.X s).succ swapped. Its sides are the columns where the state uses these two rows.

theorem TauCeti.GridDiagram.stabilizeXRowSwapRectangle_left {n : ℕ} (G : GridDiagram n) (s : Fin n) (y : GridState (n + 1)) : (G.stabilizeXRowSwapRectangle s y).left = y.transpose.toPerm (G.X.toPerm s).castSucc

The initial side of the row swap rectangle is the column using the row (G.X s).castSucc.

theorem TauCeti.GridDiagram.stabilizeXRowSwapRectangle_right {n : ℕ} (G : GridDiagram n) (s : Fin n) (y : GridState (n + 1)) : (G.stabilizeXRowSwapRectangle s y).right = y.transpose.toPerm (G.X.toPerm s).succ

The terminal side of the row swap rectangle is the column using the row (G.X s).succ.

theorem TauCeti.GridDiagram.stabilizeXRowSwapRectangle_bottom {n : ℕ} (G : GridDiagram n) (s : Fin n) (y : GridState (n + 1)) : (G.stabilizeXRowSwapRectangle s y).bottom = (G.X.toPerm s).castSucc

The bottom row of the row swap rectangle is (G.X s).castSucc.

theorem TauCeti.GridDiagram.stabilizeXRowSwapRectangle_top {n : ℕ} (G : GridDiagram n) (s : Fin n) (y : GridState (n + 1)) : (G.stabilizeXRowSwapRectangle s y).top = (G.X.toPerm s).succ

The top row of the row swap rectangle is (G.X s).succ.

theorem TauCeti.GridDiagram.coveredRows_stabilizeXRowSwapRectangle {n : ℕ} (G : GridDiagram n) (s : Fin n) (y : GridState (n + 1)) : (G.stabilizeXRowSwapRectangle s y).toGridRectangle.coveredRows = {(G.X.toPerm s).castSucc}

The row swap rectangle covers only the row (G.X s).castSucc.

@[simp]

theorem TauCeti.GridDiagram.isEmpty_stabilizeXRowSwapRectangle {n : ℕ} (G : GridDiagram n) (s : Fin n) (y : GridState (n + 1)) : (G.stabilizeXRowSwapRectangle s y).IsEmpty

The row swap rectangle is empty: its two rows are cyclically consecutive.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXLevel_swapRows {n : ℕ} (G : GridDiagram n) (s : Fin n) (y : GridState (n + 1)) : G.stabilizeXLevel s (GridState.swapRows (G.X.toPerm s).castSucc (G.X.toPerm s).succ y) = G.stabilizeXLevel s y

The stabilization level is unchanged by swapping the two stabilization rows. The swap is realized by the row swap rectangle, which covers only the row of the new O-marking and hence no outer square.