The braid relation in braid-word closures #
The braid relation σ i σ (i + 1) σ i = σ (i + 1) σ i σ (i + 1) is the third Reidemeister move:
the three crossings of either side bound a triangle in the closure diagram, and the move slides one
strand across the crossing of the other two. This file proves that replacing the three letters
σ i ^ ε₁ σ (i + 1) ^ ε₂ σ i ^ ε₃ of a braid word by σ (i + 1) ^ ε₃ σ i ^ ε₂ σ (i + 1) ^ ε₁
gives a Reidemeister equivalent closure, provided the signs give the three strands an acyclic height
order (ε₁ = ε₃ forces ε₂ = ε₁). With all three signs equal this is the braid relation itself.
Like cyclic rotation (TauCeti.BraidWord.reidemeisterEquiv_closure_rotate) and the exchange of
letters on disjoint strands (TauCeti.BraidWord.reidemeisterEquiv_closure_append_cons_cons_comm),
this is the diagram-level form of a relation of the braid group: it is one step towards showing
that braid words representing the same braid have Reidemeister equivalent closures, the
combinatorial half of the comparison between Markov equivalence of braids and Reidemeister
equivalence of their closures.
Main results #
TauCeti.BraidWord.reidemeisterEquiv_closure_append_cons_cons_cons_braid: the closures of two braid words related by the braid relation are Reidemeister equivalent.
Implementation notes #
After a cyclic rotation the three letters are at the bottom of the word. In the closure their
crossings 0, 1, 2 form the triangular tangle of TauCeti.PDCode.reidemeisterThree once each
of them is read from its opposite slot: the closure numbers the slots of a crossing from the
south-east and the move from the north-west. The move at the triangle 2, 1, 0 then produces
exactly the closure of the other word, read in the same way. Its arcs are compared at the slots
where strands leave their crossings (TauCeti.BraidWord.edgePair_closure_eq_of_outgoingSlot).
Along the three strand positions of the triangle the crossings of the remaining letters are met in
the same order in both words, and only the arcs entering or leaving the triangle are moved.
References #
- E. Artin, Theorie der Zöpfe, Abh. Math. Sem. Univ. Hamburg 4 (1925), 47-72.
- J. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82 (1974), Chapters 1 and 2.
- W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 1.
Reading a crossing from its opposite slot #
The three bottom crossings, read from their opposite slots #
Successors along a strand position #
Entry and exit slots #
TauCeti.BraidWord.incomingSlot_strand and its siblings, with the strand position given by a
hypothesis, so that simp applies them once it has computed the letter of the crossing.
Closures of words with three letters at the bottom #
The closure of x :: y :: z :: v has v.length + 1 + 1 + 1 crossings, definitionally but not
syntactically (x :: y :: z :: v).length. The following restatements of the closure lemmas use
the former, so that they apply to half-edges named through it.
The braid relation #
The arcs of the closure of W₂ at the slots where strands leave their crossings, compared
with the arcs of the closure of W₁ moved by the rewire: first at the three crossings of the
triangle, from the top down, then at the crossings of v.
The braid relation in braid-word closures. Replacing three adjacent letters
σ i ^ ε₁ σ (i + 1) ^ ε₂ σ i ^ ε₃ of a braid word by σ (i + 1) ^ ε₃ σ i ^ ε₂ σ (i + 1) ^ ε₁
gives a Reidemeister equivalent closure, as long as ε₁ = ε₃ forces ε₂ = ε₁. With all three
signs equal this is the braid relation σ i σ (i + 1) σ i = σ (i + 1) σ i σ (i + 1). The condition
on the signs says that the three strands crossing in the triangle have an acyclic height order, so
that the move is a third Reidemeister move.