The closure of a braid word as a PD-code

Closing a braid, by joining the top end of each strand position to its bottom end, presents an oriented link. This file writes that link down as an oriented PD-code, with one crossing for every letter of a braid word. It is the combinatorial edge from the braid presentation of a link to the diagram presentation.

The braid is drawn with its strands running upwards, the letters of the word from the bottom to the top, and the closing strands passing to the side. The four slots of the crossing of a letter (i, ε) are, counterclockwise: slot 0 entering from below on position i + 1, slot 1 leaving above on position i + 1, slot 2 leaving above on position i, and slot 3 entering from below on position i. So the strand entering on position i occupies slots 3 and 1; it is the over-strand when ε = 1, which makes the crossing positive, and the under-strand when ε = -1. Leaving a crossing upwards on position p, a strand next meets the first crossing above it that involves position p, or else runs through the closure back to the lowest such crossing; that successor is TauCeti.BraidWord.nextCrossing. A position involved in no crossing closes up to a crossing-free circle.

Main definitions

• TauCeti.BraidWord.crossingsAt: the crossings involving a strand position, from the bottom.
• TauCeti.BraidWord.nextCrossing: the next crossing met along a strand position.
• TauCeti.BraidWord.closure: the oriented PD-code of the closure of a braid word.

Main results

• TauCeti.BraidWord.crossingsAt_cons: a letter added at the bottom of a word comes first along its two strand positions.
• TauCeti.BraidWord.edgePair_closure_outgoingSlot: the arcs of the closure join each crossing to the next crossing along the same strand position.
• TauCeti.BraidWord.edgePair_closure_incomingSlot: the same arcs, read from the crossing they enter.
• TauCeti.BraidWord.edgePair_closure_crossingSlotEquiv_zero and its siblings for the slots 1, 2 and 3: the arc at each slot of a crossing of the closure.
• TauCeti.BraidWord.edgePair_closure_eq_of_outgoingSlot: a perfect matching of the half-edges agreeing with the arcs of the closure at the slots where strands leave their crossings is the arc matching of the closure.
• TauCeti.BraidWord.crossingSign_closure: the sign of each crossing is the sign of its letter.
• TauCeti.BraidWord.writhe_closure: the writhe of the closure is the exponent sum of the braid.
• TauCeti.BraidWord.closure_nil: the closure of the empty word on n strands is the n-component unlink.

References

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

Following a strand position through the crossings

def TauCeti.BraidWord.crossingsAt {n : ℕ} (w : BraidWord n) (p : Fin n) : List (Fin (List.length w))

The crossings of a braid word involving the strand position p, listed from the bottom: the letters (i, ε) with p = i or p = i + 1.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.BraidWord.crossingsAt_def {n : ℕ} (w : BraidWord n) (p : Fin n) : w.crossingsAt p = List.filter (fun (j : Fin (List.length w)) => decide (p = BraidGroup.strand w[↑j].1 ∨ p = BraidGroup.strandSucc w[↑j].1)) (List.finRange (List.length w))

The crossings involving a strand position are the indices of the letters with that position as one of their two strands, in increasing order.

@[simp]

theorem TauCeti.BraidWord.mem_crossingsAt {n : ℕ} (w : BraidWord n) {p : Fin n} {j : Fin (List.length w)} : j ∈ w.crossingsAt p ↔ p = BraidGroup.strand w[↑j].1 ∨ p = BraidGroup.strandSucc w[↑j].1

A crossing involves a strand position exactly when that position is one of its two strands.

theorem TauCeti.BraidWord.mem_crossingsAt_strand {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) : j ∈ w.crossingsAt (BraidGroup.strand w[↑j].1)

A crossing involves the lower position of its letter.

theorem TauCeti.BraidWord.mem_crossingsAt_strandSucc {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) : j ∈ w.crossingsAt (BraidGroup.strandSucc w[↑j].1)

A crossing involves the upper position of its letter.

theorem TauCeti.BraidWord.crossingsAt_eq_nil_iff {n : ℕ} (w : BraidWord n) {p : Fin n} : w.crossingsAt p = [] ↔ ∀ (j : Fin (List.length w)), p ≠ BraidGroup.strand w[↑j].1 ∧ p ≠ BraidGroup.strandSucc w[↑j].1

A strand position is involved in no crossing exactly when it is neither position of any letter.

theorem TauCeti.BraidWord.sortedLT_crossingsAt {n : ℕ} (w : BraidWord n) (p : Fin n) : (w.crossingsAt p).SortedLT

The crossings involving a strand position are listed from the bottom.

theorem TauCeti.BraidWord.crossingsAt_cons {n : ℕ} (x : Fin (n - 1) × ℤˣ) (v : BraidWord n) (p : Fin n) : crossingsAt (x :: v) p = (if p = BraidGroup.strand x.1 ∨ p = BraidGroup.strandSucc x.1 then [0] else []) ++ List.map Fin.succ (v.crossingsAt p)

Adding a letter at the bottom of a braid word: along a strand position, its crossing comes first when the letter involves that position, followed by the crossings of the old word.

theorem TauCeti.BraidWord.crossingsAt_cons_cons_same_index {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε η : ℤˣ) (p : Fin n) : crossingsAt ((i, ε) :: (i, η) :: v) p = (if p = BraidGroup.strand i ∨ p = BraidGroup.strandSucc i then [0, 1] else []) ++ List.map (fun (j : Fin (List.length v)) => j.succ.succ) (v.crossingsAt p)

Two letters on the same positions come first on either position, followed by the old crossings shifted by two. Positions outside the pair see only the shifted old crossings.

def TauCeti.BraidWord.nextCrossing {n : ℕ} (w : BraidWord n) (p : Fin n) : Equiv.Perm (Fin (List.length w))

The crossing met next along the strand position p after the crossing j: the next crossing above j involving p, or, through the closure, the lowest one. Crossings not involving p are fixed.

Equations

• w.nextCrossing p = (w.crossingsAt p).formPerm

theorem TauCeti.BraidWord.nextCrossing_def {n : ℕ} (w : BraidWord n) (p : Fin n) : w.nextCrossing p = (w.crossingsAt p).formPerm

The successor along a strand position is the cyclic permutation of the crossings involving it, listed from the bottom.

theorem TauCeti.BraidWord.nextCrossing_apply_getElem {n : ℕ} (w : BraidWord n) (p : Fin n) (k : ℕ) (hk : k < (w.crossingsAt p).length) : (w.nextCrossing p) (w.crossingsAt p)[k] = (w.crossingsAt p)[(k + 1) % (w.crossingsAt p).length]

Along a strand position, each crossing involving it is followed by the next one in the bottom-to-top list TauCeti.BraidWord.crossingsAt, and the topmost by the lowest.

theorem TauCeti.BraidWord.nextCrossing_mem_crossingsAt_iff {n : ℕ} (w : BraidWord n) {p : Fin n} {j : Fin (List.length w)} : (w.nextCrossing p) j ∈ w.crossingsAt p ↔ j ∈ w.crossingsAt p

The next crossing along a position involves that position exactly when the current one does.

theorem TauCeti.BraidWord.nextCrossing_symm_mem_crossingsAt_iff {n : ℕ} (w : BraidWord n) {p : Fin n} {j : Fin (List.length w)} : (Equiv.symm (w.nextCrossing p)) j ∈ w.crossingsAt p ↔ j ∈ w.crossingsAt p

The previous crossing along a position involves that position exactly when the current one does.

def TauCeti.BraidWord.incomingSlot {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) (p : Fin n) : Fin 4

The slot of the crossing j at which a strand enters it from below on the position p: slot 3 on the lower position i of the letter, slot 0 on the upper position i + 1.

Equations

• w.incomingSlot j p = if p = TauCeti.BraidGroup.strand w[↑j].1 then 3 else 0

def TauCeti.BraidWord.outgoingSlot {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) (p : Fin n) : Fin 4

The slot of the crossing j at which a strand leaves it upwards on the position p: slot 2 on the lower position i of the letter, slot 1 on the upper position i + 1.

Equations

• w.outgoingSlot j p = if p = TauCeti.BraidGroup.strand w[↑j].1 then 2 else 1

@[simp]

theorem TauCeti.BraidWord.incomingSlot_strand {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) : w.incomingSlot j (BraidGroup.strand w[↑j].1) = 3

A strand enters a crossing on the lower position of its letter at slot 3.

@[simp]

theorem TauCeti.BraidWord.incomingSlot_strandSucc {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) : w.incomingSlot j (BraidGroup.strandSucc w[↑j].1) = 0

A strand enters a crossing on the upper position of its letter at slot 0.

@[simp]

theorem TauCeti.BraidWord.outgoingSlot_strand {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) : w.outgoingSlot j (BraidGroup.strand w[↑j].1) = 2

A strand leaves a crossing on the lower position of its letter at slot 2.

@[simp]

theorem TauCeti.BraidWord.outgoingSlot_strandSucc {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) : w.outgoingSlot j (BraidGroup.strandSucc w[↑j].1) = 1

A strand leaves a crossing on the upper position of its letter at slot 1.

theorem TauCeti.BraidWord.incomingSlot_eq_zero_or_three {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) (p : Fin n) : w.incomingSlot j p = 0 ∨ w.incomingSlot j p = 3

A strand enters a crossing at slot 0 or slot 3.

theorem TauCeti.BraidWord.outgoingSlot_eq_one_or_two {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) (p : Fin n) : w.outgoingSlot j p = 1 ∨ w.outgoingSlot j p = 2

A strand leaves a crossing at slot 1 or slot 2.

theorem TauCeti.BraidWord.eq_of_outgoingSlot_eq {n : ℕ} (w : BraidWord n) {j : Fin (List.length w)} {p q : Fin n} (hp : j ∈ w.crossingsAt p) (hq : j ∈ w.crossingsAt q) (h : w.outgoingSlot j p = w.outgoingSlot j q) : p = q

A crossing is left upwards along the two positions of its letter at different slots.

theorem TauCeti.BraidWord.incomingSlot_congr {n : ℕ} {w w' : BraidWord n} {j : Fin (List.length w')} {i : Fin (List.length w)} (h : w'[↑j] = w[↑i]) (p : Fin n) : w'.incomingSlot j p = w.incomingSlot i p

The incoming slot at a crossing depends only on the letter of that crossing.

theorem TauCeti.BraidWord.outgoingSlot_congr {n : ℕ} {w w' : BraidWord n} {j : Fin (List.length w')} {i : Fin (List.length w)} (h : w'[↑j] = w[↑i]) (p : Fin n) : w'.outgoingSlot j p = w.outgoingSlot i p

The outgoing slot at a crossing depends only on the letter of that crossing.

The arcs of the closure

The closure

def TauCeti.BraidWord.closure {n : ℕ} (w : BraidWord n) : OrientedPDCode (List.length w)

The closure of a braid word, as an oriented PD-code with one crossing for each letter.

The half-edges are labelled by their crossing slots. The strands run upwards, so a half-edge points away from its crossing exactly at the slots 1 and 2. The strand entering the crossing of a letter (i, ε) on position i occupies slots 3 and 1 and is over exactly when ε = 1. Every strand position involved in no crossing closes up to a crossing-free circle, all of them with the orientation true.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.BraidWord.halfEdge_closure {n : ℕ} (w : BraidWord n) : w.closure.halfEdge = 1

The half-edges of the closure are labelled by their crossing slots.

theorem TauCeti.BraidWord.crossing_closure {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) (slot : Fin 4) : w.closure.crossing j slot = (PDCode.crossingSlotEquiv (List.length w)) (j, slot)

The half-edge in a crossing slot of the closure is the label of that slot.

theorem TauCeti.BraidWord.edgePair_closure_outgoingSlot {n : ℕ} (w : BraidWord n) {j : Fin (List.length w)} {p : Fin n} (hj : j ∈ w.crossingsAt p) : ↑w.closure.edgePair (w.closure.crossing j (w.outgoingSlot j p)) = w.closure.crossing ((w.nextCrossing p) j) (w.incomingSlot ((w.nextCrossing p) j) p)

The arc leaving a crossing upwards on the position p enters the next crossing along p from below. Since every slot is the incoming or the outgoing slot of its crossing on one of the two positions of its letter, this determines every arc of the closure.

theorem TauCeti.BraidWord.edgePair_closure_incomingSlot {n : ℕ} (w : BraidWord n) {j : Fin (List.length w)} {p : Fin n} (hj : j ∈ w.crossingsAt p) : ↑w.closure.edgePair (w.closure.crossing j (w.incomingSlot j p)) = w.closure.crossing ((Equiv.symm (w.nextCrossing p)) j) (w.outgoingSlot ((Equiv.symm (w.nextCrossing p)) j) p)

The arc entering a crossing from below on the position p leaves the previous crossing along p upwards.

@[simp]

theorem TauCeti.BraidWord.edgePair_closure_crossingSlotEquiv_zero {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) : ↑w.closure.edgePair ((PDCode.crossingSlotEquiv (List.length w)) (j, 0)) = (PDCode.crossingSlotEquiv (List.length w)) ((Equiv.symm (w.nextCrossing (BraidGroup.strandSucc w[↑j].1))) j, w.outgoingSlot ((Equiv.symm (w.nextCrossing (BraidGroup.strandSucc w[↑j].1))) j) (BraidGroup.strandSucc w[↑j].1))

The arc at slot 0 of a crossing, entering it from below on the upper position of its letter, leaves the previous crossing along that position upwards.

@[simp]

theorem TauCeti.BraidWord.edgePair_closure_crossingSlotEquiv_one {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) : ↑w.closure.edgePair ((PDCode.crossingSlotEquiv (List.length w)) (j, 1)) = (PDCode.crossingSlotEquiv (List.length w)) ((w.nextCrossing (BraidGroup.strandSucc w[↑j].1)) j, w.incomingSlot ((w.nextCrossing (BraidGroup.strandSucc w[↑j].1)) j) (BraidGroup.strandSucc w[↑j].1))

The arc at slot 1 of a crossing, leaving it upwards on the upper position of its letter, enters the next crossing along that position from below.

@[simp]

theorem TauCeti.BraidWord.edgePair_closure_crossingSlotEquiv_two {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) : ↑w.closure.edgePair ((PDCode.crossingSlotEquiv (List.length w)) (j, 2)) = (PDCode.crossingSlotEquiv (List.length w)) ((w.nextCrossing (BraidGroup.strand w[↑j].1)) j, w.incomingSlot ((w.nextCrossing (BraidGroup.strand w[↑j].1)) j) (BraidGroup.strand w[↑j].1))

The arc at slot 2 of a crossing, leaving it upwards on the lower position of its letter, enters the next crossing along that position from below.

@[simp]

theorem TauCeti.BraidWord.edgePair_closure_crossingSlotEquiv_three {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) : ↑w.closure.edgePair ((PDCode.crossingSlotEquiv (List.length w)) (j, 3)) = (PDCode.crossingSlotEquiv (List.length w)) ((Equiv.symm (w.nextCrossing (BraidGroup.strand w[↑j].1))) j, w.outgoingSlot ((Equiv.symm (w.nextCrossing (BraidGroup.strand w[↑j].1))) j) (BraidGroup.strand w[↑j].1))

The arc at slot 3 of a crossing, entering it from below on the lower position of its letter, leaves the previous crossing along that position upwards.

@[simp]

theorem TauCeti.BraidWord.overPair_closure {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) : w.closure.overPair j = decide (w[↑j].2 = 1)

The strand entering the crossing of a letter on the lower position of the letter is over exactly for a positive letter.

@[simp]

theorem TauCeti.BraidWord.orientation_closure {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) (slot : Fin 4) : w.closure.orientation ((PDCode.crossingSlotEquiv (List.length w)) (j, slot)) = decide (slot = 1 ∨ slot = 2)

A half-edge of the closure points away from its crossing exactly at the slots 1 and 2, where the strands leave the crossing upwards.

theorem TauCeti.BraidWord.edgePair_closure_eq_of_outgoingSlot {n : ℕ} (w : BraidWord n) {M : PerfectMatching (Fin (4 * List.length w))} (h : ∀ (j : Fin (List.length w)) (p : Fin n), j ∈ w.crossingsAt p → ↑w.closure.edgePair ((PDCode.crossingSlotEquiv (List.length w)) (j, w.outgoingSlot j p)) = ↑M ((PDCode.crossingSlotEquiv (List.length w)) (j, w.outgoingSlot j p))) : w.closure.edgePair = M

The arcs of the closure are determined by the arcs leaving the crossings upwards: a perfect matching of the half-edges agreeing with them is the arc matching of the closure.

@[simp]

theorem TauCeti.BraidWord.crossinglessComponentCount_closure {n : ℕ} (w : BraidWord n) : w.closure.crossinglessComponentCount = {p : Fin n | w.crossingsAt p = []}.card

The crossing-free circles of the closure are the strand positions involved in no crossing.

@[simp]

theorem TauCeti.BraidWord.crossinglessComponents_closure {n : ℕ} (w : BraidWord n) : w.closure.crossinglessComponents = Multiset.replicate {p : Fin n | w.crossingsAt p = []}.card true

The crossing-free circles of the closure all carry the orientation true.

@[simp]

theorem TauCeti.BraidWord.crossingSign_closure {n : ℕ} (w : BraidWord n) (j : Fin (List.length w)) : w.closure.crossingSign j = ↑w[↑j].2

The sign of each crossing of the closure is the sign of its letter.

@[simp]

theorem TauCeti.BraidWord.writhe_closure {n : ℕ} (w : BraidWord n) : w.closure.writhe = Multiplicative.toAdd ((ArtinGroup.exponentSum (CoxeterMatrix.A (n - 1))) w.toBraid)

The writhe of the closure of a braid word is the exponent sum of the braid it represents.

Small closures

@[simp]

theorem TauCeti.BraidWord.closure_nil {n : ℕ} : closure [] = OrientedPDCode.unlink (Multiset.replicate n true)

The closure of the empty word on n strands is the n-component unlink.