Off-diagonal unpaired hexagon composites have a mixed-side overlap

On the left-hand side ∂ ∘ H + H ∘ ∂ of the homotopy equation of a column commutation, a counted hexagon composite whose two rectangles share exactly one side column cancels against its recut whenever that recut is again a counted composite (Homotopy.Recut). This file shows that this always happens when the shared column is initial for both rectangles or terminal for both. Consequently, off the diagonal, every unpaired composite has a mixed-side overlap.

The argument has two independent parts.

• Markings. A counted composite covers exactly one X-marking, that of the column its hexagon cuts away. If a repartition of its domain into two empty rectangles has a piece with the shape of a commutation hexagon, that piece covers the X-marking of its own cut-away column, which must therefore be the single one. Its hexagon carries no X-marking, the other piece carries none either, and the repartition is a counted composite (GridDiagram.exists_toRectangleDecomposition_eq_of_isRepartition, an instance of GridDiagram.exists_toRectangleDecomposition_eq_of_isRepartition_of_mem_iff via GridDiagram.mem_commutationHexagons_iff_XSet_inter_eq).
• Shapes. For a same-side overlap, the recut cuts the L-shaped union the other way, and one of its pieces again underlies a commutation hexagon of the same kind (GridHexagonCompositeDecomposition.exists_hexagon_of_isRecut).

Main results

• TauCeti.GridDiagram.exists_toRectangleDecomposition_eq_of_isRepartition: a repartition of a counted composite into empty rectangles, one of which underlies a commutation hexagon, underlies a counted composite.
• TauCeti.GridDiagram.exists_isRecut_of_hasSameSideOverlap: the recut of a counted composite with a same-side overlap underlies a counted composite.
• TauCeti.GridDiagram.hasMixedSideOverlap_of_mem_unpairedHexagonComposites: off the diagonal, every unpaired composite has a mixed-side overlap.

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).

Promoting a repartition to a counted composite

theorem TauCeti.GridDiagram.mem_hexagonCompositeDecompositions_iff_mem_disjSum {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (F : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z) : F ∈ G.hexagonCompositeDecompositions C x z ↔ F ∈ (GridTwoStepDecomposition.decompositionsOf (G.commutationHexagons C) G.unblockedRectangles x z).disjSum (GridTwoStepDecomposition.decompositionsOf G.unblockedRectangles (G.commutationHexagons C) x z)

The counted composites are the counted hexagons and unblocked rectangles, in either order.

theorem TauCeti.GridDiagram.exists_toRectangleDecomposition_eq_of_isRepartition {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} {F : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z} (hF : F ∈ G.hexagonCompositeDecompositions C x z) {E : GridRectangleDecomposition x z} (hrep : F.toRectangleDecomposition.IsRepartition E) (hfirst : E.first.IsEmpty) (hsecond : E.second.IsEmpty) (hhex : (∃ (P : GridCommutationHexagonBetween C.column C.turnRow C.oppositeTurnRow x E.middle), P.toGridRectangleBetween = E.first) ∨ ∃ (P : GridCommutationHexagonBetween C.column C.turnRow C.oppositeTurnRow E.middle z), P.toGridRectangleBetween = E.second) : ∃ F' ∈ G.hexagonCompositeDecompositions C x z, F'.toRectangleDecomposition = E

A repartition of a counted composite into two empty rectangles, one of which underlies a commutation hexagon, is the underlying rectangle decomposition of a counted composite.

Same-side composites are paired

theorem TauCeti.GridDiagram.exists_isRecut_of_hasSameSideOverlap {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} {F : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z} (hF : F ∈ G.hexagonCompositeDecompositions C x z) (hsame : F.toRectangleDecomposition.HasSameSideOverlap) : ∃ F' ∈ G.hexagonCompositeDecompositions C x z, F.toRectangleDecomposition.IsRecut F'.toRectangleDecomposition

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.

theorem TauCeti.GridDiagram.hasMixedSideOverlap_of_mem_unpairedHexagonComposites {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (hzx : z ≠ x) {F : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z} (hF : F ∈ G.unpairedHexagonComposites C x z) : F.toRectangleDecomposition.HasMixedSideOverlap

Off the diagonal, every unpaired hexagon composite has a mixed-side overlap: its two rectangles share exactly one side column, initial for one and terminal for the other.