mathlib documentation


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.

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

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


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