Removing mixed-side pentagon pairs from the commutation homotopy equation

Off the diagonal, a counted pair of a forward and a reverse commutation pentagon turning on opposite sides of the replaced grid line has the same underlying rectangle decomposition as a unique unpaired hexagon composite, and the two have the same weight (Homotopy.Mixed.Pair). Since a pentagon pair is determined by its underlying rectangles, this matches the mixed-side pairs bijectively with their image, which therefore has the same total weight.

That image is disjoint from the recut image of the same-side pairs removed in Homotopy.SameSide. Every rectangle of a commutation pentagon has the replaced grid line as a side, so this line is the unique common side of a mixed-side pair. A same-side pair shares it as an initial or as a terminal side of both rectangles, and the recut of such a decomposition never has the original common column as a common side.

Removing both families, the homotopy equation ∂ ∘ H + H ∘ ∂ = 1 + Ψ ∘ Φ in characteristic two becomes the statement that, off the diagonal, the unpaired hexagon composites lying in neither partner image have total weight zero. No classification of these residual composites is assumed here.

Main results

• TauCeti.GridDiagram.sum_pentagonPairWeight_mixedSide_eq_sum_partners: off the diagonal, the mixed-side pentagon pairs and their hexagon-composite image have equal total weight.
• TauCeti.GridDiagram.disjoint_sameSidePentagonPartners_mixedSidePentagonPartners: the two partner images are disjoint.
• TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq_iff_sum_residual_eq_zero: in characteristic two, the homotopy equation holds exactly when the residual unpaired composites have total weight zero off the diagonal.

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 mixed-side pentagon pairs

noncomputable def TauCeti.GridDiagram.mixedSidePentagonPairs {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : Finset (GridPentagonPairDecomposition C.column C.turnRow C.reverse.column C.reverse.turnRow x z)

The counted forward--reverse pentagon pairs whose turns lie on opposite sides of the replaced grid line: terminal--initial and initial--terminal pairs.

@[simp]

theorem TauCeti.GridDiagram.mem_mixedSidePentagonPairs {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (D : GridPentagonPairDecomposition C.column C.turnRow C.reverse.column C.reverse.turnRow x z) : D ∈ G.mixedSidePentagonPairs C x z ↔ D ∈ G.pentagonPairDecompositions C x z ∧ Sum.isLeft D.first ≠ Sum.isLeft D.second

A mixed-side pair is counted and has distinct turn-side indicators.

theorem TauCeti.GridDiagram.mixedSidePentagonPairs_subset {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : G.mixedSidePentagonPairs C x z ⊆ G.pentagonPairDecompositions C x z

Every mixed-side pair is a term of the full round-trip coefficient sum.

theorem TauCeti.GridDiagram.pentagonPairDecompositions_sdiff_sameSidePentagonPairs {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : G.pentagonPairDecompositions C x z \ G.sameSidePentagonPairs C x z = G.mixedSidePentagonPairs C x z

The counted pentagon pairs that do not turn on the same side are exactly the mixed-side pairs.

Matching with unpaired hexagon composites

noncomputable def TauCeti.GridDiagram.mixedSidePentagonPartners {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : Finset (GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z)

The unpaired hexagon composites with the underlying rectangle decomposition of a counted mixed-side pentagon pair. This is their exact image, without a claim that it exhausts the unpaired composites.

@[simp]

theorem TauCeti.GridDiagram.mem_mixedSidePentagonPartners {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (F : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z) : F ∈ G.mixedSidePentagonPartners C x z ↔ F ∈ G.unpairedHexagonComposites C x z ∧ ∃ D ∈ G.mixedSidePentagonPairs C x z, D.toRectangleDecomposition = F.toRectangleDecomposition

Partners are exactly the unpaired composites sharing their underlying rectangle decomposition with a counted mixed-side pair.

theorem TauCeti.GridDiagram.mixedSidePentagonPartners_subset {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (x z : GridState n) : G.mixedSidePentagonPartners C x z ⊆ G.unpairedHexagonComposites C x z

Every partner belongs to the unpaired-composite coefficient sum.

theorem TauCeti.GridDiagram.sum_pentagonPairWeight_mixedSide_eq_sum_partners {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} (hzx : z ≠ x) : ∑ D ∈ G.mixedSidePentagonPairs C x z, G.pentagonPairWeight C R D = ∑ F ∈ G.mixedSidePentagonPartners C x z, G.hexagonCompositeWeight C R F

Off the diagonal, the mixed-side pentagon pairs and their hexagon-composite image have equal total polynomial weight over every commutative semiring.

Disjointness of the two partner images

theorem TauCeti.GridDiagram.disjoint_sameSidePentagonPartners_mixedSidePentagonPartners {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} : Disjoint (G.sameSidePentagonPartners C x z) (G.mixedSidePentagonPartners C x z)

No unpaired composite is both the recut of a same-side pentagon pair and the underlying decomposition of a mixed-side pentagon pair: the replaced grid line is a common side of the latter but not of the former.

The residual coefficient equation

theorem TauCeti.GridDiagram.sum_sdiff_sameSide_eq_sum_sdiff_sameSide_iff_sum_residual_eq_zero {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] [IsCancelAdd R] {x z : GridState n} (hzx : z ≠ x) : ∑ F ∈ G.unpairedHexagonComposites C x z \ G.sameSidePentagonPartners C x z, G.hexagonCompositeWeight C R F = ∑ D ∈ G.pentagonPairDecompositions C x z \ G.sameSidePentagonPairs C x z, G.pentagonPairWeight C R D ↔ ∑ F ∈ (G.unpairedHexagonComposites C x z \ G.sameSidePentagonPartners C x z) \ G.mixedSidePentagonPartners C x z, G.hexagonCompositeWeight C R F = 0

Off the diagonal, after removing the same-side pairs and their recut image, the coefficient equation holds exactly when the unpaired composites in neither partner image have total weight zero.

theorem TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq_iff_sum_residual_eq_zero {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), z ≠ x → ∑ F ∈ (G.unpairedHexagonComposites C x z \ G.sameSidePentagonPartners C x z) \ G.mixedSidePentagonPartners C x z, G.hexagonCompositeWeight C R F = 0

In characteristic two, the commutation homotopy equation ∂ ∘ H + H ∘ ∂ = 1 + Ψ ∘ Φ holds on every chain exactly when, off the diagonal, the unpaired hexagon composites lying neither in the recut image of the same-side pentagon pairs nor in the image of the mixed-side pentagon pairs have total weight zero.