Uniqueness from the HOMFLY specializations

The substitutions a = q ^ N and z = q - q⁻¹, for positive integers N, jointly detect two-variable Laurent polynomials over any field. These are the substitutions relating HOMFLY to its sl_N specializations, as obtained from enhanced Jimbo traces. Thus, if a two-variable Laurent polynomial realizing the specializations exists, it is unique. This file proves uniqueness, without asserting the existence of that polynomial.

We represent K[a, a⁻¹, z, z⁻¹] by LaurentPolynomial (LaurentPolynomial K), with z the inner variable and a the outer variable. Values lie in RatFunc K, where q is RatFunc.X. Using rational functions permits negative powers of z; q - q⁻¹ is transcendental and hence nonzero. No characteristic restriction is needed. In fact, any infinite set of ranks suffices for uniqueness.

References

• V. F. R. Jones, Hecke algebra representations of braid groups and link polynomials, Ann. of Math. 126 (1987), 335–388 (the HOMFLY specialization of braid traces).
• V. G. Turaev, The Yang-Baxter equation and invariants of links, Invent. Math. 92 (1988), 527–553 (enhanced representations).

noncomputable def TauCeti.KnotTheory.homflySpecialization (K : Type u_1) [Field K] (N : ℕ) : LaurentPolynomial (LaurentPolynomial K) →+* RatFunc K

The HOMFLY substitution a ↦ q ^ N, z ↦ q - q⁻¹ into K(q). The inner Laurent variable is z and the outer one is a.

theorem TauCeti.KnotTheory.homflySpecialization_def (K : Type u_1) [Field K] (N : ℕ) (p : LaurentPolynomial (LaurentPolynomial K)) : (homflySpecialization K N) p = (LaurentPolynomial.eval₂ (LaurentPolynomial.eval₂ (algebraMap K (RatFunc K)) (Units.mk0 (RatFunc.X - RatFunc.X⁻¹) ⋯)) (Units.mk0 RatFunc.X ⋯ ^ N)) p

The defining equation of the two-variable HOMFLY substitution.

@[simp]

theorem TauCeti.KnotTheory.homflySpecialization_C (K : Type u_1) [Field K] (N : ℕ) (p : LaurentPolynomial K) : (homflySpecialization K N) (LaurentPolynomial.C p) = (LaurentPolynomial.eval₂ (algebraMap K (RatFunc K)) (Units.mk0 (RatFunc.X - RatFunc.X⁻¹) ⋯)) p

The constant coefficient polynomial is evaluated at z = q - q⁻¹.

@[simp]

theorem TauCeti.KnotTheory.homflySpecialization_T (K : Type u_1) [Field K] (N : ℕ) (i : ℤ) : (homflySpecialization K N) (LaurentPolynomial.T i) = RatFunc.X ^ (↑N * i)

The outer Laurent variable is evaluated at a = q ^ N.

theorem TauCeti.KnotTheory.homflySpecialization_injective_of_infinite (K : Type u_1) [Field K] {s : Set ℕ} (hs : s.Infinite) : Function.Injective fun (p : LaurentPolynomial (LaurentPolynomial K)) (N : ↑s) => (homflySpecialization K ↑N) p

An infinite set of HOMFLY ranks detects two-variable Laurent polynomials.

theorem TauCeti.KnotTheory.homflySpecialization_jointly_injective (K : Type u_1) [Field K] : Function.Injective fun (p : LaurentPolynomial (LaurentPolynomial K)) (N : ℕ) => (homflySpecialization K (N + 1)) p

All positive-rank specializations jointly detect two-variable Laurent polynomials. Rank zero is not needed.