Documentation

TauCeti.KnotTheory.Grid.Commutation.Homotopy.InitialPair.Basic

Recutting pairs of initial-side commutation pentagons #

Two empty pentagons turning on the initial side of the replaced grid line share that side. Their distinct terminal sides have two possible cyclic orders. When the second lies inside the first column interval, the recut is an initial-side hexagon followed by a rectangle; in the complementary order it is a rectangle followed by an initial-side hexagon. The two turn rows occur in the required order on either hexagon.

If the pentagons avoid the X-markings in the forward and reverse diagrams, both recuts are counted and have no counted hexagon-composite recut partner. These are the two initial--initial geometric cases in the matching between unpaired hexagon composites and pentagon pairs in the commutation homotopy equation. No homotopy equation or weight identity is asserted 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).

source
noncomputable def TauCeti.GridInitialPentagonBetween.recutHexagonRectangle {n : ℕ} {a s t : Fin n} {x y z : GridState n} (P : GridInitialPentagonBetween a s x y) (Q : GridInitialPentagonBetween a t y z) (hcol : Q.right ∈ Grid.cIoo ((finRotate n) a) P.right) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
GridHexagonRectangleDecomposition a s t x z

Recut two empty initial-side pentagons into an initial-side hexagon followed by a rectangle, when the second terminal side is inside the first column interval.

Instances For
    source
    @[simp]
    theorem TauCeti.GridInitialPentagonBetween.recutHexagonRectangle_toRectangleDecomposition {n : ℕ} {a s t : Fin n} {x y z : GridState n} (P : GridInitialPentagonBetween a s x y) (Q : GridInitialPentagonBetween a t y z) (hcol : Q.right ∈ Grid.cIoo ((finRotate n) a) P.right) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
    (P.recutHexagonRectangle Q hcol hP hQ).toRectangleDecomposition = GridRectangleDecomposition.recut { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } ⋯ hP hQ

    Forgetting the hexagon turns returns the canonical empty-rectangle recut.

    source
    theorem TauCeti.GridInitialPentagonBetween.isRecut_recutHexagonRectangle {n : ℕ} {a s t : Fin n} {x y z : GridState n} (P : GridInitialPentagonBetween a s x y) (Q : GridInitialPentagonBetween a t y z) (hcol : Q.right ∈ Grid.cIoo ((finRotate n) a) P.right) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
    GridRectangleDecomposition.IsRecut { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } (P.recutHexagonRectangle Q hcol hP hQ).toRectangleDecomposition

    The hexagon--rectangle composite is an empty-rectangle recut of the pentagon pair.

    source
    @[simp]
    theorem TauCeti.GridInitialPentagonBetween.recutHexagonRectangle_hexagon_isLeft {n : ℕ} {a s t : Fin n} {x y z : GridState n} (P : GridInitialPentagonBetween a s x y) (Q : GridInitialPentagonBetween a t y z) (hcol : Q.right ∈ Grid.cIoo ((finRotate n) a) P.right) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
    Sum.isLeft (P.recutHexagonRectangle Q hcol hP hQ).hexagon = false

    The recut hexagon turns on its initial side.

    source
    noncomputable def TauCeti.GridInitialPentagonBetween.recutRectangleHexagon {n : ℕ} {a s t : Fin n} {x y z : GridState n} (P : GridInitialPentagonBetween a s x y) (Q : GridInitialPentagonBetween a t y z) (hcol : P.right ∈ Grid.cIoo ((finRotate n) a) Q.right) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
    GridRectangleHexagonDecomposition a s t x z

    Recut two empty initial-side pentagons into a rectangle followed by an initial-side hexagon, when the first terminal side is inside the second column interval.

    Instances For
      source
      @[simp]
      theorem TauCeti.GridInitialPentagonBetween.recutRectangleHexagon_toRectangleDecomposition {n : ℕ} {a s t : Fin n} {x y z : GridState n} (P : GridInitialPentagonBetween a s x y) (Q : GridInitialPentagonBetween a t y z) (hcol : P.right ∈ Grid.cIoo ((finRotate n) a) Q.right) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
      (P.recutRectangleHexagon Q hcol hP hQ).toRectangleDecomposition = GridRectangleDecomposition.recut { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } ⋯ hP hQ

      Forgetting the hexagon turns returns the canonical empty-rectangle recut.

      source
      theorem TauCeti.GridInitialPentagonBetween.isRecut_recutRectangleHexagon {n : ℕ} {a s t : Fin n} {x y z : GridState n} (P : GridInitialPentagonBetween a s x y) (Q : GridInitialPentagonBetween a t y z) (hcol : P.right ∈ Grid.cIoo ((finRotate n) a) Q.right) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
      GridRectangleDecomposition.IsRecut { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } (P.recutRectangleHexagon Q hcol hP hQ).toRectangleDecomposition

      The rectangle--hexagon composite is an empty-rectangle recut of the pentagon pair.

      source
      @[simp]
      theorem TauCeti.GridInitialPentagonBetween.recutRectangleHexagon_hexagon_isLeft {n : ℕ} {a s t : Fin n} {x y z : GridState n} (P : GridInitialPentagonBetween a s x y) (Q : GridInitialPentagonBetween a t y z) (hcol : P.right ∈ Grid.cIoo ((finRotate n) a) Q.right) (hP : P.IsEmpty) (hQ : Q.IsEmpty) :
      Sum.isLeft (P.recutRectangleHexagon Q hcol hP hQ).hexagon = false

      The hexagon in the complementary recut turns on its initial side.

      source
      theorem TauCeti.GridDiagram.recutHexagonRectangle_mem_hexagonRectangleDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {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) (hPX : Disjoint P.coveredSquares G.XSet) (hQX : Disjoint Q.coveredSquares (swapColumns C.column ((finRotate n) C.column) G).XSet) :
      P.recutHexagonRectangle Q hcol hP hQ ∈ G.hexagonRectangleDecompositions C x z

      The initial-side pentagon recut is a counted hexagon--rectangle composite when the forward pentagon and the reverse pentagon avoid their respective X-markings.

      source
      theorem TauCeti.GridDiagram.recutRectangleHexagon_mem_rectangleHexagonDecompositions {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {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) (hPX : Disjoint P.coveredSquares G.XSet) (hQX : Disjoint Q.coveredSquares (swapColumns C.column ((finRotate n) C.column) G).XSet) :
      P.recutRectangleHexagon Q hcol hP hQ ∈ G.rectangleHexagonDecompositions C x z

      The complementary initial-side pentagon recut is a counted rectangle--hexagon composite when the forward and reverse pentagons avoid their respective X-markings.

      source
      theorem TauCeti.GridDiagram.recutHexagonRectangle_mem_unpairedHexagonComposites {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {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) (hPX : Disjoint P.coveredSquares G.XSet) (hQX : Disjoint Q.coveredSquares (swapColumns C.column ((finRotate n) C.column) G).XSet) :
      Sum.inl (P.recutHexagonRectangle Q hcol hP hQ) ∈ G.unpairedHexagonComposites C x z

      The counted initial-side pentagon recut has no counted composite recut partner. The original pentagon pair cannot contain a hexagon: neither of its row intervals contains both turn rows in the required order.

      source
      theorem TauCeti.GridDiagram.recutRectangleHexagon_mem_unpairedHexagonComposites {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {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) (hPX : Disjoint P.coveredSquares G.XSet) (hQX : Disjoint Q.coveredSquares (swapColumns C.column ((finRotate n) C.column) G).XSet) :
      Sum.inr (P.recutRectangleHexagon Q hcol hP hQ) ∈ G.unpairedHexagonComposites C x z

      The counted complementary initial-side recut has no counted composite recut partner.

      source
      theorem TauCeti.GridDiagram.exists_unpairedHexagonComposite_of_initialPentagonPair {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) {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) (hcol : Q.right ∈ Grid.cIoo ((finRotate n) C.column) P.right) :
      ∃ F ∈ G.unpairedHexagonComposites C x z, GridRectangleDecomposition.IsRecut { middle := y, first := P.toGridRectangleBetween, second := Q.toGridRectangleBetween } F.toRectangleDecomposition

      Two counted initial-side pentagons for an actual commutation and its reverse admit an unpaired hexagon-composite recut in the strict interior-terminal-side branch. The reverse pentagon retains the indices of C.reverse.