# mathlibdocumentation

category_theory.triangulated.pretriangulated

# Pretriangulated Categories #

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 https://arxiv.org/abs/1006.4592

@[class]
structure category_theory.triangulated.pretriangulated (C : Type u)  :
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. See https://stacks.math.columbia.edu/tag/0145

Given any distinguished triangle T, then we know T.rotate is also distinguished.

Given any distinguished triangle T, then we know T.inv_rotate is also distinguished.

Given any distinguished triangle

      f       g       h
X  ───> Y  ───> Z  ───> X⟦1⟧


the composition f ≫ g = 0. See https://stacks.math.columbia.edu/tag/0146

Given any distinguished triangle

      f       g       h
X  ───> Y  ───> Z  ───> X⟦1⟧


the composition g ≫ h = 0. See https://stacks.math.columbia.edu/tag/0146

Given any distinguished triangle

      f       g       h
X  ───> Y  ───> Z  ───> X⟦1⟧


the composition h ≫ f⟦1⟧ = 0. See https://stacks.math.columbia.edu/tag/0146

structure category_theory.triangulated.pretriangulated.triangulated_functor_struct (C : Type u₁) (D : Type u₂)  :
Type (max u₁ u₂ v₁ v₂)
• to_functor : C D
• comm_shift :

The underlying structure of a triangulated functor between pretriangulated categories C and D is a functor F : C ⥤ D together with given functorial isomorphisms ξ X : F(X⟦1⟧) ⟶ F(X)⟦1⟧.

@[instance]
Equations
@[simp]

Given a triangulated_functor_struct we can define a function from triangles of C to triangles of D.

Equations
• to_triangulated_functor_struct :
• map_distinguished' : ∀ (T : , (T dist_triangC)

A triangulated functor between pretriangulated categories C and D is a functor F : C ⥤ D together with given functorial isomorphisms ξ X : F(X⟦1⟧) ⟶ F(X)⟦1⟧ such that for every distinguished triangle (X,Y,Z,f,g,h) of C, the triangle (F(X), F(Y), F(Z), F(f), F(g), F(h) ≫ (ξ X)) is a distinguished triangle of D. See https://stacks.math.columbia.edu/tag/014V

@[instance]
Equations
@[simp]

Given a triangulated_functor we can define a function from triangles of C to triangles of D.

Equations

Given a triangulated_functor and a distinguished triangle T of C, then the triangle it maps onto in D is also distinguished.