Translation of cochain indices and the signed shift

Restriction along i ↦ i + k translates the terms of a cochain complex without changing its differential. The native shift by k also multiplies the differential by (-1)^k. CochainComplex.restrictionAddIsoShift compares these functors by multiplication by (-1)^(i * k) in degree i. This comparison allows state-indexed complexes with unchanged edge signs to use native cochain shifts.

noncomputable def CochainComplex.restrictionAddIsoShift (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : ℤ) : (ComplexShape.embeddingUp'Add 1 k).restrictionFunctor C ≅ CategoryTheory.shiftFunctor (CochainComplex C ℤ) k

Translating cochain indices without changing the differential agrees with the native signed shift, through the degreewise sign (-1)^(i * k).

@[simp]

theorem CochainComplex.restrictionAddIsoShift_hom_app_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : ℤ) (K : CochainComplex C ℤ) (i : ℤ) : ((restrictionAddIsoShift C k).hom.app K).f i = (i * k).negOnePow • CategoryTheory.CategoryStruct.id (K.X (i + k))

The forward comparison multiplies degree i by (-1)^(i * k).

@[simp]

theorem CochainComplex.restrictionAddIsoShift_inv_app_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : ℤ) (K : CochainComplex C ℤ) (i : ℤ) : ((restrictionAddIsoShift C k).inv.app K).f i = (i * k).negOnePow • CategoryTheory.CategoryStruct.id (K.X (i + k))

The inverse comparison has the same degreewise sign.