The shift on cochain complexes and on the homotopy category #
In this file, we show that for any preadditive category C
, the categories
CochainComplex C ℤ
and HomotopyCategory C (ComplexShape.up ℤ)
are
equipped with a shift by ℤ
.
The shift functor by n : ℤ
on CochainComplex C ℤ
which sends a cochain
complex K
to the complex which is K.X (i + n)
in degree i
, and which
multiplies the differentials by (-1)^n
.
Instances For
The canonical isomorphism ((shiftFunctor C n).obj K).X i ≅ K.X m
when m = i + n
.
Instances For
The shift functor by n
on CochainComplex C ℤ
identifies to the identity
functor when n = 0
.
Instances For
The compatibility of the shift functors on CochainComplex C ℤ
with respect
to the addition of integers.
Instances For
The commutation with the shift isomorphism for the functor on cochain complexes induced by an additive functor between preadditive categories.
Instances For
If h : Homotopy φ₁ φ₂
and n : ℤ
, this is the induced homotopy
between φ₁⟦n⟧'
and φ₂⟦n⟧'
.