Hexagon shapes in a same-side recut

A hexagon composite F : GridHexagonCompositeDecomposition a s s' x z is a commutation hexagon followed by a rectangle, or a rectangle followed by a commutation hexagon. The left-hand sides of the homotopy equations of a column commutation and of a crossing change both count such composites, with different conditions on the markings. When the two rectangles of F are empty and share exactly one side column, initial for both or terminal for both, the recut from the proof of ∂² = 0 cuts their L-shaped union the other way. This file shows that one piece of that recut again underlies a commutation hexagon for the same column and rows.

The recut keeps the outer sides of the original rectangles in the same position, and the rows of each of its pieces are either the rows of the corresponding original rectangle or the union of both row intervals. The replaced grid line is a side of the hexagon of F. If it is that hexagon's outer side, the corresponding recut piece keeps it; if it is the common side, the recut piece spanning both row intervals has it. In both cases the two turn rows remain on that side, in the same order, so this piece has the shape of a commutation hexagon of the same kind.

Whether that hexagon is counted depends on the markings. Both homotopies count a hexagon exactly when its rectangle is empty and carries only the X-marking of the column the hexagon cuts away, which that rectangle always covers. For any family of hexagons counted this way, a counted composite covers exactly one X-marking, so a repartition of its domain into two empty rectangles, one of which underlies a hexagon, is again a counted composite; in particular so is the recut of a same-side overlap. Each homotopy instantiates this with its own counted hexagons.

Main results

• TauCeti.GridHexagonCompositeDecomposition.exists_hexagon_of_isRecut: for a hexagon composite whose two empty rectangles have a same-side overlap, one piece of its recut underlies a commutation hexagon.
• TauCeti.GridDiagram.isEmpty_of_mem_disjSum_of_mem_iff: for a hexagon family counted by its markings, both rectangles of a counted composite are empty.
• TauCeti.GridDiagram.exists_toRectangleDecomposition_eq_of_isRepartition_of_mem_iff: for a hexagon family counted by its markings, a repartition of a counted composite into empty rectangles, one of which underlies a hexagon, underlies a counted composite.
• TauCeti.GridDiagram.exists_isRecut_of_hasSameSideOverlap_of_mem_iff: for such a family, the recut of a counted composite with a same-side overlap underlies a counted composite.

References

This is the same-side case of the hexagon--rectangle juxtaposition argument of 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, Proposition 3.2 (arXiv:math/0610559).

theorem TauCeti.GridHexagonCompositeDecomposition.exists_hexagon_of_isRecut {n : ℕ} {a s s' : Fin n} {x z : GridState n} (F : GridHexagonCompositeDecomposition a s s' x z) (hsame : F.toRectangleDecomposition.HasSameSideOverlap) (hfirst : F.toRectangleDecomposition.first.IsEmpty) (hsecond : F.toRectangleDecomposition.second.IsEmpty) {E : GridRectangleDecomposition x z} (hE : F.toRectangleDecomposition.IsRecut E) : (∃ (P : GridCommutationHexagonBetween a s s' x E.middle), P.toGridRectangleBetween = E.first) ∨ ∃ (P : GridCommutationHexagonBetween a s s' E.middle z), P.toGridRectangleBetween = E.second

If the two rectangles of a hexagon composite are empty and share exactly one side column, initial for both or terminal for both, then one piece of the recut of their union underlies a commutation hexagon for the same column and rows.

Promoting a repartition to a counted composite

Both homotopies count a hexagon exactly when its rectangle is empty and carries only the X-marking of its cut-away column, which that rectangle always covers. The argument below is stated for any family of hexagons counted this way, with the composites counted as a counted hexagon and an unblocked rectangle in either order.

theorem TauCeti.GridDiagram.exists_toRectangleDecomposition_eq_of_isRepartition_of_mem_iff {n : ℕ} {G : GridDiagram n} {a s s' : Fin n} {H : (u v : GridState n) → Finset (GridCommutationHexagonBetween a s s' u v)} (hH : ∀ {u v : GridState n} (P : GridCommutationHexagonBetween a s s' u v), P ∈ H u v ↔ P.toGridRectangleBetween.IsEmpty ∧ G.XSet ∩ P.toGridRectangleBetween.toGridRectangle.coveredSquares = {(P.cutColumn, G.X.toPerm P.cutColumn)}) (hcut : ∀ {u v : GridState n} (P : GridCommutationHexagonBetween a s s' u v), (P.cutColumn, G.X.toPerm P.cutColumn) ∈ P.toGridRectangleBetween.toGridRectangle.coveredSquares) {x z : GridState n} {F : GridHexagonCompositeDecomposition a s s' x z} (hF : F ∈ (GridTwoStepDecomposition.decompositionsOf H G.unblockedRectangles x z).disjSum (GridTwoStepDecomposition.decompositionsOf G.unblockedRectangles H x z)) {E : GridRectangleDecomposition x z} (hrep : F.toRectangleDecomposition.IsRepartition E) (hfirst : E.first.IsEmpty) (hsecond : E.second.IsEmpty) (hhex : (∃ (P : GridCommutationHexagonBetween a s s' x E.middle), P.toGridRectangleBetween = E.first) ∨ ∃ (P : GridCommutationHexagonBetween a s s' E.middle z), P.toGridRectangleBetween = E.second) : ∃ F' ∈ (GridTwoStepDecomposition.decompositionsOf H G.unblockedRectangles x z).disjSum (GridTwoStepDecomposition.decompositionsOf G.unblockedRectangles H x z), F'.toRectangleDecomposition = E

For a hexagon family counted by its markings, a repartition of a counted composite into two empty rectangles, one of which underlies a hexagon, is the underlying rectangle decomposition of a counted composite.

theorem TauCeti.GridDiagram.isEmpty_of_mem_disjSum_of_mem_iff {n : ℕ} {G : GridDiagram n} {a s s' : Fin n} {H : (u v : GridState n) → Finset (GridCommutationHexagonBetween a s s' u v)} (hH : ∀ {u v : GridState n} (P : GridCommutationHexagonBetween a s s' u v), P ∈ H u v ↔ P.toGridRectangleBetween.IsEmpty ∧ G.XSet ∩ P.toGridRectangleBetween.toGridRectangle.coveredSquares = {(P.cutColumn, G.X.toPerm P.cutColumn)}) {x z : GridState n} {F : GridHexagonCompositeDecomposition a s s' x z} (hF : F ∈ (GridTwoStepDecomposition.decompositionsOf H G.unblockedRectangles x z).disjSum (GridTwoStepDecomposition.decompositionsOf G.unblockedRectangles H x z)) : F.toRectangleDecomposition.first.IsEmpty ∧ F.toRectangleDecomposition.second.IsEmpty

For a hexagon family counted by its markings, both rectangles of a counted composite are empty.

theorem TauCeti.GridDiagram.exists_isRecut_of_hasSameSideOverlap_of_mem_iff {n : ℕ} {G : GridDiagram n} {a s s' : Fin n} {H : (u v : GridState n) → Finset (GridCommutationHexagonBetween a s s' u v)} (hH : ∀ {u v : GridState n} (P : GridCommutationHexagonBetween a s s' u v), P ∈ H u v ↔ P.toGridRectangleBetween.IsEmpty ∧ G.XSet ∩ P.toGridRectangleBetween.toGridRectangle.coveredSquares = {(P.cutColumn, G.X.toPerm P.cutColumn)}) (hcut : ∀ {u v : GridState n} (P : GridCommutationHexagonBetween a s s' u v), (P.cutColumn, G.X.toPerm P.cutColumn) ∈ P.toGridRectangleBetween.toGridRectangle.coveredSquares) {x z : GridState n} {F : GridHexagonCompositeDecomposition a s s' x z} (hF : F ∈ (GridTwoStepDecomposition.decompositionsOf H G.unblockedRectangles x z).disjSum (GridTwoStepDecomposition.decompositionsOf G.unblockedRectangles H x z)) (hsame : F.toRectangleDecomposition.HasSameSideOverlap) : ∃ F' ∈ (GridTwoStepDecomposition.decompositionsOf H G.unblockedRectangles x z).disjSum (GridTwoStepDecomposition.decompositionsOf G.unblockedRectangles H x z), F.toRectangleDecomposition.IsRecut F'.toRectangleDecomposition

For a hexagon family counted by its markings, the recut of a counted composite whose two rectangles share a side column with the same orientation, initial for both or terminal for both, is the underlying rectangle decomposition of a counted composite.