The homotopy equation of a grid commutation

Let C be a validated column commutation of a grid diagram G, with commutation map Φ : GC⁻(G) → GC⁻(G'), reverse commutation map Ψ : GC⁻(G') → GC⁻(G) and hexagon-counting map H : GC⁻(G) → GC⁻(G). This file proves the homotopy equation

∂ ∘ H + H ∘ ∂ = 1 + Ψ ∘ Φ

over every commutative semiring of characteristic two.

By the diagonal, disjoint, recut and pentagon-pair cancellations, the equation says that, off the diagonal, every unpaired hexagon composite is the partner of a pentagon pair: either the recut of a same-side pair, or the composite with the rectangles of a mixed-side pair. This is GridDiagram.unblockedDifferential_commutationHomotopy_add_eq_iff_sum_residual_eq_zero. An unpaired composite has a mixed-side overlap (GridDiagram.hasMixedSideOverlap_of_mem_unpairedHexagonComposites), and the case analysis showing that such a composite is a pentagon partner is shared with the homotopy of a crossing change: it is GridDiagram.exists_pentagonPair_of_hasMixedSideOverlap_of_mem_iff, applied with the reverse commutation, whose turn row is the opposite intersection row. Its hypotheses on the X-markings of the commuted columns are the facts that these markings lie in the bigons between the two intersection rows.

Main results

• TauCeti.GridDiagram.mem_sameSidePentagonPartners_or_mem_mixedSidePentagonPartners: off the diagonal, every unpaired hexagon composite is a same-side or a mixed-side pentagon partner.
• TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq: the homotopy equation ∂ ∘ H + H ∘ ∂ = 1 + Ψ ∘ Φ in characteristic two.
• TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_reverse_add_eq: the homotopy equation ∂' ∘ H' + H' ∘ ∂' = 1 + Φ ∘ Ψ of the reverse commutation, on the commuted diagram.
• TauCeti.GridDiagram.commutationMap_reverse_commutationMap_of_mem_ker and TauCeti.GridDiagram.commutationMap_commutationMap_reverse_of_mem_ker: on cycles, both round trips are the identity up to a boundary.

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

Exhausting the unpaired composites

theorem TauCeti.GridDiagram.mem_sameSidePentagonPartners_or_mem_mixedSidePentagonPartners {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 ∈ G.sameSidePentagonPartners C x z ∨ F ∈ G.mixedSidePentagonPartners C x z

Off the diagonal, every unpaired hexagon composite is a pentagon partner: the recut of a counted same-side pentagon pair, or the composite with the rectangles of a counted mixed-side pentagon pair.

theorem TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq {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)

The homotopy equation ∂ ∘ H + H ∘ ∂ = 1 + Ψ ∘ Φ of a column commutation, over any commutative semiring of characteristic two: the hexagon-counting map H is a chain homotopy between the identity of GC⁻(G) and the round trip through the commuted diagram.

theorem TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_reverse_add_eq {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] [CharP R 2] (c : GridChainMinus R n) : ((swapColumns C.column ((finRotate n) C.column) G).unblockedDifferential R) (((swapColumns C.column ((finRotate n) C.column) G).commutationHomotopy R C.reverse) c) + ((swapColumns C.column ((finRotate n) C.column) G).commutationHomotopy R C.reverse) (((swapColumns C.column ((finRotate n) C.column) G).unblockedDifferential R) c) = c + (G.commutationMap R C.toColumnTurn) (((swapColumns C.column ((finRotate n) C.column) G).commutationMap R C.reverse.toColumnTurn) c)

The homotopy equation on the commuted diagram. The hexagon map H' of the reverse commutation is a chain homotopy between the identity of GC⁻(G') and the round trip Φ ∘ Ψ through G: ∂' ∘ H' + H' ∘ ∂' = 1 + Φ ∘ Ψ.

theorem TauCeti.GridDiagram.commutationMap_reverse_commutationMap_of_mem_ker {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] [CharP R 2] {z : GridChainMinus R n} (hz : z ∈ (G.unblockedDifferential R).ker) : ((swapColumns C.column ((finRotate n) C.column) G).commutationMap R C.reverse.toColumnTurn) ((G.commutationMap R C.toColumnTurn) z) = z + (G.unblockedDifferential R) ((G.commutationHomotopy R C) z)

On a cycle z of GC⁻(G), the round trip Ψ ∘ Φ through the commuted diagram is the identity up to the boundary of H z.

theorem TauCeti.GridDiagram.commutationMap_commutationMap_reverse_of_mem_ker {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] [CharP R 2] {z : GridChainMinus R n} (hz : z ∈ ((swapColumns C.column ((finRotate n) C.column) G).unblockedDifferential R).ker) : (G.commutationMap R C.toColumnTurn) (((swapColumns C.column ((finRotate n) C.column) G).commutationMap R C.reverse.toColumnTurn) z) = z + ((swapColumns C.column ((finRotate n) C.column) G).unblockedDifferential R) (((swapColumns C.column ((finRotate n) C.column) G).commutationHomotopy R C.reverse) z)

On a cycle z of GC⁻(G'), the round trip Φ ∘ Ψ through G is the identity up to the boundary of H' z.