Transporting braid-closure components through Markov moves

Conjugation relabels components by the conjugating braid's permutation. Stabilization includes each old strand and inserts the new strand into the component of the old last strand. These explicit bijections transport per-component data; an equality of component counts alone does not specify that transport.

For framed closures the coefficients are relative to the Seifert framing. Transporting these coefficients preserves them on each corresponding component, for either sign of stabilization. They are independent of the blackboard framing, which stabilization changes.

Reference: J. Birman, Braids, Links, and Mapping Class Groups, Theorem 2.3, for Markov moves; R. Gompf and A. Stipsicz, 4-Manifolds and Kirby Calculus, Section 4.5, for integer framing coefficients relative to the Seifert framing.

def TauCeti.MarkovBraid.conjComponentsEquiv {n : ℕ} (b c : BraidGroup (n + 1)) : { predStrands := n, braid := b }.Components ≃ { predStrands := n, braid := c * b * c⁻¹ }.Components

Conjugation carries each component along the conjugating braid's strand permutation.

@[simp]

theorem TauCeti.MarkovBraid.conjComponentsEquiv_mk {n : ℕ} (b c : BraidGroup (n + 1)) (i : Fin (n + 1)) : (conjComponentsEquiv b c) ⟦i⟧ = ⟦((BraidGroup.permHom (n + 1)) c) i⟧

The component bijection for conjugation applies the conjugating strand permutation.

@[simp]

theorem TauCeti.MarkovBraid.conjComponentsEquiv_symm_mk {n : ℕ} (b c : BraidGroup (n + 1)) (i : Fin (n + 1)) : (conjComponentsEquiv b c).symm ⟦i⟧ = ⟦(Equiv.symm ((BraidGroup.permHom (n + 1)) c)) i⟧

The inverse conjugation correspondence follows the inverse strand permutation.

noncomputable def TauCeti.MarkovBraid.stabilizeComponentsEquiv {n : ℕ} (b : BraidGroup (n + 1)) : { predStrands := n, braid := b }.Components ≃ { predStrands := n + 1, braid := BraidGroup.strandIncl b * BraidGroup.sigma (Fin.last n) }.Components

Positive stabilization preserves components by including the old strands.

noncomputable def TauCeti.MarkovBraid.stabilizeInvComponentsEquiv {n : ℕ} (b : BraidGroup (n + 1)) : { predStrands := n, braid := b }.Components ≃ { predStrands := n + 1, braid := BraidGroup.strandIncl b * (BraidGroup.sigma (Fin.last n))⁻¹ }.Components

Negative stabilization has the same component correspondence as positive stabilization.

@[simp]

theorem TauCeti.MarkovBraid.stabilizeComponentsEquiv_mk {n : ℕ} (b : BraidGroup (n + 1)) (i : Fin (n + 1)) : (stabilizeComponentsEquiv b) ⟦i⟧ = ⟦i.castSucc⟧

Positive stabilization sends each old strand to its inclusion.

@[simp]

theorem TauCeti.MarkovBraid.stabilizeInvComponentsEquiv_mk {n : ℕ} (b : BraidGroup (n + 1)) (i : Fin (n + 1)) : (stabilizeInvComponentsEquiv b) ⟦i⟧ = ⟦i.castSucc⟧

Negative stabilization sends each old strand to its inclusion.

@[simp]

theorem TauCeti.MarkovBraid.stabilizeComponentsEquiv_symm_mk {n : ℕ} (b : BraidGroup (n + 1)) (i : Fin (n + 1)) : (stabilizeComponentsEquiv b).symm ⟦i.castSucc⟧ = ⟦i⟧

The inverse positive-stabilization correspondence recovers the component of an old strand.

@[simp]

theorem TauCeti.MarkovBraid.stabilizeInvComponentsEquiv_symm_mk {n : ℕ} (b : BraidGroup (n + 1)) (i : Fin (n + 1)) : (stabilizeInvComponentsEquiv b).symm ⟦i.castSucc⟧ = ⟦i⟧

The inverse negative-stabilization correspondence recovers the component of an old strand.

@[simp]

theorem TauCeti.MarkovBraid.stabilizeComponentsEquiv_symm_mk_last {n : ℕ} (b : BraidGroup (n + 1)) : (stabilizeComponentsEquiv b).symm ⟦Fin.last (n + 1)⟧ = ⟦Fin.last n⟧

Under positive stabilization the new strand joins the old last strand's component.

@[simp]

theorem TauCeti.MarkovBraid.stabilizeInvComponentsEquiv_symm_mk_last {n : ℕ} (b : BraidGroup (n + 1)) : (stabilizeInvComponentsEquiv b).symm ⟦Fin.last (n + 1)⟧ = ⟦Fin.last n⟧

Under negative stabilization the new strand joins the old last strand's component.

@[reducible, inline]

abbrev TauCeti.FramedMarkovBraid.conj (β : FramedMarkovBraid) (c : BraidGroup (β.forgetFraming.predStrands + 1)) : FramedMarkovBraid

Conjugate a framed braid closure, carrying its Seifert-relative coefficients along the conjugating strand permutation.

@[simp]

theorem TauCeti.FramedMarkovBraid.forgetFraming_conj (β : FramedMarkovBraid) (c : BraidGroup (β.forgetFraming.predStrands + 1)) : (β.conj c).forgetFraming = { predStrands := β.forgetFraming.predStrands, braid := c * β.forgetFraming.braid * c⁻¹ }

Forgetting the framing of conjugation gives ordinary braid conjugation.

@[simp]

theorem TauCeti.FramedMarkovBraid.framing_conj_mk (β : FramedMarkovBraid) (c : BraidGroup (β.forgetFraming.predStrands + 1)) (i : Fin (β.forgetFraming.predStrands + 1)) : (β.conj c).framing ⟦i⟧ = β.framing ⟦(Equiv.symm ((BraidGroup.permHom (β.forgetFraming.predStrands + 1)) c)) i⟧

Conjugation reads the old framing at the inverse image of the strand.

@[simp]

theorem TauCeti.FramedMarkovBraid.framing_conj_componentsEquiv (β : FramedMarkovBraid) (c : BraidGroup (β.forgetFraming.predStrands + 1)) (q : β.forgetFraming.Components) : (β.conj c).framing ((MarkovBraid.conjComponentsEquiv β.forgetFraming.braid c) q) = β.framing q

Conjugation preserves the coefficient on each corresponding component.

@[reducible, inline]

noncomputable abbrev TauCeti.FramedMarkovBraid.stabilize (β : FramedMarkovBraid) : FramedMarkovBraid

Positively stabilize a framed closure, preserving the Seifert-relative framing of every component. The new strand joins the component of the old last strand.

@[reducible, inline]

noncomputable abbrev TauCeti.FramedMarkovBraid.stabilizeInv (β : FramedMarkovBraid) : FramedMarkovBraid

Negatively stabilize a framed closure, preserving its Seifert-relative coefficients.

@[simp]

theorem TauCeti.FramedMarkovBraid.forgetFraming_stabilize (β : FramedMarkovBraid) : β.stabilize.forgetFraming = { predStrands := β.forgetFraming.predStrands + 1, braid := BraidGroup.strandIncl β.forgetFraming.braid * BraidGroup.sigma (Fin.last β.forgetFraming.predStrands) }

Forgetting framing gives positive stabilization of the underlying braid.

@[simp]

theorem TauCeti.FramedMarkovBraid.forgetFraming_stabilizeInv (β : FramedMarkovBraid) : β.stabilizeInv.forgetFraming = { predStrands := β.forgetFraming.predStrands + 1, braid := BraidGroup.strandIncl β.forgetFraming.braid * (BraidGroup.sigma (Fin.last β.forgetFraming.predStrands))⁻¹ }

Forgetting framing gives negative stabilization of the underlying braid.

@[simp]

theorem TauCeti.FramedMarkovBraid.framing_stabilize_componentsEquiv (β : FramedMarkovBraid) (q : β.forgetFraming.Components) : β.stabilize.framing ((MarkovBraid.stabilizeComponentsEquiv β.forgetFraming.braid) q) = β.framing q

Positive stabilization preserves the coefficient on each corresponding component.

@[simp]

theorem TauCeti.FramedMarkovBraid.framing_stabilizeInv_componentsEquiv (β : FramedMarkovBraid) (q : β.forgetFraming.Components) : β.stabilizeInv.framing ((MarkovBraid.stabilizeInvComponentsEquiv β.forgetFraming.braid) q) = β.framing q

Negative stabilization preserves the coefficient on each corresponding component.

@[simp]

theorem TauCeti.FramedMarkovBraid.framing_stabilize_mk (β : FramedMarkovBraid) (i : Fin (β.forgetFraming.predStrands + 1)) : β.stabilize.framing ⟦i.castSucc⟧ = β.framing ⟦i⟧

Positive stabilization retains the framing coefficient at every old strand.

@[simp]

theorem TauCeti.FramedMarkovBraid.framing_stabilizeInv_mk (β : FramedMarkovBraid) (i : Fin (β.forgetFraming.predStrands + 1)) : β.stabilizeInv.framing ⟦i.castSucc⟧ = β.framing ⟦i⟧

Negative stabilization retains the framing coefficient at every old strand.

@[simp]

theorem TauCeti.FramedMarkovBraid.framing_stabilize_mk_last (β : FramedMarkovBraid) : β.stabilize.framing ⟦Fin.last (β.forgetFraming.predStrands + 1)⟧ = β.framing ⟦Fin.last β.forgetFraming.predStrands⟧

The new strand in positive stabilization has the old last strand's framing coefficient.

@[simp]

theorem TauCeti.FramedMarkovBraid.framing_stabilizeInv_mk_last (β : FramedMarkovBraid) : β.stabilizeInv.framing ⟦Fin.last (β.forgetFraming.predStrands + 1)⟧ = β.framing ⟦Fin.last β.forgetFraming.predStrands⟧

The new strand in negative stabilization has the old last strand's framing coefficient.