The normalized Khovanov complex

For a planar oriented PD-code, TauCeti.OrientedPDCode.khovanovComplex is a quantum-indexed family of native cochain complexes. A state with B-resolutions S occurs in cochain degree |S| - n₋ and carries the quantum shift |S| + n₊ - 2n₋. The differential retains the cube sign (-1)^(#{b ∈ S | b < a}) on the saddle adding a.

khovanovComplexXIso identifies its terms with the finite biproduct of these quantum pieces. The inclusions and projections characterize the terms, and ι_khovanovComplex_d gives the signed saddle differential. The complex is supported in [-n₋, n₊].

khovanovComplexShiftIso compares this explicit state convention to the native cochain shift of the bracket. Its degree-i component is (-1)^(i * n₋), since native shifts change the differential by (-1)^n₋. Quantum shifts raise degrees: the component at j uses the bracket at j - (n₊ - 2n₋).

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.

noncomputable def TauCeti.OrientedPDCode.khovanovComplex {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] : CategoryTheory.GradedObject ℤ (CochainComplex (ModuleCat R) ℤ)

The normalized Khovanov complex of a planar oriented diagram. Quantum degree j uses bracket degree j - n₊ + 2n₋, and cochain degree i uses cube height i + n₋. Restriction translates indices while preserving the original signed saddle differential.

theorem TauCeti.OrientedPDCode.khovanovComplex_apply {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : D.khovanovComplex hD R j = ((ComplexShape.embeddingUp'Add 1 ↑D.negativeCrossingCount).restrictionFunctor (ModuleCat R)).obj (D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).cubeComplex

The definition of the normalized complex as an index translation of the bracket.

theorem TauCeti.OrientedPDCode.khovanovComplex_X {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j i : ℤ) : (D.khovanovComplex hD R j).X i = (D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).cubeComplex.X (i + ↑D.negativeCrossingCount)

The normalized term in degree i is the signed cube term of height i + n₋.

theorem TauCeti.OrientedPDCode.khovanovComplex_d {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j i l : ℤ) : (D.khovanovComplex hD R j).d i l = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).cubeComplex.d (i + ↑D.negativeCrossingCount) (l + ↑D.negativeCrossingCount)) (CategoryTheory.eqToHom ⋯))

Normalization translates the differential without changing its cube signs.

noncomputable def TauCeti.OrientedPDCode.khovanovComplexShiftIso {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : D.khovanovComplex hD R j ≅ D.khovanovBracket hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)⟦↑D.negativeCrossingCount⟧

Comparison with the native cochain shift of the quantum-shifted bracket. The comparison multiplies cochain degree i by (-1)^(i * n₋).

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplexShiftIso_hom_f {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j i : ℤ) : (D.khovanovComplexShiftIso hD R j).hom.f i = (i * ↑D.negativeCrossingCount).negOnePow • CategoryTheory.eqToHom ⋯

The forward shift comparison carries the degreewise normalization sign.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplexShiftIso_inv_f {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j i : ℤ) : (D.khovanovComplexShiftIso hD R j).inv.f i = (i * ↑D.negativeCrossingCount).negOnePow • CategoryTheory.eqToHom ⋯

The inverse shift comparison carries the same degreewise sign.

theorem TauCeti.OrientedPDCode.resolutionCube_obj_normalized {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) (S : Finset (Fin n)) : (D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).obj S = ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState S))).piece ℤ (j - D.stateQuantumShift (PDCode.cubeState S)))

The normalized cube vertex is precisely the quantum piece shifted by the state's stateQuantumShift.

noncomputable def TauCeti.OrientedPDCode.khovanovComplexι {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) : (D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).obj ↑S ⟶ (D.khovanovComplex hD R j).X i

The inclusion of a state vertex into the normalized cochain term of height i + n₋.

theorem TauCeti.OrientedPDCode.khovanovComplexι_def {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) : D.khovanovComplexι hD R j S = CategoryTheory.CategoryStruct.comp ((D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).cubeComplexι S) (CategoryTheory.eqToHom ⋯)

The inclusion of a state vertex is its inclusion into the signed cube term of height i + n₋, which is the normalized term in degree i.

noncomputable def TauCeti.OrientedPDCode.khovanovComplexπ {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) : (D.khovanovComplex hD R j).X i ⟶ (D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).obj ↑S

The projection of a normalized cochain term onto a state vertex.

theorem TauCeti.OrientedPDCode.khovanovComplexπ_def {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) : D.khovanovComplexπ hD R j S = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).cubeComplexπ S)

The normalized state projection is the cube projection after the index translation.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplex_total {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j i : ℤ) : ∑ S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }, CategoryTheory.CategoryStruct.comp (D.khovanovComplexπ hD R j S) (D.khovanovComplexι hD R j S) = CategoryTheory.CategoryStruct.id ((D.khovanovComplex hD R j).X i)

The state projections followed by their inclusions sum to the identity of a normalized cochain term.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplexι_π_self {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) : CategoryTheory.CategoryStruct.comp (D.khovanovComplexι hD R j S) (D.khovanovComplexπ hD R j S) = CategoryTheory.CategoryStruct.id ((D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).obj ↑S)

Inclusion followed by projection is the identity on a state summand.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplexι_π_self_assoc {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) {Z : ModuleCat R} (h : (D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).obj ↑S ⟶ Z) : CategoryTheory.CategoryStruct.comp (D.khovanovComplexι hD R j S) (CategoryTheory.CategoryStruct.comp (D.khovanovComplexπ hD R j S) h) = h

Inclusion followed by projection is the identity on a state summand.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplexι_π_of_ne {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} {S T : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }} (h : S ≠ T) : CategoryTheory.CategoryStruct.comp (D.khovanovComplexι hD R j S) (D.khovanovComplexπ hD R j T) = 0

Inclusion followed by projection onto a distinct state vanishes.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplexι_π_of_ne_assoc {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} {S T : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }} (h : S ≠ T) {Z : ModuleCat R} (h✝ : (D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).obj ↑T ⟶ Z) : CategoryTheory.CategoryStruct.comp (D.khovanovComplexι hD R j S) (CategoryTheory.CategoryStruct.comp (D.khovanovComplexπ hD R j T) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

Inclusion followed by projection onto a distinct state vanishes.

theorem TauCeti.OrientedPDCode.khovanovComplex_hom_ext {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} {A : ModuleCat R} {f g : (D.khovanovComplex hD R j).X i ⟶ A} (h : ∀ (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }), CategoryTheory.CategoryStruct.comp (D.khovanovComplexι hD R j S) f = CategoryTheory.CategoryStruct.comp (D.khovanovComplexι hD R j S) g) : f = g

Morphisms out of a normalized term are determined by their state restrictions.

theorem TauCeti.OrientedPDCode.khovanovComplex_hom_ext_iff {n : ℕ} {D : OrientedPDCode n} {hD : D.IsPlanar} {R : Type u} [CommRing R] {j i : ℤ} {A : ModuleCat R} {f g : (D.khovanovComplex hD R j).X i ⟶ A} : f = g ↔ ∀ (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }), CategoryTheory.CategoryStruct.comp (D.khovanovComplexι hD R j S) f = CategoryTheory.CategoryStruct.comp (D.khovanovComplexι hD R j S) g

theorem TauCeti.OrientedPDCode.khovanovComplex_hom_ext' {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} {A : ModuleCat R} {f g : A ⟶ (D.khovanovComplex hD R j).X i} (h : ∀ (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }), CategoryTheory.CategoryStruct.comp f (D.khovanovComplexπ hD R j S) = CategoryTheory.CategoryStruct.comp g (D.khovanovComplexπ hD R j S)) : f = g

Morphisms into a normalized term are determined by their state projections.

theorem TauCeti.OrientedPDCode.khovanovComplex_hom_ext'_iff {n : ℕ} {D : OrientedPDCode n} {hD : D.IsPlanar} {R : Type u} [CommRing R] {j i : ℤ} {A : ModuleCat R} {f g : A ⟶ (D.khovanovComplex hD R j).X i} : f = g ↔ ∀ (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }), CategoryTheory.CategoryStruct.comp f (D.khovanovComplexπ hD R j S) = CategoryTheory.CategoryStruct.comp g (D.khovanovComplexπ hD R j S)

noncomputable def TauCeti.OrientedPDCode.khovanovComplexXIso {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j i : ℤ) : (D.khovanovComplex hD R j).X i ≅ ⨁ fun (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) => ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ↑S))).piece ℤ (j - D.stateQuantumShift (PDCode.cubeState ↑S)))

Each normalized term is the finite biproduct of the quantum pieces of its states. The index equation |S| = i + n₋ is equivalent to stateCochainDegree(S) = i.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplexι_comp_khovanovComplexXIso_hom {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) : CategoryTheory.CategoryStruct.comp (D.khovanovComplexι hD R j S) (D.khovanovComplexXIso hD R j i).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.biproduct.ι (fun (T : { T : Finset (Fin n) // ↑T.card = i + ↑D.negativeCrossingCount }) => ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ↑T))).piece ℤ (j - D.stateQuantumShift (PDCode.cubeState ↑T)))) S)

On a state summand, the term comparison is the quantum-piece identification.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplexι_comp_khovanovComplexXIso_hom_assoc {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) {Z : ModuleCat R} (h : (⨁ fun (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) => ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ↑S))).piece ℤ (j - D.stateQuantumShift (PDCode.cubeState ↑S)))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (D.khovanovComplexι hD R j S) (CategoryTheory.CategoryStruct.comp (D.khovanovComplexXIso hD R j i).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (T : { T : Finset (Fin n) // ↑T.card = i + ↑D.negativeCrossingCount }) => ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ↑T))).piece ℤ (j - D.stateQuantumShift (PDCode.cubeState ↑T)))) S) h)

On a state summand, the term comparison is the quantum-piece identification.

@[simp]

theorem TauCeti.OrientedPDCode.ι_comp_khovanovComplexXIso_inv {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (T : { T : Finset (Fin n) // ↑T.card = i + ↑D.negativeCrossingCount }) => ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ↑T))).piece ℤ (j - D.stateQuantumShift (PDCode.cubeState ↑T)))) S) (D.khovanovComplexXIso hD R j i).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (D.khovanovComplexι hD R j S)

The inverse term comparison includes a quantum piece as its state summand.

@[simp]

theorem TauCeti.OrientedPDCode.ι_comp_khovanovComplexXIso_inv_assoc {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) {Z : ModuleCat R} (h : (D.khovanovComplex hD R j).X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (T : { T : Finset (Fin n) // ↑T.card = i + ↑D.negativeCrossingCount }) => ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ↑T))).piece ℤ (j - D.stateQuantumShift (PDCode.cubeState ↑T)))) S) (CategoryTheory.CategoryStruct.comp (D.khovanovComplexXIso hD R j i).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (D.khovanovComplexι hD R j S) h)

The inverse term comparison includes a quantum piece as its state summand.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplexXIso_hom_comp_π {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) : CategoryTheory.CategoryStruct.comp (D.khovanovComplexXIso hD R j i).hom (CategoryTheory.Limits.biproduct.π (fun (T : { T : Finset (Fin n) // ↑T.card = i + ↑D.negativeCrossingCount }) => ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ↑T))).piece ℤ (j - D.stateQuantumShift (PDCode.cubeState ↑T)))) S) = CategoryTheory.CategoryStruct.comp (D.khovanovComplexπ hD R j S) (CategoryTheory.eqToHom ⋯)

Projecting the term comparison onto a quantum piece gives the state projection.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplexXIso_hom_comp_π_assoc {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) {Z : ModuleCat R} (h : ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ↑S))).piece ℤ (j - D.stateQuantumShift (PDCode.cubeState ↑S))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (D.khovanovComplexXIso hD R j i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (T : { T : Finset (Fin n) // ↑T.card = i + ↑D.negativeCrossingCount }) => ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ↑T))).piece ℤ (j - D.stateQuantumShift (PDCode.cubeState ↑T)))) S) h) = CategoryTheory.CategoryStruct.comp (D.khovanovComplexπ hD R j S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

Projecting the term comparison onto a quantum piece gives the state projection.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplexXIso_biproductIsoPi_apply {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j i : ℤ) (x : ↑((D.khovanovComplex hD R j).X i)) (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) : (CategoryTheory.ConcreteCategory.hom (ModuleCat.biproductIsoPi fun (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) => ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ↑S))).piece ℤ (j - D.stateQuantumShift (PDCode.cubeState ↑S)))).hom) ((CategoryTheory.ConcreteCategory.hom (D.khovanovComplexXIso hD R j i).hom) x) S = (ModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((ModuleCat.Hom.hom (D.khovanovComplexπ hD R j S)) x)

The product coordinates of the term comparison are its normalized state projections.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplexXIso_inv_comp_π {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) : CategoryTheory.CategoryStruct.comp (D.khovanovComplexXIso hD R j i).inv (D.khovanovComplexπ hD R j S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (T : { T : Finset (Fin n) // ↑T.card = i + ↑D.negativeCrossingCount }) => ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ↑T))).piece ℤ (j - D.stateQuantumShift (PDCode.cubeState ↑T)))) S) (CategoryTheory.eqToHom ⋯)

The inverse term comparison projects a quantum piece onto its state vertex.

@[simp]

theorem TauCeti.OrientedPDCode.khovanovComplexXIso_inv_comp_π_assoc {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) {Z : ModuleCat R} (h : (D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).obj ↑S ⟶ Z) : CategoryTheory.CategoryStruct.comp (D.khovanovComplexXIso hD R j i).inv (CategoryTheory.CategoryStruct.comp (D.khovanovComplexπ hD R j S) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (T : { T : Finset (Fin n) // ↑T.card = i + ↑D.negativeCrossingCount }) => ↧↥((Khovanov.circleQuantumGrading R (D.ResolvedCircle (PDCode.cubeState ↑T))).piece ℤ (j - D.stateQuantumShift (PDCode.cubeState ↑T)))) S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

The inverse term comparison projects a quantum piece onto its state vertex.

theorem TauCeti.OrientedPDCode.ι_khovanovComplex_d {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) : CategoryTheory.CategoryStruct.comp (D.khovanovComplexι hD R j S) ((D.khovanovComplex hD R j).d i (i + 1)) = ∑ a : ↥(↑S)ᶜ, (-1) ^ {b ∈ ↑S | b < ↑a}.card • CategoryTheory.CategoryStruct.comp ((D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).map (CategoryTheory.homOfLE ⋯)) (D.khovanovComplexι hD R j ⟨insert ↑a ↑S, ⋯⟩)

The normalized differential on a state is the sum of the saddle edges with the original cube signs. Each cube edge is identified with its actual saddle by PDCode.resolutionCube_map_homOfLE_insert_comp_resolutionCubeι.

theorem TauCeti.OrientedPDCode.ι_khovanovComplex_d_assoc {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) {i : ℤ} (S : { S : Finset (Fin n) // ↑S.card = i + ↑D.negativeCrossingCount }) {Z : ModuleCat R} (h : (D.khovanovComplex hD R j).X (i + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (D.khovanovComplexι hD R j S) (CategoryTheory.CategoryStruct.comp ((D.khovanovComplex hD R j).d i (i + 1)) h) = CategoryTheory.CategoryStruct.comp (∑ a : ↥(↑S)ᶜ, (-1) ^ {b ∈ ↑S | b < ↑a}.card • CategoryTheory.CategoryStruct.comp ((D.resolutionCube hD R (j - ↑D.positiveCrossingCount + 2 * ↑D.negativeCrossingCount)).map (CategoryTheory.homOfLE ⋯)) (D.khovanovComplexι hD R j ⟨insert ↑a ↑S, ⋯⟩)) h

The normalized differential on a state is the sum of the saddle edges with the original cube signs. Each cube edge is identified with its actual saddle by PDCode.resolutionCube_map_homOfLE_insert_comp_resolutionCubeι.

instance TauCeti.OrientedPDCode.khovanovComplex_isStrictlyGE {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : (D.khovanovComplex hD R j).IsStrictlyGE (-↑D.negativeCrossingCount)

No cochain terms occur below -n₋.

instance TauCeti.OrientedPDCode.khovanovComplex_isStrictlyLE {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] (j : ℤ) : (D.khovanovComplex hD R j).IsStrictlyLE ↑D.positiveCrossingCount

No cochain terms occur above n₊.

theorem TauCeti.OrientedPDCode.isZero_khovanovComplex_X_of_cochain_notMem_Icc {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] {i : ℤ} (hi : i ∉ Set.Icc (-↑D.negativeCrossingCount) ↑D.positiveCrossingCount) (j : ℤ) : CategoryTheory.Limits.IsZero ((D.khovanovComplex hD R j).X i)

The normalized chain groups vanish outside the cochain interval [-n₋, n₊].

theorem TauCeti.OrientedPDCode.isZero_khovanovComplex_X_of_quantum_notMem_Icc {n : ℕ} (D : OrientedPDCode n) (hD : D.IsPlanar) (R : Type u) [CommRing R] {j : ℤ} (hj : j ∉ Set.Icc (↑D.positiveCrossingCount - 2 * ↑D.negativeCrossingCount - ↑(D.stateLoopCount (PDCode.cubeState ∅))) (↑D.positiveCrossingCount - 2 * ↑D.negativeCrossingCount + ↑n + ↑(D.stateLoopCount (PDCode.cubeState Finset.univ)))) (i : ℤ) : CategoryTheory.Limits.IsZero ((D.khovanovComplex hD R j).X i)

The normalized chain groups vanish outside the translated extreme-resolution quantum interval. Circle counts include all crossing-free components.

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

The normalized chain groups are supported in a finite rectangle in the two gradings jointly.