Theorems · Definition · category theory

CategoryTheory.Pretriangulated.Triangle.invRotate

{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

Given a triangle of the form: `` f g h X ───> Y ───> Z ───> X⟦1⟧ ` applying invRotate gives a triangle that can be thought of as: ` -h⟦-1⟧' f g Z⟦-1⟧ ───> X ───> Y ───> Z ` (note that this diagram doesn't technically fit the definition of triangle, as Z⟦-1⟧⟦1⟧ is not necessarily equal to Z, but it is isomorphic, by the counitIso of shiftEquiv C 1`)

Defined in

Mathlib.CategoryTheory.Triangulated.Rotate

Cited by

38 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.HasShift