Documentation

TauCeti.KnotTheory.Grid.Commutation.Move

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 #

Main results #

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.

source
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.

Equations
Instances For
    source
    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.

    source
    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.

    source
    theorem TauCeti.GridDiagram.isColumnCommutation_comm {n : β„•} {G G' : GridDiagram n} :
    G.IsColumnCommutation G' ↔ G'.IsColumnCommutation G

    An elementary column commutation is reversible.

    source
    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.

    Equations
    Instances For
      source
      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.

      source
      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.

      source
      theorem TauCeti.GridDiagram.isRowCommutation_comm {n : β„•} {G G' : GridDiagram n} :
      G.IsRowCommutation G' ↔ G'.IsRowCommutation G

      An elementary row commutation is reversible.

      source
      @[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.

      source
      @[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.

      source
      def TauCeti.GridDiagram.IsCommutation {n : β„•} (G G' : GridDiagram n) :
      Prop

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

      Equations
      Instances For
        source
        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.

        source
        theorem TauCeti.GridDiagram.isCommutation_comm {n : β„•} {G G' : GridDiagram n} :
        G.IsCommutation G' ↔ G'.IsCommutation G

        The elementary grid commutation relation is symmetric.

        source
        @[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.