Cancelling disjoint hexagon--rectangle terms

In the commutation homotopy equation, a hexagon followed by a rectangle and a rectangle followed by a hexagon contribute to the same coefficient. If the two pairs of vertical sides are disjoint, the underlying rectangles can be applied in the opposite order. Their toroidal domains are unchanged, so the hexagon retains both intersection rows and its turn-side kind. Emptiness, X-avoidance and the O-monomial weight are preserved.

This gives a weight-preserving bijection for both kinds of commutation hexagon at once. In characteristic two, the two disjoint-side sums cancel. Consequently the hexagon side of the homotopy equation can be restricted to domains sharing a vertical side.

References

Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.1, and Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.1 (arXiv:math/0610559).

The reordering and emptiness proofs reuse the rectangle pairing in TauCeti.KnotTheory.Grid.Differential.Square.Disjoint.

def TauCeti.GridRectangleHexagonDecomposition.commute {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridRectangleHexagonDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : GridHexagonRectangleDecomposition a s s' x z

Apply a rectangle and a commutation hexagon in the opposite order when their vertical side pairs are disjoint.

@[simp]

theorem TauCeti.GridRectangleHexagonDecomposition.commute_toRectangleDecomposition {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridRectangleHexagonDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : (D.commute h).toRectangleDecomposition = D.toRectangleDecomposition.commute h

Forgetting the turns after reordering agrees with rectangle reordering.

@[simp]

theorem TauCeti.GridRectangleHexagonDecomposition.commute_middle {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridRectangleHexagonDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : (D.commute h).middle = GridState.swapColumns D.second.toGridRectangleBetween.left D.second.toGridRectangleBetween.right x

The intermediate state after reordering is obtained by applying the hexagon first.

theorem TauCeti.GridRectangleHexagonDecomposition.hasDisjointSides_commute {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridRectangleHexagonDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : (D.commute h).toRectangleDecomposition.HasDisjointSides

Reordering preserves disjointness of the side pairs.

@[simp]

theorem TauCeti.GridRectangleHexagonDecomposition.commute_hexagon_coveredSquares {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridRectangleHexagonDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : (D.commute h).first.coveredSquares = D.second.coveredSquares

Reordering preserves the squares covered by the hexagon.

@[simp]

theorem TauCeti.GridRectangleHexagonDecomposition.commute_rectangle_toGridRectangle {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridRectangleHexagonDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : (D.commute h).second.toGridRectangle = D.first.toGridRectangle

Reordering preserves the toroidal rectangle.

def TauCeti.GridHexagonRectangleDecomposition.commute {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridHexagonRectangleDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : GridRectangleHexagonDecomposition a s s' x z

Apply a commutation hexagon and a rectangle in the opposite order when their vertical side pairs are disjoint.

@[simp]

theorem TauCeti.GridHexagonRectangleDecomposition.commute_toRectangleDecomposition {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridHexagonRectangleDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : (D.commute h).toRectangleDecomposition = D.toRectangleDecomposition.commute h

Forgetting the turns after reordering agrees with rectangle reordering.

@[simp]

theorem TauCeti.GridHexagonRectangleDecomposition.commute_middle {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridHexagonRectangleDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : (D.commute h).middle = GridState.swapColumns D.second.left D.second.right x

The intermediate state after reordering is obtained by applying the rectangle first.

theorem TauCeti.GridHexagonRectangleDecomposition.hasDisjointSides_commute {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridHexagonRectangleDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : (D.commute h).toRectangleDecomposition.HasDisjointSides

Reordering preserves disjointness of the side pairs.

@[simp]

theorem TauCeti.GridHexagonRectangleDecomposition.commute_hexagon_coveredSquares {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridHexagonRectangleDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : (D.commute h).second.coveredSquares = D.first.coveredSquares

Reordering preserves the squares covered by the hexagon.

@[simp]

theorem TauCeti.GridHexagonRectangleDecomposition.commute_rectangle_toGridRectangle {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridHexagonRectangleDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : (D.commute h).first.toGridRectangle = D.second.toGridRectangle

Reordering preserves the toroidal rectangle.

@[simp]

theorem TauCeti.GridHexagonRectangleDecomposition.commute_commute {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridHexagonRectangleDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : (D.commute h).commute ⋯ = D

Reordering a disjoint hexagon--rectangle domain twice recovers it.

@[simp]

theorem TauCeti.GridRectangleHexagonDecomposition.commute_commute {n : ℕ} {a s s' : Fin n} {x z : GridState n} (D : GridRectangleHexagonDecomposition a s s' x z) (h : D.toRectangleDecomposition.HasDisjointSides) : (D.commute h).commute ⋯ = D

Reordering a disjoint rectangle--hexagon domain twice recovers it.

theorem TauCeti.GridDiagram.commute_mem_hexagonRectangleDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (D : GridRectangleHexagonDecomposition C.column C.turnRow C.oppositeTurnRow x z) (h : D.toRectangleDecomposition.HasDisjointSides) (hD : D ∈ G.rectangleHexagonDecompositions C x z) : D.commute h ∈ G.hexagonRectangleDecompositions C x z

Reordering a counted disjoint rectangle--hexagon domain gives a counted hexagon--rectangle domain.

theorem TauCeti.GridDiagram.commute_mem_rectangleHexagonDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (D : GridHexagonRectangleDecomposition C.column C.turnRow C.oppositeTurnRow x z) (h : D.toRectangleDecomposition.HasDisjointSides) (hD : D ∈ G.hexagonRectangleDecompositions C x z) : D.commute h ∈ G.rectangleHexagonDecompositions C x z

Reordering a counted disjoint hexagon--rectangle domain gives a counted rectangle--hexagon domain.

theorem TauCeti.GridDiagram.hexagonRectangleWeight_commute_rectangleHexagon {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridRectangleHexagonDecomposition C.column C.turnRow C.oppositeTurnRow x z) (h : D.toRectangleDecomposition.HasDisjointSides) : G.hexagonRectangleWeight C R (D.commute h) = G.rectangleHexagonWeight C R D

Reordering a disjoint rectangle--hexagon domain preserves its monomial weight.

theorem TauCeti.GridDiagram.rectangleHexagonWeight_commute_hexagonRectangle {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridHexagonRectangleDecomposition C.column C.turnRow C.oppositeTurnRow x z) (h : D.toRectangleDecomposition.HasDisjointSides) : G.rectangleHexagonWeight C R (D.commute h) = G.hexagonRectangleWeight C R D

Reordering a disjoint hexagon--rectangle domain preserves its monomial weight.

theorem TauCeti.GridDiagram.sum_rectangleHexagonWeight_disjoint_eq_sum_hexagonRectangleWeight_disjoint {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] (x z : GridState n) : ∑ D ∈ G.rectangleHexagonDecompositions C x z with D.toRectangleDecomposition.HasDisjointSides, G.rectangleHexagonWeight C R D = ∑ D ∈ G.hexagonRectangleDecompositions C x z with D.toRectangleDecomposition.HasDisjointSides, G.hexagonRectangleWeight C R D

The disjoint rectangle--hexagon and hexagon--rectangle contributions to the commutation homotopy equation have the same total weight, for both hexagon kinds.

theorem TauCeti.GridDiagram.sum_hexagonRectangleWeight_add_sum_rectangleHexagonWeight_eq_overlap {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] [CharP R 2] (x z : GridState n) : ∑ D ∈ G.hexagonRectangleDecompositions C x z, G.hexagonRectangleWeight C R D + ∑ D ∈ G.rectangleHexagonDecompositions C x z, G.rectangleHexagonWeight C R D = ∑ D ∈ G.hexagonRectangleDecompositions C x z with ¬D.toRectangleDecomposition.HasDisjointSides, G.hexagonRectangleWeight C R D + ∑ D ∈ G.rectangleHexagonDecompositions C x z with ¬D.toRectangleDecomposition.HasDisjointSides, G.rectangleHexagonWeight C R D

In characteristic two, only hexagon--rectangle domains sharing a side contribute to the left-hand side of the commutation homotopy equation.

theorem TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq_iff_overlap {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] [CharP R 2] : (∀ (c : GridChainMinus R n), (G.unblockedDifferential R) ((G.commutationHomotopy R C) c) + (G.commutationHomotopy R C) ((G.unblockedDifferential R) c) = c + ((swapColumns C.column ((finRotate n) C.column) G).commutationMap R C.reverse.toColumnTurn) ((G.commutationMap R C.toColumnTurn) c)) ↔ ∀ (x z : GridState n), ∑ D ∈ G.hexagonRectangleDecompositions C x z with ¬D.toRectangleDecomposition.HasDisjointSides, G.hexagonRectangleWeight C R D + ∑ D ∈ G.rectangleHexagonDecompositions C x z with ¬D.toRectangleDecomposition.HasDisjointSides, G.rectangleHexagonWeight C R D = (if x = z then 1 else 0) + ∑ D ∈ G.pentagonPairDecompositions C x z, G.pentagonPairWeight C R D

In characteristic two, the commutation homotopy equation is equivalent to the coefficient identity restricted to hexagon--rectangle domains sharing a vertical side.