The grid differentials under cyclic permutation

A grid diagram lives on a torus, so cyclically permuting its rows or its columns does not change the diagram it draws; these are the cyclic permutation moves GridDiagram.IsMove.cyclicRows and GridDiagram.IsMove.cyclicColumns. This file shows that the grid differentials see no difference either: relabeling every grid state by the same cyclic permutation identifies the rectangles counted by the differential of G with those counted by the differential of the permuted diagram, together with their weights.

For a cyclic permutation of the rows the variables V_c of the unblocked complex, which are indexed by columns, are untouched, and the chain relabeling GridChain.relabelRowsEquiv is a linear isomorphism intertwining the two unblocked differentials. For a cyclic permutation of the columns the rectangle weights are renamed by the same permutation, so the intertwining map on GC⁻ also renames the variables in the coefficients. The fully blocked complex has no variables, so there the chain relabelings intertwine the differentials for rows and columns alike.

Main results

• TauCeti.GridDiagram.unblockedCoefficient_relabelRows_finRotate, TauCeti.GridDiagram.unblockedCoefficient_relabelColumns_finRotate: the matrix coefficients of the unblocked differential of a cyclically permuted diagram.
• TauCeti.GridDiagram.fullyBlockedRectangleCount_relabelRows_finRotate, TauCeti.GridDiagram.fullyBlockedRectangleCount_relabelColumns_finRotate: the fully blocked rectangle counts are invariant.
• TauCeti.GridDiagram.unblockedDifferential_relabelRows_finRotate: the row relabeling intertwines the unblocked differentials.
• TauCeti.GridDiagram.unblockedDifferential_relabelColumns_finRotate: the column relabeling, followed by renaming the variables, intertwines the unblocked differentials.
• TauCeti.GridDiagram.unblockedDifferential_relabelRows_finRotate_apply, TauCeti.GridDiagram.unblockedDifferential_relabelColumns_finRotate_apply: the same two intertwining statements, pointwise.
• TauCeti.GridDiagram.fullyBlockedDifferential_relabelRows_finRotate, TauCeti.GridDiagram.fullyBlockedDifferential_relabelColumns_finRotate: the chain relabelings intertwine the fully blocked differentials.

References

The invariance of the grid complexes under cyclic permutation follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapters 3--5.

Cyclic permutation of the rows

theorem TauCeti.GridDiagram.disjoint_XSet_relabelRows_finRotate {n : ℕ} (G : GridDiagram n) {x y : GridState n} (r : GridRectangleBetween x y) : Disjoint ((GridRectangleBetween.relabelRowsEquiv (finRotate n) x y) r).toGridRectangle.coveredSquares (relabelRows (finRotate n) G).XSet ↔ Disjoint r.toGridRectangle.coveredSquares G.XSet

A cyclic permutation of the rows preserves and reflects X-avoidance of a rectangle.

theorem TauCeti.GridDiagram.mem_unblockedRectangles_relabelRows_finRotate {n : ℕ} (G : GridDiagram n) {x y : GridState n} (r : GridRectangleBetween x y) : (GridRectangleBetween.relabelRowsEquiv (finRotate n) x y) r ∈ (relabelRows (finRotate n) G).unblockedRectangles (GridState.relabelRows (finRotate n) x) (GridState.relabelRows (finRotate n) y) ↔ r ∈ G.unblockedRectangles x y

A cyclic permutation of the rows identifies the rectangles counted by the unblocked differentials.

@[simp]

theorem TauCeti.GridDiagram.OColumns_relabelRows_finRotate {n : ℕ} (G : GridDiagram n) {x y : GridState n} (r : GridRectangleBetween x y) : (relabelRows (finRotate n) G).OColumns ((GridRectangleBetween.relabelRowsEquiv (finRotate n) x y) r).toGridRectangle = G.OColumns r.toGridRectangle

A cyclic permutation of the rows does not change which O-columns a rectangle covers.

@[simp]

theorem TauCeti.GridDiagram.OMonomial_relabelRows_finRotate {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x y : GridState n} (r : GridRectangleBetween x y) : (relabelRows (finRotate n) G).OMonomial R ((GridRectangleBetween.relabelRowsEquiv (finRotate n) x y) r).toGridRectangle = G.OMonomial R r.toGridRectangle

A cyclic permutation of the rows leaves the weight of a rectangle unchanged.

@[simp]

theorem TauCeti.GridDiagram.unblockedCoefficient_relabelRows_finRotate {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (x y : GridState n) : (relabelRows (finRotate n) G).unblockedCoefficient R (GridState.relabelRows (finRotate n) x) (GridState.relabelRows (finRotate n) y) = G.unblockedCoefficient R x y

A cyclic permutation of the rows leaves the matrix coefficients of the unblocked differential unchanged.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedRectangleCount_relabelRows_finRotate {n : ℕ} (G : GridDiagram n) (x y : GridState n) : (relabelRows (finRotate n) G).fullyBlockedRectangleCount (GridState.relabelRows (finRotate n) x) (GridState.relabelRows (finRotate n) y) = G.fullyBlockedRectangleCount x y

A cyclic permutation of the rows leaves the fully blocked rectangle counts unchanged.

theorem TauCeti.GridDiagram.unblockedDifferential_relabelRows_finRotate {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] : (relabelRows (finRotate n) G).unblockedDifferential R ∘ₗ ↑(GridChain.relabelRowsEquiv (finRotate n)) = ↑(GridChain.relabelRowsEquiv (finRotate n)) ∘ₗ G.unblockedDifferential R

The chain relabeling by a cyclic permutation of the rows intertwines the unblocked differentials of G and of the row-permuted diagram.

@[simp]

theorem TauCeti.GridDiagram.unblockedDifferential_relabelRows_finRotate_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (c : GridChainMinus R n) : ((relabelRows (finRotate n) G).unblockedDifferential R) ((GridChain.relabelRowsEquiv (finRotate n)) c) = (GridChain.relabelRowsEquiv (finRotate n)) ((G.unblockedDifferential R) c)

The chain relabeling by a cyclic permutation of the rows intertwines the unblocked differentials pointwise.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_relabelRows_finRotate {n : ℕ} (G : GridDiagram n) : (relabelRows (finRotate n) G).fullyBlockedDifferential ∘ₗ ↑(GridChain.relabelRowsEquiv (finRotate n)) = ↑(GridChain.relabelRowsEquiv (finRotate n)) ∘ₗ G.fullyBlockedDifferential

The chain relabeling by a cyclic permutation of the rows intertwines the fully blocked differentials of G and of the row-permuted diagram.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedDifferential_relabelRows_finRotate_apply {n : ℕ} (G : GridDiagram n) (c : GridChain (ZMod 2) n) : (relabelRows (finRotate n) G).fullyBlockedDifferential ((GridChain.relabelRowsEquiv (finRotate n)) c) = (GridChain.relabelRowsEquiv (finRotate n)) (G.fullyBlockedDifferential c)

The cyclic row relabelling intertwines the fully blocked differentials pointwise.

Cyclic permutation of the columns

theorem TauCeti.GridDiagram.disjoint_XSet_relabelColumns_finRotate {n : ℕ} (G : GridDiagram n) {x y : GridState n} (r : GridRectangleBetween x y) : Disjoint ((GridRectangleBetween.relabelColumnsEquiv (finRotate n) x y) r).toGridRectangle.coveredSquares (relabelColumns (finRotate n) G).XSet ↔ Disjoint r.toGridRectangle.coveredSquares G.XSet

A cyclic permutation of the columns preserves and reflects X-avoidance of a rectangle.

theorem TauCeti.GridDiagram.mem_unblockedRectangles_relabelColumns_finRotate {n : ℕ} (G : GridDiagram n) {x y : GridState n} (r : GridRectangleBetween x y) : (GridRectangleBetween.relabelColumnsEquiv (finRotate n) x y) r ∈ (relabelColumns (finRotate n) G).unblockedRectangles (GridState.relabelColumns (finRotate n) x) (GridState.relabelColumns (finRotate n) y) ↔ r ∈ G.unblockedRectangles x y

A cyclic permutation of the columns identifies the rectangles counted by the unblocked differentials.

@[simp]

theorem TauCeti.GridDiagram.OColumns_relabelColumns_finRotate {n : ℕ} (G : GridDiagram n) {x y : GridState n} (r : GridRectangleBetween x y) : (relabelColumns (finRotate n) G).OColumns ((GridRectangleBetween.relabelColumnsEquiv (finRotate n) x y) r).toGridRectangle = Finset.map (Equiv.toEmbedding (finRotate n)) (G.OColumns r.toGridRectangle)

A cyclic permutation of the columns renames the O-columns a rectangle covers.

@[simp]

theorem TauCeti.GridDiagram.OMonomial_relabelColumns_finRotate {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x y : GridState n} (r : GridRectangleBetween x y) : (relabelColumns (finRotate n) G).OMonomial R ((GridRectangleBetween.relabelColumnsEquiv (finRotate n) x y) r).toGridRectangle = (MvPolynomial.rename ⇑(finRotate n)) (G.OMonomial R r.toGridRectangle)

A cyclic permutation of the columns renames the variables in the weight of a rectangle.

@[simp]

theorem TauCeti.GridDiagram.unblockedCoefficient_relabelColumns_finRotate {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (x y : GridState n) : (relabelColumns (finRotate n) G).unblockedCoefficient R (GridState.relabelColumns (finRotate n) x) (GridState.relabelColumns (finRotate n) y) = (MvPolynomial.rename ⇑(finRotate n)) (G.unblockedCoefficient R x y)

A cyclic permutation of the columns renames the variables in the matrix coefficients of the unblocked differential.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedRectangleCount_relabelColumns_finRotate {n : ℕ} (G : GridDiagram n) (x y : GridState n) : (relabelColumns (finRotate n) G).fullyBlockedRectangleCount (GridState.relabelColumns (finRotate n) x) (GridState.relabelColumns (finRotate n) y) = G.fullyBlockedRectangleCount x y

A cyclic permutation of the columns leaves the fully blocked rectangle counts unchanged.

theorem TauCeti.GridDiagram.unblockedDifferential_relabelColumns_finRotate {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] : (relabelColumns (finRotate n) G).unblockedDifferential R ∘ₛₗ ↑(GridChain.relabelColumnsRenameEquiv R (finRotate n)) = ↑(GridChain.relabelColumnsRenameEquiv R (finRotate n)) ∘ₛₗ G.unblockedDifferential R

The chain relabeling by a cyclic permutation of the columns, which also renames the variables of the coefficients by the same permutation, intertwines the unblocked differentials of G and of the column-permuted diagram.

@[simp]

theorem TauCeti.GridDiagram.unblockedDifferential_relabelColumns_finRotate_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (c : GridChainMinus R n) : ((relabelColumns (finRotate n) G).unblockedDifferential R) ((GridChain.relabelColumnsRenameEquiv R (finRotate n)) c) = (GridChain.relabelColumnsRenameEquiv R (finRotate n)) ((G.unblockedDifferential R) c)

The chain relabeling by a cyclic permutation of the columns, followed by renaming the variables, intertwines the unblocked differentials pointwise.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_relabelColumns_finRotate {n : ℕ} (G : GridDiagram n) : (relabelColumns (finRotate n) G).fullyBlockedDifferential ∘ₗ ↑(GridChain.relabelColumnsEquiv (finRotate n)) = ↑(GridChain.relabelColumnsEquiv (finRotate n)) ∘ₗ G.fullyBlockedDifferential

The chain relabeling by a cyclic permutation of the columns intertwines the fully blocked differentials of G and of the column-permuted diagram.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedDifferential_relabelColumns_finRotate_apply {n : ℕ} (G : GridDiagram n) (c : GridChain (ZMod 2) n) : (relabelColumns (finRotate n) G).fullyBlockedDifferential ((GridChain.relabelColumnsEquiv (finRotate n)) c) = (GridChain.relabelColumnsEquiv (finRotate n)) (G.fullyBlockedDifferential c)

The cyclic column relabelling intertwines the fully blocked differentials pointwise.