mathlib3 documentation


Pretriangulated Categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains the definition of pretriangulated categories and triangulated functors between them.

Implementation Notes #

We work under the assumption that pretriangulated categories are preadditive categories, but not necessarily additive categories, as is assumed in some sources.

TODO: generalise this to n-angulated categories as in


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  ───> X1
      a      b               a1⟧'
      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.


Instances for category_theory.pretriangulated
  • category_theory.pretriangulated.has_sizeof_inst