Completeness of braid-word moves

Two braid words represent the same braid if and only if they are connected by Artin relations and insertion or deletion of adjacent inverse letters. This is the algebraic input to comparing closures of arbitrary words representing a fixed braid: a closure invariant need only respect these elementary moves.

References

• J. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82 (1974), Chapter 1 (the Artin presentation).

def TauCeti.BraidWord.WordEquiv {n : ℕ} : BraidWord n → BraidWord n → Prop

The equivalence relation on braid words generated by Artin relations and free cancellation. Each elementary step already includes its surrounding word.

theorem TauCeti.BraidWord.WordEquiv.equivalence {n : ℕ} : Equivalence WordEquiv

Braid-word equivalence is an equivalence relation.

theorem TauCeti.BraidWord.WordEquiv.refl {n : ℕ} (w : BraidWord n) : w.WordEquiv w

Braid-word equivalence is reflexive.

theorem TauCeti.BraidWord.WordEquiv.symm {n : ℕ} {w w' : BraidWord n} (h : w.WordEquiv w') : w'.WordEquiv w

Braid-word equivalence is symmetric.

theorem TauCeti.BraidWord.WordEquiv.trans {n : ℕ} {w w' w'' : BraidWord n} (h : w.WordEquiv w') (h' : w'.WordEquiv w'') : w.WordEquiv w''

Braid-word equivalence is transitive.

theorem TauCeti.BraidWord.WordEquiv.of_artinStep {n : ℕ} {w w' : BraidWord n} (h : w.ArtinStep w') : w.WordEquiv w'

An Artin step is a braid-word equivalence.

theorem TauCeti.BraidWord.WordEquiv.of_freeCancelStep {n : ℕ} {w w' : BraidWord n} (h : w.FreeCancelStep w') : w.WordEquiv w'

A free insertion or deletion is a braid-word equivalence.

theorem TauCeti.BraidWord.WordEquiv.induction {n : ℕ} {w w' : BraidWord n} {motive : BraidWord n → BraidWord n → Prop} (artin : ∀ {u v : BraidWord n}, u.ArtinStep v → motive u v) (cancel : ∀ {u v : BraidWord n}, u.FreeCancelStep v → motive u v) (refl : ∀ (u : BraidWord n), motive u u) (symm : ∀ {u v : BraidWord n}, u.WordEquiv v → motive u v → motive v u) (trans : ∀ {u v z : BraidWord n}, u.WordEquiv v → v.WordEquiv z → motive u v → motive v z → motive u z) (h : w.WordEquiv w') : motive w w'

Induct over a sequence of Artin relations and free insertions or deletions.

theorem TauCeti.BraidWord.WordEquiv.of_artinEquiv {n : ℕ} {w w' : BraidWord n} (h : w.ArtinEquiv w') : w.WordEquiv w'

Artin equivalence embeds into braid-word equivalence.

theorem TauCeti.BraidWord.WordEquiv.of_freeCancelEquiv {n : ℕ} {w w' : BraidWord n} (h : w.FreeCancelEquiv w') : w.WordEquiv w'

Free-cancellation equivalence embeds into braid-word equivalence.

theorem TauCeti.BraidWord.WordEquiv.append_left {n : ℕ} {w w' : BraidWord n} (pre : BraidWord n) (h : w.WordEquiv w') : (pre ++ w).WordEquiv (pre ++ w')

A common prefix preserves braid-word equivalence.

theorem TauCeti.BraidWord.WordEquiv.cons {n : ℕ} {w w' : BraidWord n} (a : Fin (n - 1) × ℤˣ) (h : w.WordEquiv w') : WordEquiv (a :: w) (a :: w')

Prepending a common letter preserves braid-word equivalence.

theorem TauCeti.BraidWord.WordEquiv.append_right {n : ℕ} {w w' : BraidWord n} (h : w.WordEquiv w') (suf : BraidWord n) : (w ++ suf).WordEquiv (w' ++ suf)

A common suffix preserves braid-word equivalence.

theorem TauCeti.BraidWord.WordEquiv.append {n : ℕ} {w w' u u' : BraidWord n} (hu : u.WordEquiv u') (h : w.WordEquiv w') : (u ++ w).WordEquiv (u' ++ w')

Concatenating equivalent braid words preserves equivalence.

theorem TauCeti.BraidWord.WordEquiv.toBraid_eq {n : ℕ} {w w' : BraidWord n} (h : w.WordEquiv w') : w.toBraid = w'.toBraid

Equivalent braid words represent the same braid.

theorem TauCeti.BraidWord.toBraid_eq_iff_wordEquiv {n : ℕ} {w w' : BraidWord n} : w.toBraid = w'.toBraid ↔ w.WordEquiv w'

Completeness of the Artin word moves: two braid words represent the same braid exactly when Artin relations and free insertions or deletions connect them.