Closures of braid words with the same crossings along every strand

The closure of a braid word is determined by its letters together with, for each strand position, the cyclic order in which a strand running along that position meets the crossings involving it. Two words with the same letters, listed in different orders, therefore have the same closure up to renaming crossings and half-edges, as soon as along every strand position the crossings of one word are met in the same cyclic order as the corresponding crossings of the other.

This is the common source of the word-level moves that keep the closure diagram: cyclically rotating a word (TauCeti.BraidWord.closure_rotate) and exchanging two adjacent letters on disjoint strands (TauCeti.BraidWord.closure_append_cons_cons_comm).

Main results

• TauCeti.BraidWord.closure_eq_relabel_of_isRotated: if a renaming of crossings matches the letters of two words and carries the crossings of one word along each strand position to a cyclic rotation of those of the other, the two closures differ by that renaming.

theorem TauCeti.BraidWord.closure_eq_relabel_of_isRotated {n : ℕ} {w w' : BraidWord n} (e : Fin (List.length w') ≃ Fin (List.length w)) (he : ∀ (j : Fin (List.length w')), w'[↑j] = w[↑(e j)]) (hrot : ∀ (p : Fin n), List.map (⇑e) (w'.crossingsAt p) ~r w.crossingsAt p) : w'.closure = w.closure.relabel (PDCode.crossingBlockEquiv e.symm) e.symm

Two braid words have the same closure up to renaming, if a renaming e of their crossings matches their letters and carries the crossings of w' along every strand position to a cyclic rotation of the crossings of w along that position. The crossings are renamed by e.symm, and PDCode.crossingBlockEquiv applies the same renaming to all four slots of each crossing.