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

source
structure CategoryTheory.Pretriangulated.Triangle (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] :
Type (max u v)
  • 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
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) :
    (CategoryTheory.Pretriangulated.Triangle.mk f g h).mor₃ = h
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) :
    (CategoryTheory.Pretriangulated.Triangle.mk f g h).mor₂ = g
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) :
    (CategoryTheory.Pretriangulated.Triangle.mk f g h).obj₂ = Y
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) :
    (CategoryTheory.Pretriangulated.Triangle.mk f g h).obj₁ = X
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.mk_mor₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) :
    (CategoryTheory.Pretriangulated.Triangle.mk f g h).mor₁ = f
    source
    @[simp]
    theorem CategoryTheory.Pretriangulated.Triangle.mk_obj₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) :
    (CategoryTheory.Pretriangulated.Triangle.mk f g h).obj₃ = Z
    source
    def CategoryTheory.Pretriangulated.Triangle.mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) :
    CategoryTheory.Pretriangulated.Triangle C

    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
      source
      instance CategoryTheory.Pretriangulated.instInhabitedTriangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] :
      Inhabited (CategoryTheory.Pretriangulated.Triangle C)
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.contractibleTriangle_mor₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) :
      (CategoryTheory.Pretriangulated.contractibleTriangle X).mor₃ = 0
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.contractibleTriangle_mor₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) :
      (CategoryTheory.Pretriangulated.contractibleTriangle X).mor₁ = CategoryTheory.CategoryStruct.id X
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.contractibleTriangle_obj₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) :
      (CategoryTheory.Pretriangulated.contractibleTriangle X).obj₁ = X
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.contractibleTriangle_obj₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) :
      (CategoryTheory.Pretriangulated.contractibleTriangle X).obj₂ = X
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.contractibleTriangle_mor₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) :
      (CategoryTheory.Pretriangulated.contractibleTriangle X).mor₂ = 0
      source
      @[simp]
      theorem CategoryTheory.Pretriangulated.contractibleTriangle_obj₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) :
      (CategoryTheory.Pretriangulated.contractibleTriangle X).obj₃ = 0
      source
      def CategoryTheory.Pretriangulated.contractibleTriangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) :
      CategoryTheory.Pretriangulated.Triangle C

      For each object in C, there is a triangle of the form (X,X,0,𝟙 X,0,0)

      Instances For
        source
        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₃
        source
        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
        source
        structure CategoryTheory.Pretriangulated.TriangleMorphism {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (T₁ : CategoryTheory.Pretriangulated.Triangle C) (T₂ : CategoryTheory.Pretriangulated.Triangle C) :
        Type v

        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
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.TriangleMorphism.comm₁_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {T₁ : CategoryTheory.Pretriangulated.Triangle C} {T₂ : CategoryTheory.Pretriangulated.Triangle C} (self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂) {Z : C} (h : T₂.obj₂ ⟶ Z) :
          CategoryTheory.CategoryStruct.comp T₁.mor₁ (CategoryTheory.CategoryStruct.comp self.hom₂ h) = CategoryTheory.CategoryStruct.comp self.hom₁ (CategoryTheory.CategoryStruct.comp T₂.mor₁ h)
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.TriangleMorphism.comm₃_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {T₁ : CategoryTheory.Pretriangulated.Triangle C} {T₂ : CategoryTheory.Pretriangulated.Triangle C} (self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj T₂.obj₁ ⟶ Z) :
          CategoryTheory.CategoryStruct.comp T₁.mor₃ (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.hom₁) h) = CategoryTheory.CategoryStruct.comp self.hom₃ (CategoryTheory.CategoryStruct.comp T₂.mor₃ h)
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.TriangleMorphism.comm₂_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {T₁ : CategoryTheory.Pretriangulated.Triangle C} {T₂ : CategoryTheory.Pretriangulated.Triangle C} (self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂) {Z : C} (h : T₂.obj₃ ⟶ Z) :
          CategoryTheory.CategoryStruct.comp T₁.mor₂ (CategoryTheory.CategoryStruct.comp self.hom₃ h) = CategoryTheory.CategoryStruct.comp self.hom₂ (CategoryTheory.CategoryStruct.comp T₂.mor₂ h)
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.triangleMorphismId_hom₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :
          (CategoryTheory.Pretriangulated.triangleMorphismId T).hom₂ = CategoryTheory.CategoryStruct.id T.obj₂
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.triangleMorphismId_hom₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :
          (CategoryTheory.Pretriangulated.triangleMorphismId T).hom₃ = CategoryTheory.CategoryStruct.id T.obj₃
          source
          @[simp]
          theorem CategoryTheory.Pretriangulated.triangleMorphismId_hom₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :
          (CategoryTheory.Pretriangulated.triangleMorphismId T).hom₁ = CategoryTheory.CategoryStruct.id T.obj₁
          source
          def CategoryTheory.Pretriangulated.triangleMorphismId {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :
          CategoryTheory.Pretriangulated.TriangleMorphism T T

          The identity triangle morphism.

          Instances For
            source
            instance CategoryTheory.Pretriangulated.instInhabitedTriangleMorphism {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :
            Inhabited (CategoryTheory.Pretriangulated.TriangleMorphism T T)
            source
            @[simp]
            theorem CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {T₁ : CategoryTheory.Pretriangulated.Triangle C} {T₂ : CategoryTheory.Pretriangulated.Triangle C} {T₃ : CategoryTheory.Pretriangulated.Triangle C} (f : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂) (g : CategoryTheory.Pretriangulated.TriangleMorphism T₂ T₃) :
            (CategoryTheory.Pretriangulated.TriangleMorphism.comp f g).hom₁ = CategoryTheory.CategoryStruct.comp f.hom₁ g.hom₁
            source
            @[simp]
            theorem CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {T₁ : CategoryTheory.Pretriangulated.Triangle C} {T₂ : CategoryTheory.Pretriangulated.Triangle C} {T₃ : CategoryTheory.Pretriangulated.Triangle C} (f : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂) (g : CategoryTheory.Pretriangulated.TriangleMorphism T₂ T₃) :
            (CategoryTheory.Pretriangulated.TriangleMorphism.comp f g).hom₂ = CategoryTheory.CategoryStruct.comp f.hom₂ g.hom₂
            source
            @[simp]
            theorem CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {T₁ : CategoryTheory.Pretriangulated.Triangle C} {T₂ : CategoryTheory.Pretriangulated.Triangle C} {T₃ : CategoryTheory.Pretriangulated.Triangle C} (f : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂) (g : CategoryTheory.Pretriangulated.TriangleMorphism T₂ T₃) :
            (CategoryTheory.Pretriangulated.TriangleMorphism.comp f g).hom₃ = CategoryTheory.CategoryStruct.comp f.hom₃ g.hom₃
            source
            def CategoryTheory.Pretriangulated.TriangleMorphism.comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {T₁ : CategoryTheory.Pretriangulated.Triangle C} {T₂ : CategoryTheory.Pretriangulated.Triangle C} {T₃ : CategoryTheory.Pretriangulated.Triangle C} (f : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂) (g : CategoryTheory.Pretriangulated.TriangleMorphism T₂ T₃) :
            CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₃

            Composition of triangle morphisms gives a triangle morphism.

            Instances For
              source
              @[simp]
              theorem CategoryTheory.Pretriangulated.triangleCategory_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] :
              ∀ {X Y Z : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = CategoryTheory.Pretriangulated.TriangleMorphism.comp f g
              source
              @[simp]
              theorem CategoryTheory.Pretriangulated.triangleCategory_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] (A : CategoryTheory.Pretriangulated.Triangle C) :
              CategoryTheory.CategoryStruct.id A = CategoryTheory.Pretriangulated.triangleMorphismId A
              source
              instance CategoryTheory.Pretriangulated.triangleCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] :
              CategoryTheory.Category.{v, max u v} (CategoryTheory.Pretriangulated.Triangle C)

              Triangles with triangle morphisms form a category.

              source
              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
              source
              @[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✝) :
              (CategoryTheory.Pretriangulated.Triangle.homMk A B hom₁ hom₂ hom₃).hom₂ = hom₂
              source
              @[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✝) :
              (CategoryTheory.Pretriangulated.Triangle.homMk A B hom₁ hom₂ hom₃).hom₃ = hom₃
              source
              @[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✝) :
              (CategoryTheory.Pretriangulated.Triangle.homMk A B hom₁ hom₂ hom₃).hom₁ = hom₁
              source
              def CategoryTheory.Pretriangulated.Triangle.homMk {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 ⟶ B
              Instances For
                source
                @[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
                source
                @[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
                source
                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
                  source
                  theorem CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {A : CategoryTheory.Pretriangulated.Triangle C} {B : CategoryTheory.Pretriangulated.Triangle C} (h : A = B) :
                  (CategoryTheory.eqToHom h).hom₁ = CategoryTheory.eqToHom (_ : A.obj₁ = B.obj₁)
                  source
                  theorem CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {A : CategoryTheory.Pretriangulated.Triangle C} {B : CategoryTheory.Pretriangulated.Triangle C} (h : A = B) :
                  (CategoryTheory.eqToHom h).hom₂ = CategoryTheory.eqToHom (_ : A.obj₂ = B.obj₂)
                  source
                  theorem CategoryTheory.Pretriangulated.Triangle.eqToHom_hom₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {A : CategoryTheory.Pretriangulated.Triangle C} {B : CategoryTheory.Pretriangulated.Triangle C} (h : A = B) :
                  (CategoryTheory.eqToHom h).hom₃ = CategoryTheory.eqToHom (_ : A.obj₃ = B.obj₃)