Documentation

Mathlib.CategoryTheory.Triangulated.Basic

Triangles #

This file contains the definition of triangles in an additive category with an additive shift. It also defines morphisms between these triangles.

TODO: generalise this to n-angles in n-angulated categories as in https://arxiv.org/abs/1006.4592

  • mk' :: (
    • obj₁ : C

      the first object of a triangle

    • obj₂ : C

      the second object of a triangle

    • obj₃ : C

      the third object of a triangle

    • mor₁ : s.obj₁ s.obj₂

      the first morphism of a triangle

    • mor₂ : s.obj₂ s.obj₃

      the second morphism of a triangle

    • mor₃ : s.obj₃ (CategoryTheory.shiftFunctor C 1).obj s.obj₁

      the third morphism of a triangle

  • )

A triangle in C is a sextuple (X,Y,Z,f,g,h) where X,Y,Z are objects of C, and f : X ⟶ Y, g : Y ⟶ Z, h : Z ⟶ X⟦1⟧ are morphisms in C. See https://stacks.math.columbia.edu/tag/0144.

Instances For

    A triangle (X,Y,Z,f,g,h) in C is defined by the morphisms f : X ⟶ Y, g : Y ⟶ Z and h : Z ⟶ X⟦1⟧.

    Instances For
      theorem CategoryTheory.Pretriangulated.TriangleMorphism.ext_iff {C : Type u} :
      ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.HasShift C } {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} (x y : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂), x = y x.hom₁ = y.hom₁ x.hom₂ = y.hom₂ x.hom₃ = y.hom₃
      theorem CategoryTheory.Pretriangulated.TriangleMorphism.ext {C : Type u} :
      ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.HasShift C } {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} (x y : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂), x.hom₁ = y.hom₁x.hom₂ = y.hom₂x.hom₃ = y.hom₃x = y

      A morphism of triangles (X,Y,Z,f,g,h) ⟶ (X',Y',Z',f',g',h') in C is a triple of morphisms a : X ⟶ X', b : Y ⟶ Y', c : Z ⟶ Z' such that a ≫ f' = f ≫ b, b ≫ g' = g ≫ c, and a⟦1⟧' ≫ h = h' ≫ c. In other words, we have a commutative diagram:

           f      g      h
        X  ───> Y  ───> Z  ───> X⟦1⟧
        │       │       │        │
        │a      │b      │c       │a⟦1⟧'
        V       V       V        V
        X' ───> Y' ───> Z' ───> X'⟦1⟧
           f'     g'     h'
      

      See https://stacks.math.columbia.edu/tag/0144.

      Instances For
        theorem CategoryTheory.Pretriangulated.Triangle.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ] {A : CategoryTheory.Pretriangulated.Triangle C} {B : CategoryTheory.Pretriangulated.Triangle C} (f : A B) (g : A B) (h₁ : f.hom₁ = g.hom₁) (h₂ : f.hom₂ = g.hom₂) (h₃ : f.hom₃ = g.hom₃) :
        f = g
        @[simp]
        theorem CategoryTheory.Pretriangulated.Triangle.isoMk_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ] (A : CategoryTheory.Pretriangulated.Triangle C) (B : CategoryTheory.Pretriangulated.Triangle C) (iso₁ : A.obj₁ B.obj₁) (iso₂ : A.obj₂ B.obj₂) (iso₃ : A.obj₃ B.obj₃) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom B.mor₁) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom B.mor₂) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map iso₁.hom) = CategoryTheory.CategoryStruct.comp iso₃.hom B.mor₃) _auto✝) :
        (CategoryTheory.Pretriangulated.Triangle.isoMk A B iso₁ iso₂ iso₃).hom = CategoryTheory.Pretriangulated.Triangle.homMk A B iso₁.hom iso₂.hom iso₃.hom
        @[simp]
        theorem CategoryTheory.Pretriangulated.Triangle.isoMk_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ] (A : CategoryTheory.Pretriangulated.Triangle C) (B : CategoryTheory.Pretriangulated.Triangle C) (iso₁ : A.obj₁ B.obj₁) (iso₂ : A.obj₂ B.obj₂) (iso₃ : A.obj₃ B.obj₃) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom B.mor₁) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom B.mor₂) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map iso₁.hom) = CategoryTheory.CategoryStruct.comp iso₃.hom B.mor₃) _auto✝) :
        (CategoryTheory.Pretriangulated.Triangle.isoMk A B iso₁ iso₂ iso₃).inv = CategoryTheory.Pretriangulated.Triangle.homMk B A iso₁.inv iso₂.inv iso₃.inv
        def CategoryTheory.Pretriangulated.Triangle.isoMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ] (A : CategoryTheory.Pretriangulated.Triangle C) (B : CategoryTheory.Pretriangulated.Triangle C) (iso₁ : A.obj₁ B.obj₁) (iso₂ : A.obj₂ B.obj₂) (iso₃ : A.obj₃ B.obj₃) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom B.mor₁) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom B.mor₂) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map iso₁.hom) = CategoryTheory.CategoryStruct.comp iso₃.hom B.mor₃) _auto✝) :
        A B
        Instances For