Elementary grid commutation moves

This file packages row and column commutations as relations between grid diagrams. Two columns are eligible for an elementary commutation when they are cyclically adjacent, their marking segments are non-interleaving, and the target diagram is obtained by swapping them. Row commutations are defined dually.

Cyclic adjacency is represented without an extra predicate: an edge of the cyclically ordered set Fin n is the pair a, finRotate n a. Requiring these endpoints to be distinct excludes the degenerate one-column identity swap. The resulting relations are symmetric because a swap is an involution and preserves non-interleaving of the swapped pair.

Main definitions

• TauCeti.GridDiagram.IsColumnCommutation: one elementary column commutation.
• TauCeti.GridDiagram.ColumnTurn: a column, distinct from its successor, together with the square row of a turn point at which the curve replacing the grid line between them crosses it; all that the pentagon-counting maps and their chain-map property depend on.
• TauCeti.GridDiagram.ColumnCommutationData: a column commutation together with the two turn rows and the placement of the adjacent-column markings in the resulting bigons; it extends ColumnTurn.
• TauCeti.GridDiagram.ColumnTurn.withTurnRow: the turn at the same columns in another row.
• TauCeti.GridDiagram.IsRowCommutation: one elementary row commutation.
• TauCeti.GridDiagram.IsCommutation: one elementary commutation of either kind.

Main results

• TauCeti.GridDiagram.isColumnCommutation_comm and TauCeti.GridDiagram.isRowCommutation_comm: elementary moves are reversible.
• TauCeti.GridDiagram.ColumnCommutationData.reverse: the validated data for the reverse column commutation.
• TauCeti.GridDiagram.ColumnCommutationData.ofNoninterleaving, TauCeti.GridDiagram.isColumnCommutation_iff_exists_columnCommutationData: every elementary column commutation admits validated commutation data.
• TauCeti.GridDiagram.isRowCommutation_transpose and TauCeti.GridDiagram.isColumnCommutation_transpose: diagonal reflection exchanges the two kinds of commutation.
• TauCeti.GridDiagram.isCommutation_comm: the combined commutation relation is symmetric.
• TauCeti.GridDiagram.IsCommutation.apply_eq_of_transpose: invariance under the diagonal reflection and under column commutations gives invariance under all commutations.

References

This is a prerequisite for TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.5, "Invariance over 𝔽₂. Grid moves = commutation + (de)stabilization": the later pentagon-counting chain maps are attached to the elementary moves defined here. The definition follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

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

Two grid diagrams differ by one elementary column commutation.

The columns are consecutive in the cyclic order on Fin n, have non-interleaving marking segments in the source diagram, and are swapped to obtain the target diagram.

theorem TauCeti.GridDiagram.isColumnCommutation_iff {n : ℕ} (G G' : GridDiagram n) : G.IsColumnCommutation G' ↔ ∃ (a : Fin n), a ≠ (finRotate n) a ∧ G.ColumnsNoninterleaving a ((finRotate n) a) ∧ G' = swapColumns a ((finRotate n) a) G

Characterization of an elementary column commutation by its exchanged columns.

theorem TauCeti.GridDiagram.isColumnCommutation_swapColumns {n : ℕ} (G : GridDiagram n) (a : Fin n) (ha : a ≠ (finRotate n) a) (hG : G.ColumnsNoninterleaving a ((finRotate n) a)) : G.IsColumnCommutation (swapColumns a ((finRotate n) a) G)

Swapping a cyclically adjacent non-interleaving pair of columns is a column commutation.

structure TauCeti.GridDiagram.ColumnTurn (n : ℕ) : Type

A turn for exchanging two adjacent columns: the column column, distinct from its cyclic successor, and a square row turnRow.

When the columns column and finRotate n column are exchanged, the vertical grid line between them is replaced by a curve γ which leaves the markings of column on its right and those of the successor on its left, so that reading the markings off with γ in place of the grid line exchanges the two columns. Such a curve may cross the grid line several times. The turn is an intersection in the square row turnRow at which γ crosses from the left of the grid line to its right going upwards; a marking of column in that row lies below it and a marking of the successor above it. Every row can serve as such a turn, whether or not the two marking segments interleave. The pentagons turning there, the pentagon-counting maps they define, and the fact that these maps intertwine the unblocked differentials depend on nothing else. Validated commutation data (TauCeti.GridDiagram.ColumnCommutationData) extends a turn by the second intersection and the placement of the markings in the two bigons, which the homotopy inverse of a commutation uses.

• column : Fin n

  The first of the two adjacent columns being exchanged.

• turnRow : Fin n

  The square row containing the distinguished intersection used by the pentagon maps.

• column_ne_next : self.column ≠ (finRotate n) self.column

  The adjacent columns are distinct.

theorem TauCeti.GridDiagram.ColumnTurn.ext_iff {n : ℕ} {x y : ColumnTurn n} : x = y ↔ x.column = y.column ∧ x.turnRow = y.turnRow

theorem TauCeti.GridDiagram.ColumnTurn.ext {n : ℕ} {x y : ColumnTurn n} (column : x.column = y.column) (turnRow : x.turnRow = y.turnRow) : x = y

theorem TauCeti.GridDiagram.ColumnTurn.one_lt {n : ℕ} (C : ColumnTurn n) : 1 < n

A grid with a turn for exchanging two adjacent columns has at least two columns.

@[reducible, inline]

abbrev TauCeti.GridDiagram.ColumnTurn.withTurnRow {n : ℕ} (C : ColumnTurn n) (t : Fin n) : ColumnTurn n

The turn at the same pair of columns as C, turning in row t instead.

It is reducible, so that the pentagons of this turn are the pentagons at the column C.column turning in row t.

@[simp]

theorem TauCeti.GridDiagram.ColumnTurn.withTurnRow_column {n : ℕ} (C : ColumnTurn n) (t : Fin n) : (C.withTurnRow t).column = C.column

The turn in another row exchanges the same columns.

@[simp]

theorem TauCeti.GridDiagram.ColumnTurn.withTurnRow_turnRow {n : ℕ} (C : ColumnTurn n) (t : Fin n) : (C.withTurnRow t).turnRow = t

The turn in row t turns in row t.

structure TauCeti.GridDiagram.ColumnCommutationData {n : ℕ} (G : GridDiagram n) extends TauCeti.GridDiagram.ColumnTurn n : Type

Validated geometric data for a column commutation.

The column column and its cyclic successor are distinct and non-interleaving. The curves in the combined diagram meet in the square rows turnRow and oppositeTurnRow. Going upwards from the opposite turn to turnRow gives the bigon containing both markings of column; going upwards from turnRow to the opposite turn gives the bigon containing both markings of the successor. At an intersection row, which side of the intersection contains a marking is determined by its column, so the terminal row of either discrete interval is admitted.

• column : Fin n
• turnRow : Fin n
• column_ne_next : self.column ≠ (finRotate n) self.column
• oppositeTurnRow : Fin n

  The square row containing the other intersection of the two vertical curves.

• noninterleaving : G.ColumnsNoninterleaving self.column ((finRotate n) self.column)

  The two marking segments satisfy the hypothesis for a column commutation.

• O_column_below : G.O.toPerm self.column ∈ insert self.turnRow (Grid.cIco self.oppositeTurnRow self.turnRow)

  The O-marking of the first column lies in the bigon below the distinguished turn.

• X_column_below : G.X.toPerm self.column ∈ insert self.turnRow (Grid.cIco self.oppositeTurnRow self.turnRow)

  The X-marking of the first column lies in the bigon below the distinguished turn.

• O_next_above : G.O.toPerm ((finRotate n) self.column) ∈ insert self.oppositeTurnRow (Grid.cIco self.turnRow self.oppositeTurnRow)

  The O-marking of the successor column lies in the bigon above the distinguished turn.

• X_next_above : G.X.toPerm ((finRotate n) self.column) ∈ insert self.oppositeTurnRow (Grid.cIco self.turnRow self.oppositeTurnRow)

  The X-marking of the successor column lies in the bigon above the distinguished turn.

@[instance_reducible]

instance TauCeti.GridDiagram.ColumnCommutationData.instCoeOutColumnTurn {n : ℕ} {G : GridDiagram n} : CoeOut G.ColumnCommutationData (ColumnTurn n)

Validated column-commutation data is in particular a turn, so the pentagon maps of a turn apply to it.

theorem TauCeti.GridDiagram.ColumnCommutationData.ext {n : ℕ} {G : GridDiagram n} {C D : G.ColumnCommutationData} (hcolumn : C.column = D.column) (hturnRow : C.turnRow = D.turnRow) (hoppositeTurnRow : C.oppositeTurnRow = D.oppositeTurnRow) : C = D

Two validated column commutations are equal when their geometric data agree.

theorem TauCeti.GridDiagram.ColumnCommutationData.ext_iff {n : ℕ} {G : GridDiagram n} {C D : G.ColumnCommutationData} : C = D ↔ C.column = D.column ∧ C.turnRow = D.turnRow ∧ C.oppositeTurnRow = D.oppositeTurnRow

theorem TauCeti.GridDiagram.ColumnCommutationData.turnRow_ne_oppositeTurnRow {n : ℕ} {G : GridDiagram n} (C : G.ColumnCommutationData) : C.turnRow ≠ C.oppositeTurnRow

The two intersection rows of validated commutation data are distinct: otherwise both markings of the first column would occupy the same square.

theorem TauCeti.GridDiagram.ColumnCommutationData.isColumnCommutation {n : ℕ} {G : GridDiagram n} (C : G.ColumnCommutationData) : G.IsColumnCommutation (swapColumns C.column ((finRotate n) C.column) G)

Validated column-commutation data determines an elementary column commutation.

def TauCeti.GridDiagram.ColumnCommutationData.reverse {n : ℕ} {G : GridDiagram n} (C : G.ColumnCommutationData) : (swapColumns C.column ((finRotate n) C.column) G).ColumnCommutationData

The validated data for the reverse column commutation, using the other intersection as its distinguished turn.

@[simp]

theorem TauCeti.GridDiagram.ColumnCommutationData.reverse_column {n : ℕ} {G : GridDiagram n} (C : G.ColumnCommutationData) : C.reverse.column = C.column

Reversing commutation data preserves the first column.

@[simp]

theorem TauCeti.GridDiagram.ColumnCommutationData.reverse_turnRow {n : ℕ} {G : GridDiagram n} (C : G.ColumnCommutationData) : C.reverse.turnRow = C.oppositeTurnRow

Reversing commutation data uses the other intersection as its distinguished turn.

@[simp]

theorem TauCeti.GridDiagram.ColumnCommutationData.reverse_oppositeTurnRow {n : ℕ} {G : GridDiagram n} (C : G.ColumnCommutationData) : C.reverse.oppositeTurnRow = C.turnRow

Reversing commutation data makes the old distinguished turn the other intersection.

@[simp]

theorem TauCeti.GridDiagram.ColumnCommutationData.reverse_reverse {n : ℕ} {G : GridDiagram n} (C : G.ColumnCommutationData) : _root_.cast ⋯ C.reverse.reverse = C

Reversing validated commutation data twice recovers the original data.

noncomputable def TauCeti.GridDiagram.ColumnCommutationData.ofNoninterleaving {n : ℕ} {G : GridDiagram n} (a : Fin n) (ha : a ≠ (finRotate n) a) (hG : G.ColumnsNoninterleaving a ((finRotate n) a)) : G.ColumnCommutationData

Validated commutation data for every adjacent non-interleaving pair of columns.

The two rows of the markings of a serve as the turn rows. Non-interleaving puts both markings of the successor column on one side of them, which fixes which of the two rows is the distinguished turn.

@[simp]

theorem TauCeti.GridDiagram.ColumnCommutationData.ofNoninterleaving_column {n : ℕ} {G : GridDiagram n} (a : Fin n) (ha : a ≠ (finRotate n) a) (hG : G.ColumnsNoninterleaving a ((finRotate n) a)) : (ofNoninterleaving a ha hG).column = a

The data built from a non-interleaving pair commutes the given column.

theorem TauCeti.GridDiagram.ColumnCommutationData.ofNoninterleaving_turnRow_ne {n : ℕ} {G : GridDiagram n} {a : Fin n} (ha : a ≠ (finRotate n) a) (hG : G.ColumnsNoninterleaving a ((finRotate n) a)) : (ofNoninterleaving a ha hG).turnRow ≠ G.X.toPerm ((finRotate n) a)

The distinguished turn of the data built from a non-interleaving pair is not in the row of the X-marking of the successor column.

theorem TauCeti.GridDiagram.isColumnCommutation_iff_exists_columnCommutationData {n : ℕ} {G G' : GridDiagram n} : G.IsColumnCommutation G' ↔ ∃ (C : G.ColumnCommutationData), G' = swapColumns C.column ((finRotate n) C.column) G

Every elementary column commutation is realised by validated column-commutation data.

theorem TauCeti.GridDiagram.isColumnCommutation_comm {n : ℕ} {G G' : GridDiagram n} : G.IsColumnCommutation G' ↔ G'.IsColumnCommutation G

An elementary column commutation is reversible.

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

Two grid diagrams differ by one elementary row commutation.

The rows are consecutive in the cyclic order on Fin n, have non-interleaving marking segments in the source diagram, and are swapped to obtain the target diagram.

theorem TauCeti.GridDiagram.isRowCommutation_iff {n : ℕ} (G G' : GridDiagram n) : G.IsRowCommutation G' ↔ ∃ (a : Fin n), a ≠ (finRotate n) a ∧ G.RowsNoninterleaving a ((finRotate n) a) ∧ G' = swapRows a ((finRotate n) a) G

Characterization of an elementary row commutation by its exchanged rows.

theorem TauCeti.GridDiagram.isRowCommutation_swapRows {n : ℕ} (G : GridDiagram n) (a : Fin n) (ha : a ≠ (finRotate n) a) (hG : G.RowsNoninterleaving a ((finRotate n) a)) : G.IsRowCommutation (swapRows a ((finRotate n) a) G)

Swapping a cyclically adjacent non-interleaving pair of rows is a row commutation.

theorem TauCeti.GridDiagram.isRowCommutation_comm {n : ℕ} {G G' : GridDiagram n} : G.IsRowCommutation G' ↔ G'.IsRowCommutation G

An elementary row commutation is reversible.

@[simp]

theorem TauCeti.GridDiagram.isRowCommutation_transpose {n : ℕ} (G G' : GridDiagram n) : G.transpose.IsRowCommutation G'.transpose ↔ G.IsColumnCommutation G'

Diagonal reflection turns a row commutation into a column commutation.

@[simp]

theorem TauCeti.GridDiagram.isColumnCommutation_transpose {n : ℕ} (G G' : GridDiagram n) : G.transpose.IsColumnCommutation G'.transpose ↔ G.IsRowCommutation G'

Diagonal reflection turns a column commutation into a row commutation.

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

One elementary grid commutation, either of rows or of columns.

theorem TauCeti.GridDiagram.isCommutation_iff {n : ℕ} (G G' : GridDiagram n) : G.IsCommutation G' ↔ G.IsRowCommutation G' ∨ G.IsColumnCommutation G'

A commutation is either an elementary row commutation or an elementary column commutation.

theorem TauCeti.GridDiagram.isCommutation_comm {n : ℕ} {G G' : GridDiagram n} : G.IsCommutation G' ↔ G'.IsCommutation G

The elementary grid commutation relation is symmetric.

@[simp]

theorem TauCeti.GridDiagram.isCommutation_transpose {n : ℕ} (G G' : GridDiagram n) : G.transpose.IsCommutation G'.transpose ↔ G.IsCommutation G'

Diagonal reflection preserves the elementary commutation relation, exchanging row and column moves.

theorem TauCeti.GridDiagram.IsCommutation.apply_eq_of_transpose {n : ℕ} {α : Sort u_1} (f : GridDiagram n → α) (htranspose : ∀ (H : GridDiagram n), f H.transpose = f H) (hcolumn : ∀ {H H' : GridDiagram n}, H.IsColumnCommutation H' → f H = f H') {G G' : GridDiagram n} (h : G.IsCommutation G') : f G = f G'

Row commutations from column commutations. A function on grid diagrams that is invariant under the diagonal reflection and under column commutations is invariant under every commutation: the reflection turns a row commutation into a column commutation.