# mathlibdocumentation

category_theory.shift

# Shift #

A shift on a category is nothing more than an automorphism of the category. An example to keep in mind might be the category of complexes ⋯ → C_{n-1} → C_n → C_{n+1} → ⋯ with the shift operator re-indexing the terms, so the degree n term of shift C would be the degree n+1 term of C.

@[class]
structure category_theory.has_shift (C : Type u)  :
Type (max u v)
• shift : C C

A category has a shift, or translation, if it is equipped with an automorphism.

Instances
def category_theory.shift (C : Type u)  :
C C

The shift autoequivalence, moving objects and morphisms 'up'.

Equations
@[simp]
theorem category_theory.shift_zero_eq_zero (C : Type u) (X Y : C) (n : ) :