Theorems · Inductive type · category theory

CategoryTheory.Pretriangulated

(C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] → Type (max u v)

A preadditive category C with an additive shift, and a class of "distinguished triangles" relative to that shift is called pretriangulated if the following hold: * Any triangle that is isomorphic to a distinguished triangle is also distinguished. * Any triangle of the form (X,X,0,id,0,0) is distinguished. * For any morphism f : X ⟶ Y there exists a distinguished triangle of the form (X,Y,Z,f,g,h). * The triangle (X,Y,Z,f,g,h) is distinguished if and only if (Y,Z,X⟦1⟧,g,h,-f⟦1⟧) is. * Given a diagram: `` f g h X ───> Y ───> Z ───> X⟦1⟧ │ │ │ │a │b │a⟦1⟧' V V V X' ───> Y' ───> Z' ───> X'⟦1⟧ f' g' h' ` where the left square commutes, and whose rows are distinguished triangles, there exists a morphism c : Z ⟶ Z' such that (a,b,c)` is a triangle morphism.

Defined in

Mathlib.CategoryTheory.Triangulated.Pretriangulated

Cited by

669 results in Mathlib

Foundations

Depth 31 from the axioms, rests on 310 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroObjectCategoryTheory.HasShiftCategoryTheory.PreadditiveCategoryTheory.Functor.Additive