Cancelling two identity blocks in a three-term cochain complex

Let a cochain complex in a preadditive category with a zero object and binary biproducts be supported in degrees -1, 0, and 1, with terms identified as U, Z ⊞ (W ⊞ U), and W. Suppose the differential from U projects to the identity on the last middle summand, and the differential to W is the identity on the second middle summand. These two identity blocks cancel, leaving a contraction onto Z concentrated in degree zero.

In these coordinates write the differentials as (δ, x, id) and (ε, id, y). Their composite vanishes, so δ ≫ ε + x + y = 0. The corrected projection is (id, 0, -δ) and the corrected inclusion is (id, -ε, 0). The homotopy projects from degree zero to its U summand and includes degree one into its W summand. Thus the construction allows nonzero off-diagonal components; it does not assume the displayed splitting is already a direct sum of complexes.

Contraction.ThreeTermCancellationData.toContraction packages these maps as a TauCeti.Contraction, whose homotopyEquiv supplies the homotopy equivalence. The degree-zero projection and inclusion are projectionZero and inclusionZero.

References

• D. Bar-Natan, Fast Khovanov homology computations, J. Knot Theory Ramifications 16 (2007), Lemma 4.2 (Gaussian elimination for complexes); the construction here cancels two identity blocks by two such eliminations.

structure TauCeti.Contraction.ThreeTermCancellationData {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (K : CochainComplex C ℤ) (U Z W : C) : Type v_1

Component identifications for a three-term complex with two cancellable identity blocks.

• minusIso : K.X (-1) ≅ U

  Identify the term in degree -1.

• zeroIso : K.X 0 ≅ Z ⊞ W ⊞ U

  Split the middle term into the surviving object and the two cancellable objects.

• oneIso : K.X 1 ≅ W

  Identify the term in degree 1.

• vanish (n : ℤ) : n ≠ -1 → n ≠ 0 → n ≠ 1 → CategoryTheory.Limits.IsZero (K.X n)

  The complex vanishes outside these three consecutive degrees.

• d_snd_snd : CategoryTheory.CategoryStruct.comp (K.d (-1) 0) (CategoryTheory.CategoryStruct.comp self.zeroIso.hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.snd)) = self.minusIso.hom

  The bottom differential has identity component in the last middle summand.

• inl_inr_d : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp self.zeroIso.inv (CategoryTheory.CategoryStruct.comp (K.d 0 1) self.oneIso.hom))) = CategoryTheory.CategoryStruct.id W

  The top differential restricts to the identity on the second middle summand.

noncomputable def TauCeti.Contraction.ThreeTermCancellationData.projectionZero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K : CochainComplex C ℤ} {U Z W : C} (h : ThreeTermCancellationData K U Z W) : K.X 0 ⟶ Z

The degree-zero projection after eliminating the two identity blocks.

theorem TauCeti.Contraction.ThreeTermCancellationData.projectionZero_def {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K : CochainComplex C ℤ} {U Z W : C} (h : ThreeTermCancellationData K U Z W) : h.projectionZero = CategoryTheory.CategoryStruct.comp h.zeroIso.hom (CategoryTheory.Limits.biprod.fst - CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.snd) (CategoryTheory.CategoryStruct.comp h.minusIso.inv (CategoryTheory.CategoryStruct.comp (K.d (-1) 0) (CategoryTheory.CategoryStruct.comp h.zeroIso.hom CategoryTheory.Limits.biprod.fst))))

The corrected projection subtracts the bottom differential's surviving component.

noncomputable def TauCeti.Contraction.ThreeTermCancellationData.inclusionZero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K : CochainComplex C ℤ} {U Z W : C} (h : ThreeTermCancellationData K U Z W) : Z ⟶ K.X 0

The degree-zero inclusion corrected by the differential into the upper identity block.

theorem TauCeti.Contraction.ThreeTermCancellationData.inclusionZero_def {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K : CochainComplex C ℤ} {U Z W : C} (h : ThreeTermCancellationData K U Z W) : h.inclusionZero = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl - CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp h.zeroIso.inv (CategoryTheory.CategoryStruct.comp (K.d 0 1) h.oneIso.hom))) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr)) h.zeroIso.inv

The corrected inclusion subtracts the surviving component of the top differential.

noncomputable def TauCeti.Contraction.ThreeTermCancellationData.toContraction {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K : CochainComplex C ℤ} {U Z W : C} (h : ThreeTermCancellationData K U Z W) [CategoryTheory.Limits.HasZeroObject C] : Contraction K ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj Z)

Cancel the lower and upper identity blocks and retract onto Z in degree zero.

@[simp]

theorem TauCeti.Contraction.ThreeTermCancellationData.toContraction_proj_f_zero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K : CochainComplex C ℤ} {U Z W : C} (h : ThreeTermCancellationData K U Z W) [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.CategoryStruct.comp (h.toContraction.proj.f 0) (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 Z).hom = h.projectionZero

The degree-zero projection is the corrected projection to the surviving summand.

@[simp]

theorem TauCeti.Contraction.ThreeTermCancellationData.toContraction_proj_f_zero_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K : CochainComplex C ℤ} {U Z W : C} (h : ThreeTermCancellationData K U Z W) [CategoryTheory.Limits.HasZeroObject C] {Z✝ : C} (h✝ : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (h.toContraction.proj.f 0) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 Z).hom h✝) = CategoryTheory.CategoryStruct.comp h.projectionZero h✝

The degree-zero projection is the corrected projection to the surviving summand.

@[simp]

theorem TauCeti.Contraction.ThreeTermCancellationData.toContraction_incl_f_zero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K : CochainComplex C ℤ} {U Z W : C} (h : ThreeTermCancellationData K U Z W) [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 Z).inv (h.toContraction.incl.f 0) = h.inclusionZero

The contraction's degree-zero inclusion is the corrected inclusion of the surviving summand.

@[simp]

theorem TauCeti.Contraction.ThreeTermCancellationData.toContraction_incl_f_zero_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K : CochainComplex C ℤ} {U Z W : C} (h : ThreeTermCancellationData K U Z W) [CategoryTheory.Limits.HasZeroObject C] {Z✝ : C} (h✝ : K.X 0 ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 Z).inv (CategoryTheory.CategoryStruct.comp (h.toContraction.incl.f 0) h✝) = CategoryTheory.CategoryStruct.comp h.inclusionZero h✝

The contraction's degree-zero inclusion is the corrected inclusion of the surviving summand.