Braid words

A braid word on n strands is a finite list of letters σ i ^ ε, an elementary braid together with a sign ε = ±1. Unlike an element of TauCeti.BraidGroup n, a word remembers its individual crossings, which is what the closure of a braid into a link diagram consumes. This file defines the words and the braid each word represents.

Main definitions

• TauCeti.BraidWord: the braid words on n strands.
• TauCeti.BraidWord.toBraid: the braid represented by a word, the product of its letters.
• TauCeti.BraidWord.strandIncl: the same word on one strand more, the new strand uncrossed.
• TauCeti.BraidWord.stabilize: the Markov stabilization of a word, which adds a strand and crosses it once with the previous last strand.

Main results

• TauCeti.BraidWord.toBraid_surjective: every braid is represented by a word.
• TauCeti.BraidWord.exponentSum_toBraid: the exponent sum of the represented braid is the sum of the signs of the letters.
• TauCeti.BraidWord.toBraid_strandIncl and TauCeti.BraidWord.toBraid_stabilize: these word operations represent TauCeti.BraidGroup.strandIncl and the stabilization of TauCeti.IsMarkovMove.

References

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

@[reducible, inline]

abbrev TauCeti.BraidWord (n : ℕ) : Type

A braid word on n strands. The letter (i, ε) stands for the elementary braid σ i ^ ε, the crossing of strands i and i + 1 with sign ε = ±1; the letters are read from the bottom of the braid to its top.

Equations

• TauCeti.BraidWord n = List (Fin (n - 1) × ℤˣ)

def TauCeti.BraidWord.toBraid {n : ℕ} (w : BraidWord n) : BraidGroup n

The braid represented by a word: the product of the signed elementary braids it lists.

Equations

• w.toBraid = (List.map (fun (x : Fin (n - 1) × ℤˣ) => TauCeti.BraidGroup.sigma x.1 ^ ↑x.2) w).prod

@[simp]

theorem TauCeti.BraidWord.toBraid_nil {n : ℕ} : toBraid [] = 1

The empty word represents the trivial braid.

@[simp]

theorem TauCeti.BraidWord.toBraid_cons {n : ℕ} (x : Fin (n - 1) × ℤˣ) (w : BraidWord n) : toBraid (x :: w) = BraidGroup.sigma x.1 ^ ↑x.2 * w.toBraid

Prepending a letter multiplies the represented braid on the left by that letter.

@[simp]

theorem TauCeti.BraidWord.toBraid_append {n : ℕ} (w w' : BraidWord n) : (w ++ w').toBraid = w.toBraid * w'.toBraid

Concatenating words multiplies the represented braids.

theorem TauCeti.BraidWord.toBraid_reverse_map_neg {n : ℕ} (w : BraidWord n) : toBraid (List.map (fun (x : Fin (n - 1) × ℤˣ) => (x.1, -x.2)) (List.reverse w)) = w.toBraid⁻¹

Reversing a word and negating all its signs represents the inverse braid.

theorem TauCeti.BraidWord.toBraid_surjective {n : ℕ} : Function.Surjective toBraid

Every braid is represented by a braid word.

@[simp]

theorem TauCeti.BraidWord.exponentSum_toBraid {n : ℕ} (w : BraidWord n) : (ArtinGroup.exponentSum (CoxeterMatrix.A (n - 1))) w.toBraid = Multiplicative.ofAdd (List.map (fun (x : Fin (n - 1) × ℤˣ) => ↑x.2) w).sum

The exponent sum of the braid represented by a word is the sum of the signs of its letters.

Adding a strand

def TauCeti.BraidWord.strandIncl {n : ℕ} (w : BraidWord (n + 1)) : BraidWord (n + 2)

The same braid word on one strand more: every letter keeps its index, so the new top strand is never crossed. It represents TauCeti.BraidGroup.strandIncl of the braid of the word.

Equations

• w.strandIncl = List.map (fun (x : Fin (n + 1 - 1) × ℤˣ) => (x.1.castSucc, x.2)) w

theorem TauCeti.BraidWord.strandIncl_def {n : ℕ} (w : BraidWord (n + 1)) : w.strandIncl = List.map (fun (x : Fin (n + 1 - 1) × ℤˣ) => (x.1.castSucc, x.2)) w

The defining equation of TauCeti.BraidWord.strandIncl: each letter keeps its index.

@[simp]

theorem TauCeti.BraidWord.length_strandIncl {n : ℕ} (w : BraidWord (n + 1)) : List.length w.strandIncl = List.length w

Adding a strand keeps the number of letters.

@[simp]

theorem TauCeti.BraidWord.toBraid_strandIncl {n : ℕ} (w : BraidWord (n + 1)) : w.strandIncl.toBraid = BraidGroup.strandIncl w.toBraid

Adding a strand to a word adds an uncrossed strand to the braid it represents.

def TauCeti.BraidWord.stabilize {n : ℕ} (w : BraidWord (n + 1)) (ε : ℤˣ) : BraidWord (n + 2)

The Markov stabilization of a braid word with sign ε: add a strand and cross it once with the previous last strand, by the letter σ (Fin.last n) ^ ε placed at the top.

Equations

• w.stabilize ε = w.strandIncl ++ [(Fin.last n, ε)]

theorem TauCeti.BraidWord.stabilize_def {n : ℕ} (w : BraidWord (n + 1)) (ε : ℤˣ) : w.stabilize ε = w.strandIncl ++ [(Fin.last n, ε)]

The defining equation of TauCeti.BraidWord.stabilize: the new letter is placed at the top.

@[simp]

theorem TauCeti.BraidWord.length_stabilize {n : ℕ} (w : BraidWord (n + 1)) (ε : ℤˣ) : List.length (w.stabilize ε) = List.length w + 1

Stabilization adds one letter.

@[simp]

theorem TauCeti.BraidWord.toBraid_stabilize {n : ℕ} (w : BraidWord (n + 1)) (ε : ℤˣ) : (w.stabilize ε).toBraid = BraidGroup.strandIncl w.toBraid * BraidGroup.sigma (Fin.last n) ^ ↑ε

A stabilized word represents the braid strandIncl b * σ (Fin.last n) ^ ε, the stabilization of the braid b of the word, as in TauCeti.IsMarkovMove.stabilize and TauCeti.IsMarkovMove.stabilizeInv.