Cross-commutations of grid diagrams

A commutation exchanges two adjacent columns (or rows) whose marking segments do not interleave, and does not change the represented link. Exchanging two adjacent columns whose segments do interleave is a cross-commutation. Topologically, the two diagrams then present links that differ by a single crossing change, and every crossing change between two knots arises this way for suitable grid diagrams (Ozsváth--Stipsicz--Szabó, Chapter 6); these statements about embedded links are not formalised here. Grid homology reaches crossing changes through this move: the crossing change maps of Ozsváth--Stipsicz--Szabó, which bound the change of τ, are maps between the grid complexes of two diagrams related by a cross-commutation.

Two columns interleave when one marking of the first lies on the open arc of the second, from its O-marking up to its X-marking, and the other marking lies on the opposite open arc (GridDiagram.ColumnsInterleaving). The four markings then lie in four distinct rows that alternate between the two columns around the vertical circle. On a planar picture of the grid, this says that the two vertical segments overlap but neither contains the other. This is exactly the failure of the non-interleaving hypothesis of a commutation, except in the degenerate case in which an O-marking of one column shares its row with the X-marking of the other (GridDiagram.columnsInterleaving_iff_not_columnsNoninterleaving). Two segments sharing an endpoint are never interleaving.

Main definitions

• TauCeti.GridDiagram.ColumnsInterleaving, TauCeti.GridDiagram.RowsInterleaving: the marking segments of two columns, or of two rows, interleave.
• TauCeti.GridDiagram.IsColumnCrossCommutation, TauCeti.GridDiagram.IsRowCrossCommutation: two diagrams differ by exchanging two adjacent interleaving columns, or rows.
• TauCeti.GridDiagram.IsCrossCommutation: one cross-commutation of either kind.

Main results

• TauCeti.GridDiagram.columnsInterleaving_iff_not_columnsNoninterleaving: interleaving is the negation of non-interleaving, for segments with four distinct endpoints.
• TauCeti.GridDiagram.columnsInterleaving_comm: interleaving is symmetric in the two columns.
• TauCeti.GridDiagram.ColumnsInterleaving.O_mem_columnArc_iff: for interleaving segments, exactly one O-marking lies on the arc of the other column.
• TauCeti.GridDiagram.ColumnsInterleaving.O_swapColumns_mem_columnArc_iff: exchanging the two columns exchanges the two orders of the markings.
• TauCeti.GridDiagram.isCrossCommutation_comm: cross-commutations are reversible.
• TauCeti.GridDiagram.isCrossCommutation_transpose: diagonal reflection exchanges row and column cross-commutations.
• TauCeti.GridDiagram.IsCrossCommutation.componentCount_eq, TauCeti.GridDiagram.IsCrossCommutation.isKnot_iff: a cross-commutation preserves the number of components, as a crossing change must.

References

• P. Ozsváth, A. Stipsicz, Z. Szabó, Grid Homology for Knots and Links, AMS Mathematical Surveys and Monographs 208, 2015, Chapter 6: crossing changes realised by cross-commutations, and the crossing change maps.
• M. Kendall, Crossing change maps in filtered grid homology, arXiv:2303.04227, Definition 2.2: the cross-commutation move.

def TauCeti.GridDiagram.ColumnsInterleaving {n : ℕ} (G : GridDiagram n) (a b : Fin n) : Prop

The marking segments of columns a and b interleave: one marking of column a lies on the open arc of column b, from its O-marking up to its X-marking, and the other lies on the opposite open arc. The four markings then lie in four distinct rows which alternate between the two columns around the vertical circle.

def TauCeti.GridDiagram.RowsInterleaving {n : ℕ} (G : GridDiagram n) (a b : Fin n) : Prop

The marking segments of rows a and b interleave: one marking of row a lies on the open arc of row b, from the column of its O-marking to the column of its X-marking, and the other lies on the opposite open arc.

theorem TauCeti.GridDiagram.columnsInterleaving_iff {n : ℕ} (G : GridDiagram n) (a b : Fin n) : G.ColumnsInterleaving a b ↔ G.O.toPerm a ∈ G.columnArc b ∧ G.X.toPerm a ∈ Grid.cIoo (G.X.toPerm b) (G.O.toPerm b) ∨ G.O.toPerm a ∈ Grid.cIoo (G.X.toPerm b) (G.O.toPerm b) ∧ G.X.toPerm a ∈ G.columnArc b

The defining condition for interleaving columns.

theorem TauCeti.GridDiagram.rowsInterleaving_iff {n : ℕ} (G : GridDiagram n) (a b : Fin n) : G.RowsInterleaving a b ↔ G.O.transpose.toPerm a ∈ G.rowArc b ∧ G.X.transpose.toPerm a ∈ Grid.cIoo (G.X.transpose.toPerm b) (G.O.transpose.toPerm b) ∨ G.O.transpose.toPerm a ∈ Grid.cIoo (G.X.transpose.toPerm b) (G.O.transpose.toPerm b) ∧ G.X.transpose.toPerm a ∈ G.rowArc b

The defining condition for interleaving rows.

theorem TauCeti.GridDiagram.ColumnsInterleaving.ne {n : ℕ} {G : GridDiagram n} {a b : Fin n} (h : G.ColumnsInterleaving a b) : a ≠ b

A column does not interleave with itself.

theorem TauCeti.GridDiagram.ColumnsInterleaving.symm {n : ℕ} {G : GridDiagram n} {a b : Fin n} (h : G.ColumnsInterleaving a b) : G.ColumnsInterleaving b a

Interleaving of columns is symmetric.

theorem TauCeti.GridDiagram.columnsInterleaving_comm {n : ℕ} (G : GridDiagram n) (a b : Fin n) : G.ColumnsInterleaving a b ↔ G.ColumnsInterleaving b a

Interleaving of columns is symmetric in the two columns.

theorem TauCeti.GridDiagram.columnsInterleaving_iff_not_columnsNoninterleaving {n : ℕ} (G : GridDiagram n) (a b : Fin n) : G.ColumnsInterleaving a b ↔ ¬G.ColumnsNoninterleaving a b ∧ G.O.toPerm a ≠ G.X.toPerm b ∧ G.X.toPerm a ≠ G.O.toPerm b

Two columns interleave exactly when they fail to be non-interleaving and no O-marking of one shares its row with the X-marking of the other.

theorem TauCeti.GridDiagram.ColumnsInterleaving.not_columnsNoninterleaving {n : ℕ} (G : GridDiagram n) {a b : Fin n} (h : G.ColumnsInterleaving a b) : ¬G.ColumnsNoninterleaving a b

Interleaving columns are not non-interleaving, so they cannot be commuted.

@[simp]

theorem TauCeti.GridDiagram.columnsInterleaving_swapColumns {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapColumns a b G).ColumnsInterleaving a b ↔ G.ColumnsInterleaving b a

Exchanging two columns exchanges their roles in the interleaving condition.

theorem TauCeti.GridDiagram.ColumnsInterleaving.O_mem_columnArc_iff {n : ℕ} {G : GridDiagram n} {a b : Fin n} (h : G.ColumnsInterleaving a b) : G.O.toPerm b ∈ G.columnArc a ↔ G.O.toPerm a ∉ G.columnArc b

For interleaving segments in columns a and b, exactly one of the two O-markings lies on the open arc of the other column: the O-marking of b lies on the arc of a exactly when that of a does not lie on the arc of b.

theorem TauCeti.GridDiagram.ColumnsInterleaving.O_swapColumns_mem_columnArc_iff {n : ℕ} {G : GridDiagram n} {a b : Fin n} (h : G.ColumnsInterleaving a b) : (swapColumns a b G).O.toPerm a ∈ (swapColumns a b G).columnArc b ↔ G.O.toPerm a ∉ G.columnArc b

A cross-commutation exchanges the two orders of the markings of interleaving columns: after the columns a and b are exchanged, the O-marking of a lies on the arc of b exactly when it did not before.

@[simp]

theorem TauCeti.GridDiagram.columnsInterleaving_transpose {n : ℕ} (G : GridDiagram n) (a b : Fin n) : G.transpose.ColumnsInterleaving a b ↔ G.RowsInterleaving a b

Diagonal reflection turns column interleaving in the reflected diagram into row interleaving in the original diagram.

@[simp]

theorem TauCeti.GridDiagram.rowsInterleaving_transpose {n : ℕ} (G : GridDiagram n) (a b : Fin n) : G.transpose.RowsInterleaving a b ↔ G.ColumnsInterleaving a b

Diagonal reflection turns row interleaving in the reflected diagram into column interleaving in the original diagram.

theorem TauCeti.GridDiagram.rowsInterleaving_comm {n : ℕ} (G : GridDiagram n) (a b : Fin n) : G.RowsInterleaving a b ↔ G.RowsInterleaving b a

Interleaving of rows is symmetric in the two rows.

theorem TauCeti.GridDiagram.rowsInterleaving_iff_not_rowsNoninterleaving {n : ℕ} (G : GridDiagram n) (a b : Fin n) : G.RowsInterleaving a b ↔ ¬G.RowsNoninterleaving a b ∧ G.O.transpose.toPerm a ≠ G.X.transpose.toPerm b ∧ G.X.transpose.toPerm a ≠ G.O.transpose.toPerm b

Two rows interleave exactly when they fail to be non-interleaving and no O-marking of one shares its column with the X-marking of the other.

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

Two grid diagrams differ by one column cross-commutation: two cyclically adjacent columns with interleaving marking segments in the source diagram are exchanged.

theorem TauCeti.GridDiagram.isColumnCrossCommutation_iff {n : ℕ} (G G' : GridDiagram n) : G.IsColumnCrossCommutation G' ↔ ∃ (a : Fin n), G.ColumnsInterleaving a ((finRotate n) a) ∧ G' = swapColumns a ((finRotate n) a) G

Characterization of a column cross-commutation by its exchanged columns.

theorem TauCeti.GridDiagram.isColumnCrossCommutation_swapColumns {n : ℕ} (G : GridDiagram n) {a : Fin n} (h : G.ColumnsInterleaving a ((finRotate n) a)) : G.IsColumnCrossCommutation (swapColumns a ((finRotate n) a) G)

Exchanging a cyclically adjacent interleaving pair of columns is a column cross-commutation.

theorem TauCeti.GridDiagram.isColumnCrossCommutation_comm {n : ℕ} {G G' : GridDiagram n} : G.IsColumnCrossCommutation G' ↔ G'.IsColumnCrossCommutation G

A column cross-commutation is reversible.

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

Two grid diagrams differ by one row cross-commutation: two cyclically adjacent rows with interleaving marking segments in the source diagram are exchanged.

theorem TauCeti.GridDiagram.isRowCrossCommutation_iff {n : ℕ} (G G' : GridDiagram n) : G.IsRowCrossCommutation G' ↔ ∃ (a : Fin n), G.RowsInterleaving a ((finRotate n) a) ∧ G' = swapRows a ((finRotate n) a) G

Characterization of a row cross-commutation by its exchanged rows.

theorem TauCeti.GridDiagram.isRowCrossCommutation_swapRows {n : ℕ} (G : GridDiagram n) {a : Fin n} (h : G.RowsInterleaving a ((finRotate n) a)) : G.IsRowCrossCommutation (swapRows a ((finRotate n) a) G)

Exchanging a cyclically adjacent interleaving pair of rows is a row cross-commutation.

@[simp]

theorem TauCeti.GridDiagram.isColumnCrossCommutation_transpose {n : ℕ} (G G' : GridDiagram n) : G.transpose.IsColumnCrossCommutation G'.transpose ↔ G.IsRowCrossCommutation G'

Diagonal reflection turns a column cross-commutation of the reflected diagrams into a row cross-commutation of the original ones.

@[simp]

theorem TauCeti.GridDiagram.isRowCrossCommutation_transpose {n : ℕ} (G G' : GridDiagram n) : G.transpose.IsRowCrossCommutation G'.transpose ↔ G.IsColumnCrossCommutation G'

Diagonal reflection turns a row cross-commutation of the reflected diagrams into a column cross-commutation of the original ones.

theorem TauCeti.GridDiagram.isRowCrossCommutation_comm {n : ℕ} {G G' : GridDiagram n} : G.IsRowCrossCommutation G' ↔ G'.IsRowCrossCommutation G

A row cross-commutation is reversible.

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

One cross-commutation, either of rows or of columns.

theorem TauCeti.GridDiagram.isCrossCommutation_iff {n : ℕ} (G G' : GridDiagram n) : G.IsCrossCommutation G' ↔ G.IsRowCrossCommutation G' ∨ G.IsColumnCrossCommutation G'

A cross-commutation is a row cross-commutation or a column cross-commutation.

theorem TauCeti.GridDiagram.isCrossCommutation_comm {n : ℕ} {G G' : GridDiagram n} : G.IsCrossCommutation G' ↔ G'.IsCrossCommutation G

The cross-commutation relation is symmetric.

@[simp]

theorem TauCeti.GridDiagram.isCrossCommutation_transpose {n : ℕ} (G G' : GridDiagram n) : G.transpose.IsCrossCommutation G'.transpose ↔ G.IsCrossCommutation G'

Diagonal reflection preserves the cross-commutation relation, exchanging row and column cross-commutations.

theorem TauCeti.GridDiagram.IsCrossCommutation.componentCycleType_eq {n : ℕ} {G G' : GridDiagram n} (h : G.IsCrossCommutation G') : G'.componentCycleType = G.componentCycleType

A cross-commutation preserves the multiset of component sizes.

theorem TauCeti.GridDiagram.IsCrossCommutation.componentCount_eq {n : ℕ} {G G' : GridDiagram n} (h : G.IsCrossCommutation G') : G'.componentCount = G.componentCount

A cross-commutation preserves the number of components of the represented link.

theorem TauCeti.GridDiagram.IsCrossCommutation.isKnot_iff {n : ℕ} {G G' : GridDiagram n} (h : G.IsCrossCommutation G') : G'.IsKnot ↔ G.IsKnot

A cross-commutation preserves whether a grid diagram represents a knot.