Documentation

TauCeti.KnotTheory.PDCode.Oriented.Reidemeister.Two.Basic

Oriented circle-and-arc Reidemeister clasps #

Lift PDCode.insertCircleClasp to oriented diagrams, retaining the direction of the chosen arc and specifying the new circle's direction. The new crossings have opposite signs, so the writhe is unchanged. The normalized Kauffman bracket and Jones polynomial agree with those of the original diagram with that oriented circle adjoined.

References #

source
def TauCeti.OrientedPDCode.insertCircleClasp {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) :
OrientedPDCode (n + 2)

Push a new oriented circle across the arc ending at p. The circle's direction is o, and the first crossing has over-pair indicator b.

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

    Forgetting orientation gives the underlying circle-and-arc clasp.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_insertCircleClasp_old {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) (x : Fin (4 * n)) :
    (D.insertCircleClasp p o b).orientation ((PDCode.halfEdgeSuccEquiv (n + 1)) (Sum.inl ((PDCode.halfEdgeSuccEquiv n) (Sum.inl x)))) = D.orientation x

    The insertion retains the orientation of every old half-edge.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_insertCircleClasp_first {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) (s : Fin 4) :
    (D.insertCircleClasp p o b).orientation ((PDCode.halfEdgeSuccEquiv (n + 1)) (Sum.inl ((PDCode.halfEdgeSuccEquiv n) (Sum.inr s)))) = ![!D.orientation p, !o, D.orientation p, o] s

    Orientations at the first new crossing.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_insertCircleClasp_second {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) (s : Fin 4) :
    (D.insertCircleClasp p o b).orientation ((PDCode.halfEdgeSuccEquiv (n + 1)) (Sum.inr s)) = ![!o, !D.orientation p, o, D.orientation p] s

    Orientations at the second new crossing.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossinglessComponents_insertCircleClasp {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) :
    (D.insertCircleClasp p o b).crossinglessComponents = D.crossinglessComponents

    Existing crossing-free components retain their chosen directions.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossingSign_insertCircleClasp_castSucc_castSucc {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) (i : Fin n) :
    (D.insertCircleClasp p o b).crossingSign i.castSucc.castSucc = D.crossingSign i

    Every old crossing keeps its sign.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossingSign_insertCircleClasp_last {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) :
    (D.insertCircleClasp p o b).crossingSign (Fin.last (n + 1)) = -(D.insertCircleClasp p o b).crossingSign (Fin.last n).castSucc

    The two new crossings have opposite signs.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.writhe_insertCircleClasp {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) :
    (D.insertCircleClasp p o b).writhe = D.writhe

    The circle-and-arc clasp preserves writhe.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.mirror_insertCircleClasp {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) :
    (D.insertCircleClasp p o b).mirror = D.mirror.insertCircleClasp p o !b

    Reflection exchanges the over-strand and retains the new circle's direction.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.reverse_insertCircleClasp {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) :
    (D.insertCircleClasp p o b).reverse = D.reverse.insertCircleClasp p (!o) b

    Reversing all components also reverses the new circle's direction.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.normalizedKauffmanBracket_insertCircleClasp {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) {R : Type u_1} [CommRing R] (a : Rˣ) :
    (D.insertCircleClasp p o b).normalizedKauffmanBracket a = (D.adjoinCircle o).normalizedKauffmanBracket a

    The writhe-normalized bracket is invariant under the circle-and-arc move.