The Jones polynomial of an oriented PD-code

Lickorish defines the Jones polynomial of an oriented link diagram D from its Kauffman bracket: V(D) is the writhe-normalized bracket (-A)^(-3 w(D)) ⟨D⟩ rewritten in t^(1/2) = A⁻². It is a Laurent polynomial in t^(1/2) with integer coefficients. This file defines it for oriented PD-codes, as TauCeti.OrientedPDCode.jonesPolynomial, with the generator T of ℤ[T;T⁻¹] standing for t^(1/2).

The substitution is possible because every power of A in the normalized bracket is even. Crossing by crossing, a positive crossing contributes A * (-A⁻³) = -t^(1/2) to a state that smooths it by A and A⁻¹ * (-A⁻³) = -t to one that smooths it by A⁻¹. A negative crossing contributes -t⁻¹ and -t^(-1/2) instead. The loop value -(A² + A⁻²) becomes -(t^(1/2) + t^(-1/2)). So the Jones polynomial is the state sum TauCeti.OrientedPDCode.jonesPolynomial with these weights, and evaluating it at t^(1/2) = A⁻² recovers the normalized bracket over every commutative ring (TauCeti.OrientedPDCode.eval₂_jonesPolynomial). The substitution T ↦ T⁻² is injective on ℤ[T;T⁻¹], so two codes have the same Jones polynomial exactly when they have the same normalized bracket (TauCeti.OrientedPDCode.jonesPolynomial_eq_jonesPolynomial_iff). Every invariance property of the normalized bracket is therefore one of the Jones polynomial.

In particular the Jones polynomial is unchanged by the first Reidemeister move, by clasp insertion, which along a common face is the second Reidemeister move, by the second-move clasps involving crossing-free circles, and by the third Reidemeister move. These are the local moves behind its invariance for oriented links (Lickorish, Theorem 3.5). Reversing the orientation of every component leaves the Jones polynomial unchanged, and mirroring substitutes t⁻¹ for t. The unknot has Jones polynomial 1, and the right-handed trefoil has t + t³ - t⁴.

Main definitions

• TauCeti.OrientedPDCode.jonesStateWeight: the weight of a state in the Jones state sum.
• TauCeti.OrientedPDCode.jonesPolynomial: the Jones polynomial of an oriented PD-code.

Main results

• TauCeti.OrientedPDCode.eval₂_jonesPolynomial: at t^(1/2) = A⁻² the Jones polynomial is the writhe-normalized Kauffman bracket.
• TauCeti.OrientedPDCode.jonesPolynomial_eq_jonesPolynomial_iff: two codes have the same Jones polynomial exactly when they have the same normalized bracket.
• TauCeti.OrientedPDCode.jonesPolynomial_reidemeisterOne, TauCeti.OrientedPDCode.jonesPolynomial_insertClasp and TauCeti.OrientedPDCode.jonesPolynomial_reidemeisterThree: invariance under the first Reidemeister move, under clasp insertion and under the third Reidemeister move.
• TauCeti.OrientedPDCode.jonesPolynomial_mirror, TauCeti.OrientedPDCode.jonesPolynomial_reverse, TauCeti.OrientedPDCode.jonesPolynomial_relabel and TauCeti.OrientedPDCode.jonesPolynomial_rotateCrossing: behaviour under reflection, reversal, relabelling and reading a crossing from another slot.
• TauCeti.OrientedPDCode.jonesPolynomial_eq_pow: a code with no crossings and c circles has Jones polynomial (-(t^(1/2) + t^(-1/2))) ^ (c - 1), and TauCeti.OrientedPDCode.jonesPolynomial_unknot: the unknot has Jones polynomial 1.
• TauCeti.jonesPolynomial_rightHandedTrefoilPDCode: the right-handed trefoil has Jones polynomial t + t³ - t⁴.

References

• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 3, Theorem 3.5 and Definition 3.6.
• V. F. R. Jones, A polynomial invariant for knots via von Neumann algebras, Bull. Amer. Math. Soc. 12 (1985), 103-111.

noncomputable def TauCeti.OrientedPDCode.jonesStateWeight {n : ℕ} (D : OrientedPDCode n) (s : Fin n → Bool) : LaurentPolynomial ℤ

The weight of a state s in the Jones state sum, a signed power of t^(1/2) = T: each positive crossing contributes -t^(1/2) when s smooths it by A and -t when by A⁻¹, and each negative crossing contributes -t⁻¹ and -t^(-1/2) respectively. These are the factors A^(±1) * (-A³)^(-ε) of the writhe-normalized bracket at a crossing of sign ε, rewritten in t^(1/2) = A⁻².

Equations

• D.jonesStateWeight s = ∏ i : Fin n, -LaurentPolynomial.T (if D.crossingSign i = 1 then bif s i then 1 else 2 else bif s i then -2 else -1)

theorem TauCeti.OrientedPDCode.jonesStateWeight_def {n : ℕ} (D : OrientedPDCode n) (s : Fin n → Bool) : D.jonesStateWeight s = ∏ i : Fin n, -LaurentPolynomial.T (if D.crossingSign i = 1 then bif s i then 1 else 2 else bif s i then -2 else -1)

The defining product of the Jones weight of a state.

noncomputable def TauCeti.OrientedPDCode.jonesPolynomial {n : ℕ} (D : OrientedPDCode n) : LaurentPolynomial ℤ

The Jones polynomial of an oriented PD-code, as a Laurent polynomial in t^(1/2) = T with integer coefficients: the sum over all states of the Jones weight of the state times the loop value -(t^(1/2) + t^(-1/2)) raised to one less than the number of circles of the smoothed diagram. It is Lickorish's V(D), the writhe-normalized Kauffman bracket at t^(1/2) = A⁻² (TauCeti.OrientedPDCode.eval₂_jonesPolynomial). As for the bracket, the exponent is truncated subtraction, so the empty code has Jones polynomial 1.

Equations

• D.jonesPolynomial = ∑ s : Fin n → Bool, D.jonesStateWeight s * (-(LaurentPolynomial.T 1 + LaurentPolynomial.T (-1))) ^ (D.stateLoopCount s - 1)

theorem TauCeti.OrientedPDCode.jonesPolynomial_def {n : ℕ} (D : OrientedPDCode n) : D.jonesPolynomial = ∑ s : Fin n → Bool, D.jonesStateWeight s * (-(LaurentPolynomial.T 1 + LaurentPolynomial.T (-1))) ^ (D.stateLoopCount s - 1)

The defining state-sum equation of the Jones polynomial.

theorem TauCeti.OrientedPDCode.eval₂_jonesPolynomial {n : ℕ} {R : Type u_1} [CommRing R] (D : OrientedPDCode n) (a : Rˣ) : (LaurentPolynomial.eval₂ (Int.castRingHom R) (a⁻¹ ^ 2)) D.jonesPolynomial = D.normalizedKauffmanBracket a

The Jones polynomial is the normalized Kauffman bracket at t^(1/2) = A⁻². Evaluating TauCeti.OrientedPDCode.jonesPolynomial at the square of a⁻¹ gives the writhe-normalized bracket at a, over every commutative ring. This is Lickorish's definition of the Jones polynomial.

theorem TauCeti.OrientedPDCode.jonesPolynomial_eq_jonesPolynomial_iff {n m : ℕ} (D : OrientedPDCode n) (D' : OrientedPDCode m) : D.jonesPolynomial = D'.jonesPolynomial ↔ D.normalizedKauffmanBracket ⋯.unit = D'.normalizedKauffmanBracket ⋯.unit

The Jones polynomial carries exactly the information of the normalized bracket: two oriented PD-codes have the same Jones polynomial exactly when they have the same writhe-normalized Kauffman bracket over ℤ[A, A⁻¹]. Every invariance statement for the normalized bracket is therefore one for the Jones polynomial.

@[simp]

theorem TauCeti.OrientedPDCode.jonesPolynomial_reidemeisterOne {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) : (D.reidemeisterOne h b).jonesPolynomial = D.jonesPolynomial

The first Reidemeister move leaves the Jones polynomial unchanged.

@[simp]

theorem TauCeti.OrientedPDCode.jonesPolynomial_adjoinKink {n : ℕ} (D : OrientedPDCode n) (o b : Bool) : (D.adjoinKink o b).jonesPolynomial = (D.adjoinCircle o).jonesPolynomial

The Jones polynomial is invariant under the first Reidemeister move on an isolated circle, including a circle in an otherwise empty diagram.

@[simp]

theorem TauCeti.OrientedPDCode.jonesPolynomial_insertClasp {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) : (D.insertClasp p q b hqp hqe).jonesPolynomial = D.jonesPolynomial

Clasp insertion leaves the Jones polynomial unchanged. Along a common face of the two arcs this is the second Reidemeister move.

@[simp]

theorem TauCeti.OrientedPDCode.jonesPolynomial_insertCircleClasp {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) : (D.insertCircleClasp p o b).jonesPolynomial = (D.adjoinCircle o).jonesPolynomial

The Jones polynomial is invariant under the circle-and-arc second Reidemeister move.

@[simp]

theorem TauCeti.OrientedPDCode.jonesPolynomial_adjoinTwoCircleClasp {n : ℕ} (D : OrientedPDCode n) (o₁ o₂ b : Bool) : (D.adjoinTwoCircleClasp o₁ o₂ b).jonesPolynomial = ((D.adjoinCircle o₁).adjoinCircle o₂).jonesPolynomial

The Jones polynomial is unchanged by the two-circle second Reidemeister move.

@[simp]

theorem TauCeti.OrientedPDCode.jonesPolynomial_reidemeisterThree {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) (h : D.HasReidemeisterThreeTriangle c) : (D.reidemeisterThree c).jonesPolynomial = D.jonesPolynomial

The third Reidemeister move leaves the Jones polynomial unchanged, for every surrounding diagram and all six height orders of the three strands.

@[simp]

theorem TauCeti.OrientedPDCode.jonesPolynomial_adjoinCircle {n : ℕ} (D : OrientedPDCode n) (orientation : Bool) (h : 0 < D.componentCount) : (D.adjoinCircle orientation).jonesPolynomial = -(LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) * D.jonesPolynomial

Adjoining a crossing-free circle to a nonempty oriented diagram multiplies its Jones polynomial by the loop value -(t^(1/2) + t^(-1/2)).

@[simp]

theorem TauCeti.OrientedPDCode.jonesPolynomial_mirror {n : ℕ} (D : OrientedPDCode n) : D.mirror.jonesPolynomial = LaurentPolynomial.invert D.jonesPolynomial

Reflection substitutes t⁻¹ for t in the Jones polynomial.

@[simp]

theorem TauCeti.OrientedPDCode.jonesPolynomial_reverse {n : ℕ} (D : OrientedPDCode n) : D.reverse.jonesPolynomial = D.jonesPolynomial

Reversing the orientation of every component leaves the Jones polynomial unchanged.

@[simp]

theorem TauCeti.OrientedPDCode.jonesPolynomial_relabel {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).jonesPolynomial = D.jonesPolynomial

The Jones polynomial depends on an oriented PD-code only through its relabelling class.

@[simp]

theorem TauCeti.OrientedPDCode.jonesPolynomial_rotateCrossing {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : (D.rotateCrossing i).jonesPolynomial = D.jonesPolynomial

Reading a crossing from another slot leaves the Jones polynomial unchanged.

theorem TauCeti.OrientedPDCode.jonesPolynomial_eq_pow (D : OrientedPDCode 0) : D.jonesPolynomial = (-(LaurentPolynomial.T 1 + LaurentPolynomial.T (-1))) ^ (D.crossinglessComponentCount - 1)

A code with no crossings and c crossing-free circles has Jones polynomial (-(t^(1/2) + t^(-1/2))) ^ (c - 1), the counterpart of TauCeti.PDCode.kauffmanBracket_eq_jonesDelta_pow.

@[simp]

theorem TauCeti.OrientedPDCode.jonesPolynomial_unknot (orientation : Bool) : (unknot orientation).jonesPolynomial = 1

The unknot has Jones polynomial 1.

@[simp]

theorem TauCeti.OrientedPDCode.jonesPolynomial_adjoinKink_empty (o b : Bool) : (empty.adjoinKink o b).jonesPolynomial = 1

An isolated kink in an otherwise empty diagram has Jones polynomial one, for either orientation and either crossing sign.

@[simp]

theorem TauCeti.jonesPolynomial_rightHandedTrefoilPDCode : rightHandedTrefoilPDCode.jonesPolynomial = LaurentPolynomial.T 2 + LaurentPolynomial.T 6 - LaurentPolynomial.T 8

The Jones polynomial of the right-handed trefoil is t + t³ - t⁴, written in t^(1/2) = T. This pins the convention: Lickorish's V(D) with t^(1/2) = A⁻².