Reducing grid stabilizations to two corner types

An elementary stabilization (GridDiagram.IsStabilization) splits an O- or an X-marking of a grid diagram G across a new 2 × 2 block, and the new row and column may sit on either side of the split marking, giving eight stabilization types. This file shows that, up to the moves that keep the size of a diagram, only two of them matter: every stabilization of G is connected by cyclic permutations and commutations to one of

• G.stabilizeX s.castSucc (G.X s).castSucc s, whose new O-marking is the south-west corner of the new block, with the two X-markings to its north and east, and
• G.stabilizeX s.succ (G.X s).succ s, whose new O-marking is the north-east corner of the new block, with the two X-markings to its south and west,

for some column s of G (GridDiagram.IsStabilization.exists_commutationMovesTo). The first of these is the stabilization whose invariance for GH⁻ is proved in TauCeti.KnotTheory.Grid.Stabilization.Homology. Consequently a function on grid diagrams that is invariant under cyclic permutations, commutations and these two stabilizations is invariant under every stabilization (GridDiagram.IsStabilization.apply_eq_apply), which is the hypothesis of GridLink.lift.

The reduction has three steps.

• A cyclic permutation of the rows or columns of the stabilized diagram moves a new row or column that wraps around the torus next to the split marking.
• With the new column just before the split column, the new row together with its two markings is a short horizontal segment that commutes with every row (GridDiagram.rowsNoninterleaving_of_X_eq_finRotate_O), so it can be slid to any height (GridDiagram.commutationMovesTo_stabilizeX_castSucc). A column commutation exchanges the two columns of the new block when one of them is a short vertical segment.
• With the new column just after the split column, the new row is a short segment with its markings in the opposite order. It still commutes with every row that has no marking in the two columns of the new block, so it slides between the rows of the two markings of the split column (GridDiagram.isRowCommutation_stabilizeX_succ). Sliding it from the X-marking up to the O-marking turns the north-east X-stabilization into an O-stabilization (GridDiagram.commutationMovesTo_stabilizeO_castSucc_stabilizeX_succ).

Every O-stabilization with the new column next to the split column is an X-stabilization with the new column on the other side (GridDiagram.stabilizeO_castSucc_eq_stabilizeX_succ, GridDiagram.stabilizeO_succ_eq_stabilizeX_castSucc), so these slides cover all eight types. The two corner types are not identified with each other here.

Main definitions

• TauCeti.GridDiagram.CommutationMovesTo: the equivalence relation on grid diagrams of one size generated by cyclic permutations and commutations.

Main results

• TauCeti.GridDiagram.IsStabilization.exists_commutationMovesTo: every stabilization is related by cyclic permutations and commutations to one of the two corner stabilizations above.
• TauCeti.GridDiagram.IsStabilization.apply_eq_apply: invariance under cyclic permutations, commutations and the two corner stabilizations implies invariance under every stabilization.

References

The grid moves and the eight stabilization types are those of Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3. Stabilization invariance of grid homology is Chapter 5 of the same book.

Moves that keep the size

def TauCeti.GridDiagram.CommutationMovesTo {n : ℕ} (G G' : GridDiagram n) : Prop

Two grid diagrams of the same size are connected by cyclic permutations of the rows or columns and by commutations, the grid moves that do not change the size of a diagram.

theorem TauCeti.GridDiagram.commutationMovesTo_def {n : ℕ} (G G' : GridDiagram n) : G.CommutationMovesTo G' ↔ Relation.EqvGen (fun (H H' : GridDiagram n) => H' = relabelRows (finRotate n) H ∨ H' = relabelColumns (finRotate n) H ∨ H.IsCommutation H') G G'

CommutationMovesTo is the equivalence relation generated by cyclic permutations of the rows, cyclic permutations of the columns, and commutations.

theorem TauCeti.GridDiagram.CommutationMovesTo.induction_on {n : ℕ} {G G' : GridDiagram n} {motive : GridDiagram n → GridDiagram n → Prop} (h : G.CommutationMovesTo G') (rows : ∀ (H : GridDiagram n), motive H (relabelRows (finRotate n) H)) (columns : ∀ (H : GridDiagram n), motive H (relabelColumns (finRotate n) H)) (comm : ∀ {H H' : GridDiagram n}, H.IsCommutation H' → motive H H') (refl : ∀ (H : GridDiagram n), motive H H) (symm : ∀ {H H' : GridDiagram n}, H.CommutationMovesTo H' → motive H H' → motive H' H) (trans : ∀ {H H' H'' : GridDiagram n}, H.CommutationMovesTo H' → H'.CommutationMovesTo H'' → motive H H' → motive H' H'' → motive H H'') : motive G G'

Induction principle for CommutationMovesTo: a relation that contains cyclic permutations of the rows and of the columns and commutations, and is reflexive, symmetric and transitive along connected diagrams, holds between any two connected diagrams.

theorem TauCeti.GridDiagram.CommutationMovesTo.refl {n : ℕ} (G : GridDiagram n) : G.CommutationMovesTo G

Every grid diagram is connected to itself.

theorem TauCeti.GridDiagram.CommutationMovesTo.symm {n : ℕ} {G G' : GridDiagram n} (h : G.CommutationMovesTo G') : G'.CommutationMovesTo G

Size-preserving grid moves can be traversed in reverse.

theorem TauCeti.GridDiagram.CommutationMovesTo.trans {n : ℕ} {G G' G'' : GridDiagram n} (h : G.CommutationMovesTo G') (h' : G'.CommutationMovesTo G'') : G.CommutationMovesTo G''

Sequences of size-preserving grid moves compose.

theorem TauCeti.GridDiagram.CommutationMovesTo.movesTo {n : ℕ} {G G' : GridDiagram n} (h : G.CommutationMovesTo G') : G.MovesTo G'

Size-preserving grid moves are grid moves.

theorem TauCeti.GridDiagram.CommutationMovesTo.apply_eq {n : ℕ} {G G' : GridDiagram n} {α : Sort u_1} (f : GridDiagram n → α) (hrows : ∀ (H : GridDiagram n), f H = f (relabelRows (finRotate n) H)) (hcolumns : ∀ (H : GridDiagram n), f H = f (relabelColumns (finRotate n) H)) (hcomm : ∀ {H H' : GridDiagram n}, H.IsCommutation H' → f H = f H') (h : G.CommutationMovesTo G') : f G = f G'

A function on grid diagrams of one size that is invariant under cyclic permutations and commutations takes the same value on diagrams connected by these moves.

theorem TauCeti.GridDiagram.IsCommutation.commutationMovesTo {n : ℕ} {G G' : GridDiagram n} (h : G.IsCommutation G') : G.CommutationMovesTo G'

An elementary commutation connects two diagrams of the same size.

theorem TauCeti.GridDiagram.IsRowCommutation.commutationMovesTo {n : ℕ} {G G' : GridDiagram n} (h : G.IsRowCommutation G') : G.CommutationMovesTo G'

An elementary row commutation connects two diagrams of the same size.

theorem TauCeti.GridDiagram.IsColumnCommutation.commutationMovesTo {n : ℕ} {G G' : GridDiagram n} (h : G.IsColumnCommutation G') : G.CommutationMovesTo G'

An elementary column commutation connects two diagrams of the same size.

theorem TauCeti.GridDiagram.commutationMovesTo_relabelRows_finRotate {n : ℕ} (G : GridDiagram n) : G.CommutationMovesTo (relabelRows (finRotate n) G)

A cyclic permutation of the rows connects two diagrams of the same size.

theorem TauCeti.GridDiagram.commutationMovesTo_relabelColumns_finRotate {n : ℕ} (G : GridDiagram n) : G.CommutationMovesTo (relabelColumns (finRotate n) G)

A cyclic permutation of the columns connects two diagrams of the same size.

Sliding the new row of a stabilization

theorem TauCeti.GridDiagram.isRowCommutation_stabilizeX_castSucc {n : ℕ} (G : GridDiagram n) (s k : Fin n) : (G.stabilizeX s.castSucc k.castSucc s).IsRowCommutation (G.stabilizeX s.castSucc k.succ s)

With the new column just before the split column, the new row of an X-stabilization carries its O-marking directly left of its X-marking, so it commutes with the old row above it.

theorem TauCeti.GridDiagram.isRowCommutation_stabilizeX_succ {n : ℕ} (G : GridDiagram n) (s : Fin n) {k : Fin n} (hO : G.O.toPerm s ≠ k) (hX : G.X.toPerm s ≠ k) : (G.stabilizeX s.succ k.castSucc s).IsRowCommutation (G.stabilizeX s.succ k.succ s)

With the new column just after the split column, the new row of an X-stabilization carries its O-marking directly right of its X-marking. It commutes with the old row k above it provided neither marking of the split column lies in that row.

theorem TauCeti.GridDiagram.commutationMovesTo_stabilizeX_castSucc {n : ℕ} (G : GridDiagram n) (s : Fin n) (t t' : Fin (n + 1)) : (G.stabilizeX s.castSucc t s).CommutationMovesTo (G.stabilizeX s.castSucc t' s)

With the new column just before the split column, all positions of the new row give X-stabilizations connected by row commutations.

theorem TauCeti.GridDiagram.movesTo_stabilizeX_castSucc {n : ℕ} (G : GridDiagram n) (s : Fin n) (t : Fin (n + 1)) : (G.stabilizeX s.castSucc t s).MovesTo G

An X-stabilization with the new column just before the split column moves back to the original diagram, wherever the new row is.

theorem TauCeti.GridDiagram.isColumnCommutation_stabilizeX_castSucc_X_castSucc {n : ℕ} (G : GridDiagram n) (s : Fin n) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).IsColumnCommutation (G.stabilizeX s.succ (G.X.toPerm s).castSucc s)

Exchanging the two columns of the new block of the south-west X-stabilization is a column commutation, since its new column is a short vertical segment.

theorem TauCeti.GridDiagram.isColumnCommutation_stabilizeX_castSucc_O_succ {n : ℕ} (G : GridDiagram n) (s : Fin n) : (G.stabilizeX s.castSucc (G.O.toPerm s).succ s).IsColumnCommutation (G.stabilizeX s.succ (G.O.toPerm s).succ s)

Exchanging the two columns of the new block of the X-stabilization with the new row just above the O-marking of the split column is a column commutation, since the split column becomes a short vertical segment.

theorem TauCeti.GridDiagram.commutationMovesTo_stabilizeO_castSucc_stabilizeX_succ {n : ℕ} (G : GridDiagram n) (s : Fin n) : (G.stabilizeO s.castSucc (G.O.toPerm s).castSucc s).CommutationMovesTo (G.stabilizeX s.succ (G.X.toPerm s).succ s)

Sliding a stabilization along a column. The O-stabilization of column s with its X-marking in the south-west corner of the new block is connected by row commutations, and possibly one cyclic permutation of the rows, to the X-stabilization of column s with its O-marking in the north-east corner: the new row slides from just above the X-marking of column s to just below its O-marking.

The reduction

theorem TauCeti.GridDiagram.IsXStabilization.exists_commutationMovesTo {n : ℕ} {G : GridDiagram n} {G' : GridDiagram (n + 1)} (h : G.IsXStabilization G') : ∃ (s : Fin n), G'.CommutationMovesTo (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s) ∨ G'.CommutationMovesTo (G.stabilizeX s.succ (G.X.toPerm s).succ s)

An elementary X-stabilization is connected by cyclic permutations and commutations to one of the two corner X-stabilizations of the split column.

theorem TauCeti.GridDiagram.IsOStabilization.exists_commutationMovesTo {n : ℕ} {G : GridDiagram n} {G' : GridDiagram (n + 1)} (h : G.IsOStabilization G') : ∃ (s : Fin n), G'.CommutationMovesTo (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s) ∨ G'.CommutationMovesTo (G.stabilizeX s.succ (G.X.toPerm s).succ s)

An elementary O-stabilization is connected by cyclic permutations and commutations to one of the two corner X-stabilizations of the split column.

theorem TauCeti.GridDiagram.IsStabilization.exists_commutationMovesTo {n : ℕ} {G : GridDiagram n} {G' : GridDiagram (n + 1)} (h : G.IsStabilization G') : ∃ (s : Fin n), G'.CommutationMovesTo (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s) ∨ G'.CommutationMovesTo (G.stabilizeX s.succ (G.X.toPerm s).succ s)

Every stabilization reduces to one of two corner types. If G' is an elementary stabilization of G, then for some column s of G, cyclic permutations and commutations connect G' to the X-stabilization of column s whose new O-marking is the south-west corner of the new block, or to the one whose new O-marking is its north-east corner.

theorem TauCeti.GridDiagram.IsStabilization.apply_eq_apply {n : ℕ} {α : Sort u_1} (f : (n : ℕ) → GridDiagram n → α) (hrows : ∀ {n : ℕ} (G : GridDiagram n), f n G = f n (relabelRows (finRotate n) G)) (hcolumns : ∀ {n : ℕ} (G : GridDiagram n), f n G = f n (relabelColumns (finRotate n) G)) (hcomm : ∀ {n : ℕ} {G G' : GridDiagram n}, G.IsCommutation G' → f n G = f n G') (hcastSucc : ∀ {n : ℕ} (G : GridDiagram n) (s : Fin n), f n G = f (n + 1) (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s)) (hsucc : ∀ {n : ℕ} (G : GridDiagram n) (s : Fin n), f n G = f (n + 1) (G.stabilizeX s.succ (G.X.toPerm s).succ s)) {G : GridDiagram n} {G' : GridDiagram (n + 1)} (h : G.IsStabilization G') : f n G = f (n + 1) G'

Invariance under stabilization from two corner types. A function on grid diagrams that is invariant under cyclic permutations, commutations, and the two corner X-stabilizations of GridDiagram.IsStabilization.exists_commutationMovesTo is invariant under every elementary stabilization.