Weights of initial-side pentagon-pair recuts

When two initial-side commutation pentagons recut to a hexagon--rectangle composite in either order, the recut preserves the polynomial weight. In the two columns adjacent to the replaced line, the bigon conditions remove precisely the markings in the column cut away by the hexagon. Away from that column the assertion follows from the rectangle repartition.

For a counted forward pentagon and a counted reverse pentagon in this branch, there is exactly one unpaired hexagon composite recutting their domain. Its weight is the weight of the pentagon pair, including the renaming of the forward coefficient. The two cyclic column orders exhaust the initial--initial pairs with distinct terminal sides. This is their part of the weighted matching needed to compare the two sides of the commutation homotopy equation; the converse assertion that every unpaired composite arises this way is not made here.

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, Proposition 3.2 (arXiv:math/0610559). The weight argument follows the terminal-side counterpart in TauCeti.KnotTheory.Grid.Commutation.Homotopy.TerminalPair.

@[simp]

theorem TauCeti.GridDiagram.hexagonRectangleWeight_recutHexagonRectangle {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x y z : GridState n} (P : GridInitialPentagonBetween C.column C.turnRow x y) (Q : GridInitialPentagonBetween C.column C.oppositeTurnRow y z) (hcol : Q.right ∈ Grid.cIoo ((finRotate n) C.column) P.right) (hp : P.IsEmpty) (hq : Q.IsEmpty) : G.hexagonRectangleWeight C R (P.recutHexagonRectangle Q hcol hp hq) = (MvPolynomial.rename ⇑(Equiv.swap C.column ((finRotate n) C.column))) (G.initialPentagonWeight R C.toColumnTurn P) * ∏ p ∈ Finset.map (Equiv.prodCongr (Equiv.swap C.column ((finRotate n) C.column)) (Equiv.refl (Fin n))).toEmbedding Q.coveredSquares, if p ∈ G.OSet then MvPolynomial.X p.1 else 1

Recutting two initial-side pentagons preserves their weight. The reverse pentagon's squares are read in the original diagram by exchanging the two commuted columns.

@[simp]

theorem TauCeti.GridDiagram.rectangleHexagonWeight_recutRectangleHexagon {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x y z : GridState n} (P : GridInitialPentagonBetween C.column C.turnRow x y) (Q : GridInitialPentagonBetween C.column C.oppositeTurnRow y z) (hcol : P.right ∈ Grid.cIoo ((finRotate n) C.column) Q.right) (hp : P.IsEmpty) (hq : Q.IsEmpty) : G.rectangleHexagonWeight C R (P.recutRectangleHexagon Q hcol hp hq) = (MvPolynomial.rename ⇑(Equiv.swap C.column ((finRotate n) C.column))) (G.initialPentagonWeight R C.toColumnTurn P) * ∏ p ∈ Finset.map (Equiv.prodCongr (Equiv.swap C.column ((finRotate n) C.column)) (Equiv.refl (Fin n))).toEmbedding Q.coveredSquares, if p ∈ G.OSet then MvPolynomial.X p.1 else 1

Recutting two initial-side pentagons in the complementary column order preserves their weight. The reverse pentagon's squares are read in the original diagram by exchanging the two commuted columns.

theorem TauCeti.GridDiagram.existsUnique_unpairedHexagonComposite_of_initialPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x y z : GridState n} (P : GridInitialPentagonBetween C.column C.turnRow x y) (Q : GridInitialPentagonBetween C.reverse.column C.reverse.turnRow y z) (hP : P ∈ G.initialPentagons C.toColumnTurn x y) (hQ : Q ∈ (swapColumns C.column ((finRotate n) C.column) G).initialPentagons C.reverse.toColumnTurn y z) (hne : P.right ≠ Q.right) : ∃! 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.inr P, second := Sum.inr Q }

Every counted pair of initial-side pentagons with distinct terminal sides has a unique unpaired hexagon-composite recut of the same polynomial weight.