Documentation

TauCeti.KnotTheory.PDCode.Oriented.ClaspInsertion

Clasp insertion on oriented PD-codes #

TauCeti.PDCode.insertClasp cuts two arcs of a PD-code open and routes them through a clasp of two new crossings; when the two arcs border a common face this is the second Reidemeister move. This file lifts the insertion to oriented codes. Each cut arc keeps its direction, which fixes the orientations of the eight new half-edges, so the oriented insertion takes no data beyond the unoriented one.

Whatever the directions of the two arcs, the two new crossings have opposite signs: they have the same orientation parity, and the same strand is over at both, which with the slot conventions of a clasp means opposite over-pair indicators. The insertion therefore keeps the writhe. Together with the invariance of the Kauffman bracket (TauCeti.PDCode.kauffmanBracket_insertClasp), this makes the writhe-normalized Kauffman bracket invariant under the oriented insertion, and in particular under the oriented second Reidemeister move.

Main definitions #

Main results #

References #

source
def TauCeti.OrientedPDCode.insertClasp {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) :
OrientedPDCode (n + 2)

Clasp insertion on an oriented PD-code: the clasp insertion TauCeti.PDCode.insertClasp into the arc ending at p and the distinct arc ending at q, with each cut arc keeping its direction. Along the arc ending at p, the new half-edges at slots 0 and 2 of the first new crossing and at slots 1 and 3 of the second alternate between the orientations !D.orientation p and D.orientation p, and likewise along the arc ending at q through slots 1 and 3 of the first new crossing and slots 0 and 2 of the second.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.OrientedPDCode.toPDCode_insertClasp {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) :
    (D.insertClasp p q b hqp hqe).toPDCode = D.insertClasp p q b hqp hqe

    Forgetting the orientation of the oriented clasp insertion gives the unoriented one.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_insertClasp_inl_inl {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) (x : Fin (4 * n)) :
    (D.insertClasp p q b hqp hqe).orientation ((PDCode.halfEdgeSuccEquiv (n + 1)) (Sum.inl ((PDCode.halfEdgeSuccEquiv n) (Sum.inl x)))) = D.orientation x

    The oriented clasp insertion keeps the orientation of every old half-edge.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_insertClasp_inl_inr {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) (slot : Fin 4) :
    (D.insertClasp p q b hqp hqe).orientation ((PDCode.halfEdgeSuccEquiv (n + 1)) (Sum.inl ((PDCode.halfEdgeSuccEquiv n) (Sum.inr slot)))) = ![!D.orientation p, !D.orientation q, D.orientation p, D.orientation q] slot

    The orientations of the slots of the first new crossing: slots 0 and 2 lie on the arc ending at p, slots 1 and 3 on the arc ending at q.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_insertClasp_inr {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) (slot : Fin 4) :
    (D.insertClasp p q b hqp hqe).orientation ((PDCode.halfEdgeSuccEquiv (n + 1)) (Sum.inr slot)) = ![!D.orientation q, !D.orientation p, D.orientation q, D.orientation p] slot

    The orientations of the slots of the second new crossing: slots 0 and 2 lie on the arc ending at q, slots 1 and 3 on the arc ending at p.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossinglessComponents_insertClasp {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) :
    (D.insertClasp p q b hqp hqe).crossinglessComponents = D.crossinglessComponents

    The oriented clasp insertion keeps the oriented crossing-free components.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossingSign_insertClasp_castSucc_castSucc {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) (i : Fin n) :
    (D.insertClasp p q b hqp hqe).crossingSign i.castSucc.castSucc = D.crossingSign i

    Every old crossing keeps its sign after the oriented clasp insertion.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossingSign_insertClasp_castSucc_last {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) :
    (D.insertClasp p q b hqp hqe).crossingSign (Fin.last n).castSucc = if (D.orientation p ^^ D.orientation q) = b then 1 else -1

    The first new crossing is positive exactly when the parity of the directions of the two cut arcs is its over-pair indicator b.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossingSign_insertClasp_last {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) :
    (D.insertClasp p q b hqp hqe).crossingSign (Fin.last (n + 1)) = -(D.insertClasp p q b hqp hqe).crossingSign (Fin.last n).castSucc

    The two new crossings of an oriented clasp have opposite signs.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.writhe_insertClasp {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) :
    (D.insertClasp p q b hqp hqe).writhe = D.writhe

    The oriented clasp insertion keeps the writhe.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.normalizedKauffmanBracket_insertClasp {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) {R : Type u_1} [CommRing R] (a : Rˣ) :
    (D.insertClasp p q b hqp hqe).normalizedKauffmanBracket a = D.normalizedKauffmanBracket a

    The writhe-normalized Kauffman bracket is invariant under the oriented clasp insertion, in particular under the oriented second Reidemeister move.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.mirror_insertClasp {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) :
    (D.insertClasp p q b hqp hqe).mirror = D.mirror.insertClasp p q (!b) hqp ⋯

    Reflecting the oriented clasp insertion inserts the clasp with the other strand over into the reflected code.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.reverse_insertClasp {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) :
    (D.insertClasp p q b hqp hqe).reverse = D.reverse.insertClasp p q b hqp ⋯

    Reversing the oriented clasp insertion inserts the clasp into the reversed code.