The Jones representation of the braid group

For a unit a : Rˣ, set the Temperley-Lieb loop value to δ = -(a ^ 2 + a⁻¹ ^ 2). The Kauffman-bracket assignment

σ i ↦ a • 1 + a⁻¹ • e i

satisfies the braid relations and defines TauCeti.TemperleyLieb.jones, a representation of TauCeti.BraidGroup n in the units of TemperleyLieb R δ n. At this loop value the coefficient-swapped element a⁻¹ • 1 + a • e i is the inverse of the assigned crossing. Composing this representation with the Markov trace TauCeti.TemperleyLieb.markovTrace of the Temperley-Lieb algebra, at q = a ^ 2, is the braid route to the Jones polynomial. For a braid b on n + 1 strands with exponent sum w, TauCeti.MarkovBraid.jonesTrace is the writhe-normalized trace (-a ^ 3) ^ (-w) * tr (jones b). The trace property makes it invariant under conjugation. Under stabilization the new crossing a • 1 + a⁻¹ • e contributes a * δ + a⁻¹ = -a ^ 3 to the trace, by the two compatibilities of the Markov trace with adding a strand, and the writhe normalization absorbs this factor; the negative crossing contributes -a⁻¹ ^ 3 in the same way. So jonesTrace is constant along Markov equivalence (TauCeti.MarkovEquiv.jonesTrace_eq); by Markov's theorem, which is not formalized, it is an invariant of the closed braid as an oriented link. With the normalization tr 1 = δ ^ (n + 1) of the Markov trace, the closure of the trivial one-strand braid, the unknot, has value δ, and the closure of σ₀ ^ 3, the right-handed trefoil, has value δ * (A⁻⁴ + A⁻¹² - A⁻¹⁶) at a = A. This is δ times the writhe-normalized Kauffman bracket TauCeti.normalizedKauffmanBracket_rightHandedTrefoilPDCode of a PD-code of the trefoil, so the braid route and the diagram route agree on it.

Main definitions

• TauCeti.TemperleyLieb.jonesDelta: the loop value -(a ^ 2 + a⁻¹ ^ 2).
• TauCeti.TemperleyLieb.jonesUnit: the Kauffman-bracket expansion of one crossing as a unit.
• TauCeti.TemperleyLieb.jones: the Jones representation BraidGroup n →* (TemperleyLieb R (jonesDelta a) n)ˣ.
• TauCeti.MarkovBraid.jonesTrace: the writhe-normalized Markov trace of the Jones representation of a braid.

Main results

• TauCeti.TemperleyLieb.jonesDelta_inv: the loop value is unchanged by inverting the unit.
• TauCeti.TemperleyLieb.mul_jonesDelta_add_inv and TauCeti.TemperleyLieb.inv_mul_jonesDelta_add: closing up the two smoothings of a positive or negative crossing on a new strand multiplies by -a ^ 3 or by its inverse, the identities behind invariance under stabilization.
• TauCeti.TemperleyLieb.jones_sigma: the representation sends sigma i to jonesUnit a i.
• TauCeti.TemperleyLieb.jonesUnit_mul_jonesUnit_comm: units for disjoint crossings satisfy the distant-generator braid relation.
• TauCeti.TemperleyLieb.jonesUnit_braid: units for adjacent crossings satisfy the braid relation corresponding to the third Reidemeister move.
• TauCeti.TemperleyLieb.jones_sigma_ne_one_two: the representation is nontrivial on two strands over a nontrivial base ring.
• TauCeti.TemperleyLieb.jones_strandIncl: the representation commutes with adding a strand.
• TauCeti.MarkovEquiv.jonesTrace_eq: the writhe-normalized trace is a Markov invariant.
• TauCeti.MarkovBraid.jonesTrace_one_strand and TauCeti.MarkovBraid.jonesTrace_sigma_pow_three: its values on the unknot and the trefoil braids.

References

• V. F. R. Jones, A polynomial invariant for knots via von Neumann algebras, Bull. Amer. Math. Soc. 12 (1985), 103-111.
• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 3 (the Kauffman bracket and Jones polynomial).
• L. H. Kauffman, State models and the Jones polynomial, Topology 26 (1987), 395-407.
• V. F. R. Jones, Hecke algebra representations of braid groups and link polynomials, Ann. of Math. 126 (1987), 335-388 (the link invariant from the Markov trace).

def TauCeti.TemperleyLieb.jonesDelta {R : Type u_1} [CommRing R] (a : Rˣ) : R

The loop value -(a ^ 2 + a⁻¹ ^ 2) at which the Jones representation is defined.

Equations

• TauCeti.TemperleyLieb.jonesDelta a = -(↑a ^ 2 + ↑a⁻¹ ^ 2)

@[simp]

theorem TauCeti.TemperleyLieb.jonesDelta_def {R : Type u_1} [CommRing R] (a : Rˣ) : jonesDelta a = -(↑a ^ 2 + ↑a⁻¹ ^ 2)

The defining equation of the Jones loop value.

theorem TauCeti.TemperleyLieb.jonesDelta_eq_neg_inv_sq_add_sq {R : Type u_1} [CommRing R] (a : Rˣ) : jonesDelta a = -(↑a⁻¹ ^ 2 + ↑a ^ 2)

The Jones loop value is symmetric in a and a⁻¹, which is what lets the two coefficients of a crossing be swapped.

theorem TauCeti.TemperleyLieb.jonesDelta_inv {R : Type u_1} [CommRing R] (a : Rˣ) : jonesDelta a⁻¹ = jonesDelta a

The Jones loop value is unchanged by inverting the unit.

def TauCeti.TemperleyLieb.jonesUnit {R : Type u_1} [CommRing R] {n : ℕ} (a : Rˣ) (i : Fin (n - 1)) : (TemperleyLieb R (jonesDelta a) n)ˣ

The Kauffman-bracket expansion of an elementary braid, as a unit of the Temperley-Lieb algebra: a • 1 + a⁻¹ • e i, with inverse a⁻¹ • 1 + a • e i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.TemperleyLieb.jonesUnit_val {R : Type u_1} [CommRing R] {n : ℕ} (a : Rˣ) (i : Fin (n - 1)) : ↑(jonesUnit a i) = crossing (jonesDelta a) (↑a) (↑a⁻¹) i

The value of the Kauffman-bracket unit.

@[simp]

theorem TauCeti.TemperleyLieb.jonesUnit_inv_val {R : Type u_1} [CommRing R] {n : ℕ} (a : Rˣ) (i : Fin (n - 1)) : ↑(jonesUnit a i)⁻¹ = crossing (jonesDelta a) (↑a⁻¹) (↑a) i

The value of the inverse of the Kauffman-bracket unit.

def TauCeti.TemperleyLieb.jones {R : Type u_1} [CommRing R] (n : ℕ) (a : Rˣ) : BraidGroup n →* (TemperleyLieb R (jonesDelta a) n)ˣ

The Jones representation of the braid group in the units of the Temperley-Lieb algebra: the elementary braid σ i goes to the Kauffman-bracket expansion a • 1 + a⁻¹ • e i of a crossing. Composing it with the Markov trace is the braid route to the Jones polynomial.

Equations

• TauCeti.TemperleyLieb.jones n a = TauCeti.BraidGroup.lift (fun (i : Fin (n - 1)) => TauCeti.TemperleyLieb.jonesUnit a i) ⋯ ⋯

@[simp]

theorem TauCeti.TemperleyLieb.jones_sigma {R : Type u_1} [CommRing R] {n : ℕ} (a : Rˣ) (i : Fin (n - 1)) : (jones n a) (BraidGroup.sigma i) = jonesUnit a i

The Jones representation takes an elementary braid to the Kauffman-bracket unit.

theorem TauCeti.TemperleyLieb.jonesUnit_mul_jonesUnit_comm {R : Type u_1} [CommRing R] {n : ℕ} (a : Rˣ) {i j : Fin (n - 1)} (h : ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i) : jonesUnit a i * jonesUnit a j = jonesUnit a j * jonesUnit a i

Jones units on disjoint pairs of strands commute, the distant-generator braid relation.

theorem TauCeti.TemperleyLieb.jonesUnit_braid {R : Type u_1} [CommRing R] {n : ℕ} (a : Rˣ) {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : jonesUnit a i * jonesUnit a j * jonesUnit a i = jonesUnit a j * jonesUnit a i * jonesUnit a j

Jones units on adjacent pairs of strands satisfy the braid relation corresponding to the third Reidemeister move.

theorem TauCeti.TemperleyLieb.jones_sigma_ne_one_two {R : Type u_1} [CommRing R] [Nontrivial R] (a : Rˣ) (i : Fin (2 - 1)) : (jones 2 a) (BraidGroup.sigma i) ≠ 1

The Jones representation of the two-strand braid group is nontrivial: the elementary braid does not go to the identity.

theorem TauCeti.TemperleyLieb.jonesDelta_eq_neg_sq_add_inv_sq {R : Type u_1} [CommRing R] (a : Rˣ) : jonesDelta a = -(↑(a ^ 2) + ↑(a ^ 2)⁻¹)

The Jones loop value is -(q + q⁻¹) for the unit q = a ^ 2, the form in which the Markov trace TauCeti.TemperleyLieb.markovTrace is built.

theorem TauCeti.TemperleyLieb.mul_jonesDelta_add_inv {R : Type u_1} [CommRing R] (a : Rˣ) : ↑a * jonesDelta a + ↑a⁻¹ = ↑(-a ^ 3)

The two smoothings of a positive crossing on a new strand, closed up by the Markov trace, contribute a * δ + a⁻¹ = -a ^ 3.

theorem TauCeti.TemperleyLieb.inv_mul_jonesDelta_add {R : Type u_1} [CommRing R] (a : Rˣ) : ↑a⁻¹ * jonesDelta a + ↑a = ↑(-a ^ 3)⁻¹

The two smoothings of a negative crossing on a new strand, closed up by the Markov trace, contribute a⁻¹ * δ + a = -a⁻¹ ^ 3.

@[simp]

theorem TauCeti.TemperleyLieb.jones_strandIncl {R : Type u_1} [CommRing R] {n : ℕ} (a : Rˣ) (b : BraidGroup (n + 1)) : ↑((jones (n + 2) a) (BraidGroup.strandIncl b)) = strandIncl ↑((jones (n + 1) a) b)

Adding a straight last strand commutes with the Jones representation: the braid with an added uncrossed strand goes to the image of its Jones representative under TauCeti.TemperleyLieb.strandIncl.

def TauCeti.MarkovBraid.jonesTrace {R : Type u_1} [CommRing R] (β : MarkovBraid) (a : Rˣ) : R

The writhe-normalized Markov trace of the Jones representation of a braid: for a braid b on n + 1 strands with exponent sum w it is (-a ^ 3) ^ (-w) * tr (jones b), where tr is the Markov trace TauCeti.TemperleyLieb.markovTrace at q = a ^ 2, normalized by tr 1 = δ ^ (n + 1). It is a Markov invariant (TauCeti.MarkovEquiv.jonesTrace_eq), and the unknot braid has value δ (TauCeti.MarkovBraid.jonesTrace_one_strand).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.MarkovBraid.jonesTrace_def {R : Type u_1} [CommRing R] (β : MarkovBraid) (a : Rˣ) : β.jonesTrace a = ↑((-a ^ 3) ^ (-Multiplicative.toAdd ((ArtinGroup.exponentSum (CoxeterMatrix.A (β.predStrands + 1 - 1))) β.braid))) * (TemperleyLieb.markovTrace (a ^ 2) ⋯) ↑((TemperleyLieb.jones (β.predStrands + 1) a) β.braid)

The writhe-normalized trace is the Markov trace of the Jones representative times the writhe correction.

theorem TauCeti.MarkovBraid.jonesTrace_conj {R : Type u_1} [CommRing R] {n : ℕ} (a : Rˣ) (b c : BraidGroup (n + 1)) : { predStrands := n, braid := c * b * c⁻¹ }.jonesTrace a = { predStrands := n, braid := b }.jonesTrace a

Markov move I leaves the writhe-normalized trace unchanged, by the trace property.

theorem TauCeti.MarkovBraid.jonesTrace_stabilize {R : Type u_1} [CommRing R] {n : ℕ} (a : Rˣ) (b : BraidGroup (n + 1)) : { predStrands := n + 1, braid := BraidGroup.strandIncl b * BraidGroup.sigma (Fin.last n) }.jonesTrace a = { predStrands := n, braid := b }.jonesTrace a

Positive stabilization leaves the writhe-normalized trace unchanged. The new crossing multiplies the trace by -a ^ 3 and raises the exponent sum by one.

theorem TauCeti.MarkovBraid.jonesTrace_stabilizeInv {R : Type u_1} [CommRing R] {n : ℕ} (a : Rˣ) (b : BraidGroup (n + 1)) : { predStrands := n + 1, braid := BraidGroup.strandIncl b * (BraidGroup.sigma (Fin.last n))⁻¹ }.jonesTrace a = { predStrands := n, braid := b }.jonesTrace a

Negative stabilization leaves the writhe-normalized trace unchanged. The new crossing multiplies the trace by -a⁻¹ ^ 3 and lowers the exponent sum by one.

@[simp]

theorem TauCeti.MarkovBraid.jonesTrace_one_strand {R : Type u_1} [CommRing R] (a : Rˣ) (b : BraidGroup 1) : { predStrands := 0, braid := b }.jonesTrace a = TemperleyLieb.jonesDelta a

On one strand the only braid is trivial, and its closure, the unknot, has writhe-normalized trace δ.

theorem TauCeti.MarkovBraid.jonesTrace_sigma_pow_three {R : Type u_1} [CommRing R] (a : Rˣ) : { predStrands := 1, braid := BraidGroup.sigma 0 ^ 3 }.jonesTrace a = TemperleyLieb.jonesDelta a * (↑a⁻¹ ^ 4 + ↑a⁻¹ ^ 12 - ↑a⁻¹ ^ 16)

The trefoil. The closure of σ₀ ^ 3 on two strands is the right-handed trefoil, and its writhe-normalized trace is δ * (a⁻⁴ + a⁻¹² - a⁻¹⁶): δ times the writhe-normalized Kauffman bracket of the trefoil computed from a PD-code in TauCeti.normalizedKauffmanBracket_rightHandedTrefoilPDCode.

theorem TauCeti.IsMarkovMove.jonesTrace_eq {R : Type u_1} [CommRing R] {β γ : MarkovBraid} (h : IsMarkovMove β γ) (a : Rˣ) : β.jonesTrace a = γ.jonesTrace a

A single Markov move does not change the writhe-normalized trace.

theorem TauCeti.MarkovEquiv.jonesTrace_eq {R : Type u_1} [CommRing R] {β γ : MarkovBraid} (h : MarkovEquiv β γ) (a : Rˣ) : β.jonesTrace a = γ.jonesTrace a

The writhe-normalized Markov trace of the Jones representation is a Markov invariant. By Markov's theorem this makes it an invariant of the oriented link obtained by closing the braid.