Diagonal reflection of grid stabilizations

Transposition exchanges the new row and column of a stabilization and sends the split marking to its transposed position. In particular it preserves all eight elementary stabilization types, including those crossing the chosen cut of the torus. This lets transposition act on grid diagrams modulo moves.

The stabilization conventions follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

@[simp]

theorem TauCeti.GridDiagram.transpose_stabilizeO {n : ℕ} (G : GridDiagram n) (c r : Fin (n + 1)) (s : Fin n) : (G.stabilizeO c r s).transpose = G.transpose.stabilizeO r c (G.O.toPerm s)

Transposition exchanges the inserted row and column of an O-stabilization.

@[simp]

theorem TauCeti.GridDiagram.transpose_stabilizeX {n : ℕ} (G : GridDiagram n) (c r : Fin (n + 1)) (s : Fin n) : (G.stabilizeX c r s).transpose = G.transpose.stabilizeX r c (G.X.toPerm s)

Transposition exchanges the inserted row and column of an X-stabilization.

@[simp]

theorem TauCeti.GridDiagram.isOStabilization_transpose {n : ℕ} (G : GridDiagram n) (G' : GridDiagram (n + 1)) : G.transpose.IsOStabilization G'.transpose ↔ G.IsOStabilization G'

Diagonal reflection preserves elementary O-stabilizations.

@[simp]

theorem TauCeti.GridDiagram.isXStabilization_transpose {n : ℕ} (G : GridDiagram n) (G' : GridDiagram (n + 1)) : G.transpose.IsXStabilization G'.transpose ↔ G.IsXStabilization G'

Diagonal reflection preserves elementary X-stabilizations.

@[simp]

theorem TauCeti.GridDiagram.isStabilization_transpose {n : ℕ} (G : GridDiagram n) (G' : GridDiagram (n + 1)) : G.transpose.IsStabilization G'.transpose ↔ G.IsStabilization G'

Diagonal reflection preserves elementary stabilizations of either marking type.

@[simp]

theorem TauCeti.GridDiagram.isDestabilization_transpose {n : ℕ} (G : GridDiagram n) (G' : GridDiagram (n + 1)) : G'.transpose.IsDestabilization G.transpose ↔ G'.IsDestabilization G

Diagonal reflection preserves elementary destabilizations.