Theorems · Definition · category theory

CategoryTheory.Pretriangulated.Triangle.isoMk

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (A B : CategoryTheory.Pretriangulated.Triangle C) →
        (iso₁ : A.obj₁ ≅ B.obj₁) →
          (iso₂ : A.obj₂ ≅ B.obj₂) →
            (iso₃ : A.obj₃ ≅ B.obj₃) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp A.mor₁ iso₂.hom =
                    CategoryTheory.CategoryStruct.comp iso₁.hom B.mor₁)
                  CategoryTheory.Pretriangulated.Triangle.isoMk._auto_1 →
                autoParam
                    (CategoryTheory.CategoryStruct.comp A.mor₂ iso₃.hom =
                      CategoryTheory.CategoryStruct.comp iso₂.hom B.mor₂)
                    CategoryTheory.Pretriangulated.Triangle.isoMk._auto_3 →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map iso₁.hom) =
                        CategoryTheory.CategoryStruct.comp iso₃.hom B.mor₃)
                      CategoryTheory.Pretriangulated.Triangle.isoMk._auto_5 →
                    (A ≅ B)

Make an isomorphism between triangles from the required data.

Defined in

Mathlib.CategoryTheory.Triangulated.Basic

Cited by

27 results in Mathlib

Foundations

Depth 44 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.HasShift