Free cancellation in braid words

The word presentation of a braid has the elementary free relation σ i ^ ε σ i ^ (-ε) = 1. This file records the relation on words, its closure under insertion and deletion, and the invariants that the relation preserves. The relation is the word-level prerequisite for the second Reidemeister move on braid closures.

The list and group calculations here are the input for the diagrammatic statement that inserting an inverse pair changes a closure by a Reidemeister-II clasp: that statement must identify the two new crossings with the corresponding clasp in the PD-code.

Main declarations

• TauCeti.BraidWord.FreeCancelStep: insertion or deletion of one adjacent inverse pair.
• TauCeti.BraidWord.FreeCancelEquiv: the equivalence relation generated by those steps.
• TauCeti.BraidWord.toBraid_freeCancel and writhe_closure_freeCancel: invariance of the represented braid and closure writhe under one step.

The closure-level crossing signs and over-pair data for an appended inverse pair are in TauCeti.KnotTheory.BraidWord.FreeCancellation.Reidemeister.

The general crossing-order formula is TauCeti.BraidWord.crossingsAt_cons_cons_same_index in BraidWord.PDCode; successor and internal-arc formulas are in BraidWord.DoubleCrossing.

References

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

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

One free-cancellation step inserts or deletes adjacent inverse letters in a braid word.

• insert {n : ℕ} (u v : BraidWord n) (i : Fin (n - 1)) (ε : ℤˣ) : (u ++ v).FreeCancelStep (u ++ [(i, ε), (i, -ε)] ++ v)
• delete {n : ℕ} (u v : BraidWord n) (i : Fin (n - 1)) (ε : ℤˣ) : (u ++ [(i, ε), (i, -ε)] ++ v).FreeCancelStep (u ++ v)

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

A common prefix preserves a free-cancellation step.

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

A common suffix preserves a free-cancellation step.

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

The equivalence relation generated by free insertion and deletion of inverse pairs.

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

Free-cancellation equivalence is an equivalence relation.

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

Free-cancellation equivalence is reflexive.

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

Free-cancellation equivalence is symmetric.

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

Free-cancellation equivalence is transitive.

theorem TauCeti.BraidWord.FreeCancelEquiv.of_step {n : ℕ} {w w' : BraidWord n} (h : w.FreeCancelStep w') : w.FreeCancelEquiv w'

A single free-cancellation step is a free-cancellation equivalence.

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

The induction principle exposes the generated relation to closure-level consumers.

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

A common prefix preserves free-cancellation equivalence.

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

A common suffix preserves free-cancellation equivalence.

theorem TauCeti.BraidWord.FreeCancelEquiv.append {n : ℕ} {u u' v v' : BraidWord n} (hu : u.FreeCancelEquiv u') (hv : v.FreeCancelEquiv v') : (u ++ v).FreeCancelEquiv (u' ++ v')

Concatenating freely equivalent words preserves free-cancellation equivalence.

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

A free-cancellation step does not change the braid represented by a word.

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

Free-cancellation equivalence preserves the represented braid.

theorem TauCeti.BraidWord.length_freeCancel_insert {n : ℕ} (u v : BraidWord n) (i : Fin (n - 1)) (ε : ℤˣ) : List.length (u ++ [(i, ε), (i, -ε)] ++ v) = List.length (u ++ v) + 2

Inserting a free-cancelled pair adds two crossings.

theorem TauCeti.BraidWord.writhe_closure_freeCancel {n : ℕ} {w w' : BraidWord n} (h : w.FreeCancelStep w') : w.closure.writhe = w'.closure.writhe

The closure writhe is unchanged by one free-cancellation step.

theorem TauCeti.BraidWord.writhe_closure_freeCancelEquiv {n : ℕ} {w w' : BraidWord n} (h : w.FreeCancelEquiv w') : w.closure.writhe = w'.closure.writhe

The closure writhe is invariant under the equivalence generated by free cancellations.