Documentation

TauCeti.KnotTheory.PDCode.Oriented.Reidemeister.Three

The third Reidemeister move on oriented PD-codes #

TauCeti.PDCode.reidemeisterThree replaces the triangular tangle σ₁ σ₂ σ₁ at three crossings of a PD-code by σ₂ σ₁ σ₂, moving the twelve local half-edges by the permutation TauCeti.PDCode.reidemeisterThreePerm. This file lifts the move to oriented codes. Each of the three strands of the tangle keeps its direction, so every half-edge takes the orientation of the half-edge it is moved from, and the oriented move takes no data beyond the unoriented one. The strands may be oriented in any of the eight ways.

The three crossings of the new tangle carry the signs of the old ones, with the first and the third crossing exchanging their signs, exactly as they exchange their over-pair indicators. So the move keeps the writhe. Together with the invariance of the Kauffman bracket (TauCeti.PDCode.kauffmanBracket_reidemeisterThree), this makes the writhe-normalized Kauffman bracket invariant under the oriented third Reidemeister move. The sign and writhe statements only use the three internal arcs of the triangle, not the height order of its strands.

Main definitions #

Main results #

References #

source
def TauCeti.OrientedPDCode.reidemeisterThree {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) :
OrientedPDCode n

The third Reidemeister move on an oriented PD-code: the rewire TauCeti.PDCode.reidemeisterThree at the crossings c 0, c 1, c 2, with every half-edge oriented as the half-edge that TauCeti.PDCode.reidemeisterThreePerm moves to it, so that each strand of the tangle keeps its direction. It is a Reidemeister move when the three crossings satisfy TauCeti.PDCode.HasReidemeisterThreeTriangle.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.OrientedPDCode.toPDCode_reidemeisterThree {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) :
    (D.reidemeisterThree c).toPDCode = D.reidemeisterThree c

    Forgetting the orientation of the oriented third Reidemeister move gives the unoriented one.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_reidemeisterThree {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) (x : Fin (4 * n)) :
    (D.reidemeisterThree c).orientation x = D.orientation ((Equiv.symm (D.reidemeisterThreePerm c)) x)

    The oriented third Reidemeister move orients each half-edge as the half-edge moved to it.

    source
    theorem TauCeti.OrientedPDCode.orientation_reidemeisterThree_reidemeisterThreePerm {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) (x : Fin (4 * n)) :
    (D.reidemeisterThree c).orientation ((D.reidemeisterThreePerm c) x) = D.orientation x

    The oriented third Reidemeister move transports the orientation of every half-edge along the local rewire.

    source
    theorem TauCeti.OrientedPDCode.orientation_reidemeisterThree_crossing {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) (i : Fin 3) (s : Fin 4) :
    (D.reidemeisterThree c).orientation (D.crossing (c i) s) = D.orientation (D.crossing (c ((Equiv.symm PDCode.reidemeisterThreeSlots) (i, s)).1) ((Equiv.symm PDCode.reidemeisterThreeSlots) (i, s)).2)

    The orientation of a slot of one of the three crossings of the new tangle, read off the slot of the old tangle that the local rewire moves to it.

    source
    theorem TauCeti.OrientedPDCode.orientation_reidemeisterThree_crossing_of_notMem {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) {i : Fin n} (hi : i ∉ Set.range ⇑c) (s : Fin 4) :
    (D.reidemeisterThree c).orientation (D.crossing i s) = D.orientation (D.crossing i s)

    The oriented third Reidemeister move keeps the orientation of every slot of a crossing outside the triangle.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossinglessComponents_reidemeisterThree {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) :
    (D.reidemeisterThree c).crossinglessComponents = D.crossinglessComponents

    The oriented third Reidemeister move keeps the oriented crossing-free components.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossingSign_reidemeisterThree {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) (h : D.HasReidemeisterThreeTriangleArcs c) (i : Fin n) :
    (D.reidemeisterThree c).crossingSign i = D.crossingSign ((Equiv.swap (c 0) (c 2)) i)

    The oriented third Reidemeister move permutes the crossing signs: the first and the third crossing of the triangle exchange their signs, and every other crossing keeps its sign. Only the three internal arcs of the triangle are needed, not the height order of its strands.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.writhe_reidemeisterThree {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) (h : D.HasReidemeisterThreeTriangleArcs c) :
    (D.reidemeisterThree c).writhe = D.writhe

    The oriented third Reidemeister move keeps the writhe.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.normalizedKauffmanBracket_reidemeisterThree {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) (h : D.HasReidemeisterThreeTriangle c) {R : Type u_1} [CommRing R] (a : Rˣ) :
    (D.reidemeisterThree c).normalizedKauffmanBracket a = D.normalizedKauffmanBracket a

    The writhe-normalized Kauffman bracket is invariant under the oriented third Reidemeister move, for every surrounding diagram and all six height orders of the three strands.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.mirror_reidemeisterThree {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) :
    (D.reidemeisterThree c).mirror = D.mirror.reidemeisterThree c

    Reflecting the oriented third Reidemeister move performs the move on the reflected code.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.reverse_reidemeisterThree {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) :
    (D.reidemeisterThree c).reverse = D.reverse.reidemeisterThree c

    Reversing the oriented third Reidemeister move performs the move on the reversed code.