Grid diagram commutation moves

This file starts the commutation-move API for grid diagrams. The total row and column swap operations used as underlying relabelings live in TauCeti.KnotTheory.Grid.Diagram.Basic, next to the general row and column relabeling API. Here we add the move-specific hypothesis: two rows or columns are commutable when their marking segments do not interleave around the torus.

For columns, the vertical segment in column c has endpoints G.O c and G.X c, and two columns are non-interleaving when each pair of endpoints lies on one side of the other column's endpoint pair. The row version is the same definition after reading, in each row, the unique columns containing the O and X markings.

The predicates are intentionally just the combinatorial hypotheses. The pentagon-counting maps and chain homotopies for commutation invariance are later Lane G.5 targets.

Main definitions

• TauCeti.GridDiagram.columnArc: the open cyclic interval between the two markings in a column.
• TauCeti.GridDiagram.rowArc: the open cyclic interval between the two markings in a row.
• TauCeti.GridDiagram.ColumnsNoninterleaving: the hypothesis for a column commutation.
• TauCeti.GridDiagram.RowsNoninterleaving: the hypothesis for a row commutation.

Main results

• TauCeti.GridDiagram.columnsNoninterleaving_comm and TauCeti.GridDiagram.rowsNoninterleaving_comm: non-interleaving is symmetric in the two rows or columns.
• TauCeti.GridDiagram.rowsNoninterleaving_transpose and TauCeti.GridDiagram.columnsNoninterleaving_transpose: diagonal reflection exchanges row and column non-interleaving.
• TauCeti.GridDiagram.columnsNoninterleaving_of_X_eq_finRotate_O and TauCeti.GridDiagram.rowsNoninterleaving_of_X_eq_finRotate_O: a column (or row) whose two markings are adjacent, with the X-marking cyclically after the O-marking, is non-interleaving with every column (or row).
• TauCeti.GridDiagram.rowsNoninterleaving_of_apply: row non-interleaving read off the columns of the markings in the two rows.

References

This supplies a prerequisite for TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.5, "Invariance over 𝔽₂. Grid moves = commutation + (de)stabilization." It isolates the non-interleaving condition for row and column commutations in the grid homology construction of Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

noncomputable def TauCeti.GridDiagram.columnArc {n : ℕ} (G : GridDiagram n) (c : Fin n) : Finset (Fin n)

The open vertical arc from the O marking to the X marking in a column of a grid diagram.

This is the one-dimensional cyclic interval in the row coordinate. Its opposite arc is obtained by swapping the two markings, not by changing the column.

@[simp]

theorem TauCeti.GridDiagram.mem_columnArc {n : ℕ} (G : GridDiagram n) (c r : Fin n) : r ∈ G.columnArc c ↔ r ∈ Grid.cIoo (G.O.toPerm c) (G.X.toPerm c)

Membership in a column arc is membership in the open cyclic interval from that column's O row to its X row.

theorem TauCeti.GridDiagram.O_notMem_columnArc {n : ℕ} (G : GridDiagram n) (c : Fin n) : G.O.toPerm c ∉ G.columnArc c

The O endpoint of a column is not in its own open column arc.

theorem TauCeti.GridDiagram.X_notMem_columnArc {n : ℕ} (G : GridDiagram n) (c : Fin n) : G.X.toPerm c ∉ G.columnArc c

The X endpoint of a column is not in its own open column arc.

noncomputable def TauCeti.GridDiagram.rowArc {n : ℕ} (G : GridDiagram n) (r : Fin n) : Finset (Fin n)

The open horizontal arc from the O marking to the X marking in a row of a grid diagram.

This is the column-coordinate version of columnArc: it starts at the unique column containing the row's O marking and ends at the unique column containing the row's X marking.

@[simp]

theorem TauCeti.GridDiagram.mem_rowArc {n : ℕ} (G : GridDiagram n) (r c : Fin n) : c ∈ G.rowArc r ↔ c ∈ Grid.cIoo (G.O.transpose.toPerm r) (G.X.transpose.toPerm r)

Membership in a row arc is membership in the open cyclic interval from that row's O column to its X column.

theorem TauCeti.GridDiagram.OColumn_notMem_rowArc {n : ℕ} (G : GridDiagram n) (r : Fin n) : G.O.transpose.toPerm r ∉ G.rowArc r

The O endpoint of a row is not in its own open row arc.

theorem TauCeti.GridDiagram.XColumn_notMem_rowArc {n : ℕ} (G : GridDiagram n) (r : Fin n) : G.X.transpose.toPerm r ∉ G.rowArc r

The X endpoint of a row is not in its own open row arc.

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

Two columns of a grid diagram have non-interleaving marking segments.

The condition is phrased in both directions: the two endpoints in column a lie on the same side of the endpoint pair in column b, and conversely. This symmetric form is robust in degenerate row-sharing cases, where one endpoint of a segment may have the same row coordinate as an endpoint of the other segment.

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

Two rows of a grid diagram have non-interleaving marking segments.

theorem TauCeti.GridDiagram.columnsNoninterleaving_iff {n : ℕ} (G : GridDiagram n) (a b : Fin n) : G.ColumnsNoninterleaving a b ↔ (G.O.toPerm a ∈ G.columnArc b ↔ G.X.toPerm a ∈ G.columnArc b) ∧ (G.O.toPerm b ∈ G.columnArc a ↔ G.X.toPerm b ∈ G.columnArc a)

The defining endpoint-side conditions for column non-interleaving.

theorem TauCeti.GridDiagram.rowsNoninterleaving_iff {n : ℕ} (G : GridDiagram n) (a b : Fin n) : G.RowsNoninterleaving a b ↔ (G.O.transpose.toPerm a ∈ G.rowArc b ↔ G.X.transpose.toPerm a ∈ G.rowArc b) ∧ (G.O.transpose.toPerm b ∈ G.rowArc a ↔ G.X.transpose.toPerm b ∈ G.rowArc a)

The defining endpoint-side conditions for row non-interleaving.

@[simp]

theorem TauCeti.GridDiagram.columnsNoninterleaving_self {n : ℕ} (G : GridDiagram n) (a : Fin n) : G.ColumnsNoninterleaving a a

A column is non-interleaving with itself.

@[simp]

theorem TauCeti.GridDiagram.rowsNoninterleaving_self {n : ℕ} (G : GridDiagram n) (a : Fin n) : G.RowsNoninterleaving a a

A row is non-interleaving with itself.

theorem TauCeti.GridDiagram.columnsNoninterleaving_of_X_eq_finRotate_O {n : ℕ} (G : GridDiagram n) {a : Fin n} (h : G.X.toPerm a = (finRotate n) (G.O.toPerm a)) (b : Fin n) : G.ColumnsNoninterleaving a b

A column whose X-marking lies directly above its O-marking is non-interleaving with every column.

theorem TauCeti.GridDiagram.rowsNoninterleaving_of_X_eq_finRotate_O {n : ℕ} (G : GridDiagram n) {a : Fin n} (h : G.X.transpose.toPerm a = (finRotate n) (G.O.transpose.toPerm a)) (b : Fin n) : G.RowsNoninterleaving a b

A row whose X-marking lies directly right of its O-marking is non-interleaving with every row.

theorem TauCeti.GridDiagram.rowsNoninterleaving_of_apply {n : ℕ} {G : GridDiagram n} {a b c d c' d' : Fin n} (hc : G.O.toPerm c = a) (hd : G.X.toPerm d = a) (hc' : G.O.toPerm c' = b) (hd' : G.X.toPerm d' = b) (h : Grid.Noninterleaving c d c' d') : G.RowsNoninterleaving a b

Two rows do not interleave when the columns of their markings, c and d for the first and c' and d' for the second, do not interleave.

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

Column non-interleaving is symmetric in the two columns.

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

Row non-interleaving is symmetric in the two rows.

@[simp]

theorem TauCeti.GridDiagram.rowArc_transpose {n : ℕ} (G : GridDiagram n) (c : Fin n) : G.transpose.rowArc c = G.columnArc c

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

@[simp]

theorem TauCeti.GridDiagram.columnArc_transpose {n : ℕ} (G : GridDiagram n) (r : Fin n) : G.transpose.columnArc r = G.rowArc r

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

@[simp]

theorem TauCeti.GridDiagram.rowsNoninterleaving_transpose {n : ℕ} (G : GridDiagram n) (a b : Fin n) : G.transpose.RowsNoninterleaving a b ↔ G.ColumnsNoninterleaving a b

Diagonal reflection exchanges row non-interleaving with column non-interleaving.

@[simp]

theorem TauCeti.GridDiagram.columnsNoninterleaving_transpose {n : ℕ} (G : GridDiagram n) (a b : Fin n) : G.transpose.ColumnsNoninterleaving a b ↔ G.RowsNoninterleaving a b

Diagonal reflection exchanges column non-interleaving with row non-interleaving.