Exactness and cycles of shifted cochain complexes

The shift K⟦n⟧ of a cochain complex K has K.X (i + n) in degree i and differential (-1)ⁿ • d. Mathlib identifies the short complex of K⟦n⟧ in degree i with the short complex of K in degree n + i (CochainComplex.shiftShortComplexFunctorIso). This file records the two consequences used for degreewise arguments: exactness at i of K⟦n⟧ is exactness at n + i of K, so that shifting preserves and reflects acyclicity, and the cycles of K⟦n⟧ in degree i are the cycles of K in degree n + i.

Main results

• CochainComplex.exactAt_shift_iff: K⟦n⟧ is exact at i iff K is exact at n + i.
• CochainComplex.acyclic_shift_iff: K⟦n⟧ is acyclic iff K is.
• CochainComplex.shiftCyclesIso: the isomorphism (K⟦n⟧).cycles i ≅ K.cycles (n + i).

theorem CochainComplex.exactAt_shift_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n i i' : ℤ) (hi : n + i = i') : HomologicalComplex.ExactAt ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i ↔ HomologicalComplex.ExactAt K i'

The shift K⟦n⟧ is exact in degree i exactly when K is exact in degree i' = n + i.

@[simp]

theorem CochainComplex.acyclic_shift_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n : ℤ) : HomologicalComplex.Acyclic ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) ↔ HomologicalComplex.Acyclic K

A shift of a cochain complex is acyclic exactly when the complex is.

noncomputable def CochainComplex.shiftCyclesIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) [CategoryTheory.CategoryWithHomology C] (n i i' : ℤ) (hi : n + i = i') : HomologicalComplex.cycles ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i ≅ HomologicalComplex.cycles K i'

The cycles of K⟦n⟧ in degree i are the cycles of K in degree i' = n + i.

Equations

• K.shiftCyclesIso n i i' hi = CategoryTheory.ShortComplex.cyclesMapIso ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).app K)

@[simp]

theorem CochainComplex.shiftCyclesIso_hom_iCycles {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) [CategoryTheory.CategoryWithHomology C] (n i i' : ℤ) (hi : n + i = i') : CategoryTheory.CategoryStruct.comp (K.shiftCyclesIso n i i' hi).hom (HomologicalComplex.iCycles K i') = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i) (K.shiftFunctorObjXIso n i i' ⋯).hom

The isomorphism CochainComplex.shiftCyclesIso commutes with the inclusions of the cycles, up to the identification (K⟦n⟧).X i = K.X (i + n).

@[simp]

theorem CochainComplex.shiftCyclesIso_hom_iCycles_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) [CategoryTheory.CategoryWithHomology C] (n i i' : ℤ) (hi : n + i = i') {Z : C} (h : K.X i' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.shiftCyclesIso n i i' hi).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K i') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i) (CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso n i i' ⋯).hom h)

The isomorphism CochainComplex.shiftCyclesIso commutes with the inclusions of the cycles, up to the identification (K⟦n⟧).X i = K.X (i + n).