Reidemeister clasps between two crossing-free circles

The closed two-crossing clasp has two link components and four faces. Its two crossings have complementary over-pair indicators, so one component passes over the other twice. Its Kauffman bracket is the circle value, just as for the two-component unlink.

PDCode.adjoinTwoCircleClasp places this clasp beside any surrounding diagram. It is compared with adjoining two crossing-free circles, including when the surrounding diagram is empty. This supplies the second Reidemeister move whose two participating components have no half-edges before the move. The matching closes the four ports of the local clasp used by PDCode.insertCircleClasp.

References

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

def TauCeti.PDCode.twoCircleClasp (b : Bool) : PDCode 2

The closed Reidemeister II clasp on two circles. The arcs pair labels x and 7 - x: slots 2–1 and 3–0 form the bigon, and slots 0–3 and 1–2 close its ports. The bit b selects the over-strand at the first crossing.

Equations

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

@[simp]

theorem TauCeti.PDCode.twoCircleClasp_halfEdge (b : Bool) : (twoCircleClasp b).halfEdge = 1

The clasp numbers half-edges consecutively by crossing slots.

@[simp]

theorem TauCeti.PDCode.twoCircleClasp_edgePair_val (b : Bool) : ↑(twoCircleClasp b).edgePair = (crossingSlotEquiv 2).permCongr (Equiv.prodCongr Fin.revPerm Fin.revPerm)

The arc matching reverses both the crossing index and the slot index.

@[simp]

theorem TauCeti.PDCode.twoCircleClasp_crossinglessComponentCount (b : Bool) : (twoCircleClasp b).crossinglessComponentCount = 0

Both circles visit the crossings.

@[simp]

theorem TauCeti.PDCode.twoCircleClasp_overPair (b : Bool) (i : Fin 2) : (twoCircleClasp b).overPair i = ![b, !b] i

The over-pair indicators are complementary, keeping the same physical component over.

@[simp]

theorem TauCeti.PDCode.mirror_twoCircleClasp (b : Bool) : (twoCircleClasp b).mirror = twoCircleClasp !b

Reflection exchanges the two choices of over-component.

@[simp]

theorem TauCeti.PDCode.componentCount_twoCircleClasp (b : Bool) : (twoCircleClasp b).componentCount = 2

The clasp has two link components.

@[simp]

theorem TauCeti.PDCode.faceCount_twoCircleClasp (b : Bool) : (twoCircleClasp b).faceCount = 4

The closed clasp has four complementary regions.

theorem TauCeti.PDCode.isConnected_twoCircleClasp (b : Bool) : (twoCircleClasp b).toPermutationTriple.IsConnected

The crossing graph of the closed clasp is connected.

@[simp]

theorem TauCeti.PDCode.isPlanar_twoCircleClasp (b : Bool) : (twoCircleClasp b).IsPlanar

The closed clasp is a planar diagram.

@[simp]

theorem TauCeti.PDCode.stateLoopCount_twoCircleClasp (b : Bool) (s : Fin 2 → Bool) : (twoCircleClasp b).stateLoopCount s = if s 0 = s 1 then 1 else 2

Equal state choices yield one smoothing circle, and unequal choices yield two.

@[simp]

theorem TauCeti.PDCode.kauffmanBracket_twoCircleClasp {R : Type u_1} [CommRing R] (b : Bool) (a : Rˣ) : (twoCircleClasp b).kauffmanBracket a = TemperleyLieb.jonesDelta a

The bracket of the closed clasp equals that of the two-component unlink.

def TauCeti.PDCode.adjoinTwoCircleClasp {n : ℕ} (D : PDCode n) (b : Bool) : PDCode (n + 2)

Adjoin a cancelling clasp between two additional circles in a disc disjoint from D. It replaces the two circles of D.adjoinCircle.adjoinCircle by crossing-bearing circles.

Equations

• D.adjoinTwoCircleClasp b = D.disjointUnion (TauCeti.PDCode.twoCircleClasp b)

theorem TauCeti.PDCode.adjoinTwoCircleClasp_def {n : ℕ} (D : PDCode n) (b : Bool) : D.adjoinTwoCircleClasp b = D.disjointUnion (twoCircleClasp b)

The disjoint-union characterization of clasp adjunction.

@[simp]

theorem TauCeti.PDCode.crossinglessComponentCount_adjoinTwoCircleClasp {n : ℕ} (D : PDCode n) (b : Bool) : (D.adjoinTwoCircleClasp b).crossinglessComponentCount = D.crossinglessComponentCount

The old crossing-free components are retained.

@[simp]

theorem TauCeti.PDCode.componentCount_adjoinTwoCircleClasp {n : ℕ} (D : PDCode n) (b : Bool) : (D.adjoinTwoCircleClasp b).componentCount = D.componentCount + 2

The two clasp circles contribute two link components.

@[simp]

theorem TauCeti.PDCode.mirror_adjoinTwoCircleClasp {n : ℕ} (D : PDCode n) (b : Bool) : (D.adjoinTwoCircleClasp b).mirror = D.mirror.adjoinTwoCircleClasp !b

Reflection swaps the over-component in the adjoined clasp.

@[simp]

theorem TauCeti.PDCode.isPlanar_adjoinTwoCircleClasp {n : ℕ} (D : PDCode n) (b : Bool) : (D.adjoinTwoCircleClasp b).IsPlanar ↔ D.IsPlanar

Adjoining the planar clasp preserves and reflects planarity of the surrounding diagram.

@[simp]

theorem TauCeti.PDCode.kauffmanBracket_adjoinTwoCircleClasp {n : ℕ} {R : Type u_1} [CommRing R] (D : PDCode n) (b : Bool) (a : Rˣ) : (D.adjoinTwoCircleClasp b).kauffmanBracket a = D.adjoinCircle.adjoinCircle.kauffmanBracket a

The two-circle second move preserves the bracket in every surrounding diagram, including the empty diagram.