Theorems · Definition · category theory

CategoryTheory.Triangulated.Octahedron.map

{C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.HasShift C ℤ] →
          [inst_3 : CategoryTheory.HasShift D ℤ] →
            [inst_4 : CategoryTheory.Limits.HasZeroObject C] →
              [inst_5 : CategoryTheory.Limits.HasZeroObject D] →
                [inst_6 : CategoryTheory.Preadditive C] →
                  [inst_7 : CategoryTheory.Preadditive D] →
                    [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                      [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] →
                        [inst_10 : CategoryTheory.Pretriangulated C] →
                          [inst_11 : CategoryTheory.Pretriangulated D] →
                            {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                              {u₁₂ : X₁ ⟶ X₂} →
                                {u₂₃ : X₂ ⟶ X₃} →
                                  {u₁₃ : X₁ ⟶ X₃} →
                                    {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} →
                                      {v₁₂ : X₂ ⟶ Z₁₂} →
                                        {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                                          {h₁₂ :
                                              CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈
                                                CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                            {v₂₃ : X₃ ⟶ Z₂₃} →
                                              {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} →
                                                {h₂₃ :
                                                    CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈
                                                      CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                                  {v₁₃ : X₃ ⟶ Z₁₃} →
                                                    {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                                                      {h₁₃ :
                                                          CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈
                                                            CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                                        CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃ →
                                                          (F : CategoryTheory.Functor C D) →
                                                            [inst_12 : F.CommShift ℤ] →
                                                              [inst_13 : F.IsTriangulated] →
                                                                CategoryTheory.Triangulated.Octahedron ⋯ ⋯ ⋯ ⋯

The image of an octahedron by a triangulated functor.

Defined in

Mathlib.CategoryTheory.Triangulated.Functor

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.Limits.HasZeroObjectCategoryTheory.Limits.HasZeroObjectCategoryTheory.PreadditiveCategoryTheory.PreadditiveCategoryTheory.Functor.AdditiveCategoryTheory.Functor.AdditiveCategoryTheory.PretriangulatedCategoryTheory.PretriangulatedCategoryTheory.Functor.CommShiftCategoryTheory.Functor.IsTriangulated