Theorems · Definition · category theory

CategoryTheory.Pretriangulated.mk.noConfusion

{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.Limits.HasZeroObject C} →
      {inst_2 : CategoryTheory.HasShift C ℤ} →
        {inst_3 : CategoryTheory.Preadditive C} →
          {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} →
            {P : Sort u_1} →
              {distinguishedTriangles : Set (CategoryTheory.Pretriangulated.Triangle C)} →
                {isomorphic_distinguished :
                    ∀ T₁ ∈ distinguishedTriangles,
                      ∀ (T₂ : CategoryTheory.Pretriangulated.Triangle C) (x : T₂ ≅ T₁), T₂ ∈ distinguishedTriangles} →
                  {contractible_distinguished :
                      ∀ (X : C), CategoryTheory.Pretriangulated.contractibleTriangle X ∈ distinguishedTriangles} →
                    {distinguished_cocone_triangle :
                        ∀ {X Y : C} (f : X ⟶ Y),
                          ∃ Z g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ distinguishedTriangles} →
                      {rotate_distinguished_triangle :
                          ∀ (T : CategoryTheory.Pretriangulated.Triangle C),
                            T ∈ distinguishedTriangles ↔ T.rotate ∈ distinguishedTriangles} →
                        {complete_distinguished_triangle_morphism :
                            ∀ (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C),
                              T₁ ∈ distinguishedTriangles →
                                T₂ ∈ distinguishedTriangles →
                                  ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂),
                                    CategoryTheory.CategoryStruct.comp T₁.mor₁ b =
                                        CategoryTheory.CategoryStruct.comp a T₂.mor₁ →
                                      ∃ c,
                                        CategoryTheory.CategoryStruct.comp T₁.mor₂ c =
                                            CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧
                                          CategoryTheory.CategoryStruct.comp T₁.mor₃
                                              ((CategoryTheory.shiftFunctor C 1).map a) =
                                            CategoryTheory.CategoryStruct.comp c T₂.mor₃} →
                          {distinguishedTriangles' : Set (CategoryTheory.Pretriangulated.Triangle C)} →
                            {isomorphic_distinguished' :
                                ∀ T₁ ∈ distinguishedTriangles',
                                  ∀ (T₂ : CategoryTheory.Pretriangulated.Triangle C) (x : T₂ ≅ T₁),
                                    T₂ ∈ distinguishedTriangles'} →
                              {contractible_distinguished' :
                                  ∀ (X : C),
                                    CategoryTheory.Pretriangulated.contractibleTriangle X ∈ distinguishedTriangles'} →
                                {distinguished_cocone_triangle' :
                                    ∀ {X Y : C} (f : X ⟶ Y),
                                      ∃ Z g h,
                                        CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ distinguishedTriangles'} →
                                  {rotate_distinguished_triangle' :
                                      ∀ (T : CategoryTheory.Pretriangulated.Triangle C),
                                        T ∈ distinguishedTriangles' ↔ T.rotate ∈ distinguishedTriangles'} →
                                    {complete_distinguished_triangle_morphism' :
                                        ∀ (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C),
                                          T₁ ∈ distinguishedTriangles' →
                                            T₂ ∈ distinguishedTriangles' →
                                              ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂),
                                                CategoryTheory.CategoryStruct.comp T₁.mor₁ b =
                                                    CategoryTheory.CategoryStruct.comp a T₂.mor₁ →
                                                  ∃ c,
                                                    CategoryTheory.CategoryStruct.comp T₁.mor₂ c =
                                                        CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧
                                                      CategoryTheory.CategoryStruct.comp T₁.mor₃
                                                          ((CategoryTheory.shiftFunctor C 1).map a) =
                                                        CategoryTheory.CategoryStruct.comp c T₂.mor₃} →
                                      { distinguishedTriangles := distinguishedTriangles,
                                            isomorphic_distinguished := isomorphic_distinguished,
                                            contractible_distinguished := contractible_distinguished,
                                            distinguished_cocone_triangle := distinguished_cocone_triangle,
                                            rotate_distinguished_triangle := rotate_distinguished_triangle,
                                            complete_distinguished_triangle_morphism :=
                                              complete_distinguished_triangle_morphism } =
                                          { distinguishedTriangles := distinguishedTriangles',
                                            isomorphic_distinguished := isomorphic_distinguished',
                                            contractible_distinguished := contractible_distinguished',
                                            distinguished_cocone_triangle := distinguished_cocone_triangle',
                                            rotate_distinguished_triangle := rotate_distinguished_triangle',
                                            complete_distinguished_triangle_morphism :=
                                              complete_distinguished_triangle_morphism' } →
                                        (distinguishedTriangles ≍ distinguishedTriangles' → P) → P

Defined in

Mathlib.CategoryTheory.Triangulated.Pretriangulated

Cited by

0 results in Mathlib

Foundations

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