The weighted trace of the Jimbo braid representation

The weighted trace is tr (ρ(b) * μ^{⊗n}), where ρ is the Jimbo representation and μ is Turaev's diagonal enhancement. It is invariant under braid conjugation and satisfies the unnormalized HOMFLY skein relation. On the identity braid it is the n-th power of the quantum dimension ∑ a, q ^ (N - 1 - 2 * a).

The coefficient formula makes the trace computable in the canonical word basis. The two single-crossing values check both signs of the enhancement against the one-strand value. The weighted trace itself still changes under stabilization; the writhe normalization and the general stabilization laws are separate results.

References

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

The trace uses Mathlib's basis-independent LinearMap.trace; the representation and enhancement are constructed in the companion modules.

noncomputable def TauCeti.KnotTheory.jimboWeightedTrace {R : Type u_1} [CommRing R] {N n : ℕ} (q : Rˣ) (b : BraidGroup n) : R

Turaev's weighted trace of a braid in the Jimbo representation with N colours. No division by the quantum dimension or by q - q⁻¹ is required.

theorem TauCeti.KnotTheory.jimboWeightedTrace_def {R : Type u_1} [CommRing R] {N n : ℕ} (q : Rˣ) (b : BraidGroup n) : jimboWeightedTrace q b = (LinearMap.trace R ((Fin n → Fin N) →₀ R)) (↑((jimbo (Fin N) q) b) * jimboEnhancement q)

The defining equation of the weighted braid trace.

theorem TauCeti.KnotTheory.jimboWeightedTrace_eq_sum {R : Type u_1} [CommRing R] {N n : ℕ} (q : Rˣ) (b : BraidGroup n) : jimboWeightedTrace q b = ∑ w : Fin n → Fin N, (↑((jimbo (Fin N) q) b) (Finsupp.single w 1)) w * ∏ i : Fin n, jimboWeight q (w i)

The weighted trace is the sum of diagonal coefficients times their word weights.

@[simp]

theorem TauCeti.KnotTheory.jimboWeightedTrace_one {R : Type u_1} [CommRing R] {N n : ℕ} (q : Rˣ) : jimboWeightedTrace q 1 = (∑ a : Fin N, jimboWeight q a) ^ n

The trace of the identity braid, whose closure is the n-component unlink.

theorem TauCeti.KnotTheory.jimboWeightedTrace_mul_comm {R : Type u_1} [CommRing R] {N n : ℕ} (q : Rˣ) (b c : BraidGroup n) : jimboWeightedTrace q (b * c) = jimboWeightedTrace q (c * b)

The weighted trace has the cyclic property on products of braids.

@[simp]

theorem TauCeti.KnotTheory.jimboWeightedTrace_conj {R : Type u_1} [CommRing R] {N n : ℕ} (q : Rˣ) (b c : BraidGroup n) : jimboWeightedTrace q (c * b * c⁻¹) = jimboWeightedTrace q b

Conjugation, the first Markov move, preserves the weighted trace.

theorem TauCeti.KnotTheory.jimboWeightedTrace_skein {R : Type u_1} [CommRing R] {N n : ℕ} (q : Rˣ) (b c : BraidGroup n) (i : Fin (n - 1)) : jimboWeightedTrace q (b * BraidGroup.sigma i * c) = jimboWeightedTrace q (b * (BraidGroup.sigma i)⁻¹ * c) + (↑q - ↑q⁻¹) * jimboWeightedTrace q (b * c)

Changing one crossing gives the unnormalized HOMFLY skein relation, in any braid context.

@[simp]

theorem TauCeti.KnotTheory.jimboWeightedTrace_sigma_two {R : Type u_1} [CommRing R] {N : ℕ} (q : Rˣ) : jimboWeightedTrace q (BraidGroup.sigma 0) = ↑(q ^ N) * ∑ a : Fin N, jimboWeight q a

The positive crossing on two strands has trace q ^ N times the quantum dimension.

@[simp]

theorem TauCeti.KnotTheory.jimboWeightedTrace_sigma_two_inv {R : Type u_1} [CommRing R] {N : ℕ} (q : Rˣ) : jimboWeightedTrace q (BraidGroup.sigma 0)⁻¹ = ↑(q⁻¹ ^ N) * ∑ a : Fin N, jimboWeight q a

The negative crossing on two strands has trace q ^ (-N) times the quantum dimension.

@[simp]

theorem TauCeti.KnotTheory.jimboWeightedTrace_one_parameter {R : Type u_1} [CommRing R] {N n : ℕ} (b : BraidGroup n) : jimboWeightedTrace 1 b = ↑{w : Fin n → Fin N | w ∘ ⇑((BraidGroup.permHom n) b)⁻¹ = w}.card

At q = 1, the trace counts colourings fixed by the underlying strand permutation.