Documentation

TauCeti.KnotTheory.Grid.Commutation.Homotopy.Mixed.Pair

Mixed-side commutation pentagon pairs #

Let C be a column commutation and consider a pentagon for C followed by a pentagon for the reverse commutation. When the two pentagons turn on opposite sides of the replaced grid line, their underlying rectangles automatically share that line: it is terminal for the first and initial for the second, or initial for the first and terminal for the second. Away from the diagonal this is their unique common side, so the general empty-rectangle recut applies.

In the homotopy equation of the commutation, such a pair is matched with a hexagon composite through the same intermediate state and with the same two rectangles, not with its recut. The two rectangles share a corner row on the replaced line: the bottom row for a terminal--initial pair and the top row for an initial--terminal pair. Both turn rows lie on the replaced-line side of the rectangle of the pentagon whose turn row is farther from that shared row. That rectangle is a commutation hexagon cutting away the bigon between the two turn points, and the other one is an ordinary rectangle. Column by column, the bigon markings that the two pentagons cover are the ones the hexagon and the rectangle cover, so the composite is counted and has the weight of the pair. Its recut underlies no hexagon composite: one recut rectangle has no side on the replaced line, and the other misses one of the turn rows. Hence the composite is unpaired, and it is the only counted composite with these two rectangles.

Main definitions #

Main results #

References #

The mixed turn-side cases of the hexagon homotopy argument 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, Proposition 3.2 (arXiv:math/0610559).

Terminal-side followed by initial-side #

source
theorem TauCeti.GridDiagram.hasOneCommonSide_terminalInitialPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridInitialPentagonBetween C.reverse.column C.reverse.turnRow y z) (hzx : z ≠ x) :
GridRectangleDecomposition.HasOneCommonSide { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween }

The underlying rectangles of a terminal-side pentagon and a following initial-side pentagon for the reverse commutation share their intermediate grid line. Away from the diagonal it is their unique common side.

source
noncomputable def TauCeti.GridDiagram.recutTerminalInitialPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridInitialPentagonBetween C.reverse.column C.reverse.turnRow y z) (hzx : z ≠ x) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
GridRectangleDecomposition x z

The canonical empty-rectangle recut of an off-diagonal terminal--initial pentagon pair.

Instances For
    source
    theorem TauCeti.GridDiagram.recutTerminalInitialPentagonPair_def {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridInitialPentagonBetween C.reverse.column C.reverse.turnRow y z) (hzx : z ≠ x) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
    let D := { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween }; G.recutTerminalInitialPentagonPair C P Q hzx hP hQ = D.recut ⋯ hP hQ

    The terminal--initial construction is the canonical recut of the underlying rectangle decomposition.

    source
    theorem TauCeti.GridDiagram.isRecut_recutTerminalInitialPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridInitialPentagonBetween C.reverse.column C.reverse.turnRow y z) (hzx : z ≠ x) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
    GridRectangleDecomposition.IsRecut { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } (G.recutTerminalInitialPentagonPair C P Q hzx hP hQ)

    The terminal--initial recut is a repartition of the pentagon pair's two underlying rectangles, through a different intermediate state.

    source
    theorem TauCeti.GridDiagram.isRecutOfRightEqLeft_recutTerminalInitialPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) (Q : GridInitialPentagonBetween C.reverse.column C.reverse.turnRow y z) (hzx : z ≠ x) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
    GridRectangleDecomposition.IsRecutOfRightEqLeft { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } (G.recutTerminalInitialPentagonPair C P Q hzx hP hQ)

    The terminal--initial recut has the side-data orientation in which the terminal side of the first pentagon is the initial side of the second.

    Initial-side followed by terminal-side #

    source
    theorem TauCeti.GridDiagram.hasOneCommonSide_initialTerminalPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridInitialPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hzx : z ≠ x) :
    GridRectangleDecomposition.HasOneCommonSide { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween }

    The underlying rectangles of an initial-side pentagon and a following terminal-side pentagon for the reverse commutation share their intermediate grid line. Away from the diagonal it is their unique common side.

    source
    noncomputable def TauCeti.GridDiagram.recutInitialTerminalPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridInitialPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hzx : z ≠ x) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
    GridRectangleDecomposition x z

    The canonical empty-rectangle recut of an off-diagonal initial--terminal pentagon pair.

    Instances For
      source
      theorem TauCeti.GridDiagram.recutInitialTerminalPentagonPair_def {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridInitialPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hzx : z ≠ x) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
      let D := { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween }; G.recutInitialTerminalPentagonPair C P Q hzx hP hQ = D.recut ⋯ hP hQ

      The initial--terminal construction is the canonical recut of the underlying rectangle decomposition.

      source
      theorem TauCeti.GridDiagram.isRecut_recutInitialTerminalPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridInitialPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hzx : z ≠ x) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
      GridRectangleDecomposition.IsRecut { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } (G.recutInitialTerminalPentagonPair C P Q hzx hP hQ)

      The initial--terminal recut is a repartition of the pentagon pair's two underlying rectangles, through a different intermediate state.

      source
      theorem TauCeti.GridDiagram.isRecutOfLeftEqRight_recutInitialTerminalPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {x y z : GridState n} (P : GridInitialPentagonBetween C.column C.turnRow x y) (Q : GridPentagonBetween C.reverse.column C.reverse.turnRow y z) (hzx : z ≠ x) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
      GridRectangleDecomposition.IsRecutOfLeftEqRight { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } (G.recutInitialTerminalPentagonPair C P Q hzx hP hQ)

      The initial--terminal recut has the side-data orientation in which the initial side of the first pentagon is the terminal side of the second.

      Square bookkeeping for the matching composites #

      Cyclic order of the turns and the markings #

      The matching composite of a terminal--initial pair #

      The matching composite of an initial--terminal pair #

      The matching #

      source
      theorem TauCeti.GridDiagram.existsUnique_unpairedHexagonComposite_of_terminalInitialPentagonPair {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 : GridInitialPentagonBetween 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).initialPentagons C.reverse.toColumnTurn y z) (hzx : z ≠ x) :
      ∃! F : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z, F ∈ G.unpairedHexagonComposites C x z ∧ F.toRectangleDecomposition = { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } ∧ G.hexagonCompositeWeight C R F = G.pentagonPairWeight C R { middle := y, first := Sum.inl P, second := Sum.inr Q }

      A counted off-diagonal pair of a terminal-side pentagon and an initial-side reverse pentagon has the same underlying rectangles as exactly one unpaired hexagon composite, and their polynomial weights agree. Its hexagon is the rectangle of the pentagon whose turn row is farther from the common bottom row.

      source
      theorem TauCeti.GridDiagram.existsUnique_unpairedHexagonComposite_of_initialTerminalPentagonPair {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 : GridPentagonBetween 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).pentagons C.reverse.toColumnTurn y z) (hzx : z ≠ x) :
      ∃! F : GridHexagonCompositeDecomposition C.column C.turnRow C.oppositeTurnRow x z, F ∈ G.unpairedHexagonComposites C x z ∧ F.toRectangleDecomposition = { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } ∧ G.hexagonCompositeWeight C R F = G.pentagonPairWeight C R { middle := y, first := Sum.inr P, second := Sum.inl Q }

      A counted off-diagonal pair of an initial-side pentagon and a terminal-side reverse pentagon has the same underlying rectangles as exactly one unpaired hexagon composite, and their polynomial weights agree. Its hexagon is the rectangle of the pentagon whose turn row is farther from the common top row.