Documentation

TauCeti.KnotTheory.Grid.CrossingChange.UnknottingNumber

Crossing changes and the unknotting number of grid links #

A grid link is a grid diagram modulo grid moves. Two grid links differ by a crossing change when they are presented by two diagrams related by a cross-commutation (GridLink.IsCrossingChange). The unknotting number of a grid link is the least number of crossing changes needed to turn it into the unknot (GridLink.unknottingNumber). It is defined as the distance from the unknot in the graph whose edges are the crossing changes (GridLink.crossingChangeGraph), so it takes values in ℕ∞. Crossing changes preserve the number of components, so a grid link with several components never reaches the unknot, and its unknotting number is ⊤.

This is the unknotting number of the grid-diagram presentation of links. It agrees with the classical unknotting number of the presented knot by Cromwell's theorem together with the fact, proved in Ozsváth--Stipsicz--Szabó, that a crossing change between two knots is realised by a cross-commutation of suitable grid diagrams; neither fact is formalised here. The definition is the one in which the inequality |τ(K)| ≤ u(K) of grid homology is proved: the crossing change maps bound the change of τ across a single cross-commutation, and summing along an unknotting sequence bounds τ by the unknotting number.

The unknotting numbers of specific torus links are bounded in TauCeti.KnotTheory.Grid.TorusLink.UnknottingNumber.

Main definitions #

Main results #

References #

source
def TauCeti.GridLink.IsCrossingChange (L L' : GridLink) :
Prop

Two grid links differ by a crossing change when they are presented by two grid diagrams related by a cross-commutation.

Instances For
    source
    theorem TauCeti.GridLink.isCrossingChange_iff (L L' : GridLink) :
    L.IsCrossingChange L' ↔ ∃ (n : ℕ) (G : GridDiagram n) (G' : GridDiagram n), G.IsCrossCommutation G' ∧ G.toGridLink = L ∧ G'.toGridLink = L'

    Characterization of a crossing change by presenting diagrams.

    source
    theorem TauCeti.GridDiagram.IsCrossCommutation.isCrossingChange {n : ℕ} {G G' : GridDiagram n} (h : G.IsCrossCommutation G') :
    G.toGridLink.IsCrossingChange G'.toGridLink

    The grid links of two diagrams related by a cross-commutation differ by a crossing change.

    source
    theorem TauCeti.GridLink.IsCrossingChange.symm {L L' : GridLink} (h : L.IsCrossingChange L') :
    L'.IsCrossingChange L

    A crossing change can be undone by a crossing change.

    source
    theorem TauCeti.GridLink.isCrossingChange_comm {L L' : GridLink} :
    L.IsCrossingChange L' ↔ L'.IsCrossingChange L

    The crossing change relation is symmetric.

    source
    theorem TauCeti.GridLink.IsCrossingChange.componentCount_eq {L L' : GridLink} (h : L.IsCrossingChange L') :
    L'.componentCount = L.componentCount

    A crossing change preserves the number of components.

    source
    def TauCeti.GridLink.crossingChangeGraph :
    SimpleGraph GridLink

    The crossing change graph: two distinct grid links are adjacent when they differ by a crossing change.

    Instances For
      source
      @[simp]
      theorem TauCeti.GridLink.crossingChangeGraph_adj {L L' : GridLink} :
      crossingChangeGraph.Adj L L' ↔ L ≠ L' ∧ L.IsCrossingChange L'

      Two grid links are adjacent in the crossing change graph exactly when they are distinct and differ by a crossing change.

      source
      noncomputable def TauCeti.GridLink.unknottingNumber (L : GridLink) :
      ℕ∞

      The unknotting number of a grid link: the least number of crossing changes turning it into the unknot, or ⊤ if no sequence of crossing changes does.

      Instances For
        source
        theorem TauCeti.GridLink.unknottingNumber_def (L : GridLink) :
        L.unknottingNumber = crossingChangeGraph.edist L unknot

        The unknotting number is the distance from the unknot in the crossing change graph.

        source
        @[simp]
        theorem TauCeti.GridLink.unknottingNumber_eq_zero_iff {L : GridLink} :
        L.unknottingNumber = 0 ↔ L = unknot

        Only the unknot has unknotting number zero.

        source
        @[simp]
        theorem TauCeti.GridLink.unknottingNumber_unknot :
        unknot.unknottingNumber = 0

        The unknot has unknotting number zero.

        source
        theorem TauCeti.GridLink.IsCrossingChange.edist_le_one {L L' : GridLink} (h : L.IsCrossingChange L') :
        crossingChangeGraph.edist L L' ≤ 1

        Two grid links differing by a crossing change are at distance at most one in the crossing change graph.

        source
        theorem TauCeti.GridLink.IsCrossingChange.unknottingNumber_le {L L' : GridLink} (h : L.IsCrossingChange L') :
        L.unknottingNumber ≤ L'.unknottingNumber + 1

        A crossing change changes the unknotting number by at most one.

        source
        theorem TauCeti.GridLink.isKnot_of_unknottingNumber_ne_top {L : GridLink} (h : L.unknottingNumber ≠ ⊤) :
        L.IsKnot

        A grid link with finite unknotting number is a knot: crossing changes preserve the number of components.