Documentation

TauCeti.KnotTheory.Grid.Move.Transpose

Transposition on grid links #

Diagonal reflection exchanges row and column moves and preserves stabilizations. It therefore descends to an involution on grid links, not merely on their presenting diagrams. No identification of a link with its transpose is imposed.

The grid move conventions follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.

source
theorem TauCeti.GridDiagram.IsMove.transpose {A B : (n : ℕ) × GridDiagram n} (h : IsMove A B) :
IsMove ⟨A.fst, A.snd.transpose⟩ ⟨B.fst, B.snd.transpose⟩

Diagonal reflection sends an elementary grid move to an elementary grid move.

source
theorem TauCeti.GridDiagram.MovesTo.transpose {n m : ℕ} {G : GridDiagram n} {G' : GridDiagram m} (h : G.MovesTo G') :
G.transpose.MovesTo G'.transpose

Diagonal reflection transports a sequence of grid moves.

source
@[simp]
theorem TauCeti.GridDiagram.movesTo_transpose {n m : ℕ} {G : GridDiagram n} {G' : GridDiagram m} :
G.transpose.MovesTo G'.transpose ↔ G.MovesTo G'

Two transposed diagrams are move-equivalent exactly when the original diagrams are.

source
def TauCeti.GridLink.transpose :
GridLink → GridLink

Diagonal reflection of a grid link, defined independently of a presenting diagram.

Instances For
    source
    @[simp]
    theorem TauCeti.GridLink.transpose_transpose (L : GridLink) :
    L.transpose.transpose = L

    Diagonal reflection is involutive on grid links.

    source
    @[simp]
    theorem TauCeti.GridLink.componentCount_transpose (L : GridLink) :
    L.transpose.componentCount = L.componentCount

    Diagonal reflection preserves the number of link components.

    source
    @[simp]
    theorem TauCeti.GridLink.isKnot_transpose {L : GridLink} :
    L.transpose.IsKnot ↔ L.IsKnot

    A transposed grid link is a knot exactly when the original link is.

    source
    def TauCeti.GridLink.transposeEquiv :
    GridLink ≃ GridLink

    Transposition as an equivalence of grid links.

    Instances For
      source
      @[simp]
      theorem TauCeti.GridLink.transposeEquiv_apply (L : GridLink) :
      transposeEquiv L = L.transpose

      The transposition equivalence acts by diagonal reflection.

      source
      @[simp]
      theorem TauCeti.GridLink.transposeEquiv_symm_apply (L : GridLink) :
      transposeEquiv.symm L = L.transpose

      The inverse transposition equivalence also acts by diagonal reflection.

      source
      @[simp]
      theorem TauCeti.GridLink.transpose_inj {L L' : GridLink} :
      L.transpose = L'.transpose ↔ L = L'

      Equality of transposes is equality of grid links.