Reordering rectangle decompositions with disjoint side columns

A two-step term in the square of the grid differential consists of a rectangle from x to an intermediate state and a second rectangle from that state to z. When the two rectangles use disjoint pairs of side columns, their column transpositions commute. They may therefore be applied in the opposite order, through a different intermediate state.

This file reorders such a GridRectangleDecomposition. The first reordered rectangle has exactly the toroidal domain of the old second rectangle, and conversely for the second. In particular, both marking-avoidance conditions are preserved. Reordering is an involution and changes the intermediate state, giving the fixed-point-free pairing needed in the disjoint-side case of the eventual rectangle juxtaposition argument.

Reordering also transfers emptiness. If both rectangles of the original decomposition are empty, then so are both rectangles of the reordered one. This is the one genuinely geometric step of the disjoint-side case: the two side columns of one rectangle sit on opposite cyclic arcs of the other pair, and Grid.mem_cIoo_and_mem_cIoo_swap_of_notMem turns that separation around to produce a grid-state point inside the rectangle assumed empty. The overlapping and annular cases remain separate parts of the square-zero proof.

Main definitions

• TauCeti.GridRectangleDecomposition.HasDisjointSides: the two side-column pairs are disjoint.
• TauCeti.GridRectangleDecomposition.commute: apply two rectangles with disjoint side columns in the opposite order.

Main results

• TauCeti.GridRectangleDecomposition.commute_first_toGridRectangle and commute_second_toGridRectangle: reordering exchanges the two toroidal domains.
• TauCeti.GridRectangleDecomposition.avoidsMarkings_commute_first_iff and avoidsMarkings_commute_second_iff: reordering preserves the marking-avoidance conditions.
• TauCeti.GridRectangleDecomposition.commute_commute: reordering twice is the identity.
• TauCeti.GridRectangleDecomposition.commute_middle_ne and TauCeti.GridRectangleDecomposition.commute_ne: the intermediate state changes, so reordering has no fixed point.
• TauCeti.GridRectangleDecomposition.isEmpty_commute_first and TauCeti.GridRectangleDecomposition.isEmpty_commute_second: reordering a decomposition into two empty rectangles again gives two empty rectangles.

References

This supplies the disjoint-side orientation step for TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.3, "The complexes and ∂² = 0". The decomposition pairing follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6.

def TauCeti.GridRectangleDecomposition.HasDisjointSides {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : Prop

The two rectangles in a decomposition use disjoint pairs of side columns.

Equations

• D.HasDisjointSides = Disjoint D.first.sideColumns D.second.sideColumns

theorem TauCeti.GridRectangleDecomposition.hasDisjointSides_iff {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) : D.HasDisjointSides ↔ D.first.left ≠ D.second.left ∧ D.first.left ≠ D.second.right ∧ D.first.right ≠ D.second.left ∧ D.first.right ≠ D.second.right

Disjointness of the two side-column pairs, expanded into the four cross-inequalities.

def TauCeti.GridRectangleDecomposition.commute {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : GridRectangleDecomposition x z

Reorder two rectangle moves whose pairs of side columns are disjoint.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GridRectangleDecomposition.commute_first_left {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : (D.commute h).first.left = D.second.left

The initial side of the first reordered rectangle.

@[simp]

theorem TauCeti.GridRectangleDecomposition.commute_first_right {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : (D.commute h).first.right = D.second.right

The terminal side of the first reordered rectangle.

@[simp]

theorem TauCeti.GridRectangleDecomposition.commute_second_left {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : (D.commute h).second.left = D.first.left

The initial side of the second reordered rectangle.

@[simp]

theorem TauCeti.GridRectangleDecomposition.commute_second_right {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : (D.commute h).second.right = D.first.right

The terminal side of the second reordered rectangle.

@[simp]

theorem TauCeti.GridRectangleDecomposition.commute_middle {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : (D.commute h).middle = GridState.swapColumns D.second.left D.second.right x

The intermediate state of the reordered decomposition.

@[simp]

theorem TauCeti.GridRectangleDecomposition.commute_first_toGridRectangle {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : (D.commute h).first.toGridRectangle = D.second.toGridRectangle

Reordering exchanges the first toroidal rectangle with the old second rectangle.

@[simp]

theorem TauCeti.GridRectangleDecomposition.commute_second_toGridRectangle {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : (D.commute h).second.toGridRectangle = D.first.toGridRectangle

Reordering exchanges the second toroidal rectangle with the old first rectangle.

@[simp]

theorem TauCeti.GridRectangleDecomposition.avoidsMarkings_commute_first_iff {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) (G : GridDiagram n) : (D.commute h).first.AvoidsMarkings G ↔ D.second.AvoidsMarkings G

Reordering preserves the marking-avoidance condition on the first domain.

@[simp]

theorem TauCeti.GridRectangleDecomposition.avoidsMarkings_commute_second_iff {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) (G : GridDiagram n) : (D.commute h).second.AvoidsMarkings G ↔ D.first.AvoidsMarkings G

Reordering preserves the marking-avoidance condition on the second domain.

theorem TauCeti.GridRectangleDecomposition.hasDisjointSides_commute {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : (D.commute h).HasDisjointSides

The reordered decomposition again has disjoint side-column pairs.

@[simp]

theorem TauCeti.GridRectangleDecomposition.commute_commute {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : (D.commute h).commute ⋯ = D

Reordering two disjoint-side rectangle decompositions twice recovers the original decomposition.

theorem TauCeti.GridRectangleDecomposition.commute_middle_ne {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : (D.commute h).middle ≠ D.middle

The reordered decomposition passes through a different intermediate state.

theorem TauCeti.GridRectangleDecomposition.commute_ne {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : D.commute h ≠ D

Reordering never fixes a decomposition with disjoint side columns: its intermediate state changes.

theorem TauCeti.GridRectangleDecomposition.commute_middle_mem_twoStepColumnSwapIntermediates {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : (D.commute h).middle ∈ x.twoStepColumnSwapIntermediates z

The reordered intermediate state belongs to the endpoint pair's two-step intermediate set.

Reordering preserves emptiness

theorem TauCeti.GridRectangleDecomposition.isEmpty_commute_first {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) (h₁ : D.first.IsEmpty) (h₂ : D.second.IsEmpty) : (D.commute h).first.IsEmpty

Reordering two empty rectangles with disjoint side columns leaves the new first rectangle empty.

With isEmpty_commute_second, this makes reordering an operation on decompositions into empty rectangles, which is the form the rectangle juxtaposition argument consumes.

theorem TauCeti.GridRectangleDecomposition.isEmpty_commute_second {n : ℕ} {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) (h₁ : D.first.IsEmpty) (h₂ : D.second.IsEmpty) : (D.commute h).second.IsEmpty

Reordering two empty rectangles with disjoint side columns leaves the new second rectangle empty.

This is the companion of isEmpty_commute_first for the other rectangle of the reordered decomposition.