The Jimbo representation of the braid group

Let ι be a linearly ordered type of colours and q a unit of a commutative ring R. The q-tensor space on n strands is the free R-module (Fin n → ι) →₀ R on the words of length n in ι; for ι = Fin N it is the n-th tensor power of R ^ N. The Jimbo R-matrix acts on two strands j and k of a word w, depending only on how the colours a = w j and b = w k compare:

• if a = b, the word is multiplied by q;
• if a < b, the two colours are exchanged;
• if b < a, the two colours are exchanged, and (q - q⁻¹) times the word is added.

This is TauCeti.KnotTheory.jimboGenerator q j k. It satisfies the Hecke quadratic relation T * T = (q - q⁻¹) • T + 1, equivalently (T - q) * (T + q⁻¹) = 0, so it is invertible with inverse T + (q⁻¹ - q); operators on disjoint pairs of strands commute; and operators on two pairs sharing a strand satisfy the braid relation, which is the Yang-Baxter equation for this R-matrix. Hence the adjacent operators define a representation TauCeti.KnotTheory.jimbo ι q of the braid group TauCeti.BraidGroup n on the q-tensor space, in which every elementary braid satisfies the Hecke relation. The representation therefore factors through the Iwahori-Hecke algebra of type A; for ι = Fin N it is the action of that algebra on the n-th tensor power of the vector representation of U_q(gl_N) in quantum Schur-Weyl duality.

For ι = Fin N, Turaev's enhancement of the R-matrix gives a weighted trace of this representation. The weighted trace alone is not a Markov invariant: positive and negative stabilization multiply it by α * β and α⁻¹ * β, where α and β are the constants of the enhancement (for this R-matrix α is q ^ N, up to the choice of orientation conventions). Turaev's invariant of a braid on n strands with exponent sum (writhe) e is the weighted trace multiplied by α ^ (-e) * β ^ (-n). It is a Markov invariant of braids, the sl_N specialization of the HOMFLY polynomial at z = q - q⁻¹ and a = q ^ N; these specializations, over all N, determine the HOMFLY polynomial. The weighted trace is constructed in TauCeti/KnotTheory/Jimbo/Trace.lean; its stabilization laws and writhe normalization are constructed in TauCeti/KnotTheory/Jimbo/Stabilization.lean and TauCeti/KnotTheory/Jimbo/Normalization.lean. For N = 2 this is the vertex-model route to the Jones polynomial, which TauCeti.TemperleyLieb.markovTrace follows through the Temperley-Lieb algebra.

At q = 1 the correction term vanishes, and the representation is the permutation action of braids on the positions of the letters of a word (TauCeti.KnotTheory.jimbo_one_apply_single), so the Jimbo representation is a one-parameter deformation of the permutation representation.

Main definitions

• TauCeti.KnotTheory.jimboGenerator: the Jimbo R-matrix acting on two strands of the q-tensor space.
• TauCeti.KnotTheory.jimboUnit: the R-matrix on two adjacent strands, as a unit.
• TauCeti.KnotTheory.jimbo: the Jimbo representation BraidGroup n →* (Module.End R ((Fin n → ι) →₀ R))ˣ.

Main results

• TauCeti.KnotTheory.jimboGenerator_mul_self: the Hecke quadratic relation T * T = (q - q⁻¹) • T + 1.
• TauCeti.KnotTheory.jimboGenerator_mul_comm: operators on disjoint pairs of strands commute.
• TauCeti.KnotTheory.jimboGenerator_braid: the braid relation (Yang-Baxter equation).
• TauCeti.KnotTheory.jimbo_sigma: the representation takes σ i to the R-matrix on the strands i and i + 1.
• TauCeti.KnotTheory.val_jimbo_sigma_eq_val_inv_add: the skein relation σ = σ⁻¹ + (q - q⁻¹) in the representation.
• TauCeti.KnotTheory.jimbo_one_apply_single: at q = 1 it is the permutation action on words.

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. F. R. Jones, Hecke algebra representations of braid groups and link polynomials, Ann. of Math. 126 (1987), 335-388.
• V. G. Turaev, The Yang-Baxter equation and invariants of links, Invent. Math. 92 (1988), 527-553.

noncomputable def TauCeti.KnotTheory.jimboGenerator {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) (j k : Fin n) : Module.End R ((Fin n → ι) →₀ R)

The Jimbo R-matrix acting on the strands j and k of the q-tensor space (Fin n → ι) →₀ R. On a basis word w, it multiplies w by q if w j = w k; it exchanges the letters at j and k if w j < w k; and if w k < w j it exchanges them and adds (q - q⁻¹) times w.

@[simp]

theorem TauCeti.KnotTheory.jimboGenerator_single_one {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) (j k : Fin n) (w : Fin n → ι) : (jimboGenerator q j k) (Finsupp.single w 1) = if w j = w k then ↑q • Finsupp.single w 1 else if w j < w k then Finsupp.single (w ∘ ⇑(Equiv.swap j k)) 1 else Finsupp.single (w ∘ ⇑(Equiv.swap j k)) 1 + (↑q - ↑q⁻¹) • Finsupp.single w 1

The value of the Jimbo R-matrix on a basis word.

theorem TauCeti.KnotTheory.jimboGenerator_single_update_update {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) {j k : Fin n} (hjk : j ≠ k) (w : Fin n → ι) (x y : ι) : (jimboGenerator q j k) (Finsupp.single (Function.update (Function.update w j x) k y) 1) = if x = y then ↑q • Finsupp.single (Function.update (Function.update w j x) k y) 1 else if x < y then Finsupp.single (Function.update (Function.update w j y) k x) 1 else Finsupp.single (Function.update (Function.update w j y) k x) 1 + (↑q - ↑q⁻¹) • Finsupp.single (Function.update (Function.update w j x) k y) 1

The value of the Jimbo R-matrix on the strands j and k on a basis word whose letters at j and k are x and y.

theorem TauCeti.KnotTheory.jimboGenerator_mul_self {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) {j k : Fin n} (hjk : j ≠ k) : jimboGenerator q j k * jimboGenerator q j k = (↑q - ↑q⁻¹) • jimboGenerator q j k + 1

The Hecke quadratic relation T * T = (q - q⁻¹) • T + 1 for the Jimbo R-matrix.

theorem TauCeti.KnotTheory.jimboGenerator_mul_add {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) {j k : Fin n} (hjk : j ≠ k) : jimboGenerator q j k * (jimboGenerator q j k + (↑q⁻¹ - ↑q) • 1) = 1

The Jimbo R-matrix is invertible, with right inverse T + (q⁻¹ - q).

theorem TauCeti.KnotTheory.add_mul_jimboGenerator {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) {j k : Fin n} (hjk : j ≠ k) : (jimboGenerator q j k + (↑q⁻¹ - ↑q) • 1) * jimboGenerator q j k = 1

The Jimbo R-matrix is invertible, with left inverse T + (q⁻¹ - q).

theorem TauCeti.KnotTheory.jimboGenerator_mul_comm {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) {j k l m : Fin n} (h : [j, k, l, m].Nodup) : jimboGenerator q j k * jimboGenerator q l m = jimboGenerator q l m * jimboGenerator q j k

Jimbo R-matrices on disjoint pairs of strands commute.

theorem TauCeti.KnotTheory.jimboGenerator_braid {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) {j k l : Fin n} (hjk : j ≠ k) (hkl : k ≠ l) (hjl : j ≠ l) : jimboGenerator q j k * jimboGenerator q k l * jimboGenerator q j k = jimboGenerator q k l * jimboGenerator q j k * jimboGenerator q k l

The braid relation for Jimbo R-matrices on two pairs of strands sharing the strand k. This is the Yang-Baxter equation for the Jimbo R-matrix.

@[simp]

theorem TauCeti.KnotTheory.jimboGenerator_one_apply_single {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (j k : Fin n) (w : Fin n → ι) (c : R) : (jimboGenerator 1 j k) (Finsupp.single w c) = Finsupp.single (w ∘ ⇑(Equiv.swap j k)) c

At q = 1 the Jimbo R-matrix exchanges the letters at the strands j and k.

noncomputable def TauCeti.KnotTheory.jimboUnit {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) (i : Fin (n - 1)) : (Module.End R ((Fin n → ι) →₀ R))ˣ

The Jimbo R-matrix on the two strands crossed by the elementary braid σ i, as a unit, with inverse T + (q⁻¹ - q).

@[simp]

theorem TauCeti.KnotTheory.jimboUnit_val {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) (i : Fin (n - 1)) : ↑(jimboUnit q i) = jimboGenerator q (BraidGroup.strand i) (BraidGroup.strandSucc i)

The value of the unit TauCeti.KnotTheory.jimboUnit.

@[simp]

theorem TauCeti.KnotTheory.jimboUnit_inv_val {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) (i : Fin (n - 1)) : ↑(jimboUnit q i)⁻¹ = jimboGenerator q (BraidGroup.strand i) (BraidGroup.strandSucc i) + (↑q⁻¹ - ↑q) • 1

The value of the inverse of the unit TauCeti.KnotTheory.jimboUnit.

noncomputable def TauCeti.KnotTheory.jimbo {R : Type u_1} [CommRing R] (ι : Type u_2) [LinearOrder ι] {n : ℕ} (q : Rˣ) : BraidGroup n →* (Module.End R ((Fin n → ι) →₀ R))ˣ

The Jimbo representation of the braid group on the q-tensor space (Fin n → ι) →₀ R: the elementary braid σ i acts by the Jimbo R-matrix on the strands i and i + 1.

@[simp]

theorem TauCeti.KnotTheory.jimbo_sigma {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) (i : Fin (n - 1)) : (jimbo ι q) (BraidGroup.sigma i) = jimboUnit q i

The Jimbo representation takes the elementary braid σ i to the Jimbo R-matrix on the strands i and i + 1.

theorem TauCeti.KnotTheory.val_jimbo_sigma_eq_val_inv_add {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (q : Rˣ) (i : Fin (n - 1)) : ↑((jimbo ι q) (BraidGroup.sigma i)) = ↑((jimbo ι q) (BraidGroup.sigma i))⁻¹ + (↑q - ↑q⁻¹) • 1

The skein relation T = T⁻¹ + (q - q⁻¹) of an elementary braid in the Jimbo representation, the relation behind the HOMFLY skein relation.

@[simp]

theorem TauCeti.KnotTheory.jimbo_one_apply_single {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] {n : ℕ} (b : BraidGroup n) (w : Fin n → ι) (c : R) : ↑((jimbo ι 1) b) (Finsupp.single w c) = Finsupp.single (w ∘ ⇑((BraidGroup.permHom n) b)⁻¹) c

At q = 1 the Jimbo representation is the permutation action of braids on words: a braid b sends the word w to w ∘ π⁻¹, where π is the permutation of the strands underlying b.