The first Reidemeister move on PD-codes

The first Reidemeister move adds a kink to an arc of a diagram: the arc is cut open and a small loop crossing itself once is spliced in. On a PD-code with n crossings, TauCeti.PDCode.reidemeisterOne D h b adds this kink to the arc ending at the half-edge h. The new crossing is the last one, Fin.last n, and its four slots take the last four half-edge positions (TauCeti.PDCode.halfEdgeSuccEquiv). Slot 0 is joined to h, slot 1 to the other end of the old arc, and slots 2 and 3 to each other. So the strand coming from h enters at slot 0, leaves through slot 2, comes back round the loop into slot 3, and leaves through slot 1. The Boolean b is the over-pair indicator of the new crossing. With b = true the crossing looks like the one of TauCeti.PDCode.kink, which is the kink added to a crossing-free circle instead.

The move keeps the number of components. A state of the new code leaves the circles of its restriction to the old crossings, plus one more exactly when its smoothing at the new crossing joins slot 2 to slot 3 and so cuts the loop off; the other smoothing runs along the kink. That first smoothing is the A-smoothing when b = true and the B-smoothing when b = false, so the Kauffman bracket gets multiplied by a * δ + a⁻¹ = -a ^ 3 when b = true and by a + a⁻¹ * δ = -a⁻¹ ^ 3 when b = false, where δ = -(a ^ 2 + a⁻¹ ^ 2). Up to this framing factor the bracket is invariant under the first Reidemeister move. The writhe of an oriented code corrects that factor, and the second and third moves leave the bracket unchanged; neither is treated here.

Main definitions

• TauCeti.PDCode.reidemeisterOne: add a kink to an arc of a PD-code.

Main results

• TauCeti.PDCode.stateLoopCount_reidemeisterOne: a state of the new code leaves one circle more than its restriction to the old crossings exactly when it cuts off the loop of the kink.
• TauCeti.PDCode.crossingComponentCount_reidemeisterOne: the move keeps the number of components.
• TauCeti.PDCode.kauffmanBracket_reidemeisterOne: the move multiplies the Kauffman bracket by -a ^ 3 or -a⁻¹ ^ 3, depending on the crossing it adds.
• TauCeti.PDCode.mirror_reidemeisterOne: mirroring the new code adds the mirror kink to the mirror code.

References

• L. H. Kauffman, State models and the Jones polynomial, Topology 26 (1987), 395-407.
• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 1 (the Reidemeister moves) and Chapter 3 (the bracket under the Reidemeister moves).
• M. Mastin, Links and Planar Diagram Codes, Definitions 2-3 (the PD convention).

The arcs of a kink, on the sum of the old half-edges and the new slots

A kink's arcs are built as a permutation of α ⊕ Fin 4: α holds the old half-edges and Fin 4 the four slots of the new crossing. With e the old arcs and h a half-edge, the arc from h to e h is cut and spliced through the slots. This helper and the orbit counts below serve only the proofs in this file.

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

The first Reidemeister move: add a kink, with over-pair indicator b, to the arc of D ending at the half-edge h. The new crossing is Fin.last n. Its slot 0 is joined to h, its slot 1 to the other end D.edgePair.val h of the old arc, and its slots 2 and 3 to each other.

Equations

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

@[simp]

theorem TauCeti.PDCode.reidemeisterOne_crossing_castSucc {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) (i : Fin n) (slot : Fin 4) : (D.reidemeisterOne h b).halfEdge ((halfEdgeSuccEquiv n) (Sum.inl ((crossingSlotEquiv n) (i, slot)))) = (halfEdgeSuccEquiv n) (Sum.inl (D.crossing i slot))

The old crossings keep their half-edges.

@[simp]

theorem TauCeti.PDCode.reidemeisterOne_crossing_last {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) (slot : Fin 4) : (D.reidemeisterOne h b).halfEdge ((halfEdgeSuccEquiv n) (Sum.inr slot)) = (halfEdgeSuccEquiv n) (Sum.inr slot)

The slots of the new crossing are the four new half-edges.

@[simp]

theorem TauCeti.PDCode.reidemeisterOne_overPair_castSucc {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) (i : Fin n) : (D.reidemeisterOne h b).overPair i.castSucc = D.overPair i

The old crossings keep their over-strands.

@[simp]

theorem TauCeti.PDCode.reidemeisterOne_overPair_last {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) : (D.reidemeisterOne h b).overPair (Fin.last n) = b

The over-pair indicator of the new crossing is b.

@[simp]

theorem TauCeti.PDCode.reidemeisterOne_crossinglessComponentCount {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) : (D.reidemeisterOne h b).crossinglessComponentCount = D.crossinglessComponentCount

The move keeps the crossing-free circles.

@[simp]

theorem TauCeti.PDCode.reidemeisterOne_edgePair_inl_self {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) : ↑(D.reidemeisterOne h b).edgePair ((halfEdgeSuccEquiv n) (Sum.inl h)) = (halfEdgeSuccEquiv n) (Sum.inr 0)

The half-edge h is joined to slot 0 of the new crossing.

@[simp]

theorem TauCeti.PDCode.reidemeisterOne_edgePair_inr_zero {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) : ↑(D.reidemeisterOne h b).edgePair ((halfEdgeSuccEquiv n) (Sum.inr 0)) = (halfEdgeSuccEquiv n) (Sum.inl h)

Slot 0 of the new crossing is joined to the half-edge h.

@[simp]

theorem TauCeti.PDCode.reidemeisterOne_edgePair_inl_edgePair {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) : ↑(D.reidemeisterOne h b).edgePair ((halfEdgeSuccEquiv n) (Sum.inl (↑D.edgePair h))) = (halfEdgeSuccEquiv n) (Sum.inr 1)

The other end of the old arc is joined to slot 1 of the new crossing.

@[simp]

theorem TauCeti.PDCode.reidemeisterOne_edgePair_inr_one {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) : ↑(D.reidemeisterOne h b).edgePair ((halfEdgeSuccEquiv n) (Sum.inr 1)) = (halfEdgeSuccEquiv n) (Sum.inl (↑D.edgePair h))

Slot 1 of the new crossing is joined to the other end of the old arc.

@[simp]

theorem TauCeti.PDCode.reidemeisterOne_edgePair_inr_two {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) : ↑(D.reidemeisterOne h b).edgePair ((halfEdgeSuccEquiv n) (Sum.inr 2)) = (halfEdgeSuccEquiv n) (Sum.inr 3)

Slot 2 of the new crossing is joined to slot 3: this arc is the loop of the kink.

@[simp]

theorem TauCeti.PDCode.reidemeisterOne_edgePair_inr_three {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) : ↑(D.reidemeisterOne h b).edgePair ((halfEdgeSuccEquiv n) (Sum.inr 3)) = (halfEdgeSuccEquiv n) (Sum.inr 2)

Slot 3 of the new crossing is joined to slot 2.

@[simp]

theorem TauCeti.PDCode.reidemeisterOne_edgePair_inl_of_ne {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) {x : Fin (4 * n)} (hx : x ≠ h) (hx' : x ≠ ↑D.edgePair h) : ↑(D.reidemeisterOne h b).edgePair ((halfEdgeSuccEquiv n) (Sum.inl x)) = (halfEdgeSuccEquiv n) (Sum.inl (↑D.edgePair x))

Every half-edge off the cut arc keeps its old partner.

@[simp]

theorem TauCeti.PDCode.mirror_reidemeisterOne {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) : (D.reidemeisterOne h b).mirror = D.mirror.reidemeisterOne h !b

Mirroring the new code adds the mirror kink to the mirror code.

@[simp]

theorem TauCeti.PDCode.stateLoopCount_reidemeisterOne {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) (s : Fin (n + 1) → Bool) : (D.reidemeisterOne h b).stateLoopCount s = D.stateLoopCount (Fin.init s) + if s (Fin.last n) = b then 1 else 0

Circles after the first Reidemeister move. A state of the new code leaves one circle more than its restriction to the old crossings when its choice at the new crossing is b, the smoothing that cuts off the loop of the kink, and the same number of circles otherwise.

@[simp]

theorem TauCeti.PDCode.crossingComponentCount_reidemeisterOne {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) : (D.reidemeisterOne h b).crossingComponentCount = D.crossingComponentCount

The first Reidemeister move keeps the number of components.

@[simp]

theorem TauCeti.PDCode.kauffmanBracket_reidemeisterOne {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) (b : Bool) {R : Type u_1} [CommRing R] (a : Rˣ) : (D.reidemeisterOne h b).kauffmanBracket a = -↑(bif b then a else a⁻¹) ^ 3 * D.kauffmanBracket a

The Kauffman bracket under the first Reidemeister move. Adding a kink with over-pair indicator b multiplies the bracket by -a ^ 3 if b = true and by -a⁻¹ ^ 3 if b = false.