Crossing insertion and the skein relation of the Kauffman bracket

Kauffman's bracket satisfies the skein relation: at a crossing of a diagram D, ⟨D⟩ = A ⟨D_A⟩ + A⁻¹ ⟨D_B⟩, where D_A and D_B are the diagrams obtained by smoothing that crossing in its two ways. Together with its value on the unknot and its behaviour under adding a disjoint circle, this determines the bracket. This file proves the relation for the state-sum bracket TauCeti.PDCode.kauffmanBracket of PD-codes, at a crossing none of whose four arcs returns to it.

On a PD-code D with n crossings, TauCeti.PDCode.insertCrossing D p q b adds such a crossing: it cuts the arc P ending at the half-edge p and the arc Q ending at the half-edge q, and routes them across each other through one new crossing, the last one, Fin.last n. With the slots of a crossing in counterclockwise order, its slot 0 is joined to p, slot 1 to q, slot 2 to the other end D.edgePair.val p of P and slot 3 to the other end D.edgePair.val q of Q, so that P runs through slots 0 and 2 and Q through slots 1 and 3. The Boolean b is the over-pair indicator of the new crossing: with b = false the strand along P is over. The insertion is meaningful for two distinct arcs, that is, for q ≠ p and q ≠ D.edgePair.val p, and the results below assume this. Like TauCeti.PDCode.insertClasp, it is an algebraic operation on the code: it makes no claim about planarity.

A smoothing of the new crossing joins the four cut ends in two pairs without crossing. One of them joins p to q and D.edgePair.val p to D.edgePair.val q; this is the code TauCeti.PDCode.reconnect D p q, in which only these two arcs of D change. The other joins p to D.edgePair.val q and q to D.edgePair.val p, which is D.reconnect p (D.edgePair.val q). A state of the new code is a state of D together with a choice at the new crossing, and its smoothed diagram is the smoothed diagram of the corresponding reconnection of D (TauCeti.PDCode.stateLoopCount_insertCrossing). Summing over the states gives the skein relation TauCeti.PDCode.kauffmanBracket_insertCrossing: the bracket of the new code is a times the bracket of the reconnection by its A-smoothing plus a⁻¹ times that of the reconnection by its B-smoothing. Comparing the two crossings with opposite over-strands eliminates one reconnection, TauCeti.PDCode.kauffmanBracket_insertCrossing_sub. Following the strands instead of a smoothing, both of them go straight through the new crossing, so the insertion keeps the number of components.

Main definitions

• TauCeti.PDCode.insertCrossing: route two arcs across each other through a new crossing.

Main results

• TauCeti.PDCode.stateLoopCount_insertCrossing: a state of the new code leaves as many circles as the corresponding reconnection of the old code.
• TauCeti.PDCode.kauffmanBracket_insertCrossing: the skein relation of the Kauffman bracket.
• TauCeti.PDCode.kauffmanBracket_insertCrossing_sub: a times the bracket with the strand along Q over, minus a⁻¹ times the bracket with the strand along P over, is a multiple of the bracket of D.reconnect p q.
• TauCeti.PDCode.crossingComponentCount_insertCrossing: the insertion keeps the number of components.
• TauCeti.PDCode.mirror_insertCrossing: mirroring the new code inserts the crossing with the other strand over into 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 3, Definition 3.1 (the skein relation defining the bracket).
• M. Mastin, Links and Planar Diagram Codes, Definitions 2-3 (the PD convention).

The arcs of an inserted crossing, on the old half-edges and the new slots

The arcs of a code with a crossing inserted are built as a perfect matching of α ⊕ Fin 4: α holds the old half-edges and Fin 4 the four slots of the new crossing. With E the old arcs, the arcs from p to E.val p and from q to E.val q are cut and joined to the slots. These helpers serve only the proofs in this file.

def TauCeti.PDCode.insertCrossing {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) (b : Bool) : PDCode (n + 1)

Crossing insertion: route the arc of D ending at the half-edge p and the arc ending at q across each other through a new crossing, with over-pair indicator b. The new crossing is Fin.last n; its slots 0, 1, 2 and 3 are joined to p, q, D.edgePair.val p and D.edgePair.val q, so the first arc runs through slots 0 and 2, and the second through slots 1 and 3. With b = false the strand along the first arc is over, with b = true the strand along the second. The insertion is meaningful for two distinct arcs, q ≠ p and q ≠ D.edgePair.val p.

Equations

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

@[simp]

theorem TauCeti.PDCode.insertCrossing_crossing_castSucc {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) (b : Bool) (i : Fin n) (slot : Fin 4) : (D.insertCrossing p q 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.insertCrossing_crossing_last {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) (b : Bool) (slot : Fin 4) : (D.insertCrossing p q 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.insertCrossing_overPair_castSucc {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) (b : Bool) (i : Fin n) : (D.insertCrossing p q b).overPair i.castSucc = D.overPair i

The old crossings keep their over-strands.

@[simp]

theorem TauCeti.PDCode.insertCrossing_overPair_last {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) (b : Bool) : (D.insertCrossing p q b).overPair (Fin.last n) = b

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

@[simp]

theorem TauCeti.PDCode.insertCrossing_crossinglessComponentCount {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) (b : Bool) : (D.insertCrossing p q b).crossinglessComponentCount = D.crossinglessComponentCount

The insertion keeps the crossing-free circles.

@[simp]

theorem TauCeti.PDCode.mirror_insertCrossing {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) (b : Bool) : (D.insertCrossing p q b).mirror = D.mirror.insertCrossing p q !b

Mirroring the new code inserts the crossing with the other strand over into the mirror code.

@[simp]

theorem TauCeti.PDCode.insertCrossing_edgePair_inl_self {n : ℕ} {D : PDCode n} {p q : Fin (4 * n)} (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) : ↑(D.insertCrossing p q b).edgePair ((halfEdgeSuccEquiv n) (Sum.inl p)) = (halfEdgeSuccEquiv n) (Sum.inr 0)

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

@[simp]

theorem TauCeti.PDCode.insertCrossing_edgePair_inr_zero {n : ℕ} {D : PDCode n} {p q : Fin (4 * n)} (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) : ↑(D.insertCrossing p q b).edgePair ((halfEdgeSuccEquiv n) (Sum.inr 0)) = (halfEdgeSuccEquiv n) (Sum.inl p)

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

@[simp]

theorem TauCeti.PDCode.insertCrossing_edgePair_inl_right {n : ℕ} {D : PDCode n} {p q : Fin (4 * n)} (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) : ↑(D.insertCrossing p q b).edgePair ((halfEdgeSuccEquiv n) (Sum.inl q)) = (halfEdgeSuccEquiv n) (Sum.inr 1)

The half-edge q is joined to slot 1 of the new crossing.

@[simp]

theorem TauCeti.PDCode.insertCrossing_edgePair_inr_one {n : ℕ} {D : PDCode n} {p q : Fin (4 * n)} (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) : ↑(D.insertCrossing p q b).edgePair ((halfEdgeSuccEquiv n) (Sum.inr 1)) = (halfEdgeSuccEquiv n) (Sum.inl q)

Slot 1 of the new crossing is joined to the half-edge q.

@[simp]

theorem TauCeti.PDCode.insertCrossing_edgePair_inl_edgePair_self {n : ℕ} {D : PDCode n} {p q : Fin (4 * n)} (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) : ↑(D.insertCrossing p q b).edgePair ((halfEdgeSuccEquiv n) (Sum.inl (↑D.edgePair p))) = (halfEdgeSuccEquiv n) (Sum.inr 2)

The other end of the first cut arc is joined to slot 2 of the new crossing.

@[simp]

theorem TauCeti.PDCode.insertCrossing_edgePair_inr_two {n : ℕ} {D : PDCode n} {p q : Fin (4 * n)} (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) : ↑(D.insertCrossing p q b).edgePair ((halfEdgeSuccEquiv n) (Sum.inr 2)) = (halfEdgeSuccEquiv n) (Sum.inl (↑D.edgePair p))

Slot 2 of the new crossing is joined to the other end of the first cut arc.

@[simp]

theorem TauCeti.PDCode.insertCrossing_edgePair_inl_edgePair_right {n : ℕ} {D : PDCode n} {p q : Fin (4 * n)} (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) : ↑(D.insertCrossing p q b).edgePair ((halfEdgeSuccEquiv n) (Sum.inl (↑D.edgePair q))) = (halfEdgeSuccEquiv n) (Sum.inr 3)

The other end of the second cut arc is joined to slot 3 of the new crossing.

@[simp]

theorem TauCeti.PDCode.insertCrossing_edgePair_inr_three {n : ℕ} {D : PDCode n} {p q : Fin (4 * n)} (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) : ↑(D.insertCrossing p q b).edgePair ((halfEdgeSuccEquiv n) (Sum.inr 3)) = (halfEdgeSuccEquiv n) (Sum.inl (↑D.edgePair q))

Slot 3 of the new crossing is joined to the other end of the second cut arc.

@[simp]

theorem TauCeti.PDCode.insertCrossing_edgePair_inl_of_ne {n : ℕ} {D : PDCode n} {p q : Fin (4 * n)} (b : Bool) {x : Fin (4 * n)} (hxp : x ≠ p) (hxq : x ≠ q) (hxe : x ≠ ↑D.edgePair p) (hxe' : x ≠ ↑D.edgePair q) : ↑(D.insertCrossing p q b).edgePair ((halfEdgeSuccEquiv n) (Sum.inl x)) = (halfEdgeSuccEquiv n) (Sum.inl (↑D.edgePair x))

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

@[simp]

theorem TauCeti.PDCode.stateLoopCount_insertCrossing {n : ℕ} {D : PDCode n} {p q : Fin (4 * n)} {b : Bool} (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) (s : Fin (n + 1) → Bool) : (D.insertCrossing p q b).stateLoopCount s = (D.reconnect p (if s (Fin.last n) = b then q else ↑D.edgePair q)).stateLoopCount (Fin.init s)

Circles after a crossing insertion. A state of the new code leaves as many circles as its restriction to the old crossings leaves in the reconnection of the old code by its smoothing at the new crossing: D.reconnect p q when that choice is b, and D.reconnect p (D.edgePair.val q) otherwise.

theorem TauCeti.PDCode.kauffmanBracket_insertCrossing {n : ℕ} {D : PDCode 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.insertCrossing p q b).kauffmanBracket a = ↑a * (D.reconnect p (bif b then q else ↑D.edgePair q)).kauffmanBracket a + ↑a⁻¹ * (D.reconnect p (bif b then ↑D.edgePair q else q)).kauffmanBracket a

The skein relation of the Kauffman bracket. The bracket of a code with a crossing inserted is a times the bracket of the reconnection by the A-smoothing of the new crossing plus a⁻¹ times the bracket of the reconnection by its B-smoothing. With b = true the A-smoothing joins p to q, with b = false it joins p to D.edgePair.val q.

theorem TauCeti.PDCode.kauffmanBracket_insertCrossing_sub {n : ℕ} {D : PDCode n} {p q : Fin (4 * n)} (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) {R : Type u_1} [CommRing R] (a : Rˣ) : ↑a * (D.insertCrossing p q true).kauffmanBracket a - ↑a⁻¹ * (D.insertCrossing p q false).kauffmanBracket a = (↑a ^ 2 - ↑a⁻¹ ^ 2) * (D.reconnect p q).kauffmanBracket a

Comparing the two crossings. a times the bracket of D.insertCrossing p q true, whose new crossing has the strand along the second arc over, minus a⁻¹ times the bracket of D.insertCrossing p q false, whose new crossing has the strand along the first arc over, is a ^ 2 - a⁻¹ ^ 2 times the bracket of D.reconnect p q: the reconnection joining p to D.edgePair.val q cancels.

@[simp]

theorem TauCeti.PDCode.crossingComponentCount_insertCrossing {n : ℕ} {D : PDCode n} {p q : Fin (4 * n)} {b : Bool} (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) : (D.insertCrossing p q b).crossingComponentCount = D.crossingComponentCount

Crossing insertion keeps the number of components: both strands go straight through the new crossing.