Quantum support of the Khovanov bracket

The bracket has finite support in both cochain and quantum degree. If kA and kB are the numbers of circles in the all-A and all-B resolutions of an n-crossing diagram, every quantum degree of the bracket lies in [-kA, n + kB]. This includes the crossing-free components and the empty diagram. The bound is uniform in the cochain degree and in the coefficient ring, so the family of quantum components can be totalized using only finitely many nonzero pieces. The same bound holds for its homology.

Over a nontrivial coefficient ring, a term is nonzero exactly when there is an enhanced state of its bidegree. This describes chain groups, rather than asserting that every such state survives in homology.

References

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

theorem TauCeti.PDCode.stateLoopCount_cubeState_le_allA {n : ℕ} (D : PDCode n) (S : Finset (Fin n)) : D.stateLoopCount (cubeState S) ≤ D.stateLoopCount (cubeState ∅) + S.card

A resolution has at most one additional circle per B-smoothing relative to the all-A resolution. This also holds for nonplanar codes.

theorem TauCeti.PDCode.stateLoopCount_cubeState_le_allB {n : ℕ} (D : PDCode n) (S : Finset (Fin n)) : D.stateLoopCount (cubeState S) ≤ D.stateLoopCount (cubeState Finset.univ) + (n - S.card)

A resolution has at most one additional circle per A-smoothing relative to the all-B resolution. This also holds for nonplanar codes.

theorem TauCeti.PDCode.isZero_khovanovBracket_X_iff {n : ℕ} (D : PDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] [Nontrivial R] (j r : ℤ) : CategoryTheory.Limits.IsZero ((D.khovanovBracket hD R j).X r) ↔ ∀ (S : Finset (Fin n)), ↑S.card = r → ∀ (l : D.ResolvedCircle (cubeState S) → Bool), ↑S.card + Khovanov.labelingQuantumDegree (D.ResolvedCircle (cubeState S)) l ≠ j

A bidegree of the bracket is absent exactly when it has no enhanced states, over a nontrivial coefficient ring.

theorem TauCeti.PDCode.card_add_labelingQuantumDegree_mem_Icc {n : ℕ} (D : PDCode n) (S : Finset (Fin n)) (l : D.ResolvedCircle (cubeState S) → Bool) : ↑S.card + Khovanov.labelingQuantumDegree (D.ResolvedCircle (cubeState S)) l ∈ Set.Icc (-↑(D.stateLoopCount (cubeState ∅))) (↑n + ↑(D.stateLoopCount (cubeState Finset.univ)))

Every enhanced state of the bracket lies between the extreme-resolution quantum bounds.

theorem TauCeti.PDCode.isZero_khovanovBracket_X_of_quantum_notMem_Icc {n : ℕ} (D : PDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] {j : ℤ} (hj : j ∉ Set.Icc (-↑(D.stateLoopCount (cubeState ∅))) (↑n + ↑(D.stateLoopCount (cubeState Finset.univ)))) (r : ℤ) : CategoryTheory.Limits.IsZero ((D.khovanovBracket hD R j).X r)

Every term vanishes outside the uniform quantum interval determined by the all-A and all-B circle counts, over any commutative coefficient ring.

theorem TauCeti.PDCode.isZero_khovanovBracket_of_quantum_notMem_Icc {n : ℕ} (D : PDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] {j : ℤ} (hj : j ∉ Set.Icc (-↑(D.stateLoopCount (cubeState ∅))) (↑n + ↑(D.stateLoopCount (cubeState Finset.univ)))) : CategoryTheory.Limits.IsZero (D.khovanovBracket hD R j)

The whole quantum-component complex vanishes outside the extreme-resolution interval.

theorem TauCeti.PDCode.finite_quantumSupport_khovanovBracket {n : ℕ} (D : PDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] : {j : ℤ | ¬CategoryTheory.Limits.IsZero (D.khovanovBracket hD R j)}.Finite

Only finitely many quantum-component complexes of the bracket are nonzero.

theorem TauCeti.PDCode.isZero_homology_khovanovBracket_of_quantum_notMem_Icc {n : ℕ} (D : PDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] {j : ℤ} (hj : j ∉ Set.Icc (-↑(D.stateLoopCount (cubeState ∅))) (↑n + ↑(D.stateLoopCount (cubeState Finset.univ)))) (r : ℤ) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (D.khovanovBracket hD R j) r)

Bracket homology vanishes outside the same quantum interval as the chain groups.

theorem TauCeti.PDCode.finite_bigradedSupport_khovanovBracket {n : ℕ} (D : PDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] : {p : ℤ × ℤ | ¬CategoryTheory.Limits.IsZero ((D.khovanovBracket hD R p.2).X p.1)}.Finite

The set of nonzero chain groups is finite in the two gradings jointly.