Framing-preserving Markov equivalence

Framed braid closures carry an integer coefficient on each component relative to the Seifert framing. Conjugation and either stabilization transport these coefficients along their canonical component bijections. The equivalence generated by these operations therefore preserves the coefficient of every corresponding component, even when the number of strands changes.

Every ordinary Markov equivalence lifts starting from any framing of its initial braid. This provides the forgetful map between the framed and unframed equivalence relations. Conversely, forgetting framing can identify inequivalent framed presentations: different constant coefficients on the same underlying braid are distinguished by the component transport theorem.

These are combinatorial equivalence relations on braid presentations. No equivalence with geometric framed isotopy is asserted here. The coefficients are Seifert-relative; ordinary stabilization changes the blackboard writhe but preserves these coefficients.

References

• J. Birman, Braids, Links, and Mapping Class Groups, Theorem 2.3 (ordinary Markov moves).
• R. Gompf and A. Stipsicz, 4-Manifolds and Kirby Calculus, Section 4.5 (integer framings relative to the Seifert framing).

The component transport maps are those of TauCeti.KnotTheory.Markov.Components.

inductive TauCeti.IsFramedMarkovMove : FramedMarkovBraid → FramedMarkovBraid → Prop

Markov moves carrying the Seifert-relative framing of each component along its canonical bijection. As for IsMarkovMove, each generator points towards the unstabilized or unconjugated presentation; the generated equivalence allows both directions.

• conj (β : FramedMarkovBraid) (c : BraidGroup (β.forgetFraming.predStrands + 1)) : IsFramedMarkovMove (β.conj c) β

  Conjugation with its induced transport of component coefficients.

• stabilize (β : FramedMarkovBraid) : IsFramedMarkovMove β.stabilize β

  Positive stabilization, retaining each component's Seifert-relative coefficient.

• stabilizeInv (β : FramedMarkovBraid) : IsFramedMarkovMove β.stabilizeInv β

  Negative stabilization, retaining each component's Seifert-relative coefficient.

def TauCeti.FramedMarkovEquiv : FramedMarkovBraid → FramedMarkovBraid → Prop

Framing-preserving Markov equivalence, generated by conjugation and both stabilizations with their canonical transport of component coefficients.

theorem TauCeti.IsFramedMarkovMove.forgetFraming {β γ : FramedMarkovBraid} (h : IsFramedMarkovMove β γ) : IsMarkovMove β.forgetFraming γ.forgetFraming

A framing-preserving move is an ordinary Markov move after forgetting its coefficients.

theorem TauCeti.IsFramedMarkovMove.exists_componentsEquiv {β γ : FramedMarkovBraid} (h : IsFramedMarkovMove β γ) : ∃ (e : β.forgetFraming.Components ≃ γ.forgetFraming.Components), ∀ (q : β.forgetFraming.Components), γ.framing (e q) = β.framing q

Each framed move supplies a bijection of components preserving their individual coefficients.

theorem TauCeti.IsFramedMarkovMove.framedMarkovEquiv {β γ : FramedMarkovBraid} (h : IsFramedMarkovMove β γ) : FramedMarkovEquiv β γ

A single framing-preserving move gives a framed Markov equivalence.

theorem TauCeti.FramedMarkovEquiv.equivalence : Equivalence FramedMarkovEquiv

Framed Markov equivalence is an equivalence relation.

theorem TauCeti.FramedMarkovEquiv.refl (β : FramedMarkovBraid) : FramedMarkovEquiv β β

Every framed braid presentation is equivalent to itself.

theorem TauCeti.FramedMarkovEquiv.symm {β γ : FramedMarkovBraid} (h : FramedMarkovEquiv β γ) : FramedMarkovEquiv γ β

Framed Markov equivalence is symmetric.

theorem TauCeti.FramedMarkovEquiv.trans {β γ δ : FramedMarkovBraid} (h : FramedMarkovEquiv β γ) (h' : FramedMarkovEquiv γ δ) : FramedMarkovEquiv β δ

Framed Markov equivalences compose.

theorem TauCeti.FramedMarkovEquiv.induction {β γ : FramedMarkovBraid} {motive : FramedMarkovBraid → FramedMarkovBraid → Prop} (move : ∀ {β γ : FramedMarkovBraid}, IsFramedMarkovMove β γ → motive β γ) (refl : ∀ (β : FramedMarkovBraid), motive β β) (symm : ∀ {β γ : FramedMarkovBraid}, FramedMarkovEquiv β γ → motive β γ → motive γ β) (trans : ∀ {β γ δ : FramedMarkovBraid}, FramedMarkovEquiv β γ → FramedMarkovEquiv γ δ → motive β γ → motive γ δ → motive β δ) (h : FramedMarkovEquiv β γ) : motive β γ

Induction over framing-preserving Markov moves, their inverses, and finite composites.

theorem TauCeti.FramedMarkovEquiv.forgetFraming {β γ : FramedMarkovBraid} (h : FramedMarkovEquiv β γ) : MarkovEquiv β.forgetFraming γ.forgetFraming

Forgetting coefficients sends framed Markov equivalence to ordinary Markov equivalence.

theorem TauCeti.FramedMarkovEquiv.exists_componentsEquiv {β γ : FramedMarkovBraid} (h : FramedMarkovEquiv β γ) : ∃ (e : β.forgetFraming.Components ≃ γ.forgetFraming.Components), ∀ (q : β.forgetFraming.Components), γ.framing (e q) = β.framing q

Framed Markov equivalence preserves every component coefficient under a bijection of components. The bijection may depend on the sequence of moves; no canonical one is asserted.

theorem TauCeti.MarkovEquiv.exists_framedMarkovEquiv {β γ : MarkovBraid} (h : MarkovEquiv β γ) (a : β.Components → ℤ) : ∃ (b : γ.Components → ℤ), FramedMarkovEquiv { forgetFraming := β, framing := a } { forgetFraming := γ, framing := b }

Every ordinary Markov equivalence lifts from any given framing of its initial braid. The terminal framing is transported along the moves, rather than chosen independently.

theorem TauCeti.markovEquiv_iff_exists_framedMarkovEquiv (β : FramedMarkovBraid) (γ : MarkovBraid) : MarkovEquiv β.forgetFraming γ ↔ ∃ (b : γ.Components → ℤ), FramedMarkovEquiv β { forgetFraming := γ, framing := b }

An ordinary target braid is Markov equivalent to the underlying braid of a framed presentation exactly when some framing of that target is framed Markov equivalent to it.

theorem TauCeti.not_framedMarkovEquiv_const (β : MarkovBraid) {a b : ℤ} (hab : a ≠ b) : ¬FramedMarkovEquiv { forgetFraming := β, framing := fun (x : β.Components) => a } { forgetFraming := β, framing := fun (x : β.Components) => b }

Changing a constant framing coefficient changes the framed Markov class, even on the same underlying braid. In particular, forgetting framing identifies distinct framed classes.