The unblocked grid differential under the half-turn

Rotating a planar grid diagram by a half-turn is an isotopy of the link it draws, and it preserves the convention that vertical segments cross over horizontal ones. On the torus the half-turn moves the square named by its lower-left corner (c, r) to the square named by (c.rev, r.rev), which is GridDiagram.rotate, and it moves the grid point (c, r) to the grid point with both coordinates negated modulo n, which is GridState.halfTurn. A half-turn exchanges the south-west and north-east corners of a rectangle (and likewise the north-west and south-east ones), so the pair of corners lying on the source state is again the south-west and north-east pair. It therefore carries the rectangles counted by the unblocked differential of G to those counted by the unblocked differential of G.rotate (GridRectangleBetween.halfTurnEquiv), together with the markings they cover.

The variables V_c of GC⁻ are indexed by the columns of the O-markings, and the half-turn moves the O-marking of column c to column c.rev. So the map on GC⁻ that moves each grid state by GridState.halfTurn and renames the variables along Fin.revPerm (GridChain.halfTurnRenameEquiv) intertwines the unblocked differentials of G and of G.rotate.

Main definitions

• TauCeti.GridChain.halfTurnRenameEquiv: the semilinear equivalence on GC⁻ that moves grid states by the half-turn and renames the coefficient variables along Fin.revPerm.

Main results

• TauCeti.GridDiagram.unblockedCoefficient_rotate_halfTurn: the matrix coefficients of the unblocked differential of G.rotate are the renamed coefficients of that of G.
• TauCeti.GridDiagram.unblockedDifferential_rotate_halfTurnRenameEquiv, TauCeti.GridDiagram.unblockedDifferential_halfTurnRenameEquiv: the half-turn intertwines the unblocked differentials of G and of G.rotate, in both directions.
• TauCeti.GridChain.halfTurnRenameEquiv_halfTurnRenameEquiv: the half-turn of chains is an involution.

References

The symmetries of grid diagrams, among them the half-turn, are in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3; the unblocked complex is defined in Chapter 4.6.

noncomputable def TauCeti.GridChain.halfTurnRenameEquiv {n : ℕ} (R : Type u_1) [CommSemiring R] : GridChainMinus R n ≃ₛₗ[↑(MvPolynomial.renameEquiv R Fin.revPerm).toRingEquiv] GridChainMinus R n

The semilinear equivalence on GC⁻ induced by the half-turn: it moves every grid state by GridState.halfTurn and renames the coefficient variables along Fin.revPerm, the column permutation by which GridDiagram.rotate moves the O-markings.

@[simp]

theorem TauCeti.GridChain.halfTurnRenameEquiv_apply {n : ℕ} (R : Type u_1) [CommSemiring R] (c : GridChainMinus R n) (y : GridState n) : ((halfTurnRenameEquiv R) c) y = (MvPolynomial.rename Fin.rev) (c y.halfTurn)

The coefficient of a half-turned chain at a state is the renamed coefficient at the half-turned state.

@[simp]

theorem TauCeti.GridChain.halfTurnRenameEquiv_single {n : ℕ} (R : Type u_1) [CommSemiring R] (x : GridState n) (a : MvPolynomial (Fin n) R) : (halfTurnRenameEquiv R) (Finsupp.single x a) = Finsupp.single x.halfTurn ((MvPolynomial.rename Fin.rev) a)

The half-turn sends a generator with coefficient a to the half-turned generator with the renamed coefficient.

@[simp]

theorem TauCeti.GridChain.halfTurnRenameEquiv_halfTurnRenameEquiv {n : ℕ} (R : Type u_1) [CommSemiring R] (c : GridChainMinus R n) : (halfTurnRenameEquiv R) ((halfTurnRenameEquiv R) c) = c

The half-turn of chains is an involution.

theorem TauCeti.GridDiagram.disjoint_XSet_rotate_halfTurnEquiv {n : ℕ} (G : GridDiagram n) {x y : GridState n} (r : GridRectangleBetween x y) : Disjoint ((GridRectangleBetween.halfTurnEquiv x y) r).toGridRectangle.coveredSquares G.rotate.XSet ↔ Disjoint r.toGridRectangle.coveredSquares G.XSet

The half-turn preserves and reflects X-avoidance of a rectangle.

theorem TauCeti.GridDiagram.mem_unblockedRectangles_rotate_halfTurnEquiv {n : ℕ} (G : GridDiagram n) {x y : GridState n} (r : GridRectangleBetween x y) : (GridRectangleBetween.halfTurnEquiv x y) r ∈ G.rotate.unblockedRectangles x.halfTurn y.halfTurn ↔ r ∈ G.unblockedRectangles x y

The half-turn identifies the rectangles counted by the unblocked differentials of G and of G.rotate.

@[simp]

theorem TauCeti.GridDiagram.OColumns_rotate_halfTurnEquiv {n : ℕ} (G : GridDiagram n) {x y : GridState n} (r : GridRectangleBetween x y) : G.rotate.OColumns ((GridRectangleBetween.halfTurnEquiv x y) r).toGridRectangle = Finset.map (Equiv.toEmbedding Fin.revPerm) (G.OColumns r.toGridRectangle)

The half-turn moves the O-columns a rectangle covers by Fin.rev.

@[simp]

theorem TauCeti.GridDiagram.OMonomial_rotate_halfTurnEquiv {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x y : GridState n} (r : GridRectangleBetween x y) : G.rotate.OMonomial R ((GridRectangleBetween.halfTurnEquiv x y) r).toGridRectangle = (MvPolynomial.rename Fin.rev) (G.OMonomial R r.toGridRectangle)

The half-turn renames the variables in the weight of a rectangle along Fin.rev.

@[simp]

theorem TauCeti.GridDiagram.unblockedCoefficient_rotate_halfTurn {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (x y : GridState n) : G.rotate.unblockedCoefficient R x.halfTurn y.halfTurn = (MvPolynomial.rename Fin.rev) (G.unblockedCoefficient R x y)

The half-turn renames the variables in the matrix coefficients of the unblocked differential: those of G.rotate between half-turned states are those of G, renamed along Fin.rev.

theorem TauCeti.GridDiagram.unblockedDifferential_rotate_comp_halfTurnRenameEquiv {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] : G.rotate.unblockedDifferential R ∘ₛₗ ↑(GridChain.halfTurnRenameEquiv R) = ↑(GridChain.halfTurnRenameEquiv R) ∘ₛₗ G.unblockedDifferential R

The half-turn is a symmetry of GC⁻. Moving grid states by the half-turn and renaming the variables along Fin.rev intertwines the unblocked differentials of G and of G.rotate.

@[simp]

theorem TauCeti.GridDiagram.unblockedDifferential_rotate_halfTurnRenameEquiv {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (c : GridChainMinus R n) : (G.rotate.unblockedDifferential R) ((GridChain.halfTurnRenameEquiv R) c) = (GridChain.halfTurnRenameEquiv R) ((G.unblockedDifferential R) c)

The half-turn intertwines the unblocked differentials of G and of G.rotate, pointwise.

theorem TauCeti.GridDiagram.unblockedDifferential_halfTurnRenameEquiv {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (c : GridChainMinus R n) : (G.unblockedDifferential R) ((GridChain.halfTurnRenameEquiv R) c) = (GridChain.halfTurnRenameEquiv R) ((G.rotate.unblockedDifferential R) c)

Since the half-turn is an involution, it also intertwines the unblocked differentials of G.rotate and of G.