Adding an uncrossed strand in the Jimbo representation

Appending a fixed colour to every word intertwines the Jimbo actions on n + 1 and n + 2 strands along BraidGroup.strandIncl. Thus the added strand retains its colour, and the action on the old strands is unchanged. This is the tensor-power compatibility needed when taking a partial trace over the added strand in a Markov stabilization.

The weighted trace of the included braid is its old weighted trace multiplied by the quantum dimension. We work over arbitrary commutative rings and allow any number of colours, including zero.

References

• V. G. Turaev, The Yang-Baxter equation and invariants of links, Invent. Math. 92 (1988), 527–553 (enhanced braid representations and their Markov traces).
• V. F. R. Jones, Hecke algebra representations of braid groups and link polynomials, Ann. of Math. 126 (1987), 335–388.

The word inclusion uses Mathlib's Finsupp.lmapDomain and Fin.snoc; no separate tensor-space inclusion is introduced.

theorem TauCeti.KnotTheory.jimboGenerator_comp_lmapDomain_snoc {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) (j k : Fin n) (a : ι) : (jimboGenerator q j.castSucc k.castSucc ∘ₗ Finsupp.lmapDomain R R fun (w : Fin n → ι) => Fin.snoc w a) = (Finsupp.lmapDomain R R fun (w : Fin n → ι) => Fin.snoc w a) ∘ₗ jimboGenerator q j k

Appending a colour intertwines a Jimbo generator with the generator on the same two old strands of the larger word space.

@[simp]

theorem TauCeti.KnotTheory.jimbo_strandIncl_lmapDomain_snoc {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) (b : BraidGroup (n + 1)) (a : ι) (v : (Fin (n + 1) → ι) →₀ R) : ↑((jimbo ι q) (BraidGroup.strandIncl b)) ((Finsupp.lmapDomain R R fun (w : Fin (n + 1) → ι) => Fin.snoc w a) v) = (Finsupp.lmapDomain R R fun (w : Fin (n + 1) → ι) => Fin.snoc w a) (↑((jimbo ι q) b) v)

The action of a braid after adding an uncrossed strand is its original action with the last colour held fixed. This intertwining identity applies to arbitrary vectors.

@[simp]

theorem TauCeti.KnotTheory.jimbo_strandIncl_single_snoc {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) (b : BraidGroup (n + 1)) (w : Fin (n + 1) → ι) (a : ι) (c : R) : ↑((jimbo ι q) (BraidGroup.strandIncl b)) (Finsupp.single (Fin.snoc w a) c) = Finsupp.mapDomain (fun (u : Fin (n + 1) → ι) => Fin.snoc u a) (↑((jimbo ι q) b) (Finsupp.single w c))

Basis-vector form of compatibility with adding an uncrossed strand.

@[simp]

theorem TauCeti.KnotTheory.jimbo_strandIncl_single_snoc_apply_snoc {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) (b : BraidGroup (n + 1)) (w u : Fin (n + 1) → ι) (a d : ι) (c : R) : (↑((jimbo ι q) (BraidGroup.strandIncl b)) (Finsupp.single (Fin.snoc w a) c)) (Fin.snoc u d) = if a = d then (↑((jimbo ι q) b) (Finsupp.single w c)) u else 0

Inclusion preserves coefficients on each fixed-last-colour block and has zero coefficients between blocks with different last colours.

@[simp]

theorem TauCeti.KnotTheory.jimboWeightedTrace_strandIncl {R : Type u_1} [CommRing R] {n N : ℕ} (q : Rˣ) (b : BraidGroup (n + 1)) : jimboWeightedTrace q (BraidGroup.strandIncl b) = jimboWeightedTrace q b * ∑ a : Fin N, jimboWeight q a

An uncrossed strand multiplies the weighted braid trace by the quantum dimension.