Theorems · Definition · category theory

CategoryTheory.Pretriangulated.invRotate

(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 inverse rotation of triangles gives an endofunctor on the category of triangles in C.

Defined in

Mathlib.CategoryTheory.Triangulated.Rotate

Cited by

30 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.HasShift