Coordinate reversal of grid states and diagrams

This file adds coordinate reversal on the toroidal grid to the grid-combinatorial lane of the Heegaard Floer roadmap, alongside the already-developed diagonal reflection (transpose) and marking swap (swapMarkings). Rotation reverses both the column and the row coordinate by the map (c, r) ↦ (cᵒ, rᵒ) with ·ᵒ = Fin.rev. It is the composition of the column and row relabelings by the coordinate reversal Fin.revPerm, so it reuses the existing relabeling API rather than introducing a new primitive. It carries a grid state to a grid state and a grid diagram to a grid diagram.

In the coordinate convention used here, GridState.rotate reverses grid-point coordinates, whereas GridDiagram.rotate reverses the lower-left-coordinate names of marking squares. These are half-turns about different centres on the torus. Thus the paired operations preserve the grading results below but not marking avoidance, and do not give a symmetry of the fully blocked complex. The operation on grid states that does match GridDiagram.rotate is the half-turn GridState.halfTurn, which negates both coordinates of a grid point modulo n; together with GridDiagram.rotate it is a symmetry of the grid complexes (TauCeti.KnotTheory.Grid.Differential.HalfTurn).

Only the basic state/diagram operation and its point-set lemmas live here, parallel to where transpose is developed; the invariance of the J-pairing of two grid states under coordinate reversal is in TauCeti.KnotTheory.Grid.JFunction.Basic (GridState.J_rotate). The gradings themselves are not rotation invariant: they pair a grid state against the markings, which sit at the centres of their squares, so the half-turn about a grid point that rotates a state and the half-turn about a square centre that rotates the markings are different maps of the torus. This distinction and its grading consequence follow the analysis in TauCeti pull request #3135.

Main definitions

• TauCeti.GridState.rotate: coordinate reversal of a grid state.
• TauCeti.GridDiagram.rotate: coordinate reversal of a grid diagram's marking-square names.
• TauCeti.GridState.halfTurn: the half-turn of a grid state that matches GridDiagram.rotate, negating both coordinates of its points modulo n.

Main results

• TauCeti.GridState.rotate_rotate, TauCeti.GridDiagram.rotate_rotate, TauCeti.GridState.halfTurn_halfTurn: rotation and the half-turn are involutions on grid states and grid diagrams.
• TauCeti.GridState.rotate_pointSet, TauCeti.GridDiagram.rotate_OSet, TauCeti.GridDiagram.rotate_XSet: the state point set and the diagram's marking-square sets are the coordinate reversals of the original sets.
• TauCeti.GridState.relabelRows_rotate, TauCeti.GridState.relabelColumns_rotate, TauCeti.GridDiagram.swapMarkings_rotate: rotation interacts predictably with the existing relabeling, swap, and marking-swap operations.

References

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G item 8, "Symmetries and the genus bound": coordinate reversal is among the standard grid symmetries in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

def TauCeti.GridState.rotate {n : ℕ} (x : GridState n) : GridState n

Coordinate reversal of a grid state.

This reverses both coordinates of the occupied grid points and is the composition of the column and row relabelings by Fin.revPerm. Geometrically it is a half-turn about a square center; the same operation on lower-left square names in GridDiagram.rotate is a half-turn about a grid point, so the two operations do not together preserve marking avoidance.

@[simp]

theorem TauCeti.GridState.rotate_apply {n : ℕ} (x : GridState n) (c : Fin n) : x.rotate.toPerm c = (x.toPerm c.rev).rev

The rotated state reads off a column by reversing it, applying the original state, and reversing the resulting row.

theorem TauCeti.GridState.mem_pointSet_rotate {n : ℕ} (x : GridState n) (p : Fin n × Fin n) : p ∈ x.rotate.pointSet ↔ Prod.map Fin.rev Fin.rev p ∈ x.pointSet

A grid point lies in the rotated state exactly when its coordinate reversal lies in the original state.

theorem TauCeti.GridState.rotate_pointSet {n : ℕ} (x : GridState n) : x.rotate.pointSet = Finset.image (Prod.map Fin.rev Fin.rev) x.pointSet

The point set of the rotated state is the coordinate reversal of the original point set.

@[simp]

theorem TauCeti.GridState.rotate_rotate {n : ℕ} (x : GridState n) : x.rotate.rotate = x

Coordinate reversal is an involution on grid states.

@[simp]

theorem TauCeti.GridState.transpose_rotate {n : ℕ} (x : GridState n) : x.transpose.rotate = x.rotate.transpose

Diagonal reflection commutes with coordinate reversal of a grid state.

@[simp]

theorem TauCeti.GridState.relabelRows_rotate {n : ℕ} (ρ : Equiv.Perm (Fin n)) (x : GridState n) : (relabelRows ρ x).rotate = relabelRows (Equiv.trans Fin.revPerm (Equiv.trans ρ Fin.revPerm)) x.rotate

Row relabeling before rotation becomes row relabeling by the conjugate permutation after rotation.

@[simp]

theorem TauCeti.GridState.relabelColumns_rotate {n : ℕ} (κ : Equiv.Perm (Fin n)) (x : GridState n) : (relabelColumns κ x).rotate = relabelColumns (Equiv.trans Fin.revPerm (Equiv.trans κ Fin.revPerm)) x.rotate

Column relabeling before rotation becomes column relabeling by the conjugate permutation after rotation.

@[simp]

theorem TauCeti.GridState.swapRows_rotate {n : ℕ} (a b : Fin n) (x : GridState n) : (swapRows a b x).rotate = swapRows a.rev b.rev x.rotate

Swapping rows before rotation is the same as swapping the reversed rows after rotation.

@[simp]

theorem TauCeti.GridState.swapColumns_rotate {n : ℕ} (a b : Fin n) (x : GridState n) : (swapColumns a b x).rotate = swapColumns a.rev b.rev x.rotate

Swapping columns before rotation is the same as swapping the reversed columns after rotation.

def TauCeti.GridState.halfTurn {n : ℕ} (x : GridState n) : GridState n

The half-turn of a grid state that matches the half-turn GridDiagram.rotate of a grid diagram.

It moves the grid point (c, r) to (finRotate n c.rev, finRotate n r.rev), negating both coordinates modulo n. This is the half-turn of the torus that moves the square named by its lower-left corner (c, r) to the square named by (c.rev, r.rev), which is how GridDiagram.rotate moves the markings. So, unlike GridState.rotate, it carries the rectangles of a grid diagram to the rectangles of the rotated diagram together with the markings they cover.

theorem TauCeti.GridState.halfTurn_apply_finRotate_rev {n : ℕ} (x : GridState n) (c : Fin n) : x.halfTurn.toPerm ((finRotate n) c.rev) = (finRotate n) (x.toPerm c).rev

The half-turn of a grid state sends the point in column c to the point in column finRotate n c.rev, negating both coordinates.

theorem TauCeti.GridState.halfTurn_apply {n : ℕ} (x : GridState n) (c : Fin n) : x.halfTurn.toPerm c = (finRotate n) (x.toPerm ((finRotate n) c.rev)).rev

The half-turn of a grid state, read off a column: the column and the row are both negated modulo n.

@[simp]

theorem TauCeti.GridState.halfTurn_halfTurn {n : ℕ} (x : GridState n) : x.halfTurn.halfTurn = x

The half-turn is an involution on grid states.

theorem TauCeti.GridState.halfTurn_involutive {n : ℕ} : Function.Involutive halfTurn

The half-turn of grid states is involutive.

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

Coordinate reversal of a grid diagram's marking-square names.

It is the composition of the column and row relabelings by the coordinate reversal Fin.revPerm, applied to both marking states at once. Each relabeling is again a grid diagram, so rotation preserves the condition that no square carries both an O and an X marking. Here Fin.rev acts on the lower-left-coordinate names of marking squares, so this operation and GridState.rotate do not together preserve marking avoidance.

@[simp]

theorem TauCeti.GridDiagram.rotate_O {n : ℕ} (G : GridDiagram n) : G.rotate.O = G.O.rotate

The O-marking state of the rotated diagram is the rotation of the original O-state.

@[simp]

theorem TauCeti.GridDiagram.rotate_X {n : ℕ} (G : GridDiagram n) : G.rotate.X = G.X.rotate

The X-marking state of the rotated diagram is the rotation of the original X-state.

theorem TauCeti.GridDiagram.rotate_OSet {n : ℕ} (G : GridDiagram n) : G.rotate.OSet = Finset.image (Prod.map Fin.rev Fin.rev) G.OSet

The O-markings of the rotated diagram are the coordinate reversal of the original O-markings.

theorem TauCeti.GridDiagram.rotate_XSet {n : ℕ} (G : GridDiagram n) : G.rotate.XSet = Finset.image (Prod.map Fin.rev Fin.rev) G.XSet

The X-markings of the rotated diagram are the coordinate reversal of the original X-markings.

theorem TauCeti.GridDiagram.mem_OSet_rotate {n : ℕ} (G : GridDiagram n) (p : Fin n × Fin n) : p ∈ G.rotate.OSet ↔ Prod.map Fin.rev Fin.rev p ∈ G.OSet

A square lies in the rotated diagram's O-marking set exactly when its coordinate reversal lies in the original O-marking set.

theorem TauCeti.GridDiagram.mem_XSet_rotate {n : ℕ} (G : GridDiagram n) (p : Fin n × Fin n) : p ∈ G.rotate.XSet ↔ Prod.map Fin.rev Fin.rev p ∈ G.XSet

A square lies in the rotated diagram's X-marking set exactly when its coordinate reversal lies in the original X-marking set.

@[simp]

theorem TauCeti.GridDiagram.rotate_rotate {n : ℕ} (G : GridDiagram n) : G.rotate.rotate = G

Coordinate reversal is an involution on grid diagrams.

@[simp]

theorem TauCeti.GridDiagram.transpose_rotate {n : ℕ} (G : GridDiagram n) : G.transpose.rotate = G.rotate.transpose

Diagonal reflection commutes with coordinate reversal of a grid diagram.

@[simp]

theorem TauCeti.GridDiagram.relabelRows_rotate {n : ℕ} (G : GridDiagram n) (ρ : Equiv.Perm (Fin n)) : (relabelRows ρ G).rotate = relabelRows (Equiv.trans Fin.revPerm (Equiv.trans ρ Fin.revPerm)) G.rotate

Row relabeling before rotation becomes row relabeling by the conjugate permutation after rotation.

@[simp]

theorem TauCeti.GridDiagram.relabelColumns_rotate {n : ℕ} (G : GridDiagram n) (κ : Equiv.Perm (Fin n)) : (relabelColumns κ G).rotate = relabelColumns (Equiv.trans Fin.revPerm (Equiv.trans κ Fin.revPerm)) G.rotate

Column relabeling before rotation becomes column relabeling by the conjugate permutation after rotation.

@[simp]

theorem TauCeti.GridDiagram.swapRows_rotate {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapRows a b G).rotate = swapRows a.rev b.rev G.rotate

Swapping rows before rotation is the same as swapping the reversed rows after rotation.

@[simp]

theorem TauCeti.GridDiagram.swapColumns_rotate {n : ℕ} (G : GridDiagram n) (a b : Fin n) : (swapColumns a b G).rotate = swapColumns a.rev b.rev G.rotate

Swapping columns before rotation is the same as swapping the reversed columns after rotation.

@[simp]

theorem TauCeti.GridDiagram.swapMarkings_rotate {n : ℕ} (G : GridDiagram n) : G.swapMarkings.rotate = G.rotate.swapMarkings

Exchanging the two marking states commutes with coordinate reversal.