Quantum-component Khovanov cohomology #

The homology of each quantum component of the normalized complex defines TauCeti.OrientedPDCode.khovanovHomology. The normalized complex has finite free terms over every commutative ring, and its homology is finitely generated over a Noetherian ring (in particular over the integers), hence finite-dimensional over a field. Both gradings have finite support, uniformly in the coefficient ring, including the zero ring and the empty diagram.

khovanovHomologyBracketIso compares the normalized groups with bracket homology at the translated bidegree. It uses the signed native-shift comparison, not an unsigned identification of differentials. No Reidemeister invariance is asserted here.

References #

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

source

@[reducible, inline]

noncomputable abbrev TauCeti.OrientedPDCode.khovanovHomology {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (i j : ℤ) :

ModuleCat R

Khovanov homology Khⁱʲ(D; R) of a planar oriented code D: the cohomology in cochain degree i of the quantum component j of the normalized Khovanov complex.

Instances For

source

theorem TauCeti.OrientedPDCode.khovanovHomology_def {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (i j : ℤ) :

D.khovanovHomology hD R i j = HomologicalComplex.homology (D.khovanovComplex hD R j) i

Khovanov homology in bidegree (i, j) is the cohomology in degree i of the quantum component j of the normalized Khovanov complex.

source

noncomputable def TauCeti.OrientedPDCode.khovanovHomologyBracketIso {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (i j : ℤ) :

D.khovanovHomology hD R i j ≅ HomologicalComplex.homology (D.khovanovBracket hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)) (i + ↑D.negativeCrossingCount)

Khⁱʲ(D; R) is isomorphic to bracket homology in cochain degree i + n₋ and quantum degree j - n₊ + 2n₋. The comparison retains the degreewise sign in khovanovComplexShiftIso.

Instances For

source

instance TauCeti.OrientedPDCode.instFreeCarrierXIntModuleCatKhovanovComplex {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (i j : ℤ) :

Module.Free R ↑((D.khovanovComplex hD R j).X i)

Every term of the normalized complex is free, without a nontriviality assumption on R.

source

instance TauCeti.OrientedPDCode.instFiniteCarrierXIntModuleCatKhovanovComplex {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (i j : ℤ) :

Module.Finite R ↑((D.khovanovComplex hD R j).X i)

Every term of the normalized complex is finitely generated.

source

instance TauCeti.OrientedPDCode.instFiniteCarrierKhovanovHomologyOfIsNoetherianRing {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] [IsNoetherianRing R] (i j : ℤ) :

Module.Finite R ↑(D.khovanovHomology hD R i j)

Over a Noetherian coefficient ring Khovanov cohomology is finitely generated. This includes integral finite generation and finite-dimensionality over fields.

source