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]
- 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)
[category_theory.category C]
[category_theory.has_shift C] :
C ≌ C
The shift autoequivalence, moving objects and morphisms 'up'.
Equations
@[simp]
theorem
category_theory.shift_zero_eq_zero
(C : Type u)
[category_theory.category C]
[category_theory.has_shift C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
(n : ℤ) :
(category_theory.shift C ^ n).functor.map 0 = 0