Khovanov homology and its graded Euler characteristic

The Khovanov homology Khⁱʲ(D; R) of a planar oriented code D, defined in TauCeti.KnotTheory.Khovanov.Homology, is the cohomology in cochain degree i of the quantum component j of the normalized Khovanov complex TauCeti.OrientedPDCode.khovanovComplex. Its graded Euler characteristic is the Laurent polynomial

χ_q Kh(D; R) = ∑ⱼ (∑ᵢ (-1) ^ i rank Khⁱʲ(D; R)) qʲ,

with q = T (TauCeti.OrientedPDCode.khovanovEulerChar). Its coefficients are Mathlib's homology Euler characteristics HomologicalComplex.homologyEulerChar of the quantum components of the normalized Khovanov complex. Only finitely many of them are nonzero, because the bracket has finite quantum support.

Over a Noetherian ring with the rank-nullity property, such as ℤ or a field, the ranks are the ranks of finitely generated modules, the free ranks in the case of ℤ. Euler–Poincaré then computes each coefficient from the terms of the complex instead of its homology, and the normalized complex is a cochain shift of the bracket by n₋, so the coefficient of qʲ is the signed count of enhanced states of quantum degree j. In other words, χ_q Kh(D; R) is the enhanced state sum (TauCeti.OrientedPDCode.khovanovEulerChar_eq_enhancedStateSum). For a nonempty diagram this is Khovanov's theorem that the graded Euler characteristic is (q + q⁻¹) times the Jones polynomial at t ^ (1/2) = -q (TauCeti.OrientedPDCode.khovanovEulerChar_eq_mul_eval₂_jonesPolynomial). The empty diagram has graded Euler characteristic 1.

Main definitions

• TauCeti.OrientedPDCode.khovanovEulerChar D hD R: the graded Euler characteristic of the Khovanov homology of D with coefficients in R.

Main results

• TauCeti.OrientedPDCode.homologyEulerChar_khovanovComplex_eq_negOnePow_mul: normalization multiplies the bracket homology Euler characteristic by (-1)^n₋ and translates the quantum index.
• TauCeti.OrientedPDCode.coeff_khovanovEulerChar_eq_sum: each coefficient is the finite alternating sum of homology ranks over the cochain interval [-n₋, n₊].
• TauCeti.OrientedPDCode.homologyEulerChar_khovanovComplex: Euler–Poincaré for each quantum component, whose Euler characteristic is the coefficient of qʲ in the enhanced state sum.
• TauCeti.OrientedPDCode.khovanovEulerChar_eq_enhancedStateSum: χ_q Kh(D; R) is the enhanced state sum.
• TauCeti.OrientedPDCode.khovanovEulerChar_eq_mul_eval₂_jonesPolynomial: for a nonempty diagram, χ_q Kh(D; R) = (q + q⁻¹) J(D)|_{t ^ (1/2) = -q}.
• TauCeti.OrientedPDCode.khovanovEulerChar_empty: the empty diagram has χ_q Kh = 1.

References

• M. Khovanov, A categorification of the Jones polynomial, Duke Math. J. 101 (2000).
• D. Bar-Natan, On Khovanov's categorification of the Jones polynomial, Algebr. Geom. Topol. 2 (2002), §1.3 and §2.2.

theorem TauCeti.OrientedPDCode.homologyEulerChar_khovanovComplex_eq_negOnePow_mul {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : HomologicalComplex.homologyEulerChar (D.khovanovComplex hD R j) = ↑(↑D.negativeCrossingCount).negOnePow * HomologicalComplex.homologyEulerChar (D.khovanovBracket hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount))

Normalization multiplies the homology Euler characteristic by (-1)^n₋ and translates the quantum index. This is an equality of alternating ranks of actual cohomology modules.

theorem TauCeti.OrientedPDCode.eulerChar_khovanovComplex {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : HomologicalComplex.eulerChar (D.khovanovComplex hD R j) = ↑(↑D.negativeCrossingCount).negOnePow * HomologicalComplex.eulerChar (D.khovanovBracket hD R (j - (↑D.positiveCrossingCount - 2 * ↑D.negativeCrossingCount)))

The Euler characteristic of the terms of the quantum component j of the normalized Khovanov complex is (-1) ^ n₋ times that of the quantum component j - (n₊ - 2n₋) of the bracket.

theorem TauCeti.OrientedPDCode.finite_support_homologyEulerChar_khovanovComplex {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] [Nontrivial R] : (Function.support fun (j : ℤ) => HomologicalComplex.homologyEulerChar (D.khovanovComplex hD R j)).Finite

Only finitely many quantum components of the normalized Khovanov complex have a nonzero homology Euler characteristic.

noncomputable def TauCeti.OrientedPDCode.khovanovEulerChar {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] [Nontrivial R] : LaurentPolynomial ℤ

The graded Euler characteristic of Khovanov homology χ_q Kh(D; R) of a planar oriented code D: the Laurent polynomial in q = T whose coefficient of qʲ is the alternating sum ∑ᵢ (-1) ^ i rank Khⁱʲ(D; R), Mathlib's homology Euler characteristic of the quantum component j of the normalized Khovanov complex.

@[simp]

theorem TauCeti.OrientedPDCode.coeff_khovanovEulerChar {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] [Nontrivial R] (j : ℤ) : (D.khovanovEulerChar hD R).coeff j = HomologicalComplex.homologyEulerChar (D.khovanovComplex hD R j)

The coefficient of qʲ in the graded Euler characteristic of Khovanov homology is the homology Euler characteristic of the quantum component j of the normalized Khovanov complex.

theorem TauCeti.OrientedPDCode.coeff_khovanovEulerChar_eq_sum {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] [Nontrivial R] (j : ℤ) : (D.khovanovEulerChar hD R).coeff j = ∑ i ∈ Finset.Icc (-↑D.negativeCrossingCount) ↑D.positiveCrossingCount, ↑i.negOnePow * ↑(Module.finrank R ↑(D.khovanovHomology hD R i j))

The coefficient formula as an honest finite alternating sum of ranks of Khⁱʲ. Over a field these ranks are dimensions.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovEulerChar_empty (R : Type u) [CommRing R] [Nontrivial R] (h : empty.IsPlanar) : empty.khovanovEulerChar h R = 1

The empty diagram has graded Euler characteristic 1 over every nontrivial commutative ring.

theorem TauCeti.OrientedPDCode.homologyEulerChar_khovanovComplex {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] [IsNoetherianRing R] [HasRankNullity.{u, u} R] (j : ℤ) : HomologicalComplex.homologyEulerChar (D.khovanovComplex hD R j) = D.enhancedStateSum.coeff j

Euler–Poincaré for Khovanov homology: over a Noetherian ring with the rank-nullity property, such as ℤ or a field, the homology Euler characteristic of the quantum component j of the normalized Khovanov complex is the coefficient of qʲ in the enhanced state sum, the signed count of enhanced states of quantum degree j.

theorem TauCeti.OrientedPDCode.khovanovEulerChar_eq_enhancedStateSum {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] [IsNoetherianRing R] [HasRankNullity.{u, u} R] : D.khovanovEulerChar hD R = D.enhancedStateSum

The graded Euler characteristic of Khovanov homology is the enhanced state sum, over a Noetherian ring with the rank-nullity property, such as ℤ or a field.

theorem TauCeti.OrientedPDCode.khovanovEulerChar_eq_mul_eval₂_jonesPolynomial {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] [IsNoetherianRing R] [HasRankNullity.{u, u} R] (h : 0 < D.componentCount) : D.khovanovEulerChar hD R = (LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) * (LaurentPolynomial.eval₂ (Int.castRingHom (LaurentPolynomial ℤ)) (-LaurentPolynomial.genericUnit ℤ)) D.jonesPolynomial

Khovanov's theorem: the graded Euler characteristic of the Khovanov homology of a nonempty planar oriented code is (q + q⁻¹) times its Jones polynomial at t ^ (1/2) = -q, over a Noetherian ring with the rank-nullity property, such as ℤ or a field. The hypothesis 0 < componentCount says that the diagram is nonempty; the empty diagram has graded Euler characteristic 1 (TauCeti.OrientedPDCode.khovanovEulerChar_empty).