Markov moves and Markov equivalence of braids

Closing up a braid on n strands, by joining the i-th endpoint at the top to the i-th endpoint at the bottom, presents an oriented link. After forgetting its framing, two such braids, possibly on different numbers of strands, close to isotopic oriented links exactly when they are related by a chain of the two Markov moves: conjugation b ↦ c * b * c⁻¹ inside a fixed braid group, and stabilization b ↦ strandIncl b * (σ_last)^(±1), which adds a strand and crosses it once, in either sense, with the previous one. That is Markov's theorem; only the moves, not the theorem, are formalized here, since the link presentation the theorem is stated against does not exist yet.

This file introduces framed braid-closure data and its forgetful map, the unframed braids-of-any-width that the ordinary Markov moves act on, the equivalence relation TauCeti.MarkovEquiv they generate, and the first invariant of that relation: the number of components of the closure. The framing-preserving equivalence on framed braid closures is constructed in TauCeti.KnotTheory.Markov.Framed, using Seifert-relative coefficients rather than blackboard writhe. TauCeti.MarkovBraid.liftWord descends word-independent functions to braids; invariance under word rotation and both stabilizations then gives Markov invariance. This shared descent abstracts the signature construction in TauCeti.KnotTheory.Markov.TristramLevine.

Main definitions

• TauCeti.MarkovBraid: a braid together with the number of strands it is a braid on.
• TauCeti.FramedMarkovBraid: a braid closure with an integer framing coefficient on each component; its forgetFraming projection drops those coefficients.
• TauCeti.MarkovBraid.liftWord: descend a word-independent function to braids.
• TauCeti.MarkovBraid.componentCount: the number of components of the closure of the braid, computed as the number of orbits of the underlying permutation of the strands.
• TauCeti.IsMarkovMove: the generating moves, three constructors for the two moves — conjugation, and stabilization in each of its two signs.
• TauCeti.MarkovEquiv: Markov equivalence, the equivalence relation they generate.

Main results

• TauCeti.IsMarkovMove.liftWord_eq and TauCeti.MarkovEquiv.liftWord_eq: word independence, rotation invariance, and stabilization invariance give a Markov invariant.
• TauCeti.MarkovBraid.componentCount_conj, TauCeti.MarkovBraid.componentCount_stabilize and TauCeti.MarkovBraid.componentCount_stabilizeInv: each move separately preserves the number of components of the closure.
• TauCeti.MarkovEquiv.componentCount_eq: Markov-equivalent braids have closures with the same number of components. This is the invariant that keeps the relation from being everything.
• TauCeti.markovEquiv_sigma_last_one_one: the trivial braid on one strand and the single crossing σ₀ on two strands are Markov equivalent.
• TauCeti.not_markovEquiv_one_of_ne: trivial braids on different numbers of strands are not Markov equivalent.
• TauCeti.not_markovEquiv_sigma_last_one_two: the single crossing and the trivial braid on two strands are not Markov equivalent.
• TauCeti.MarkovEquiv.equivalence: Markov equivalence is an equivalence relation.
• TauCeti.MarkovEquiv.induction: the induction principle that makes the Prop-valued definition of Markov equivalence usable outside this file.

Implementation notes

A braid on n strands is TauCeti.BraidGroup n, a different type for each n, while the stabilization move leaves that type; so the moves are stated on the total space TauCeti.MarkovBraid, whose field predStrands records the strand count minus one. Every link that is a braid closure is the closure of a braid on at least one strand, and the stabilization move needs a strand to cross the new one with, so predStrands + 1 rather than predStrands is the strand count.

The component count is read off the underlying permutation TauCeti.BraidGroup.permHom: in the closure, the strand ending at position i is joined to the strand starting at position i, so the components of the closure are exactly the orbits of that permutation on the strands. Its invariance under stabilization is where the work is, and it is supplied by TauCeti/GroupTheory/Perm/OrbitCount/Basic.lean: stabilization adjoins a fixed point to the underlying permutation and immediately splices it into an existing orbit.

References

• A. A. Markov, Über die freie Äquivalenz der geschlossenen Zöpfe, Rec. Math. Moscou 1 (1935), 73-78.
• J. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82 (1974), Theorem 2.3.
• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 1 (printed p. 10) and Proposition 16.10 (Chapter 16).

This advances Layer 4 ("knot theory, done properly") of the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md), which asks for framed and oriented presentations, the forgetful maps between them, the equivalence attached to each presentation -- "Markov moves (braids)" -- and "braid-to-diagram via Markov" as an edge of the spanning tree of presentations. The relation in this file is specifically the ordinary unframed relation after applying TauCeti.FramedMarkovBraid.forgetFraming; framing-preserving Markov equivalence is developed in TauCeti.KnotTheory.Markov.Framed.

structure TauCeti.MarkovBraid : Type

A braid together with the number of strands it is a braid on. The Markov moves relate braids on different numbers of strands, so they are stated on this total space rather than on a single TauCeti.BraidGroup n.

• predStrands : ℕ

  The number of strands, minus one. Every braid closure is the closure of a braid on at least one strand, and stabilization needs a strand to cross the new one with.

• braid : BraidGroup (self.predStrands + 1)

  The braid itself, on predStrands + 1 strands.

@[reducible, inline]

abbrev TauCeti.MarkovBraid.Components (β : MarkovBraid) : Type

The components of a braid closure are the orbits of its strand permutation.

structure TauCeti.FramedMarkovBraid : Type

A framed oriented braid-closure presentation. The braid direction supplies the orientation. A framing of an oriented link in S³, relative to the Seifert framing, is specified by one integer coefficient on each component; the components of a braid closure are the orbits of its underlying permutation. The projection forgetFraming drops this data to the ordinary unframed braid on which TauCeti.MarkovEquiv is defined.

• forgetFraming : MarkovBraid

  Forget the framing coefficients, retaining the underlying braid and its strand count.

• framing : self.forgetFraming.Components → ℤ

  The framing coefficient of each component, relative to its Seifert framing.

noncomputable def TauCeti.MarkovBraid.componentCount (β : MarkovBraid) : ℕ

The number of components of the closure of a braid. In the closure, the strand arriving at position i is joined to the strand leaving position i, so two strands lie on the same component exactly when the underlying permutation TauCeti.BraidGroup.permHom carries one to the other; the components are therefore its orbits, and this is their number. (The closure itself is a link, which the library cannot yet express; this is the count read off the braid.)

@[simp]

theorem TauCeti.MarkovBraid.componentCount_one (n : ℕ) : { predStrands := n, braid := 1 }.componentCount = n + 1

The trivial braid on n + 1 strands has component count n + 1. Informally, its closure is the (n + 1)-component unlink.

@[simp]

theorem TauCeti.MarkovBraid.componentCount_conj {n : ℕ} (b c : BraidGroup (n + 1)) : { predStrands := n, braid := c * b * c⁻¹ }.componentCount = { predStrands := n, braid := b }.componentCount

Conjugate braids have closures with the same number of components.

@[simp]

theorem TauCeti.MarkovBraid.componentCount_stabilize {n : ℕ} (b : BraidGroup (n + 1)) : { predStrands := n + 1, braid := BraidGroup.strandIncl b * BraidGroup.sigma (Fin.last n) }.componentCount = { predStrands := n, braid := b }.componentCount

Positive stabilization does not change the number of components of the closure.

@[simp]

theorem TauCeti.MarkovBraid.componentCount_stabilizeInv {n : ℕ} (b : BraidGroup (n + 1)) : { predStrands := n + 1, braid := BraidGroup.strandIncl b * (BraidGroup.sigma (Fin.last n))⁻¹ }.componentCount = { predStrands := n, braid := b }.componentCount

Negative stabilization does not change the number of components of the closure. The sign of the new crossing is irrelevant here, a transposition being its own inverse.

inductive TauCeti.IsMarkovMove : MarkovBraid → MarkovBraid → Prop

The three generating Markov moves on braids. The first is conjugation inside a fixed braid group; the other two add a strand and cross it once, positively or negatively, with the strand below it. Each is stated as a move from the larger or conjugated braid to the smaller one; the equivalence relation TauCeti.MarkovEquiv they generate is symmetric.

• conj {n : ℕ} (b c : BraidGroup (n + 1)) : IsMarkovMove { predStrands := n, braid := c * b * c⁻¹ } { predStrands := n, braid := b }

  Markov move I: conjugation.

• stabilize {n : ℕ} (b : BraidGroup (n + 1)) : IsMarkovMove { predStrands := n + 1, braid := BraidGroup.strandIncl b * BraidGroup.sigma (Fin.last n) } { predStrands := n, braid := b }

  Markov move II, positive stabilization: the previously-last strand crosses over the new strand.

• stabilizeInv {n : ℕ} (b : BraidGroup (n + 1)) : IsMarkovMove { predStrands := n + 1, braid := BraidGroup.strandIncl b * (BraidGroup.sigma (Fin.last n))⁻¹ } { predStrands := n, braid := b }

  Markov move II, negative stabilization: the previously-last strand crosses under the new strand.

def TauCeti.MarkovEquiv : MarkovBraid → MarkovBraid → Prop

Unframed Markov equivalence: the equivalence relation generated by the ordinary Markov moves. By Markov's theorem (not formalized here), two braids are Markov equivalent exactly when their closures are isotopic oriented links after forgetting framing. This is not the framing-preserving relation on TauCeti.FramedMarkovBraid: stabilization changes the blackboard framing.

theorem TauCeti.MarkovEquiv.equivalence : Equivalence MarkovEquiv

Markov equivalence is an equivalence relation.

theorem TauCeti.MarkovEquiv.refl (β : MarkovBraid) : MarkovEquiv β β

theorem TauCeti.MarkovEquiv.symm {β γ : MarkovBraid} (h : MarkovEquiv β γ) : MarkovEquiv γ β

theorem TauCeti.MarkovEquiv.trans {β γ δ : MarkovBraid} (h : MarkovEquiv β γ) (h' : MarkovEquiv γ δ) : MarkovEquiv β δ

theorem TauCeti.MarkovEquiv.induction {motive : MarkovBraid → MarkovBraid → Prop} (move : ∀ {β γ : MarkovBraid}, IsMarkovMove β γ → motive β γ) (refl : ∀ (β : MarkovBraid), motive β β) (symm : ∀ {β γ : MarkovBraid}, MarkovEquiv β γ → motive β γ → motive γ β) (trans : ∀ {β γ δ : MarkovBraid}, MarkovEquiv β γ → MarkovEquiv γ δ → motive β γ → motive γ δ → motive β δ) {β γ : MarkovBraid} (h : MarkovEquiv β γ) : motive β γ

The induction principle for Markov equivalence. A Prop-valued definition does not unfold outside the file that introduces it, so this is what makes TauCeti.MarkovEquiv usable: a property holding of every single move and closed under reflexivity, symmetry and transitivity holds of every Markov-equivalent pair.

theorem TauCeti.IsMarkovMove.markovEquiv {β γ : MarkovBraid} (h : IsMarkovMove β γ) : MarkovEquiv β γ

A single Markov move is a Markov equivalence.

theorem TauCeti.IsMarkovMove.componentCount_eq {β γ : MarkovBraid} (h : IsMarkovMove β γ) : β.componentCount = γ.componentCount

A single Markov move does not change the number of components of the closure.

theorem TauCeti.MarkovEquiv.componentCount_eq {β γ : MarkovBraid} (h : MarkovEquiv β γ) : β.componentCount = γ.componentCount

The number of components of the closure is a Markov invariant.

Descending word invariants

noncomputable def TauCeti.MarkovBraid.liftWord {α : Sort u_1} (f : {n : ℕ} → BraidWord (n + 1) → α) (β : MarkovBraid) : α

Evaluate a word function on a chosen representative of a braid. For a word-independent function, liftWord_eq_of_toBraid_eq computes this value using any representative.

theorem TauCeti.MarkovBraid.liftWord_def {α : Sort u_1} (f : {n : ℕ} → BraidWord (n + 1) → α) (β : MarkovBraid) : liftWord (fun {n : ℕ} => f) β = f ⋯.choose

The chosen-word formula for the lifted function. Use liftWord_eq_of_toBraid_eq to compute it without reference to this choice when the function is word-independent.

theorem TauCeti.MarkovBraid.liftWord_eq_of_toBraid_eq {α : Sort u_1} (f : {n : ℕ} → BraidWord (n + 1) → α) (hf : ∀ {n : ℕ} {w w' : BraidWord (n + 1)}, w.toBraid = w'.toBraid → f w = f w') {β : MarkovBraid} {w : BraidWord (β.predStrands + 1)} (hw : w.toBraid = β.braid) : liftWord (fun {n : ℕ} => f) β = f w

A word-independent function can be evaluated using any word representing the braid.

theorem TauCeti.MarkovBraid.liftWord_mk {α : Sort u_1} (f : {n : ℕ} → BraidWord (n + 1) → α) (hf : ∀ {n : ℕ} {w w' : BraidWord (n + 1)}, w.toBraid = w'.toBraid → f w = f w') {n : ℕ} (w : BraidWord (n + 1)) : liftWord (fun {n : ℕ} => f) { predStrands := n, braid := w.toBraid } = f w

Lifting a word-independent function and evaluating it on the braid of a word recovers its original value. This is an explicit rewrite rule: simplification cannot infer the word-independence proof for an arbitrary function.

theorem TauCeti.IsMarkovMove.liftWord_eq {α : Sort u_1} (f : {n : ℕ} → BraidWord (n + 1) → α) (hf : ∀ {n : ℕ} {w w' : BraidWord (n + 1)}, w.toBraid = w'.toBraid → f w = f w') (hrot : ∀ {n : ℕ} (w : BraidWord (n + 1)) (k : ℕ), f (List.rotate w k) = f w) (hstab : ∀ {n : ℕ} (w : BraidWord (n + 1)) (ε : ℤˣ), f (w.stabilize ε) = f w) {β γ : MarkovBraid} (h : IsMarkovMove β γ) : MarkovBraid.liftWord (fun {n : ℕ} => f) β = MarkovBraid.liftWord (fun {n : ℕ} => f) γ

Word independence, cyclic rotation invariance, and invariance under either stabilization make the lifted word function invariant under a single Markov move.

theorem TauCeti.MarkovEquiv.liftWord_eq {α : Sort u_1} (f : {n : ℕ} → BraidWord (n + 1) → α) (hf : ∀ {n : ℕ} {w w' : BraidWord (n + 1)}, w.toBraid = w'.toBraid → f w = f w') (hrot : ∀ {n : ℕ} (w : BraidWord (n + 1)) (k : ℕ), f (List.rotate w k) = f w) (hstab : ∀ {n : ℕ} (w : BraidWord (n + 1)) (ε : ℤˣ), f (w.stabilize ε) = f w) {β γ : MarkovBraid} (h : MarkovEquiv β γ) : MarkovBraid.liftWord (fun {n : ℕ} => f) β = MarkovBraid.liftWord (fun {n : ℕ} => f) γ

A word-independent function invariant under rotation and both stabilizations descends to an invariant of Markov equivalence.

theorem TauCeti.markovEquiv_sigma_last_one_one : MarkovEquiv { predStrands := 1, braid := BraidGroup.sigma (Fin.last 0) } { predStrands := 0, braid := 1 }

The trivial braid on one strand and the single crossing on two strands are Markov equivalent, by one stabilization. Informally, these are the two smallest braid presentations of the unknot.

theorem TauCeti.not_markovEquiv_one_of_ne {m n : ℕ} (hmn : m ≠ n) : ¬MarkovEquiv { predStrands := m, braid := 1 } { predStrands := n, braid := 1 }

Markov equivalence is not the total relation. Trivial braids on different numbers of strands have different component counts, so they are never Markov equivalent. Informally, their closures are unlinks with different numbers of components.

theorem TauCeti.not_markovEquiv_sigma_last_one_two : ¬MarkovEquiv { predStrands := 1, braid := BraidGroup.sigma (Fin.last 0) } { predStrands := 1, braid := 1 }

The single crossing on two strands is not Markov equivalent to the trivial braid on two strands, since they have different component counts. Informally, their closures are the unknot and the two-component unlink, respectively.