Existence of the HOMFLY polynomial

For every braid, the weighted traces of the Jimbo representations with N colours, for all N, are the specializations a = q ^ N, z = q - q⁻¹ of a single two-variable Laurent polynomial (TauCeti.KnotTheory.exists_homflySpecialization_eq_jimboWeightedTrace). Writhe normalization then gives the HOMFLY polynomial of a braid closure, TauCeti.MarkovBraid.homfly, as an element of K[a, a⁻¹, z, z⁻¹], represented as in TauCeti.KnotTheory.homflySpecialization with z the inner and a the outer Laurent variable. It is characterized by its sl_N specializations, which are the writhe-normalized Jimbo traces TauCeti.MarkovBraid.jimboTrace; it is invariant under Markov equivalence and satisfies the oriented HOMFLY skein relation a P(L₊) - a⁻¹ P(L₋) = z P(L₀).

The normalization is the unreduced one inherited from the Jimbo traces: the one-strand unknot has value (a - a⁻¹) z⁻¹ (TauCeti.KnotTheory.homflyUnknot), the quantum dimension, rather than one. Every interpolating polynomial constructed here is divisible by this value; the quotient normalization is developed in TauCeti.KnotTheory.Homfly.Reduced.

The existence proof is Jones's trace argument. Modulo the Hecke skein relation, every braid on n + 2 strands is a combination of braids ι b and ι b * σ * ι c, where ι adds an uncrossed strand and σ is the last elementary braid (TauCeti.BraidGroup.strandSpan_sup_heckeSkein_eq_top). The weighted traces kill the Hecke skein relators, multiply by the quantum dimension under ι, and send ι b * σ * ι c to q ^ N times the trace of c * b. Every coefficient arising this way is the specialization of a fixed two-variable Laurent polynomial, so induction on the number of strands produces the interpolating polynomial. Uniqueness is TauCeti.KnotTheory.homflySpecialization_jointly_injective.

Main definitions

• TauCeti.KnotTheory.homflyUnknot K: the unknot value (a - a⁻¹) z⁻¹.
• TauCeti.MarkovBraid.homfly K β: the HOMFLY polynomial of the closure of β.

Main results

• TauCeti.KnotTheory.exists_homflySpecialization_eq_jimboWeightedTrace: the weighted Jimbo traces of a braid interpolate to a two-variable Laurent polynomial.
• TauCeti.MarkovBraid.homflySpecialization_homfly and TauCeti.MarkovBraid.homfly_eq_of_homflySpecialization_eq: the HOMFLY polynomial is the unique Laurent polynomial specializing to the normalized Jimbo traces.
• TauCeti.MarkovEquiv.homfly_eq: Markov-equivalent braids have the same HOMFLY polynomial.
• TauCeti.MarkovBraid.homfly_skein and TauCeti.MarkovBraid.homfly_one: the skein relation and the values on trivial braids.

References

• P. Freyd, D. Yetter, J. Hoste, W. B. R. Lickorish, K. Millett, A. Ocneanu, A new polynomial invariant of knots and links, Bull. Amer. Math. Soc. 12 (1985), 239–246.
• V. F. R. Jones, Hecke algebra representations of braid groups and link polynomials, Ann. of Math. 126 (1987), 335–388, Sections 4–6 (the trace construction of HOMFLY).
• V. G. Turaev, The Yang-Baxter equation and invariants of links, Invent. Math. 92 (1988), 527–553 (the sl_N specializations as enhanced Jimbo traces).

noncomputable def TauCeti.KnotTheory.homflyUnknot (K : Type u_1) [Field K] : LaurentPolynomial (LaurentPolynomial K)

The value (a - a⁻¹) z⁻¹ of the unreduced HOMFLY polynomial on the unknot, in K[a, a⁻¹, z, z⁻¹] with z the inner and a the outer Laurent variable. Its sl_N specialization is the quantum dimension [N]_q.

theorem TauCeti.KnotTheory.homflyUnknot_def (K : Type u_1) [Field K] : homflyUnknot K = (LaurentPolynomial.T 1 - LaurentPolynomial.T (-1)) * LaurentPolynomial.C (LaurentPolynomial.T (-1))

The defining formula of the unknot value.

@[simp]

theorem TauCeti.KnotTheory.homflySpecialization_homflyUnknot {K : Type u_1} [Field K] (N : ℕ) : (homflySpecialization K N) (homflyUnknot K) = ∑ a : Fin N, jimboWeight (Units.mk0 RatFunc.X ⋯) a

The unknot value specializes to the quantum dimension, the sum of the enhancement weights.

theorem TauCeti.KnotTheory.jimboWeight_sum_X_ne_zero {K : Type u_1} [Field K] (N : ℕ) : ∑ a : Fin (N + 1), jimboWeight (Units.mk0 RatFunc.X ⋯) a ≠ 0

The positive-rank quantum dimension at the rational-function variable is nonzero, in every characteristic.

@[simp]

theorem TauCeti.KnotTheory.homflyUnknot_ne_zero (K : Type u_2) [Field K] : homflyUnknot K ≠ 0

The unreduced unknot value is a nonzero Laurent polynomial, in every characteristic.

Interpolating the weighted traces

theorem TauCeti.KnotTheory.exists_homflySpecialization_eq_jimboWeightedTrace {K : Type u_1} [Field K] {n : ℕ} (b : BraidGroup (n + 1)) : ∃ (P : LaurentPolynomial (LaurentPolynomial K)), homflyUnknot K ∣ P ∧ ∀ (N : ℕ), (homflySpecialization K N) P = jimboWeightedTrace (Units.mk0 RatFunc.X ⋯) b

The weighted Jimbo traces interpolate. For every braid there is a two-variable Laurent polynomial whose specialization a = q ^ N, z = q - q⁻¹ is the weighted trace of the braid in the Jimbo representation with N colours, for every N. The polynomial is divisible by the unknot value, so dividing by that value still gives a Laurent polynomial.

The HOMFLY polynomial of a braid closure

noncomputable def TauCeti.MarkovBraid.homfly (K : Type u_1) [Field K] (β : MarkovBraid) : LaurentPolynomial (LaurentPolynomial K)

The HOMFLY polynomial of the closure of a braid, in K[a, a⁻¹, z, z⁻¹] with z the inner and a the outer Laurent variable. It is the writhe normalization a ^ (-e), for exponent sum e, of the interpolation of the weighted Jimbo traces, so its sl_N specializations are the normalized Jimbo traces (homflySpecialization_homfly), which determine it. The unknot has value (a - a⁻¹) z⁻¹.

theorem TauCeti.MarkovBraid.homflyUnknot_dvd_homfly (K : Type u_1) [Field K] (β : MarkovBraid) : KnotTheory.homflyUnknot K ∣ homfly K β

The unreduced HOMFLY polynomial of every nonempty braid closure is divisible by its unknot value.

@[simp]

theorem TauCeti.MarkovBraid.homflySpecialization_homfly (K : Type u_1) [Field K] (β : MarkovBraid) (N : ℕ) : (KnotTheory.homflySpecialization K N) (homfly K β) = β.jimboTrace (Units.mk0 RatFunc.X ⋯)

The sl_N specializations of the HOMFLY polynomial are the writhe-normalized Jimbo traces with N colours at q = X.

theorem TauCeti.MarkovBraid.homfly_eq_of_homflySpecialization_eq (K : Type u_1) [Field K] {β : MarkovBraid} {P : LaurentPolynomial (LaurentPolynomial K)} (h : ∀ (N : ℕ), (KnotTheory.homflySpecialization K (N + 1)) P = β.jimboTrace (Units.mk0 RatFunc.X ⋯)) : homfly K β = P

Uniqueness of the HOMFLY polynomial: a two-variable Laurent polynomial whose positive-rank specializations are the normalized Jimbo traces of a braid is its HOMFLY polynomial.

@[simp]

theorem TauCeti.MarkovBraid.homfly_one (K : Type u_1) [Field K] (n : ℕ) : homfly K { predStrands := n, braid := 1 } = KnotTheory.homflyUnknot K ^ (n + 1)

The HOMFLY polynomial of the trivial braid on n + 1 strands, whose closure is the (n + 1)-component unlink.

@[simp]

theorem TauCeti.MarkovBraid.homfly_strandIncl (K : Type u_1) [Field K] {n : ℕ} (b : BraidGroup (n + 1)) : homfly K { predStrands := n + 1, braid := BraidGroup.strandIncl b } = KnotTheory.homflyUnknot K * homfly K { predStrands := n, braid := b }

Adding an uncrossed strand multiplies the unreduced HOMFLY polynomial by the unknot value, as expected for disjoint union with an unknot.

theorem TauCeti.MarkovBraid.homfly_skein (K : Type u_1) [Field K] {n : ℕ} (b c : BraidGroup (n + 1)) (i : Fin n) : LaurentPolynomial.T 1 * homfly K { predStrands := n, braid := b * BraidGroup.sigma i * c } - LaurentPolynomial.T (-1) * homfly K { predStrands := n, braid := b * (BraidGroup.sigma i)⁻¹ * c } = LaurentPolynomial.C (LaurentPolynomial.T 1) * homfly K { predStrands := n, braid := b * c }

The HOMFLY skein relation a P(L₊) - a⁻¹ P(L₋) = z P(L₀), for a crossing in any braid context.

theorem TauCeti.MarkovEquiv.homfly_eq (K : Type u_1) [Field K] {β γ : MarkovBraid} (h : MarkovEquiv β γ) : MarkovBraid.homfly K β = MarkovBraid.homfly K γ

The HOMFLY polynomial is a link invariant on braid closures: Markov-equivalent braids have the same HOMFLY polynomial.