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

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.

  • 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₁ : self.obj₁ self.obj₂

      the first morphism of a triangle

    • mor₂ : self.obj₂ self.obj₃

      the second morphism of a triangle

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

      the third morphism of a triangle

  • )
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⟧.

    Equations
    Instances For
      Equations
      • CategoryTheory.Pretriangulated.instInhabitedTriangle = { default := { obj₁ := 0, obj₂ := 0, obj₃ := 0, mor₁ := 0, mor₂ := 0, mor₃ := 0 } }
      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
      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₃

      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

        The identity triangle morphism.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Triangles with triangle morphisms form a category.

          Equations
          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.homMk_hom₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ] (A : CategoryTheory.Pretriangulated.Triangle C) (B : CategoryTheory.Pretriangulated.Triangle C) (hom₁ : A.obj₁ B.obj₁) (hom₂ : A.obj₂ B.obj₂) (hom₃ : A.obj₃ B.obj₃) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ B.mor₁) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ B.mor₂) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) = CategoryTheory.CategoryStruct.comp hom₃ B.mor₃) _auto✝) :
          (A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₃ = hom₃
          @[simp]
          theorem CategoryTheory.Pretriangulated.Triangle.homMk_hom₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ] (A : CategoryTheory.Pretriangulated.Triangle C) (B : CategoryTheory.Pretriangulated.Triangle C) (hom₁ : A.obj₁ B.obj₁) (hom₂ : A.obj₂ B.obj₂) (hom₃ : A.obj₃ B.obj₃) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ B.mor₁) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ B.mor₂) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) = CategoryTheory.CategoryStruct.comp hom₃ B.mor₃) _auto✝) :
          (A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₁ = hom₁
          @[simp]
          theorem CategoryTheory.Pretriangulated.Triangle.homMk_hom₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ] (A : CategoryTheory.Pretriangulated.Triangle C) (B : CategoryTheory.Pretriangulated.Triangle C) (hom₁ : A.obj₁ B.obj₁) (hom₂ : A.obj₂ B.obj₂) (hom₃ : A.obj₃ B.obj₃) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ B.mor₁) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ B.mor₂) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) = CategoryTheory.CategoryStruct.comp hom₃ B.mor₃) _auto✝) :
          (A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₂ = hom₂
          Equations
          • A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃ = { hom₁ := hom₁, hom₂ := hom₂, hom₃ := hom₃, comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃ }
          Instances For
            @[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✝) :
            (A.isoMk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom = A.homMk B iso₁.hom iso₂.hom iso₃.hom comm₁ comm₂ comm₃
            @[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✝) :
            (A.isoMk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv = B.homMk 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
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              The obvious triangle X₁ ⟶ X₁ ⊞ X₂ ⟶ X₂ ⟶ X₁⟦1⟧.

              Equations
              Instances For

                The obvious triangle X₁ ⟶ X₁ ⨯ X₂ ⟶ X₂ ⟶ X₁⟦1⟧.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  The product of a family of triangles.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    A projection from the product of a family of triangles.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      A family of morphisms T' ⟶ T j lifts to a morphism T' ⟶ productTriangle T.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        The triangle productTriangle T satisfies the universal property of the categorical product of the triangles T.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem CategoryTheory.Pretriangulated.Triangle.π₁_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ] :
                          ∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X Y), CategoryTheory.Pretriangulated.Triangle.π₁.map f = f.hom₁
                          @[simp]
                          theorem CategoryTheory.Pretriangulated.Triangle.π₁_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ] (T : CategoryTheory.Pretriangulated.Triangle C) :
                          CategoryTheory.Pretriangulated.Triangle.π₁.obj T = T.obj₁

                          The first projection Triangle C ⥤ C.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem CategoryTheory.Pretriangulated.Triangle.π₂_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ] :
                            ∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X Y), CategoryTheory.Pretriangulated.Triangle.π₂.map f = f.hom₂
                            @[simp]
                            theorem CategoryTheory.Pretriangulated.Triangle.π₂_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ] (T : CategoryTheory.Pretriangulated.Triangle C) :
                            CategoryTheory.Pretriangulated.Triangle.π₂.obj T = T.obj₂

                            The second projection Triangle C ⥤ C.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem CategoryTheory.Pretriangulated.Triangle.π₃_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ] (T : CategoryTheory.Pretriangulated.Triangle C) :
                              CategoryTheory.Pretriangulated.Triangle.π₃.obj T = T.obj₃
                              @[simp]
                              theorem CategoryTheory.Pretriangulated.Triangle.π₃_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ] :
                              ∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X Y), CategoryTheory.Pretriangulated.Triangle.π₃.map f = f.hom₃

                              The third projection Triangle C ⥤ C.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For