Recutting two terminal-side commutation pentagons

Consider a counted forward pentagon and a counted reverse pentagon, both turning on their terminal side, with distinct initial sides. Their union is an L-shaped domain, which can also be cut along its other internal edge.

• When the first initial side lies strictly between the second initial side and the common terminal side, the recut is a rectangle followed by a terminal-side hexagon.
• When the second initial side lies strictly between the first initial side and the common terminal side, the recut is a terminal-side hexagon followed by a rectangle.

In both cases the two turn points lie in order on the hexagon, the resulting composite is counted, has the same weight as the pentagon pair, and has no hexagon--rectangle recut partner. Hence every counted off-diagonal pair of terminal-side pentagons is matched with exactly one unpaired hexagon composite of the same weight.

Main results

• GridDiagram.recutTerminalPentagonPair and GridDiagram.recutTerminalPentagonPairHexagonRectangle: the recuts in the two branches.
• GridDiagram.recutTerminalPentagonPair_toRectangleDecomposition and GridDiagram.recutTerminalPentagonPairHexagonRectangle_toRectangleDecomposition: their underlying rectangle decompositions are the canonical recut.
• GridDiagram.recutTerminalPentagonPair_mem_rectangleHexagonDecompositions and GridDiagram.recutTerminalPentagonPairHexagonRectangle_mem_hexagonRectangleDecompositions: countedness.
• GridDiagram.rectangleHexagonWeight_recutTerminalPentagonPair and GridDiagram.hexagonRectangleWeight_recutTerminalPentagonPairHexagonRectangle: weight preservation.
• GridDiagram.recutTerminalPentagonPair_mem_unpairedHexagonComposites and GridDiagram.recutTerminalPentagonPairHexagonRectangle_mem_unpairedHexagonComposites: the resulting composites have no counted hexagon recut partner.
• GridDiagram.existsUnique_unpairedHexagonComposite_of_terminalPentagonPair: a counted pair of terminal-side pentagons with distinct initial sides has a unique unpaired hexagon-composite recut, of the same weight.

References

Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.1, Proposition 3.2 (arXiv:math/0610559), and Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.1. The underlying rectangle recuts are GridRectangleDecomposition.recut_geometry_of_right_eq_right_of_mem_cIoo and GridRectangleDecomposition.recut_geometry_of_right_eq_right_of_second_left_mem_cIoo.

noncomputable def TauCeti.GridDiagram.recutTerminalPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : P.left ∈ Grid.cIoo Q.left ((finRotate n) C.column)) (hp : P.IsEmpty) (hq : Q.IsEmpty) : GridRectangleHexagonDecomposition C.column C.turnRow C.oppositeTurnRow x z

Recut two terminal-side pentagons when the first initial side lies strictly inside the second column interval. The second piece is a terminal-side hexagon containing both turns.

@[simp]

theorem TauCeti.GridDiagram.recutTerminalPentagonPair_toRectangleDecomposition {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : P.left ∈ Grid.cIoo Q.left ((finRotate n) C.column)) (hp : P.IsEmpty) (hq : Q.IsEmpty) : let D := { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween }; have hone := ⋯; (G.recutTerminalPentagonPair C P Q hcol hp hq).toRectangleDecomposition = D.recut hone hp hq

Forgetting the two turns in the promoted composite gives the canonical rectangle recut.

theorem TauCeti.GridDiagram.isRecut_recutTerminalPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : P.left ∈ Grid.cIoo Q.left ((finRotate n) C.column)) (hp : P.IsEmpty) (hq : Q.IsEmpty) : GridRectangleDecomposition.IsRecut { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } (G.recutTerminalPentagonPair C P Q hcol hp hq).toRectangleDecomposition

The promoted composite and the pentagon pair are the two cuts of the same domain.

theorem TauCeti.GridDiagram.recutTerminalPentagonPair_hexagon {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : P.left ∈ Grid.cIoo Q.left ((finRotate n) C.column)) (hp : P.IsEmpty) (hq : Q.IsEmpty) : ∃ (H : GridHexagonBetween C.column C.oppositeTurnRow C.turnRow (G.recutTerminalPentagonPair C P Q hcol hp hq).middle z), (G.recutTerminalPentagonPair C P Q hcol hp hq).hexagon = Sum.inl H

The hexagon in this recut turns on its terminal side.

theorem TauCeti.GridDiagram.recutTerminalPentagonPair_mem_rectangleHexagonDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : P.left ∈ Grid.cIoo Q.left ((finRotate n) C.column)) (hP : P ∈ G.pentagons C.toColumnTurn x y) (hQ : Q ∈ (swapColumns C.column ((finRotate n) C.column) G).pentagons C.reverse.toColumnTurn y z) : G.recutTerminalPentagonPair C P Q hcol ⋯ ⋯ ∈ G.rectangleHexagonDecompositions C x z

The recut of a counted terminal-side pentagon pair is a counted rectangle--hexagon composite for this order of the initial columns.

@[simp]

theorem TauCeti.GridDiagram.rectangleHexagonWeight_recutTerminalPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : P.left ∈ Grid.cIoo Q.left ((finRotate n) C.column)) (hp : P.IsEmpty) (hq : Q.IsEmpty) : G.rectangleHexagonWeight C R (G.recutTerminalPentagonPair C P Q hcol hp hq) = G.pentagonPairWeight C R { middle := y, first := Sum.inl P, second := Sum.inl Q }

Recutting this terminal-side pentagon pair preserves its polynomial weight, over any commutative semiring.

theorem TauCeti.GridDiagram.recutTerminalPentagonPair_mem_unpairedHexagonComposites {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : P.left ∈ Grid.cIoo Q.left ((finRotate n) C.column)) (hP : P ∈ G.pentagons C.toColumnTurn x y) (hQ : Q ∈ (swapColumns C.column ((finRotate n) C.column) G).pentagons C.reverse.toColumnTurn y z) : Sum.inr (G.recutTerminalPentagonPair C P Q hcol ⋯ ⋯) ∈ G.unpairedHexagonComposites C x z

The resulting counted composite is unpaired: its only rectangle recut consists of the two pentagons, each of which contains only one of the two turn points.

The complementary branch

noncomputable def TauCeti.GridDiagram.recutTerminalPentagonPairHexagonRectangle {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : Q.left ∈ Grid.cIoo P.left ((finRotate n) C.column)) (hp : P.IsEmpty) (hq : Q.IsEmpty) : GridHexagonRectangleDecomposition C.column C.turnRow C.oppositeTurnRow x z

Recut two empty terminal-side pentagons when the second initial side lies strictly inside the first column interval. The first piece is a terminal-side hexagon containing both turns.

@[simp]

theorem TauCeti.GridDiagram.recutTerminalPentagonPairHexagonRectangle_toRectangleDecomposition {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : Q.left ∈ Grid.cIoo P.left ((finRotate n) C.column)) (hp : P.IsEmpty) (hq : Q.IsEmpty) : (G.recutTerminalPentagonPairHexagonRectangle C P Q hcol hp hq).toRectangleDecomposition = GridRectangleDecomposition.recut { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } ⋯ hp hq

Forgetting the two turns in this composite gives the canonical rectangle recut.

theorem TauCeti.GridDiagram.isRecut_recutTerminalPentagonPairHexagonRectangle {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : Q.left ∈ Grid.cIoo P.left ((finRotate n) C.column)) (hp : P.IsEmpty) (hq : Q.IsEmpty) : GridRectangleDecomposition.IsRecut { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } (G.recutTerminalPentagonPairHexagonRectangle C P Q hcol hp hq).toRectangleDecomposition

This composite and the pentagon pair are the two cuts of the same domain.

theorem TauCeti.GridDiagram.recutTerminalPentagonPairHexagonRectangle_hexagon {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : Q.left ∈ Grid.cIoo P.left ((finRotate n) C.column)) (hp : P.IsEmpty) (hq : Q.IsEmpty) : ∃ (H : GridHexagonBetween C.column C.oppositeTurnRow C.turnRow x (G.recutTerminalPentagonPairHexagonRectangle C P Q hcol hp hq).middle), (G.recutTerminalPentagonPairHexagonRectangle C P Q hcol hp hq).hexagon = Sum.inl H

The hexagon in this recut turns on its terminal side.

theorem TauCeti.GridDiagram.recutTerminalPentagonPairHexagonRectangle_mem_hexagonRectangleDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : Q.left ∈ Grid.cIoo P.left ((finRotate n) C.column)) (hP : P ∈ G.pentagons C.toColumnTurn x y) (hQ : Q ∈ (swapColumns C.column ((finRotate n) C.column) G).pentagons C.reverse.toColumnTurn y z) : G.recutTerminalPentagonPairHexagonRectangle C P Q hcol ⋯ ⋯ ∈ G.hexagonRectangleDecompositions C x z

The recut of a counted terminal-side pentagon pair is a counted hexagon--rectangle composite for this order of the initial columns.

@[simp]

theorem TauCeti.GridDiagram.hexagonRectangleWeight_recutTerminalPentagonPairHexagonRectangle {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : Q.left ∈ Grid.cIoo P.left ((finRotate n) C.column)) (hp : P.IsEmpty) (hq : Q.IsEmpty) : G.hexagonRectangleWeight C R (G.recutTerminalPentagonPairHexagonRectangle C P Q hcol hp hq) = G.pentagonPairWeight C R { middle := y, first := Sum.inl P, second := Sum.inl Q }

Recutting this terminal-side pentagon pair preserves its polynomial weight, over any commutative semiring.

theorem TauCeti.GridDiagram.recutTerminalPentagonPairHexagonRectangle_mem_unpairedHexagonComposites {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hcol : Q.left ∈ Grid.cIoo P.left ((finRotate n) C.column)) (hP : P ∈ G.pentagons C.toColumnTurn x y) (hQ : Q ∈ (swapColumns C.column ((finRotate n) C.column) G).pentagons C.reverse.toColumnTurn y z) : Sum.inl (G.recutTerminalPentagonPairHexagonRectangle C P Q hcol ⋯ ⋯) ∈ G.unpairedHexagonComposites C x z

This counted composite is unpaired: its only rectangle recut consists of the two pentagons, each of which contains only one of the two turn points.

The matching

theorem TauCeti.GridDiagram.existsUnique_unpairedHexagonComposite_of_terminalPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hP : P ∈ G.pentagons C.toColumnTurn x y) (hQ : Q ∈ (swapColumns C.column ((finRotate n) C.column) G).pentagons C.reverse.toColumnTurn y z) (hne : P.left ≠ Q.left) : ∃! F : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z, F ∈ G.unpairedHexagonComposites C x z ∧ GridRectangleDecomposition.IsRecut { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } F.toRectangleDecomposition ∧ G.hexagonCompositeWeight C R F = G.pentagonPairWeight C R { middle := y, first := Sum.inl P, second := Sum.inl Q }

A counted pair of terminal-side pentagons, for an actual commutation and its reverse, with distinct initial sides has a unique unpaired hexagon-composite recut, and their polynomial weights agree.