Documentation

TauCeti.KnotTheory.Grid.Stabilization.Components

Link components under grid stabilization #

A stabilization splits one marking of a grid diagram across an inserted row and column and puts a marking of the other type at their intersection. Along the link this inserts one short horizontal and one short vertical segment into the component through the split marking, so the number of components does not change.

On the component permutation c ↦ X⁻¹(O(c)) this is visible directly. For the stabilization G.stabilizeX p q s splitting the X-marking of column s, write ι = p.succAbove for the embedding of the old columns and σ for the old component permutation. The new permutation sends the new column p to ι s, and sends ι c to ι (σ c), except that the column ι c with σ c = s now goes to p. So the new column is spliced into the cycle through ι s, just before it. An O-stabilization is an X-stabilization after exchanging the two marking types.

These statements need no adjacency of the new row and column to the split marking, so they hold for the constructions GridDiagram.stabilizeX and GridDiagram.stabilizeO themselves, and in particular for every elementary stabilization of each of the eight corner types.

Main results #

Implementation notes #

The count is compared through TauCeti.orbitCount, using TauCeti.GridDiagram.componentCount_eq_orbitCount. Cutting the new column back out of its cycle, by the transposition of p and ι s, gives a permutation that fixes p and is carried from σ by ι. Adjoining a fixed point adds one orbit (TauCeti.orbitCount_add_one_eq_of_semiconj) and splicing it into another orbit removes one (TauCeti.orbitCount_mul_swap_add_one).

References #

The stabilization moves follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

source
theorem TauCeti.GridDiagram.componentPerm_stabilizeX_newColumn {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) :
(G.stabilizeX newColumn newRow splitColumn).componentPerm newColumn = newColumn.succAbove splitColumn

In an X-stabilization, the component through the new column continues to the embedded split column: the new O-marking shares its row with the X-marking moved into the split column.

source
theorem TauCeti.GridDiagram.componentPerm_stabilizeX_succAbove {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn c : Fin n) :
(G.stabilizeX newColumn newRow splitColumn).componentPerm (newColumn.succAbove c) = if G.componentPerm c = splitColumn then newColumn else newColumn.succAbove (G.componentPerm c)

In an X-stabilization, an embedded old column continues to the embedded image of its old successor along the component, except that the column whose old successor is the split column now continues to the new column.

source
@[simp]
theorem TauCeti.GridDiagram.componentCount_stabilizeX {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) :
(G.stabilizeX newColumn newRow splitColumn).componentCount = G.componentCount

An X-stabilization does not change the number of link components: the new column is spliced into the component through the split marking.

source
@[simp]
theorem TauCeti.GridDiagram.componentCount_stabilizeO {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) :
(G.stabilizeO newColumn newRow splitColumn).componentCount = G.componentCount

An O-stabilization does not change the number of link components.

source
@[simp]
theorem TauCeti.GridDiagram.isKnot_stabilizeX {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) :
(G.stabilizeX newColumn newRow splitColumn).IsKnot ↔ G.IsKnot

An X-stabilization represents a knot exactly when the original diagram does.

source
@[simp]
theorem TauCeti.GridDiagram.isKnot_stabilizeO {n : ℕ} (G : GridDiagram n) (newColumn newRow : Fin (n + 1)) (splitColumn : Fin n) :
(G.stabilizeO newColumn newRow splitColumn).IsKnot ↔ G.IsKnot

An O-stabilization represents a knot exactly when the original diagram does.

source
theorem TauCeti.GridDiagram.IsStabilization.componentCount_eq {n : ℕ} {G : GridDiagram n} {G' : GridDiagram (n + 1)} (h : G.IsStabilization G') :
G'.componentCount = G.componentCount

Every elementary stabilization preserves the number of represented link components.

source
theorem TauCeti.GridDiagram.IsStabilization.isKnot_iff {n : ℕ} {G : GridDiagram n} {G' : GridDiagram (n + 1)} (h : G.IsStabilization G') :
G'.IsKnot ↔ G.IsKnot

Every elementary stabilization preserves whether a grid diagram represents a knot.