Documentation

TauCeti.KnotTheory.Grid.Stabilization.Matching

The generator matching for X-stabilization #

Let G' be the X-stabilization of a grid diagram G at a column s. The mapping cone of the fully blocked comparison from the off-center block to the center block has generators

G.StabilizeXOffCenterState s ⊕ GridState n.

These generators are naturally all grid states of G': an off-center generator is already such a state, while a center generator is sent to the state obtained by inserting the center of the new block (TauCeti.GridDiagram.stabilizeXConeStateEquiv). This file records the fixed-point-free involution obtained by swapping the two rows of the new block.

The source of each matched pair is selected by the orientation of the cyclic column interval between the points in those two rows: the source is the endpoint whose height-one rectangle to its partner avoids the new O-marking, so in particular no center generator is a source. Opposite nondegenerate half-open intervals partition the columns, so exactly one generator in each pair is a source. The existing stabilization level is constant on each pair because the swap is realized by a rectangle supported entirely in the row of the new O-marking (TauCeti.GridDiagram.stabilizeXLevel_swapRows). These facts provide the matching data needed to prove exactness of the reduced stabilization mapping cone.

Main definitions #

Main results #

References #

This is the generator matching in the proof of stabilization invariance in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.2, expressed using the Q-filtration from Section 5.2 and Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.2.

source
noncomputable def TauCeti.GridDiagram.stabilizeXMatching {n : ℕ} (G : GridDiagram n) (s : Fin n) (i : G.StabilizeXOffCenterState s ⊕ GridState n) :
G.StabilizeXOffCenterState s ⊕ GridState n

The matching on generators of the reduced stabilization mapping cone. Under stabilizeXConeStateEquiv, it swaps the row (G.X s).castSucc containing the new O-marking with the following row (G.X s).succ.

Instances For
    source
    @[simp]
    theorem TauCeti.GridDiagram.stabilizeXConeStateEquiv_apply_stabilizeXMatching {n : ℕ} (G : GridDiagram n) (s : Fin n) (i : G.StabilizeXOffCenterState s ⊕ GridState n) :
    (G.stabilizeXConeStateEquiv s) (G.stabilizeXMatching s i) = GridState.swapRows (G.X.toPerm s).castSucc (G.X.toPerm s).succ ((G.stabilizeXConeStateEquiv s) i)

    Under the cone-state equivalence, matching a generator swaps the stabilization rows.

    source
    @[simp]
    theorem TauCeti.GridDiagram.stabilizeXMatching_involutive {n : ℕ} (G : GridDiagram n) (s : Fin n) (i : G.StabilizeXOffCenterState s ⊕ GridState n) :
    G.stabilizeXMatching s (G.stabilizeXMatching s i) = i

    Swapping the two stabilization rows twice returns the original mapping-cone generator.

    source
    theorem TauCeti.GridDiagram.stabilizeXMatching_ne {n : ℕ} (G : GridDiagram n) (s : Fin n) (i : G.StabilizeXOffCenterState s ⊕ GridState n) :
    G.stabilizeXMatching s i ≠ i

    The stabilization matching has no fixed points.

    source
    def TauCeti.GridDiagram.StabilizeXMatchingSource {n : ℕ} (G : GridDiagram n) (s : Fin n) (i : G.StabilizeXOffCenterState s ⊕ GridState n) :
    Prop

    A generator is the source of its matching edge when the stabilization column lies in the clockwise half-open interval from the column occupied in row (G.X s).succ to the column occupied in row (G.X s).castSucc. Equivalently, the height-one rectangle from the generator to its partner, which covers the complementary interval in the row of the new O-marking, avoids that marking.

    Instances For
      source
      @[simp]
      theorem TauCeti.GridDiagram.stabilizeXMatchingSource_stabilizeXMatching_iff {n : ℕ} (G : GridDiagram n) (s : Fin n) (i : G.StabilizeXOffCenterState s ⊕ GridState n) :
      G.StabilizeXMatchingSource s (G.stabilizeXMatching s i) ↔ ¬G.StabilizeXMatchingSource s i

      Exactly one endpoint of every matched pair is selected as a matching source.

      source
      theorem TauCeti.GridDiagram.stabilizeXMatchingSource_iff_notMem_cIco {n : ℕ} (G : GridDiagram n) (s : Fin n) (i : G.StabilizeXOffCenterState s ⊕ GridState n) :
      G.StabilizeXMatchingSource s i ↔ s.castSucc ∉ Grid.cIco (((G.stabilizeXConeStateEquiv s) i).transpose.toPerm (G.X.toPerm s).castSucc) (((G.stabilizeXConeStateEquiv s) i).transpose.toPerm (G.X.toPerm s).succ)

      A generator is a matching source exactly when the stabilization column lies outside the clockwise interval from the column used in row (G.X s).castSucc to the column used in row (G.X s).succ, which is the interval covered by the row swap rectangle.

      source
      @[simp]
      theorem TauCeti.GridDiagram.not_stabilizeXMatchingSource_inr {n : ℕ} (G : GridDiagram n) (s : Fin n) (x : GridState n) :
      ¬G.StabilizeXMatchingSource s (Sum.inr x)

      A center generator is never a matching source: its partner is off-center, and the mapping cone has no component from the center block to the off-center block.

      source
      theorem TauCeti.GridDiagram.stabilizeXLevel_stabilizeXMatching {n : ℕ} (G : GridDiagram n) (s : Fin n) (i : G.StabilizeXOffCenterState s ⊕ GridState n) :
      G.stabilizeXLevel s ((G.stabilizeXConeStateEquiv s) (G.stabilizeXMatching s i)) = G.stabilizeXLevel s ((G.stabilizeXConeStateEquiv s) i)

      The stabilization level is constant on matched pairs.