Documentation

TauCeti.KnotTheory.Grid.CrossingChange.Transpose

Transposition preserves unknotting number #

Diagonal reflection carries cross-commutations to cross-commutations and fixes the unknot. It is therefore an automorphism of the crossing-change graph and preserves its extended distances, including infinite unknotting numbers.

The crossing-change conventions follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 6.

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

Transposition transports a crossing change between grid links.

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

Transposition preserves and reflects the crossing-change relation.

source
def TauCeti.GridLink.crossingChangeGraphTransposeIso :
crossingChangeGraph ≃g crossingChangeGraph

Transposition is an automorphism of the crossing-change graph.

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

    The graph automorphism acts by transposition of grid links.

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

    The inverse graph automorphism also acts by transposition.

    source
    @[simp]
    theorem TauCeti.GridLink.crossingChangeGraph_edist_transpose (L L' : GridLink) :
    crossingChangeGraph.edist L.transpose L'.transpose = crossingChangeGraph.edist L L'

    Transposition preserves the extended crossing-change distance between any two grid links.

    source
    @[simp]
    theorem TauCeti.GridLink.unknottingNumber_transpose (L : GridLink) :
    L.transpose.unknottingNumber = L.unknottingNumber

    Transposition preserves unknotting number, also when it is infinite.