Theorems · Definition · category theory

CategoryTheory.Pretriangulated.Triangle.shiftFunctor

(C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        ℤ →
          CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C) (CategoryTheory.Pretriangulated.Triangle C)

The shift functor Triangle C ⥤ Triangle C by n : ℤ sends a triangle to the triangle obtained by shifting the objects by n in C and by multiplying the three morphisms by (-1)^n.

Defined in

Mathlib.CategoryTheory.Triangulated.TriangleShift

Cited by

31 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.HasShift