Far commutation in braid-word closures

Two letters σ i ^ ε and σ j ^ δ with i + 2 ≤ j cross disjoint pairs of strands, so the elementary braids they denote commute (TauCeti.BraidGroup.sigma_mul_sigma_comm). Exchanging two such adjacent letters of a braid word slides one crossing past the other at a different height, and the closure diagram does not change: only its crossing and half-edge names do. This file proves that equality of oriented PD-codes, with the renaming exchanging the two crossings, and concludes that the two closures are Reidemeister equivalent.

No strand position is involved in both crossings, so along every position the crossings are met in the same order before and after the exchange, and TauCeti.BraidWord.closure_eq_relabel_of_isRotated applies. Together with cyclic rotation (TauCeti.BraidWord.closure_rotate), this is part of the diagram-level content of the defining relations of the braid group and of the conjugation move in Markov equivalence.

Main results

• TauCeti.BraidWord.closure_append_cons_cons_comm: exchanging two adjacent letters on disjoint strands changes the closure only by exchanging the names of their crossings.
• TauCeti.BraidWord.reidemeisterEquiv_closure_append_cons_cons_comm: the two closures are Reidemeister equivalent.

References

• J. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82 (1974), Chapters 1 and 2.
• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 1.

theorem TauCeti.BraidWord.closure_append_cons_cons_comm {n : ℕ} (u v : BraidWord n) {a b : Fin (n - 1) × ℤˣ} (h : ↑a.1 + 2 ≤ ↑b.1 ∨ ↑b.1 + 2 ≤ ↑a.1) : (u ++ b :: a :: v).closure = (u ++ a :: b :: v).closure.relabel (PDCode.crossingBlockEquiv (List.swapIndexEquiv u v b a)) (List.swapIndexEquiv u v b a)

Exchanging two adjacent letters a = (i, ε) and b = (j, δ) of a braid word with i + 2 ≤ j or j + 2 ≤ i changes its oriented closure PD-code only by renaming crossings and half-edges: the two crossings of a and b exchange their names, and PDCode.crossingBlockEquiv applies the same renaming to all four crossing slots.

theorem TauCeti.BraidWord.reidemeisterEquiv_closure_append_cons_cons_comm {n : ℕ} (u v : BraidWord n) {a b : Fin (n - 1) × ℤˣ} (h : ↑a.1 + 2 ≤ ↑b.1 ∨ ↑b.1 + 2 ≤ ↑a.1) : (u ++ a :: b :: v).closure.ReidemeisterEquiv (u ++ b :: a :: v).closure

Exchanging two adjacent letters on disjoint strands of a braid word gives a Reidemeister equivalent closure.