Khovanov homology of crossing-free diagrams

A crossing-free oriented PD-code D : OrientedPDCode 0 is an unlink: a finite family of crossing-free circles. Its cube of resolutions has the single vertex ∅, whose resolution consists of exactly these circles, so the normalized Khovanov complex in quantum degree j is concentrated in cochain degree 0, where it is the degree-j piece of the circle tensor V^{⊗ k} of the k circles. This file computes the resulting Khovanov homology of the empty link, the unknots and the unlinks, as integral free modules and over every commutative coefficient ring:

• the homology vanishes outside cochain degree 0, and in cochain degree 0 it is the degree-j piece of the circle tensor of the resolved circles, of rank the coefficient of q ^ j in (q + q⁻¹) ^ k;
• the empty link has homology R in bidegree (0, 0) and zero elsewhere;
• a crossing-free unknot, with either orientation, has homology R in bidegrees (0, 1) and (0, -1) and zero elsewhere.

These are the base values of the Khovanov invariant: the empty link and the unknot normalize it, and the unlink of k components has graded rank (q + q⁻¹) ^ k.

Main definitions

• TauCeti.OrientedPDCode.emptyVertex: the only vertex ∅ of the cube of resolutions of a crossing-free diagram, as a state of cochain degree 0.
• TauCeti.OrientedPDCode.khovanovComplexXZeroIso: the cochain term in degree 0 of a crossing-free diagram is the degree-j piece of the circle tensor of its resolved circles.
• TauCeti.OrientedPDCode.khovanovComplexHomologyZeroIso: so is its homology in degree 0.
• TauCeti.OrientedPDCode.khovanovComplexHomologyEmptyIso: the homology of the empty diagram in bidegree (0, 0) is R.
• TauCeti.OrientedPDCode.khovanovComplexHomologyUnknotIso: the homology of a crossing-free unknot in bidegrees (0, ±1) is R.

Main results

• TauCeti.OrientedPDCode.isZero_homology_khovanovComplex_of_ne_zero: the homology of a crossing-free diagram vanishes outside cochain degree 0.
• TauCeti.OrientedPDCode.coeff_pow_eq_finrank_homology_khovanovComplex: the rank of its homology in bidegree (0, j) is the coefficient of q ^ j in (q + q⁻¹) ^ k for k circles.
• TauCeti.OrientedPDCode.isZero_homology_khovanovComplex_empty, TauCeti.OrientedPDCode.isZero_homology_khovanovComplex_unknot: the homology of the empty diagram and of the unknot vanishes in every other bidegree.

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).

theorem TauCeti.OrientedPDCode.resolutionCube_obj_empty (D : OrientedPDCode 0) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : (D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).obj ∅ = ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ∅))).piece ℤ j)

The only vertex of the cube of resolutions of a crossing-free diagram is the degree-j piece of the circle tensor of its resolved circles: with no crossings there is no quantum shift.

@[reducible, inline]

abbrev TauCeti.OrientedPDCode.emptyVertex (D : OrientedPDCode 0) : { S : Finset (Fin 0) // ↑S.card = 0 + ↑D.negativeCrossingCount }

The only vertex ∅ of the cube of resolutions of a crossing-free diagram, as a state of cochain degree 0.

theorem TauCeti.OrientedPDCode.isZero_khovanovComplex_X (D : OrientedPDCode 0) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (hi : i ≠ 0) : CategoryTheory.Limits.IsZero ((D.khovanovComplex hD R j).X i)

The Khovanov complex of a crossing-free diagram vanishes outside cochain degree 0.

noncomputable def TauCeti.OrientedPDCode.khovanovComplexXZeroIso (D : OrientedPDCode 0) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : (D.khovanovComplex hD R j).X 0 ≅ ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ∅))).piece ℤ j)

The cochain term in degree 0 of a crossing-free diagram is the degree-j piece of the circle tensor of its resolved circles, through the inclusion of its only cube vertex.

theorem TauCeti.OrientedPDCode.khovanovComplexXZeroIso_hom (D : OrientedPDCode 0) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : (D.khovanovComplexXZeroIso hD R j).hom = CategoryTheory.CategoryStruct.comp (D.khovanovComplexπ hD R j D.emptyVertex) (CategoryTheory.eqToHom ⋯)

The degree-0 term comparison is the projection onto the only cube vertex.

theorem TauCeti.OrientedPDCode.khovanovComplexXZeroIso_inv (D : OrientedPDCode 0) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : (D.khovanovComplexXZeroIso hD R j).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (D.khovanovComplexι hD R j D.emptyVertex)

The inverse degree-0 term comparison is the inclusion of the only cube vertex.

noncomputable def TauCeti.OrientedPDCode.khovanovComplexHomologyZeroIso (D : OrientedPDCode 0) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : HomologicalComplex.homology (D.khovanovComplex hD R j) 0 ≅ ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ∅))).piece ℤ j)

The Khovanov homology of a crossing-free diagram in cochain degree 0 and quantum degree j is the degree-j piece of the circle tensor of its resolved circles.

@[simp]

theorem TauCeti.OrientedPDCode.homologyπ_khovanovComplexHomologyZeroIso_hom (D : OrientedPDCode 0) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (D.khovanovComplex hD R j) 0) (D.khovanovComplexHomologyZeroIso hD R j).hom = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (D.khovanovComplex hD R j) 0) (D.khovanovComplexXZeroIso hD R j).hom

The homology of a crossing-free diagram is the cochain term itself: the comparison with the circle tensor is induced by the inclusion of the cocycles.

@[simp]

theorem TauCeti.OrientedPDCode.homologyπ_khovanovComplexHomologyZeroIso_hom_assoc (D : OrientedPDCode 0) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {Z : ModuleCat R} (h : ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ∅))).piece ℤ j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (D.khovanovComplex hD R j) 0) (CategoryTheory.CategoryStruct.comp (D.khovanovComplexHomologyZeroIso hD R j).hom h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (D.khovanovComplex hD R j) 0) (CategoryTheory.CategoryStruct.comp (D.khovanovComplexXZeroIso hD R j).hom h)

The homology of a crossing-free diagram is the cochain term itself: the comparison with the circle tensor is induced by the inclusion of the cocycles.

theorem TauCeti.OrientedPDCode.isZero_homology_khovanovComplex_of_ne_zero (D : OrientedPDCode 0) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (hi : i ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (D.khovanovComplex hD R j) i)

The Khovanov homology of a crossing-free diagram vanishes outside cochain degree 0.

instance TauCeti.OrientedPDCode.instFreeCarrierHomologyModuleCatIntKhovanovComplexOfNat (D : OrientedPDCode 0) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : Module.Free R ↑(HomologicalComplex.homology (D.khovanovComplex hD R j) 0)

The Khovanov homology of a crossing-free diagram is free.

instance TauCeti.OrientedPDCode.instFiniteCarrierHomologyModuleCatIntKhovanovComplexOfNat (D : OrientedPDCode 0) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : Module.Finite R ↑(HomologicalComplex.homology (D.khovanovComplex hD R j) 0)

The Khovanov homology of a crossing-free diagram is finitely generated.

theorem TauCeti.OrientedPDCode.isZero_homology_khovanovComplex_zero_of_labelingQuantumDegree_ne (D : OrientedPDCode 0) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) (h : ∀ (l : D.ResolvedCircle (PDCode.cubeState ∅) → Bool), Khovanov.labelingQuantumDegree (D.ResolvedCircle (PDCode.cubeState ∅)) l ≠ j) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (D.khovanovComplex hD R j) 0)

The Khovanov homology of a crossing-free diagram vanishes in bidegree (0, j) when no labelling of its resolved circles has quantum degree j.

theorem TauCeti.OrientedPDCode.coeff_pow_eq_finrank_homology_khovanovComplex (D : OrientedPDCode 0) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) [Nontrivial R] : ((LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) ^ D.crossinglessComponentCount).coeff j = ↑(Module.finrank R ↑(HomologicalComplex.homology (D.khovanovComplex hD R j) 0))

The graded rank of the Khovanov homology of an unlink: for a crossing-free diagram with k circles, the rank of the homology in bidegree (0, j) is the coefficient of q ^ j in (q + q⁻¹) ^ k.

noncomputable def TauCeti.OrientedPDCode.khovanovComplexHomologyEmptyIso (R : Type u) [CommRing R] (hD : empty.IsPlanar) : HomologicalComplex.homology (empty.khovanovComplex hD R 0) 0 ≅ ↧R

The Khovanov homology of the empty link in bidegree (0, 0) is R.

@[simp]

theorem TauCeti.OrientedPDCode.homologyπ_khovanovComplexHomologyEmptyIso_hom (R : Type u) [CommRing R] (hD : empty.IsPlanar) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (empty.khovanovComplex hD R 0) 0) (khovanovComplexHomologyEmptyIso R hD).hom = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (empty.khovanovComplex hD R 0) 0) (CategoryTheory.CategoryStruct.comp (empty.khovanovComplexXZeroIso hD R 0).hom (ModuleCat.ofHom (((Khovanov.circleBasis R (empty.ResolvedCircle (PDCode.cubeState ∅))).coord fun (x : empty.ResolvedCircle (PDCode.cubeState ∅)) => false) ∘ₗ ((Khovanov.circleQuantumGrading R (empty.ResolvedCircle (PDCode.cubeState ∅))).piece ℤ 0).subtype)))

The identification of the homology of the empty diagram with R reads off the coordinate of a cocycle along the empty labelling.

@[simp]

theorem TauCeti.OrientedPDCode.homologyπ_khovanovComplexHomologyEmptyIso_hom_assoc (R : Type u) [CommRing R] (hD : empty.IsPlanar) {Z : ModuleCat R} (h : ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (empty.khovanovComplex hD R 0) 0) (CategoryTheory.CategoryStruct.comp (khovanovComplexHomologyEmptyIso R hD).hom h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (empty.khovanovComplex hD R 0) 0) (CategoryTheory.CategoryStruct.comp (empty.khovanovComplexXZeroIso hD R 0).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (((Khovanov.circleBasis R (empty.ResolvedCircle (PDCode.cubeState ∅))).coord fun (x : empty.ResolvedCircle (PDCode.cubeState ∅)) => false) ∘ₗ ((Khovanov.circleQuantumGrading R (empty.ResolvedCircle (PDCode.cubeState ∅))).piece ℤ 0).subtype)) h))

The identification of the homology of the empty diagram with R reads off the coordinate of a cocycle along the empty labelling.

@[simp]

theorem TauCeti.OrientedPDCode.coe_khovanovComplexHomologyZeroIso_hom_khovanovComplexHomologyEmptyIso_inv (R : Type u) [CommRing R] (hD : empty.IsPlanar) (r : R) : ↑((CategoryTheory.ConcreteCategory.hom (empty.khovanovComplexHomologyZeroIso hD R 0).hom) ((CategoryTheory.ConcreteCategory.hom (khovanovComplexHomologyEmptyIso R hD).inv) r)) = r • (Khovanov.circleBasis R (empty.ResolvedCircle (PDCode.cubeState ∅))) fun (x : empty.ResolvedCircle (PDCode.cubeState ∅)) => false

The homology class corresponding to r : R in the homology of the empty diagram is the multiple r of the basis vector of the empty labelling.

theorem TauCeti.OrientedPDCode.isZero_homology_khovanovComplex_empty (R : Type u) [CommRing R] (hD : empty.IsPlanar) {i j : ℤ} (hij : i ≠ 0 ∨ j ≠ 0) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (empty.khovanovComplex hD R j) i)

The Khovanov homology of the empty link vanishes outside bidegree (0, 0).

noncomputable def TauCeti.OrientedPDCode.khovanovComplexHomologyUnknotIso (R : Type u) [CommRing R] (o : Bool) (hD : (unknot o).IsPlanar) {j : ℤ} (hj : j = 1 ∨ j = -1) : HomologicalComplex.homology ((unknot o).khovanovComplex hD R j) 0 ≅ ↧R

The Khovanov homology of the unknot in bidegrees (0, 1) and (0, -1) is R: the first is spanned by the labelling 1 of its circle and the second by the labelling X.

@[simp]

theorem TauCeti.OrientedPDCode.homologyπ_khovanovComplexHomologyUnknotIso_hom (R : Type u) [CommRing R] (o : Bool) (hD : (unknot o).IsPlanar) {j : ℤ} (hj : j = 1 ∨ j = -1) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ ((unknot o).khovanovComplex hD R j) 0) (khovanovComplexHomologyUnknotIso R o hD hj).hom = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles ((unknot o).khovanovComplex hD R j) 0) (CategoryTheory.CategoryStruct.comp ((unknot o).khovanovComplexXZeroIso hD R j).hom (ModuleCat.ofHom (((Khovanov.circleBasis R ((unknot o).ResolvedCircle (PDCode.cubeState ∅))).coord fun (x : (unknot o).ResolvedCircle (PDCode.cubeState ∅)) => decide (j = -1)) ∘ₗ ((Khovanov.circleQuantumGrading R ((unknot o).ResolvedCircle (PDCode.cubeState ∅))).piece ℤ j).subtype)))

The identification of the homology of the unknot in quantum degree j = ±1 with R reads off the coordinate of a cocycle along the labelling 1 (for j = 1) or X (for j = -1) of its circle.

@[simp]

theorem TauCeti.OrientedPDCode.homologyπ_khovanovComplexHomologyUnknotIso_hom_assoc (R : Type u) [CommRing R] (o : Bool) (hD : (unknot o).IsPlanar) {j : ℤ} (hj : j = 1 ∨ j = -1) {Z : ModuleCat R} (h : ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ ((unknot o).khovanovComplex hD R j) 0) (CategoryTheory.CategoryStruct.comp (khovanovComplexHomologyUnknotIso R o hD hj).hom h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles ((unknot o).khovanovComplex hD R j) 0) (CategoryTheory.CategoryStruct.comp ((unknot o).khovanovComplexXZeroIso hD R j).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (((Khovanov.circleBasis R ((unknot o).ResolvedCircle (PDCode.cubeState ∅))).coord fun (x : (unknot o).ResolvedCircle (PDCode.cubeState ∅)) => decide (j = -1)) ∘ₗ ((Khovanov.circleQuantumGrading R ((unknot o).ResolvedCircle (PDCode.cubeState ∅))).piece ℤ j).subtype)) h))

The identification of the homology of the unknot in quantum degree j = ±1 with R reads off the coordinate of a cocycle along the labelling 1 (for j = 1) or X (for j = -1) of its circle.

@[simp]

theorem TauCeti.OrientedPDCode.coe_khovanovComplexHomologyZeroIso_hom_khovanovComplexHomologyUnknotIso_inv (R : Type u) [CommRing R] (o : Bool) (hD : (unknot o).IsPlanar) {j : ℤ} (hj : j = 1 ∨ j = -1) (r : R) : ↑((CategoryTheory.ConcreteCategory.hom ((unknot o).khovanovComplexHomologyZeroIso hD R j).hom) ((CategoryTheory.ConcreteCategory.hom (khovanovComplexHomologyUnknotIso R o hD hj).inv) r)) = r • (Khovanov.circleBasis R ((unknot o).ResolvedCircle (PDCode.cubeState ∅))) fun (x : (unknot o).ResolvedCircle (PDCode.cubeState ∅)) => decide (j = -1)

The homology class corresponding to r : R in the homology of the unknot in quantum degree j = ±1 is the multiple r of the basis vector of the labelling 1 (for j = 1) or X (for j = -1) of its circle.

theorem TauCeti.OrientedPDCode.isZero_homology_khovanovComplex_unknot (R : Type u) [CommRing R] (o : Bool) (hD : (unknot o).IsPlanar) {i j : ℤ} (hij : i ≠ 0 ∨ j ≠ 1 ∧ j ≠ -1) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((unknot o).khovanovComplex hD R j) i)

The Khovanov homology of the unknot vanishes outside bidegrees (0, 1) and (0, -1).