Grid links as diagrams modulo grid moves

A commutation keeps the size of a grid diagram fixed, whereas a stabilization changes it by one. Consequently the relation generated by both kinds of move cannot live on any one type GridDiagram n; it lives on the dependent sum Σ n, GridDiagram n of diagrams of all sizes.

This file combines cyclic permutations, commutations, and stabilizations into GridDiagram.IsMove, takes its equivalence closure as GridDiagram.MovesTo, and defines GridLink to be the quotient by that relation. Thus a grid link is, by definition, a grid diagram modulo cyclic permutations, commutations, and stabilizations. This is the combinatorial input notion of link; its later reconciliation with embedded links is a separate target.

The quotient does not identify the chain maps attached to different move sequences. Later naturality results should attach maps to GridDiagram.IsMove and prove their composition laws, rather than extracting an untracked identification from equality in GridLink.

Main definitions

• TauCeti.GridDiagram.IsMove: one cyclic permutation, commutation, stabilization, or destabilization between possibly differently sized diagrams.
• TauCeti.GridDiagram.MovesTo: the equivalence relation generated by elementary grid moves.
• TauCeti.GridLink: grid diagrams modulo grid moves.

Main results

• TauCeti.GridDiagram.toGridLink_eq_iff_movesTo: two diagrams represent the same grid link exactly when they are connected by grid moves.
• TauCeti.GridLink.lift: define a function on grid links from a function on diagrams that is invariant under commutation and stabilization.

References

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, under "Standing conventions", specifically "A link is (at first) a grid diagram modulo grid moves", using the commutation and stabilization moves of Lane G.5. The presentation follows Ozsvath--Stipsicz--Szabo, Grid Homology for Knots and Links, Chapter 3.

inductive TauCeti.GridDiagram.IsMove : (n : ℕ) × GridDiagram n → (n : ℕ) × GridDiagram n → Prop

One elementary grid move between diagrams of possibly different sizes.

Cyclic permutations and commutations relate diagrams of the same size. A stabilization relates a diagram of size n to one of size n + 1, and a destabilization records the reverse orientation of the same local move.

• cyclicRows {n : ℕ} {G G' : GridDiagram n} (h : G' = relabelRows (finRotate n) G ∨ G = relabelRows (finRotate n) G') : IsMove ⟨n, G⟩ ⟨n, G'⟩
• cyclicColumns {n : ℕ} {G G' : GridDiagram n} (h : G' = relabelColumns (finRotate n) G ∨ G = relabelColumns (finRotate n) G') : IsMove ⟨n, G⟩ ⟨n, G'⟩
• commutation {n : ℕ} {G G' : GridDiagram n} (h : G.IsCommutation G') : IsMove ⟨n, G⟩ ⟨n, G'⟩
• stabilization {n : ℕ} {G : GridDiagram n} {G' : GridDiagram (n + 1)} (h : G.IsStabilization G') : IsMove ⟨n, G⟩ ⟨n + 1, G'⟩
• destabilization {n : ℕ} {G : GridDiagram n} {G' : GridDiagram (n + 1)} (h : G'.IsDestabilization G) : IsMove ⟨n + 1, G'⟩ ⟨n, G⟩

theorem TauCeti.GridDiagram.IsMove.symm {G G' : (n : ℕ) × GridDiagram n} (h : IsMove G G') : IsMove G' G

Every elementary grid move is reversible.

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

Two grid diagrams are related by grid moves when they lie in the equivalence relation generated by cyclic permutations, commutations, stabilizations, and destabilizations.

theorem TauCeti.GridDiagram.MovesTo.induction_on {n m : ℕ} {G : GridDiagram n} {G' : GridDiagram m} {motive : (n : ℕ) × GridDiagram n → (n : ℕ) × GridDiagram n → Prop} (h : G.MovesTo G') (rel : ∀ {A B : (n : ℕ) × GridDiagram n}, IsMove A B → motive A B) (refl : ∀ (A : (n : ℕ) × GridDiagram n), motive A A) (symm : ∀ {A B : (n : ℕ) × GridDiagram n}, A.snd.MovesTo B.snd → motive A B → motive B A) (trans : ∀ {A B C : (n : ℕ) × GridDiagram n}, A.snd.MovesTo B.snd → B.snd.MovesTo C.snd → motive A B → motive B C → motive A C) : motive ⟨n, G⟩ ⟨m, G'⟩

Induction over grid moves, allowing diagrams of different sizes at intermediate steps.

theorem TauCeti.GridDiagram.MovesTo.refl {n : ℕ} (G : GridDiagram n) : G.MovesTo G

Every grid diagram is related to itself by the empty sequence of moves.

theorem TauCeti.GridDiagram.MovesTo.symm {n m : ℕ} {G : GridDiagram n} {G' : GridDiagram m} (h : G.MovesTo G') : G'.MovesTo G

A sequence of grid moves can be traversed in reverse.

theorem TauCeti.GridDiagram.MovesTo.trans {n m k : ℕ} {G : GridDiagram n} {G' : GridDiagram m} {G'' : GridDiagram k} (h : G.MovesTo G') (h' : G'.MovesTo G'') : G.MovesTo G''

Sequences of grid moves compose.

theorem TauCeti.GridDiagram.IsMove.movesTo {n m : ℕ} {G : GridDiagram n} {G' : GridDiagram m} (h : IsMove ⟨n, G⟩ ⟨m, G'⟩) : G.MovesTo G'

One elementary move gives a sequence of grid moves of length one.

theorem TauCeti.GridDiagram.cyclicRows_movesTo {n : ℕ} (G : GridDiagram n) : G.MovesTo (relabelRows (finRotate n) G)

A cyclic permutation of the rows gives a grid-move relation.

theorem TauCeti.GridDiagram.cyclicColumns_movesTo {n : ℕ} (G : GridDiagram n) : G.MovesTo (relabelColumns (finRotate n) G)

A cyclic permutation of the columns gives a grid-move relation.

theorem TauCeti.GridDiagram.IsCommutation.movesTo {n : ℕ} {G G' : GridDiagram n} (h : G.IsCommutation G') : G.MovesTo G'

An elementary commutation gives a grid-move relation.

theorem TauCeti.GridDiagram.movesTo_swapRows {n : ℕ} (G : GridDiagram n) (a : Fin n) (h : G.RowsNoninterleaving a ((finRotate n) a)) : G.MovesTo (swapRows a ((finRotate n) a) G)

Swapping a cyclically adjacent non-interleaving pair of rows gives a grid-move relation.

theorem TauCeti.GridDiagram.movesTo_swapColumns {n : ℕ} (G : GridDiagram n) (a : Fin n) (h : G.ColumnsNoninterleaving a ((finRotate n) a)) : G.MovesTo (swapColumns a ((finRotate n) a) G)

Swapping a cyclically adjacent non-interleaving pair of columns gives a grid-move relation.

theorem TauCeti.GridDiagram.IsStabilization.movesTo {n : ℕ} {G : GridDiagram n} {G' : GridDiagram (n + 1)} (h : G.IsStabilization G') : G.MovesTo G'

An elementary stabilization gives a grid-move relation.

theorem TauCeti.GridDiagram.IsDestabilization.movesTo {n : ℕ} {G : GridDiagram n} {G' : GridDiagram (n + 1)} (h : G'.IsDestabilization G) : G'.MovesTo G

An elementary destabilization gives a grid-move relation.

def TauCeti.GridLink : Type

A grid link is a grid diagram, of arbitrary size, modulo cyclic permutations, commutations, and stabilizations.

This is the combinatorial notion of link used by grid homology. Identifying it with an ambient isotopy class of embedded links is the separate Cromwell-reconciliation target.

def TauCeti.GridDiagram.toGridLink {n : ℕ} (G : GridDiagram n) : GridLink

The grid link represented by a grid diagram.

theorem TauCeti.GridDiagram.toGridLink_eq_iff_movesTo {n m : ℕ} (G : GridDiagram n) {G' : GridDiagram m} : G.toGridLink = G'.toGridLink ↔ G.MovesTo G'

Two grid diagrams represent the same grid link exactly when they are connected by grid moves.

theorem TauCeti.GridDiagram.IsMove.toGridLink_eq {n m : ℕ} {G : GridDiagram n} {G' : GridDiagram m} (h : IsMove ⟨n, G⟩ ⟨m, G'⟩) : G.toGridLink = G'.toGridLink

One elementary grid move does not change the represented grid link.

theorem TauCeti.GridDiagram.cyclicRows_toGridLink_eq {n : ℕ} (G : GridDiagram n) : G.toGridLink = (relabelRows (finRotate n) G).toGridLink

A cyclic permutation of the rows does not change the represented grid link.

theorem TauCeti.GridDiagram.cyclicColumns_toGridLink_eq {n : ℕ} (G : GridDiagram n) : G.toGridLink = (relabelColumns (finRotate n) G).toGridLink

A cyclic permutation of the columns does not change the represented grid link.

theorem TauCeti.GridDiagram.IsCommutation.toGridLink_eq {n : ℕ} {G G' : GridDiagram n} (h : G.IsCommutation G') : G.toGridLink = G'.toGridLink

A commutation does not change the represented grid link.

theorem TauCeti.GridDiagram.IsStabilization.toGridLink_eq {n : ℕ} {G : GridDiagram n} {G' : GridDiagram (n + 1)} (h : G.IsStabilization G') : G.toGridLink = G'.toGridLink

A stabilization does not change the represented grid link.

theorem TauCeti.GridDiagram.IsDestabilization.toGridLink_eq {n : ℕ} {G : GridDiagram n} {G' : GridDiagram (n + 1)} (h : G'.IsDestabilization G) : G'.toGridLink = G.toGridLink

A destabilization does not change the represented grid link.

@[simp]

theorem TauCeti.GridDiagram.toGridLink_cast {n m : ℕ} (G : GridDiagram n) (h : n = m) : (cast h G).toGridLink = G.toGridLink

Transporting a grid diagram along an equality of grid numbers does not change the represented grid link.

theorem TauCeti.GridLink.ind {motive : GridLink → Prop} (h : ∀ {n : ℕ} (G : GridDiagram n), motive G.toGridLink) (L : GridLink) : motive L

Every grid link can be handled by considering a grid diagram representing it.

theorem TauCeti.GridLink.exists_gridDiagram (L : GridLink) : ∃ (G : (n : ℕ) × GridDiagram n), G.snd.toGridLink = L

Every grid link has a presenting grid diagram.

def TauCeti.GridLink.lift {α : Sort u_1} (f : (n : ℕ) → GridDiagram n → α) (hrows : ∀ {n : ℕ} (G : GridDiagram n), f n G = f n (GridDiagram.relabelRows (finRotate n) G)) (hcolumns : ∀ {n : ℕ} (G : GridDiagram n), f n G = f n (GridDiagram.relabelColumns (finRotate n) G)) (hcomm : ∀ {n : ℕ} {G G' : GridDiagram n}, G.IsCommutation G' → f n G = f n G') (hstab : ∀ {n : ℕ} {G : GridDiagram n} {G' : GridDiagram (n + 1)}, G.IsStabilization G' → f n G = f (n + 1) G') : GridLink → α

Define a function on grid links from a function on grid diagrams that is invariant under cyclic permutations, elementary commutations, and stabilizations.

No separate destabilization hypothesis is needed: invariance under a stabilization supplies the reverse equality as well.

theorem TauCeti.GridLink.lift_toGridLink {α : Sort u_1} (f : (n : ℕ) → GridDiagram n → α) (hrows : ∀ {n : ℕ} (G : GridDiagram n), f n G = f n (GridDiagram.relabelRows (finRotate n) G)) (hcolumns : ∀ {n : ℕ} (G : GridDiagram n), f n G = f n (GridDiagram.relabelColumns (finRotate n) G)) (hcomm : ∀ {n : ℕ} {G G' : GridDiagram n}, G.IsCommutation G' → f n G = f n G') (hstab : ∀ {n : ℕ} {G : GridDiagram n} {G' : GridDiagram (n + 1)}, G.IsStabilization G' → f n G = f (n + 1) G') {n : ℕ} (G : GridDiagram n) : lift f ⋯ ⋯ ⋯ ⋯ G.toGridLink = f n G

Evaluating a lifted function on the class of a diagram recovers its value on that diagram.