Documentation

Mathlib.CategoryTheory.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

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

Instances

    distinguished triangles in a pretriangulated category

    Instances For

      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

      Any morphism Y ⟶ Z is part of a distinguished triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧

      Any morphism Z ⟶ X⟦1⟧ is part of a distinguished triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧

      theorem CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [CategoryTheory.Preadditive C] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T₁ : CategoryTheory.Pretriangulated.Triangle C) (T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ CategoryTheory.Pretriangulated.distinguishedTriangles) (b : T₁.obj₂ T₂.obj₂) (c : T₁.obj₃ T₂.obj₃) (comm : CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂) :

      A commutative square involving the morphisms mor₂ of two distinguished triangles can be extended as morphism of triangles

      theorem CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [CategoryTheory.Preadditive C] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] (T₁ : CategoryTheory.Pretriangulated.Triangle C) (T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₂ : T₂ CategoryTheory.Pretriangulated.distinguishedTriangles) (a : T₁.obj₁ T₂.obj₁) (c : T₁.obj₃ T₂.obj₃) (comm : CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃) :

      A commutative square involving the morphisms mor₃ of two distinguished triangles can be extended as morphism of triangles

      theorem CategoryTheory.Pretriangulated.isIso₂_of_isIso₁₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [CategoryTheory.Preadditive C] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] {T : CategoryTheory.Pretriangulated.Triangle C} {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : T T') (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (hT' : T' CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : CategoryTheory.IsIso φ.hom₁) (h₃ : CategoryTheory.IsIso φ.hom₃) :
      theorem CategoryTheory.Pretriangulated.isIso₃_of_isIso₁₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [CategoryTheory.Preadditive C] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] {T : CategoryTheory.Pretriangulated.Triangle C} {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : T T') (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (hT' : T' CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : CategoryTheory.IsIso φ.hom₁) (h₂ : CategoryTheory.IsIso φ.hom₂) :
      theorem CategoryTheory.Pretriangulated.isIso₁_of_isIso₂₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ] [CategoryTheory.Preadditive C] [∀ (n : ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [hC : CategoryTheory.Pretriangulated C] {T : CategoryTheory.Pretriangulated.Triangle C} {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : T T') (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (hT' : T' CategoryTheory.Pretriangulated.distinguishedTriangles) (h₂ : CategoryTheory.IsIso φ.hom₂) (h₃ : CategoryTheory.IsIso φ.hom₃) :