Oriented Reidemeister clasps between two crossing-free circles

Orient the two components of the closed clasp independently. The signs of the two crossings are opposite, and its writhe is zero. Adjoining this clasp to any oriented diagram has the same normalized bracket and Jones polynomial as adjoining the two oriented crossing-free circles. Both over-component choices and all four component orientations are included.

The slot orientations follow those of OrientedPDCode.insertCircleClasp, with both outside arcs closed. Disjoint union transports the local polynomial identity into the surrounding code without assuming that it is nonempty or planar.

References

• W. B. R. Lickorish, An Introduction to Knot Theory, GTM 175 (1997), Chapter 3, Lemma 3.3 and Theorem 3.5.
• L. H. Kauffman, State models and the Jones polynomial, Topology 26 (1987), 395–407.

def TauCeti.OrientedPDCode.twoCircleClasp (o₁ o₂ b : Bool) : OrientedPDCode 2

Orient the two circles of the closed Reidemeister clasp by o₁ and o₂. At its first crossing, slots 2 and 3 have directions o₁ and o₂, respectively. The bit b selects its over-strand.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.OrientedPDCode.toPDCode_twoCircleClasp (o₁ o₂ b : Bool) : (twoCircleClasp o₁ o₂ b).toPDCode = PDCode.twoCircleClasp b

Forgetting orientation gives the closed unoriented clasp.

@[simp]

theorem TauCeti.OrientedPDCode.orientation_twoCircleClasp (o₁ o₂ b : Bool) (i : Fin 2) (s : Fin 4) : (twoCircleClasp o₁ o₂ b).orientation ((PDCode.crossingSlotEquiv 2) (i, s)) = (if i = 0 then ![!o₁, !o₂, o₁, o₂] else ![!o₂, !o₁, o₂, o₁]) s

The first component has direction o₁, and the second has direction o₂.

@[simp]

theorem TauCeti.OrientedPDCode.crossinglessComponents_twoCircleClasp (o₁ o₂ b : Bool) : (twoCircleClasp o₁ o₂ b).crossinglessComponents = 0

Neither component remains crossing-free.

@[simp]

theorem TauCeti.OrientedPDCode.crossingSign_twoCircleClasp_one (o₁ o₂ b : Bool) : (twoCircleClasp o₁ o₂ b).crossingSign 1 = -(twoCircleClasp o₁ o₂ b).crossingSign 0

The two crossings have opposite signs for every choice of component directions.

@[simp]

theorem TauCeti.OrientedPDCode.writhe_twoCircleClasp (o₁ o₂ b : Bool) : (twoCircleClasp o₁ o₂ b).writhe = 0

The cancelling pair contributes zero writhe.

@[simp]

theorem TauCeti.OrientedPDCode.mirror_twoCircleClasp (o₁ o₂ b : Bool) : (twoCircleClasp o₁ o₂ b).mirror = twoCircleClasp o₁ o₂ !b

Reflection exchanges the over-component without changing its direction.

@[simp]

theorem TauCeti.OrientedPDCode.reverse_twoCircleClasp (o₁ o₂ b : Bool) : (twoCircleClasp o₁ o₂ b).reverse = twoCircleClasp (!o₁) (!o₂) b

Reversing all components flips the two specified circle directions.

def TauCeti.OrientedPDCode.adjoinTwoCircleClasp {n : ℕ} (D : OrientedPDCode n) (o₁ o₂ b : Bool) : OrientedPDCode (n + 2)

Adjoin a cancelling clasp between two additional oriented circles in a disc disjoint from D. Compare it with (D.adjoinCircle o₁).adjoinCircle o₂.

Equations

• D.adjoinTwoCircleClasp o₁ o₂ b = D.disjointUnion (TauCeti.OrientedPDCode.twoCircleClasp o₁ o₂ b)

theorem TauCeti.OrientedPDCode.adjoinTwoCircleClasp_def {n : ℕ} (D : OrientedPDCode n) (o₁ o₂ b : Bool) : D.adjoinTwoCircleClasp o₁ o₂ b = D.disjointUnion (twoCircleClasp o₁ o₂ b)

The oriented disjoint-union characterization of clasp adjunction.

@[simp]

theorem TauCeti.OrientedPDCode.toPDCode_adjoinTwoCircleClasp {n : ℕ} (D : OrientedPDCode n) (o₁ o₂ b : Bool) : (D.adjoinTwoCircleClasp o₁ o₂ b).toPDCode = D.adjoinTwoCircleClasp b

Forgetting directions gives the unoriented two-circle move.

@[simp]

theorem TauCeti.OrientedPDCode.crossinglessComponents_adjoinTwoCircleClasp {n : ℕ} (D : OrientedPDCode n) (o₁ o₂ b : Bool) : (D.adjoinTwoCircleClasp o₁ o₂ b).crossinglessComponents = D.crossinglessComponents

Every old crossing-free component retains its direction.

@[simp]

theorem TauCeti.OrientedPDCode.writhe_adjoinTwoCircleClasp {n : ℕ} (D : OrientedPDCode n) (o₁ o₂ b : Bool) : (D.adjoinTwoCircleClasp o₁ o₂ b).writhe = D.writhe

The two-circle move preserves writhe.

@[simp]

theorem TauCeti.OrientedPDCode.mirror_adjoinTwoCircleClasp {n : ℕ} (D : OrientedPDCode n) (o₁ o₂ b : Bool) : (D.adjoinTwoCircleClasp o₁ o₂ b).mirror = D.mirror.adjoinTwoCircleClasp o₁ o₂ !b

Reflection swaps the over-component of the adjoined clasp.

@[simp]

theorem TauCeti.OrientedPDCode.reverse_adjoinTwoCircleClasp {n : ℕ} (D : OrientedPDCode n) (o₁ o₂ b : Bool) : (D.adjoinTwoCircleClasp o₁ o₂ b).reverse = D.reverse.adjoinTwoCircleClasp (!o₁) (!o₂) b

Reversal flips both adjoined component directions.

@[simp]

theorem TauCeti.OrientedPDCode.normalizedKauffmanBracket_adjoinTwoCircleClasp {n : ℕ} {R : Type u_1} [CommRing R] (D : OrientedPDCode n) (o₁ o₂ b : Bool) (a : Rˣ) : (D.adjoinTwoCircleClasp o₁ o₂ b).normalizedKauffmanBracket a = ((D.adjoinCircle o₁).adjoinCircle o₂).normalizedKauffmanBracket a

The normalized bracket is unchanged by the two-circle second Reidemeister move, with no nonemptiness assumption on the surrounding diagram.