Theorems · Definition · category theory

CochainComplex.shiftFunctor

(C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → ℤ → CategoryTheory.Functor (CochainComplex C ℤ) (CochainComplex C ℤ)

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.

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.Shift

Cited by

50 results in Mathlib

Foundations

Depth 53 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive