Successors after inserting two crossings on the same strand positions

Prepending two letters with the same generator index inserts two consecutive crossings on both affected strand positions. On each position, the old last crossing now leads to the first inserted crossing, the first inserted crossing leads to the second, and the second leads back to the old first crossing. If the position previously carried no crossing, the two inserted crossings instead form their own cycle. All other positions keep their successors.

These formulas identify the arcs that must be reconnected when removing an inverse pair from a braid closure by the second Reidemeister move. In particular, skipping the inserted pair recovers the original successor on every old crossing. The successor calculations allow arbitrary signs on the two letters; only the over-strand calculation requires them to be opposite. This file does not identify the resulting whole diagram with a Reidemeister move, which also requires the external arcs and crossing-free components to be matched.

The list calculations reuse List.formPerm_map_apply and the two append formulas from TauCeti.Data.List.Rotate.

References

• J. Birman, Braids, Links, and Mapping Class Groups, Chapter 2.
• W. B. R. Lickorish, An Introduction to Knot Theory, Chapter 1, the second Reidemeister move.

theorem TauCeti.BraidWord.nextCrossing_cons_cons_of_ne {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε η : ℤˣ) {p : Fin n} (hp : p ≠ BraidGroup.strand i) (hp' : p ≠ BraidGroup.strandSucc i) (j : Fin (List.length v)) : (nextCrossing ((i, ε) :: (i, η) :: v) p) j.succ.succ = ((v.nextCrossing p) j).succ.succ

On an unaffected position, every old successor is unchanged, after shifting indices.

@[simp]

theorem TauCeti.BraidWord.nextCrossing_cons_cons_zero {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε η : ℤˣ) {p : Fin n} (hp : p = BraidGroup.strand i ∨ p = BraidGroup.strandSucc i) : (nextCrossing ((i, ε) :: (i, η) :: v) p) 0 = 1

On either affected position, the first inserted crossing leads to the second.

@[simp]

theorem TauCeti.BraidWord.nextCrossing_cons_cons_one_of_nil {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε η : ℤˣ) {p : Fin n} (hp : p = BraidGroup.strand i ∨ p = BraidGroup.strandSucc i) (hv : v.crossingsAt p = []) : (nextCrossing ((i, ε) :: (i, η) :: v) p) 1 = 0

If an affected position previously had no crossing, the second inserted crossing returns to the first, giving a two-element cycle.

@[simp]

theorem TauCeti.BraidWord.nextCrossing_cons_cons_one_of_ne_nil {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε η : ℤˣ) {p : Fin n} (hp : p = BraidGroup.strand i ∨ p = BraidGroup.strandSucc i) (hv : v.crossingsAt p ≠ []) : (nextCrossing ((i, ε) :: (i, η) :: v) p) 1 = ((v.crossingsAt p).head hv).succ.succ

If an affected position already carried crossings, the second inserted crossing leads to its old first crossing.

theorem TauCeti.BraidWord.nextCrossing_cons_cons_of_mem {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε η : ℤˣ) {p : Fin n} (hp : p = BraidGroup.strand i ∨ p = BraidGroup.strandSucc i) {j : Fin (List.length v)} (hj : j ∈ v.crossingsAt p) : (nextCrossing ((i, ε) :: (i, η) :: v) p) j.succ.succ = if (v.nextCrossing p) j = (v.crossingsAt p).head ⋯ then 0 else ((v.nextCrossing p) j).succ.succ

An old crossing on an affected position keeps its successor except at the end of the old cycle, where it now leads to the first inserted crossing.

theorem TauCeti.BraidWord.nextCrossing_cons_cons_skip_pair {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε η : ℤˣ) {p : Fin n} (hp : p = BraidGroup.strand i ∨ p = BraidGroup.strandSucc i) {j : Fin (List.length v)} (hj : j ∈ v.crossingsAt p) : let w := (i, ε) :: (i, η) :: v; (if (w.nextCrossing p) j.succ.succ = 0 then (w.nextCrossing p) ((w.nextCrossing p) ((w.nextCrossing p) j.succ.succ)) else (w.nextCrossing p) j.succ.succ) = ((v.nextCrossing p) j).succ.succ

Skipping the two newly inserted crossings recovers the old successor on an affected position. This includes a position with just one old crossing.

theorem TauCeti.BraidWord.edgePair_closure_cons_cons_of_mem {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε η : ℤˣ) {p : Fin n} {j : Fin (List.length v)} (hj : j ∈ v.crossingsAt p) : let w := (i, ε) :: (i, η) :: v; ↑w.closure.edgePair (w.closure.crossing j.succ.succ (v.outgoingSlot j p)) = if (p = BraidGroup.strand i ∨ p = BraidGroup.strandSucc i) ∧ (v.nextCrossing p) j = (v.crossingsAt p).head ⋯ then w.closure.crossing 0 (w.incomingSlot 0 p) else w.closure.crossing ((v.nextCrossing p) j).succ.succ (v.incomingSlot ((v.nextCrossing p) j) p)

Every arc leaving an old crossing is retained except the closing arc on an affected position, which now enters the first inserted crossing. The formula uses the original slots at old crossings, so it can be applied without unfolding the closure construction.

The incoming version of the unaffected-position formula describes the external arc at an old crossing after inserting two crossings with the same generator index. Keeping it in terms of the original word makes it usable when the closure is compared with PDCode.insertClasp, without unfolding the closure matching.

theorem TauCeti.BraidWord.edgePair_closure_cons_cons_incomingSlot_of_ne {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε η : ℤˣ) {p : Fin n} (hp : p ≠ BraidGroup.strand i) (hp' : p ≠ BraidGroup.strandSucc i) {j : Fin (List.length v)} (hj : j ∈ v.crossingsAt p) : let w := (i, ε) :: (i, η) :: v; ↑w.closure.edgePair (w.closure.crossing j.succ.succ (w.incomingSlot j.succ.succ p)) = w.closure.crossing ((Equiv.symm (v.nextCrossing p)) j).succ.succ (w.outgoingSlot ((Equiv.symm (v.nextCrossing p)) j).succ.succ p)

The incoming arc at an old crossing on an unaffected position is unchanged by inserting two crossings with the same generator index on two other positions.

theorem TauCeti.BraidWord.edgePair_closure_cons_cons_one {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε η : ℤˣ) : ↑(closure ((i, ε) :: (i, η) :: v)).edgePair ((PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (0, 1)) = (PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (1, 0)

The upper internal arc of the inserted pair joins slot 1 of the first crossing to slot 0 of the second.

theorem TauCeti.BraidWord.edgePair_closure_cons_cons_two {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε η : ℤˣ) : ↑(closure ((i, ε) :: (i, η) :: v)).edgePair ((PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (0, 2)) = (PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (1, 3)

The lower internal arc of the inserted pair joins slot 2 of the first crossing to slot 3 of the second.

theorem TauCeti.BraidWord.edgePair_closure_cons_cons_eq_of_outgoingSlot {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε η : ℤˣ) {M : PerfectMatching (Fin (4 * ((i, ε) :: (i, η) :: v).length))} (h₀₁ : ↑(closure ((i, ε) :: (i, η) :: v)).edgePair ((PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (0, 1)) = ↑M ((PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (0, 1))) (h₀₂ : ↑(closure ((i, ε) :: (i, η) :: v)).edgePair ((PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (0, 2)) = ↑M ((PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (0, 2))) (h₁₁ : ↑(closure ((i, ε) :: (i, η) :: v)).edgePair ((PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (1, 1)) = ↑M ((PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (1, 1))) (h₁₂ : ↑(closure ((i, ε) :: (i, η) :: v)).edgePair ((PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (1, 2)) = ↑M ((PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (1, 2))) (hold : ∀ {j : Fin (List.length v)} {p : Fin n}, j ∈ v.crossingsAt p → ↑(closure ((i, ε) :: (i, η) :: v)).edgePair ((PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (j.succ.succ, v.outgoingSlot j p)) = ↑M ((PDCode.crossingSlotEquiv ((i, ε) :: (i, η) :: v).length) (j.succ.succ, v.outgoingSlot j p))) : (closure ((i, ε) :: (i, η) :: v)).edgePair = M

The arc matching of the closure of a word beginning with two same-index letters is M as soon as M agrees with it on the four outgoing slots of the two new crossings and on every outgoing slot of an old crossing.

theorem TauCeti.BraidWord.overPair_closure_freeCancel_one {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε : ℤˣ) : (closure ((i, ε) :: (i, -ε) :: v)).overPair 1 = !(closure ((i, ε) :: (i, -ε) :: v)).overPair 0

Opposite letters give opposite over-pair indicators at the two inserted crossings. Together with the internal-arc formulas, this means the same physical strand is over twice.