Turaev's enhancement of the Jimbo R-matrix

The diagonal operator with eigenvalues q ^ (N - 1 - 2 * a) on colours a : Fin N enhances the Jimbo R-matrix. On words its tensor powers commute with every crossing. The weighted partial trace over the second colour of a positive crossing is q ^ N times the identity; for a negative crossing it is q ^ (-N) times the identity. These are the local identities used to normalize a weighted braid trace under Markov stabilization. The partial traces are stated as matrix-coefficient sums in the canonical word basis, so they apply over any commutative ring and require no choice of basis. The weights themselves are defined in any monoid, their summation identities hold in any ring, and the diagonal enhancement and its inverse are defined over any commutative semiring.

References

• M. Jimbo, A q-analogue of U(gl(N+1)), Hecke algebra, and the Yang-Baxter equation, Lett. Math. Phys. 11 (1986), 247-252.
• V. G. Turaev, The Yang-Baxter equation and invariants of links, Invent. Math. 92 (1988), 527-553.
• G. Massuyeau, F. F. Nichita, Yang-Baxter operators arising from algebra structures and the Alexander polynomial of knots, Comm. Algebra 33 (2005), 2375-2385, Definition 3.1 (the enhancement conditions).

The R-matrix is jimboGenerator; jimboUnit bundles an adjacent crossing with its inverse.

def TauCeti.KnotTheory.jimboWeight {R : Type u_1} {N : ℕ} [Monoid R] (q : Rˣ) (a : Fin N) : R

The diagonal eigenvalue of Turaev's enhancement on the colour a. The exponent is an integer, and the parameter is a unit, so this is defined in any monoid.

theorem TauCeti.KnotTheory.jimboWeight_def {R : Type u_1} {N : ℕ} [Monoid R] (q : Rˣ) (a : Fin N) : jimboWeight q a = ↑(q ^ (↑N - 1 - 2 * ↑↑a))

The defining equation of the enhancement weight.

@[simp]

theorem TauCeti.KnotTheory.jimboWeight_one {R : Type u_1} {N : ℕ} [Monoid R] (a : Fin N) : jimboWeight 1 a = 1

The enhancement at q = 1 assigns weight one to every colour.

@[simp]

theorem TauCeti.KnotTheory.jimboWeight_mul_inv {R : Type u_1} {N : ℕ} [Monoid R] (q : Rˣ) (a : Fin N) : jimboWeight q a * jimboWeight q⁻¹ a = 1

Replacing q by its inverse gives the inverse enhancement weight.

noncomputable def TauCeti.KnotTheory.jimboEnhancement {R : Type u_1} {N n : ℕ} [CommSemiring R] (q : Rˣ) : Module.End R ((Fin n → Fin N) →₀ R)

The tensor power of the diagonal enhancement: the product density of the enhancement weights, which multiplies a basis word by the product of the weights of its colours.

@[simp]

theorem TauCeti.KnotTheory.jimboEnhancement_single_one {R : Type u_1} {N n : ℕ} [CommSemiring R] (q : Rˣ) (w : Fin n → Fin N) : (jimboEnhancement q) (Finsupp.single w 1) = (∏ i : Fin n, jimboWeight q (w i)) • Finsupp.single w 1

The enhancement acts diagonally in the canonical word basis.

@[simp]

theorem TauCeti.KnotTheory.jimboEnhancement_apply {R : Type u_1} {N n : ℕ} [CommSemiring R] (q : Rˣ) (v : (Fin n → Fin N) →₀ R) (w : Fin n → Fin N) : ((jimboEnhancement q) v) w = (∏ i : Fin n, jimboWeight q (w i)) * v w

The coefficient of a word after applying the tensor-power enhancement is its original coefficient multiplied by the product of the colour weights.

@[simp]

theorem TauCeti.KnotTheory.jimboEnhancement_one {R : Type u_1} {N n : ℕ} [CommSemiring R] : jimboEnhancement 1 = 1

At q = 1 the enhancement is the identity.

@[simp]

theorem TauCeti.KnotTheory.jimboEnhancement_mul_inv {R : Type u_1} {N n : ℕ} [CommSemiring R] (q : Rˣ) : jimboEnhancement q * jimboEnhancement q⁻¹ = 1

The tensor-power enhancement is inverted by replacing the parameter with its inverse.

theorem TauCeti.KnotTheory.isUnit_jimboEnhancement {R : Type u_1} {N n : ℕ} [CommSemiring R] (q : Rˣ) : IsUnit (jimboEnhancement q)

The enhancement is an invertible operator.

theorem TauCeti.KnotTheory.jimboEnhancement_commute_generator {R : Type u_1} {N n : ℕ} [CommRing R] (q : Rˣ) (j k : Fin n) : Commute (jimboEnhancement q) (jimboGenerator q j k)

The tensor-power enhancement commutes with the Jimbo crossing on any pair of strands.

theorem TauCeti.KnotTheory.jimboEnhancement_commute {R : Type u_1} {N n : ℕ} [CommRing R] (q : Rˣ) (b : BraidGroup n) : Commute (jimboEnhancement q) ↑((jimbo (Fin N) q) b)

The tensor-power enhancement commutes with every braid in the Jimbo representation.

theorem TauCeti.KnotTheory.jimboWeight_sum_lt {R : Type u_1} {N : ℕ} [Ring R] (q : Rˣ) (a : Fin N) : (↑q * jimboWeight q a + (↑q - ↑q⁻¹) * ∑ c : Fin N, if c < a then jimboWeight q c else 0) = ↑(q ^ N)

Summing the enhancement weights below a colour gives the positive stabilization factor. This formula involves no division by q - q⁻¹, so it also holds at q = ±1.

theorem TauCeti.KnotTheory.jimboWeight_sum {R : Type u_1} {N : ℕ} [Ring R] (q : Rˣ) : (↑q - ↑q⁻¹) * ∑ c : Fin N, jimboWeight q c = ↑(q ^ N) - ↑(q⁻¹ ^ N)

The difference of the positive and negative stabilization factors is the quantum dimension multiplied by the Hecke parameter.

theorem TauCeti.KnotTheory.sum_jimboGenerator_coeff_mul_weight {R : Type u_1} {N : ℕ} [CommRing R] (q : Rˣ) (a b : Fin N) : ∑ c : Fin N, ((jimboGenerator q 0 1) (Finsupp.single ![b, c] 1)) ![a, c] * jimboWeight q c = if a = b then ↑(q ^ N) else 0

The weighted partial trace of a positive Jimbo crossing over its second colour.

theorem TauCeti.KnotTheory.sum_jimboUnit_inv_coeff_mul_weight {R : Type u_1} {N : ℕ} [CommRing R] (q : Rˣ) (a b : Fin N) : ∑ c : Fin N, (↑(jimboUnit q 0)⁻¹ (Finsupp.single ![b, c] 1)) ![a, c] * jimboWeight q c = if a = b then ↑(q⁻¹ ^ N) else 0

The weighted partial trace of a negative Jimbo crossing over its second colour.