The HOMFLY polynomial with unknot value one

The unreduced HOMFLY polynomial of a nonempty braid closure is divisible by the quantum dimension (a - a⁻¹) / z. Its quotient, TauCeti.MarkovBraid.reducedHomfly, is a Laurent polynomial with unknot value one. It is invariant under Markov equivalence and satisfies a P(L₊) - a⁻¹ P(L₋) = z P(L₀). Adding an uncrossed strand multiplies it by the quantum dimension, so the unlink on n + 1 components has value ((a - a⁻¹) / z) ^ n.

The quotient is constructed in the Laurent polynomial ring, without inverting the quantum dimension or requiring its specializations to be nonzero. It is characterized by multiplication by that dimension; its positive-rank sl_N specializations recover the existing reduced Jimbo traces.

The divisibility comes from the same Hecke spanning argument as the unreduced interpolation, with its submodule restricted to polynomials divisible by the unknot value. No choice of a component of a link is needed. The presentation is a braid closure; no classification of geometric knots by Markov equivalence is asserted.

References

• V. F. R. Jones, Hecke algebra representations of braid groups and link polynomials, Ann. of Math. 126 (1987), 335–388, Sections 4–6.
• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 3.

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

The classical HOMFLY polynomial of a braid closure, normalized to have unknot value one. It is the Laurent polynomial quotient of homfly by (a - a⁻¹) / z.

@[simp]

theorem TauCeti.MarkovBraid.homflyUnknot_mul_reducedHomfly (K : Type u_1) [Field K] (β : MarkovBraid) : KnotTheory.homflyUnknot K * reducedHomfly K β = homfly K β

Multiplying the reduced HOMFLY polynomial by the quantum dimension recovers the unreduced polynomial.

theorem TauCeti.MarkovBraid.reducedHomfly_eq_iff (K : Type u_1) [Field K] {β : MarkovBraid} {P : LaurentPolynomial (LaurentPolynomial K)} : reducedHomfly K β = P ↔ KnotTheory.homflyUnknot K * P = homfly K β

A Laurent polynomial is the reduced HOMFLY polynomial exactly when multiplying it by the unknot value gives the unreduced polynomial.

@[simp]

theorem TauCeti.MarkovBraid.homflySpecialization_reducedHomfly (K : Type u_1) [Field K] (β : MarkovBraid) (N : ℕ) : (KnotTheory.homflySpecialization K (N + 1)) (reducedHomfly K β) = β.jimboReducedTrace (Units.mk0 RatFunc.X ⋯)

Every positive-rank sl_N specialization of the reduced HOMFLY polynomial is the reduced Jimbo trace at the rational-function variable.

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

The positive-rank reduced Jimbo specializations uniquely characterize the reduced HOMFLY polynomial.

@[simp]

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

The reduced HOMFLY polynomial of the unlink on n + 1 components. In particular, the one-strand unknot has value one.

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

The reduced HOMFLY polynomial satisfies the oriented skein relation in every braid context, with the same parameters as the unreduced polynomial.

@[simp]

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

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

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

Markov-equivalent braids have the same classical, unknot-normalized HOMFLY polynomial.

@[simp]

theorem TauCeti.MarkovBraid.reducedHomfly_sigma (K : Type u_1) [Field K] : reducedHomfly K { predStrands := 1, braid := BraidGroup.sigma 0 } = 1

The single positive crossing on two strands closes to the unknot.

theorem TauCeti.MarkovBraid.reducedHomfly_sigma_pow_two (K : Type u_1) [Field K] : reducedHomfly K { predStrands := 1, braid := BraidGroup.sigma 0 ^ 2 } = LaurentPolynomial.T (-1) * LaurentPolynomial.C (LaurentPolynomial.T 1) + LaurentPolynomial.T (-2) * KnotTheory.homflyUnknot K

The positive Hopf link, presented by the square of the two-strand generator.

theorem TauCeti.MarkovBraid.reducedHomfly_sigma_pow_three (K : Type u_1) [Field K] : reducedHomfly K { predStrands := 1, braid := BraidGroup.sigma 0 ^ 3 } = LaurentPolynomial.T (-2) * LaurentPolynomial.C (LaurentPolynomial.T 2) + 2 * LaurentPolynomial.T (-2) - LaurentPolynomial.T (-4)

The HOMFLY polynomial of the right-handed trefoil, presented by the cube of the positive two-strand generator, is a⁻² z² + 2 a⁻² - a⁻⁴.