Artin relations in braid-word closures

This file packages the two Artin relations already proved for braid closures—far commutation and the equal-sign adjacent braid relation—into a generated word relation. The relation is useful when an argument follows a braid word through several presentation moves: it simultaneously records that the represented braid is unchanged and that the oriented closure changes by Reidemeister moves. Free cancellation is deliberately a separate relation, since its closure-level clasp calculation is a different local argument.

inductive TauCeti.BraidWord.ArtinStep {n : ℕ} : BraidWord n → BraidWord n → Prop

One Artin relation step in a braid word: commute disjoint letters, or apply the equal-sign adjacent braid relation. The surrounding word is part of the step so that the relation is already closed under insertion into a context.

• commute {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).ArtinStep (u ++ b :: a :: v)
• braid {n : ℕ} (u v : BraidWord n) {i j : Fin (n - 1)} (ε : ℤˣ) (hij : ↑j = ↑i + 1) : (u ++ (i, ε) :: (j, ε) :: (i, ε) :: v).ArtinStep (u ++ (j, ε) :: (i, ε) :: (j, ε) :: v)

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

The equivalence relation generated by the Artin relation steps.

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

Artin equivalence is an equivalence relation.

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

Every braid word is Artin equivalent to itself.

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

Artin equivalence is symmetric.

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

Artin equivalence is transitive.

theorem TauCeti.BraidWord.ArtinEquiv.of_step {n : ℕ} {w w' : BraidWord n} (h : w.ArtinStep w') : w.ArtinEquiv w'

A single Artin relation step is an Artin equivalence.

theorem TauCeti.BraidWord.ArtinEquiv.induction {n : ℕ} {motive : BraidWord n → BraidWord n → Prop} (step : ∀ {w w' : BraidWord n}, w.ArtinStep w' → motive w w') (refl : ∀ (w : BraidWord n), motive w w) (symm : ∀ {w w' : BraidWord n}, w.ArtinEquiv w' → motive w w' → motive w' w) (trans : ∀ {w w' w'' : BraidWord n}, w.ArtinEquiv w' → w'.ArtinEquiv w'' → motive w w' → motive w' w'' → motive w w'') {w w' : BraidWord n} (h : w.ArtinEquiv w') : motive w w'

Induction through the generated Artin relation.

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

Adding a common prefix preserves Artin equivalence.

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

Adding a common suffix preserves Artin equivalence.

theorem TauCeti.BraidWord.ArtinEquiv.append {n : ℕ} {w₁ w₁' w₂ w₂' : BraidWord n} (h₁ : w₁.ArtinEquiv w₁') (h₂ : w₂.ArtinEquiv w₂') : (w₁ ++ w₂).ArtinEquiv (w₁' ++ w₂')

Appending Artin-equivalent words preserves Artin equivalence.

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

A single Artin relation step preserves the braid represented by a word.

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

Artin equivalence preserves the braid represented by a word.

theorem TauCeti.BraidWord.reidemeisterEquiv_closure_of_artinStep {n : ℕ} {w w' : BraidWord n} (h : w.ArtinStep w') : w.closure.ReidemeisterEquiv w'.closure

A single Artin relation step gives Reidemeister-equivalent oriented closures.

theorem TauCeti.BraidWord.reidemeisterEquiv_closure_of_artinEquiv {n : ℕ} {w w' : BraidWord n} (h : w.ArtinEquiv w') : w.closure.ReidemeisterEquiv w'.closure

Artin-equivalent braid words have Reidemeister-equivalent oriented closures.