Documentation

TauCeti.KnotTheory.PDCode.Oriented.Reidemeister.One

The first Reidemeister move on oriented PD-codes #

The first Reidemeister move inserts a kink into an oriented planar-diagram code. The old arc orientation uniquely determines the orientations of the four new half-edges. This file lifts PDCode.reidemeisterOne to oriented codes and computes the sign of the new crossing and the resulting change in writhe.

The Kauffman bracket is invariant under the second and third Reidemeister moves, but acquires a factor -A^3 or -A⁻³ under the first. Multiplication by (-A^3) ^ (-writhe) cancels that factor. The resulting normalizedKauffmanBracket is therefore invariant under the oriented first Reidemeister move. This is the normalization used to obtain the Jones polynomial from the bracket.

The conventions follow L. H. Kauffman, State models and the Jones polynomial, Topology 26 (1987), and W. B. R. Lickorish, An Introduction to Knot Theory, Chapter 3.

Main definitions #

Main results #

source
def TauCeti.OrientedPDCode.reidemeisterOne {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) :
OrientedPDCode (n + 1)

Insert an oriented kink into the arc ending at h. The Boolean b selects which opposite pair at the new crossing is the over-strand, as for PDCode.reidemeisterOne.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.OrientedPDCode.toPDCode_reidemeisterOne {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) :
    (D.reidemeisterOne h b).toPDCode = D.reidemeisterOne h b

    Forgetting orientation after inserting an oriented kink gives the underlying unoriented first Reidemeister move.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_reidemeisterOne_inl {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) (x : Fin (4 * n)) :
    (D.reidemeisterOne h b).orientation ((PDCode.halfEdgeSuccEquiv n) (Sum.inl x)) = D.orientation x

    Inserting an oriented kink preserves the orientation of every old half-edge.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_reidemeisterOne_zero {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) :
    (D.reidemeisterOne h b).orientation ((PDCode.halfEdgeSuccEquiv n) (Sum.inr 0)) = !D.orientation h

    Slot zero of the inserted crossing points opposite to the terminal orientation of the cut arc.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_reidemeisterOne_one {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) :
    (D.reidemeisterOne h b).orientation ((PDCode.halfEdgeSuccEquiv n) (Sum.inr 1)) = D.orientation h

    Slot one of the inserted crossing has the terminal orientation of the cut arc.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_reidemeisterOne_two {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) :
    (D.reidemeisterOne h b).orientation ((PDCode.halfEdgeSuccEquiv n) (Sum.inr 2)) = D.orientation h

    Slot two of the inserted crossing has the terminal orientation of the cut arc.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_reidemeisterOne_three {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) :
    (D.reidemeisterOne h b).orientation ((PDCode.halfEdgeSuccEquiv n) (Sum.inr 3)) = !D.orientation h

    Slot three of the inserted crossing points opposite to the terminal orientation of the cut arc.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossinglessComponents_reidemeisterOne {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) :
    (D.reidemeisterOne h b).crossinglessComponents = D.crossinglessComponents

    The first Reidemeister move preserves the oriented crossing-free components.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossingSign_reidemeisterOne_castSucc {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) (i : Fin n) :
    (D.reidemeisterOne h b).crossingSign i.castSucc = D.crossingSign i

    Every old crossing keeps its sign after insertion of an oriented kink.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossingSign_reidemeisterOne_last {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) :
    (D.reidemeisterOne h b).crossingSign (Fin.last n) = if b = true then 1 else -1

    The new crossing in an oriented kink is positive exactly when its over-pair indicator is true.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.writhe_reidemeisterOne {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) :
    (D.reidemeisterOne h b).writhe = D.writhe + if b = true then 1 else -1

    Inserting an oriented kink changes the writhe by the sign of the new crossing.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.normalizedKauffmanBracket_reidemeisterOne {n : ℕ} {R : Type u_1} [CommRing R] (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) (a : Rˣ) :
    (D.reidemeisterOne h b).normalizedKauffmanBracket a = D.normalizedKauffmanBracket a

    The writhe-normalized Kauffman bracket is invariant under the oriented first Reidemeister move.