Theorems · Definition · category theory

CategoryTheory.Pretriangulated.Triangle.rotate

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

If you rotate a triangle, you get another triangle. Given a triangle of the form: `` f g h X ───> Y ───> Z ───> X⟦1⟧ ` applying rotate gives a triangle of the form: ` g h -f⟦1⟧' Y ───> Z ───> X⟦1⟧ ───> Y⟦1⟧ ``

Defined in

Mathlib.CategoryTheory.Triangulated.Rotate

Cited by

43 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.HasShift