Documentation

TauCeti.KnotTheory.Grid.Commutation.Homotopy.Recut

Recut pairing of hexagon--rectangle terms in the commutation homotopy equation #

The left-hand side ∂ ∘ H + H ∘ ∂ of the homotopy equation of a column commutation counts two-step domains made of a commutation hexagon and a rectangle of the original diagram, in either order. Forgetting the two turns of the hexagon leaves a two-step rectangle decomposition. When its two rectangles share exactly one side column, their union is an L-shaped domain, and the recut from the proof of ∂² = 0 cuts it the other way (TauCeti.GridRectangleDecomposition.recut).

Both orders of composition lie on the same side of the equation, so they are treated as one family, TauCeti.GridHexagonCompositeDecomposition. If the recut of a counted composite is again the underlying decomposition of a counted composite, the two terms cancel in characteristic two, whatever the orientation of their common side and whichever piece of the recut carries the hexagon. The weights agree because both terms cover the same squares and their rectangles carry the same single X-marking, that of the column the hexagon cuts away (TauCeti.GridCommutationHexagonBetween.cutColumn): this fixes the variable by which the underlying rectangle weight exceeds the composite weight. A counted composite determines the position of its hexagon from its underlying decomposition, since a counted rectangle carries no X-marking while the rectangle under a counted hexagon carries one. Hence recut partners form a fixed-point-free involution.

Off the diagonal, what remains of the hexagon side are the composites whose recut is not again a counted composite (TauCeti.GridDiagram.unpairedHexagonComposites). In the juxtaposition argument these are the terms matched with the pairs of pentagons counted by the round trip Ψ ∘ Φ of the two commutation maps; that matching is not part of this file.

Main definition #

Main results #

References #

This is the juxtaposition argument for the homotopy 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 (arXiv:math/0610559).

source
theorem TauCeti.GridDiagram.sum_hexagonCompositeWeight_filter_not_hasDisjointSides {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] (x z : GridState n) :
∑ D ∈ G.hexagonCompositeDecompositions C x z with ¬D.toRectangleDecomposition.HasDisjointSides, G.hexagonCompositeWeight C R D = ∑ D ∈ G.hexagonRectangleDecompositions C x z with ¬D.toRectangleDecomposition.HasDisjointSides, G.hexagonRectangleWeight C R D + ∑ D ∈ G.rectangleHexagonDecompositions C x z with ¬D.toRectangleDecomposition.HasDisjointSides, G.rectangleHexagonWeight C R D

The overlapping counted composites have the total weight of the overlapping hexagon--rectangle and rectangle--hexagon decompositions.

The recut pairing #

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

The counted composites from x to z whose two rectangles have a common side column and whose recut is not the underlying rectangle decomposition of any counted composite.

Instances For
    source
    @[simp]
    theorem TauCeti.GridDiagram.mem_unpairedHexagonComposites {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} (D : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z) :
    D ∈ G.unpairedHexagonComposites C x z ↔ D ∈ G.hexagonCompositeDecompositions C x z ∧ ¬D.toRectangleDecomposition.HasDisjointSides ∧ ∀ E ∈ G.hexagonCompositeDecompositions C x z, ¬D.toRectangleDecomposition.IsRecut E.toRectangleDecomposition

    A composite is unpaired exactly when it is counted, its rectangles have a common side column, and its recut underlies no counted composite.

    source
    theorem TauCeti.GridDiagram.mem_unpairedHexagonComposites_of_toRectangleDecomposition_eq {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x z : GridState n} {D : GridRectangleDecomposition x z} (hone : D.HasOneCommonSide) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty) (hrecut : ∀ E ∈ G.hexagonCompositeDecompositions C x z, E.toRectangleDecomposition ≠ D.recut hone hfirst hsecond) {F : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z} (hF : F ∈ G.hexagonCompositeDecompositions C x z) (hFD : F.toRectangleDecomposition = D) :
    F ∈ G.unpairedHexagonComposites C x z

    A counted composite is unpaired when its underlying decomposition has exactly one common side and the recut of that decomposition underlies no counted composite.

    source
    theorem TauCeti.GridDiagram.existsUnique_unpairedHexagonComposite_of_toRectangleDecomposition_eq {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] {x z : GridState n} {D : GridRectangleDecomposition x z} (hone : D.HasOneCommonSide) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty) (hrecut : ∀ E ∈ G.hexagonCompositeDecompositions C x z, E.toRectangleDecomposition ≠ D.recut hone hfirst hsecond) {F : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z} (hF : F ∈ G.hexagonCompositeDecompositions C x z) (hFD : F.toRectangleDecomposition = D) :
    ∃! F' : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z, F' ∈ G.unpairedHexagonComposites C x z ∧ F'.toRectangleDecomposition = D ∧ G.hexagonCompositeWeight C R F' = G.hexagonCompositeWeight C R F

    A counted composite whose underlying decomposition has exactly one common side, and whose recut underlies no counted composite, is the only unpaired composite with this decomposition.

    source
    theorem TauCeti.GridDiagram.sum_hexagonCompositeWeight_overlap_eq_sum_unpaired {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] [CharP R 2] {x z : GridState n} (hzx : z ≠ x) :
    ∑ D ∈ G.hexagonCompositeDecompositions C x z with ¬D.toRectangleDecomposition.HasDisjointSides, G.hexagonCompositeWeight C R D = ∑ D ∈ G.unpairedHexagonComposites C x z, G.hexagonCompositeWeight C R D

    Off the diagonal and in characteristic two, the counted composites whose rectangles share a side column have the total weight of the unpaired ones: recut partners cancel in pairs (GridRectangleDecomposition.sum_filter_not_hasDisjointSides_eq_sum_filter_forall_not_isRecut).

    source
    theorem TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq_iff_unpaired {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 : GridState n), ∑ D ∈ G.hexagonRectangleDecompositions C x x, G.hexagonRectangleWeight C R D + ∑ D ∈ G.rectangleHexagonDecompositions C x x, G.rectangleHexagonWeight C R D = 1 + ∑ D ∈ G.pentagonPairDecompositions C x x, G.pentagonPairWeight C R D) ∧ ∀ (x z : GridState n), z ≠ x → ∑ D ∈ G.unpairedHexagonComposites C x z, G.hexagonCompositeWeight C R D = ∑ D ∈ G.pentagonPairDecompositions C x z, G.pentagonPairWeight C R D

    In characteristic two, the commutation homotopy equation is equivalent to its diagonal coefficient identity together with the off-diagonal identity between the unpaired hexagon composites and the pentagon pairs.