Documentation

Mathlib.CategoryTheory.Triangulated.Functor

Triangulated functors #

In this file, when C and D are categories equipped with a shift by ℤ and F : C ⥤ D is a functor which commutes with the shift, we define the induced functor F.mapTriangle : Triangle C ⥤ Triangle D on the categories of triangles. When C and D are pretriangulated, a triangulated functor is such a functor F which also sends distinguished triangles to distinguished triangles: this defines the typeclass Functor.IsTriangulated.

source
def CategoryTheory.Functor.mapTriangle {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] :
CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C) (CategoryTheory.Pretriangulated.Triangle D)

The functor Triangle C ⥤ Triangle D that is induced by a functor F : C ⥤ D which commutes with shift by ℤ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Functor.mapTriangle_map_hom₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] :
    ∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), (F.mapTriangle.map f).hom₁ = F.map f.hom₁
    source
    @[simp]
    theorem CategoryTheory.Functor.mapTriangle_map_hom₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] :
    ∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), (F.mapTriangle.map f).hom₂ = F.map f.hom₂
    source
    @[simp]
    theorem CategoryTheory.Functor.mapTriangle_obj {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :
    F.mapTriangle.obj T = CategoryTheory.Pretriangulated.Triangle.mk (F.map T.mor₁) (F.map T.mor₂) (CategoryTheory.CategoryStruct.comp (F.map T.mor₃) ((F.commShiftIso 1).hom.app T.obj₁))
    source
    @[simp]
    theorem CategoryTheory.Functor.mapTriangle_map_hom₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] :
    ∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), (F.mapTriangle.map f).hom₃ = F.map f.hom₃
    source
    instance CategoryTheory.Functor.instFaithfulTriangleMapTriangle {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.Faithful] :
    F.mapTriangle.Faithful
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.Functor.instFullTriangleMapTriangleOfFaithful {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.Full] [F.Faithful] :
    F.mapTriangle.Full
    Equations
    • ⋯ = ⋯
    source
    noncomputable def CategoryTheory.Functor.mapTriangleCommShiftIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (n : ℤ) :
    (CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).comp F.mapTriangle ≅ F.mapTriangle.comp (CategoryTheory.Pretriangulated.Triangle.shiftFunctor D n)

    The functor F.mapTriangle commutes with the shift.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (n : ℤ) (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((F.mapTriangleCommShiftIso n).inv.app X).hom₃ = (F.commShiftIso n).inv.app X.obj₃
      source
      @[simp]
      theorem CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (n : ℤ) (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((F.mapTriangleCommShiftIso n).inv.app X).hom₁ = (F.commShiftIso n).inv.app X.obj₁
      source
      @[simp]
      theorem CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (n : ℤ) (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((F.mapTriangleCommShiftIso n).hom.app X).hom₃ = (F.commShiftIso n).hom.app X.obj₃
      source
      @[simp]
      theorem CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (n : ℤ) (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((F.mapTriangleCommShiftIso n).inv.app X).hom₂ = (F.commShiftIso n).inv.app X.obj₂
      source
      @[simp]
      theorem CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (n : ℤ) (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((F.mapTriangleCommShiftIso n).hom.app X).hom₂ = (F.commShiftIso n).hom.app X.obj₂
      source
      @[simp]
      theorem CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (n : ℤ) (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((F.mapTriangleCommShiftIso n).hom.app X).hom₁ = (F.commShiftIso n).hom.app X.obj₁
      source
      noncomputable instance CategoryTheory.Functor.instCommShiftTriangleMapTriangleInt {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] :
      F.mapTriangle.CommShift ℤ
      Equations
      • F.instCommShiftTriangleMapTriangleInt = { iso := F.mapTriangleCommShiftIso, zero := ⋯, add := ⋯ }
      source
      def CategoryTheory.Functor.mapTriangleRotateIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] :
      F.mapTriangle.comp (CategoryTheory.Pretriangulated.rotate D) ≅ (CategoryTheory.Pretriangulated.rotate C).comp F.mapTriangle

      F.mapTriangle commutes with the rotation of triangles.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
        (F.mapTriangleRotateIso.inv.app X).hom₃ = (F.commShiftIso 1).hom.app X.obj₁
        source
        @[simp]
        theorem CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
        (F.mapTriangleRotateIso.hom.app X).hom₃ = (F.commShiftIso 1).inv.app X.obj₁
        source
        @[simp]
        theorem CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
        (F.mapTriangleRotateIso.hom.app X).hom₁ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
        source
        @[simp]
        theorem CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
        (F.mapTriangleRotateIso.inv.app X).hom₁ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
        source
        @[simp]
        theorem CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
        (F.mapTriangleRotateIso.hom.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₃)
        source
        @[simp]
        theorem CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
        (F.mapTriangleRotateIso.inv.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₃)
        source
        noncomputable def CategoryTheory.Functor.mapTriangleInvRotateIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] :
        F.mapTriangle.comp (CategoryTheory.Pretriangulated.invRotate D) ≅ (CategoryTheory.Pretriangulated.invRotate C).comp F.mapTriangle

        F.mapTriangle commutes with the inverse of the rotation of triangles.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
          (F.mapTriangleInvRotateIso.inv.app X).hom₃ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
          (F.mapTriangleInvRotateIso.hom.app X).hom₁ = (F.commShiftIso (-1)).inv.app X.obj₃
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
          (F.mapTriangleInvRotateIso.hom.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₁)
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
          (F.mapTriangleInvRotateIso.inv.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₁)
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
          (F.mapTriangleInvRotateIso.inv.app X).hom₁ = (F.commShiftIso (-1)).hom.app X.obj₃
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [F.Additive] (X : CategoryTheory.Pretriangulated.Triangle C) :
          (F.mapTriangleInvRotateIso.hom.app X).hom₃ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
          source
          def CategoryTheory.Functor.mapTriangleIdIso (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.HasShift C ℤ] :
          (CategoryTheory.Functor.id C).mapTriangle ≅ CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle C)

          The canonical isomorphism (𝟭 C).mapTriangle ≅ 𝟭 (Triangle C).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₂ (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
            ((CategoryTheory.Functor.mapTriangleIdIso C).inv.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
            source
            @[simp]
            theorem CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₃ (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
            ((CategoryTheory.Functor.mapTriangleIdIso C).inv.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃
            source
            @[simp]
            theorem CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₂ (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
            ((CategoryTheory.Functor.mapTriangleIdIso C).hom.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
            source
            @[simp]
            theorem CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₁ (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
            ((CategoryTheory.Functor.mapTriangleIdIso C).hom.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁
            source
            @[simp]
            theorem CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₁ (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
            ((CategoryTheory.Functor.mapTriangleIdIso C).inv.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁
            source
            @[simp]
            theorem CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₃ (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
            ((CategoryTheory.Functor.mapTriangleIdIso C).hom.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃
            source
            def CategoryTheory.Functor.mapTriangleCompIso {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (G : CategoryTheory.Functor D E) [G.CommShift ℤ] :
            (F.comp G).mapTriangle ≅ F.mapTriangle.comp G.mapTriangle

            The canonical isomorphism (F ⋙ G).mapTriangle ≅ F.mapTriangle ⋙ G.mapTriangle.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₃ {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (G : CategoryTheory.Functor D E) [G.CommShift ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
              ((F.mapTriangleCompIso G).hom.app X).hom₃ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₃))
              source
              @[simp]
              theorem CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₂ {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (G : CategoryTheory.Functor D E) [G.CommShift ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
              ((F.mapTriangleCompIso G).inv.app X).hom₂ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₂))
              source
              @[simp]
              theorem CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₁ {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (G : CategoryTheory.Functor D E) [G.CommShift ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
              ((F.mapTriangleCompIso G).inv.app X).hom₁ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₁))
              source
              @[simp]
              theorem CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₁ {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (G : CategoryTheory.Functor D E) [G.CommShift ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
              ((F.mapTriangleCompIso G).hom.app X).hom₁ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₁))
              source
              @[simp]
              theorem CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₂ {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (G : CategoryTheory.Functor D E) [G.CommShift ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
              ((F.mapTriangleCompIso G).hom.app X).hom₂ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₂))
              source
              @[simp]
              theorem CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₃ {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (G : CategoryTheory.Functor D E) [G.CommShift ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
              ((F.mapTriangleCompIso G).inv.app X).hom₃ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₃))
              source
              def CategoryTheory.Functor.mapTriangleIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ] :
              F₁.mapTriangle ≅ F₂.mapTriangle

              Two isomorphic functors F₁ and F₂ induce isomorphic functors F₁.mapTriangle and F₂.mapTriangle if the isomorphism F₁ ≅ F₂ is compatible with the shifts.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.Functor.mapTriangleIso_inv_app_hom₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
                ((CategoryTheory.Functor.mapTriangleIso e).inv.app X).hom₁ = e.inv.app X.obj₁
                source
                @[simp]
                theorem CategoryTheory.Functor.mapTriangleIso_hom_app_hom₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
                ((CategoryTheory.Functor.mapTriangleIso e).hom.app X).hom₁ = e.hom.app X.obj₁
                source
                @[simp]
                theorem CategoryTheory.Functor.mapTriangleIso_inv_app_hom₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
                ((CategoryTheory.Functor.mapTriangleIso e).inv.app X).hom₂ = e.inv.app X.obj₂
                source
                @[simp]
                theorem CategoryTheory.Functor.mapTriangleIso_hom_app_hom₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
                ((CategoryTheory.Functor.mapTriangleIso e).hom.app X).hom₃ = e.hom.app X.obj₃
                source
                @[simp]
                theorem CategoryTheory.Functor.mapTriangleIso_hom_app_hom₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
                ((CategoryTheory.Functor.mapTriangleIso e).hom.app X).hom₂ = e.hom.app X.obj₂
                source
                @[simp]
                theorem CategoryTheory.Functor.mapTriangleIso_inv_app_hom₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ] (X : CategoryTheory.Pretriangulated.Triangle C) :
                ((CategoryTheory.Functor.mapTriangleIso e).inv.app X).hom₃ = e.inv.app X.obj₃
                source
                class CategoryTheory.Functor.IsTriangulated {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] :
                Prop

                A functor which commutes with the shift by ℤ is triangulated if it sends distinguished triangles to distinguished triangles.

                • map_distinguished : ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
                Instances
                  source
                  theorem CategoryTheory.Functor.IsTriangulated.map_distinguished {C : Type u_1} {D : Type u_2} :
                  ∀ {inst : CategoryTheory.Category.{u_4, u_1} C} {inst_1 : CategoryTheory.Category.{u_5, u_2} D} {inst_2 : CategoryTheory.HasShift C ℤ} {inst_3 : CategoryTheory.HasShift D ℤ} {F : CategoryTheory.Functor C D} {inst_4 : F.CommShift ℤ} {inst_5 : CategoryTheory.Limits.HasZeroObject C} {inst_6 : CategoryTheory.Limits.HasZeroObject D} {inst_7 : CategoryTheory.Preadditive C} {inst_8 : CategoryTheory.Preadditive D} {inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive} {inst_11 : CategoryTheory.Pretriangulated C} {inst_12 : CategoryTheory.Pretriangulated D} [self : F.IsTriangulated], ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
                  source
                  theorem CategoryTheory.Functor.map_distinguished {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [F.IsTriangulated] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) :
                  F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
                  source
                  @[instance 100]
                  instance CategoryTheory.Functor.IsTriangulated.instPreservesZeroMorphisms {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [F.IsTriangulated] :
                  F.PreservesZeroMorphisms
                  Equations
                  • ⋯ = ⋯
                  source
                  noncomputable instance CategoryTheory.Functor.IsTriangulated.instPreservesLimitsOfShapeDiscreteWalkingPair {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [F.IsTriangulated] :
                  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  @[instance 100]
                  instance CategoryTheory.Functor.IsTriangulated.instAdditive {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [F.IsTriangulated] :
                  F.Additive
                  Equations
                  • ⋯ = ⋯
                  source
                  instance CategoryTheory.Functor.IsTriangulated.instId {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] :
                  (CategoryTheory.Functor.id C).IsTriangulated
                  Equations
                  • ⋯ = ⋯
                  source
                  instance CategoryTheory.Functor.IsTriangulated.instComp {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (G : CategoryTheory.Functor D E) [G.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroObject E] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Preadditive E] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [CategoryTheory.Pretriangulated E] [F.IsTriangulated] [G.IsTriangulated] :
                  (F.comp G).IsTriangulated
                  Equations
                  • ⋯ = ⋯
                  source
                  theorem CategoryTheory.Functor.isTriangulated_of_iso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ] [F₁.IsTriangulated] :
                  F₂.IsTriangulated
                  source
                  theorem CategoryTheory.Functor.isTriangulated_iff_of_iso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ] :
                  F₁.IsTriangulated ↔ F₂.IsTriangulated
                  source
                  theorem CategoryTheory.Functor.mem_mapTriangle_essImage_of_distinguished {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [F.IsTriangulated] [F.mapArrow.EssSurj] (T : CategoryTheory.Pretriangulated.Triangle D) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) :
                  ∃ (T' : CategoryTheory.Pretriangulated.Triangle C) (_ : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)
                  source
                  theorem CategoryTheory.Functor.isTriangulated_of_precomp {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (G : CategoryTheory.Functor D E) [G.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroObject E] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Preadditive E] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [CategoryTheory.Pretriangulated E] [(F.comp G).IsTriangulated] [F.IsTriangulated] [F.mapArrow.EssSurj] :
                  G.IsTriangulated
                  source
                  theorem CategoryTheory.Functor.isTriangulated_of_precomp_iso {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] {F : CategoryTheory.Functor C D} [F.CommShift ℤ] {G : CategoryTheory.Functor D E} [G.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroObject E] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Preadditive E] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [CategoryTheory.Pretriangulated E] {H : CategoryTheory.Functor C E} (e : F.comp G ≅ H) [H.CommShift ℤ] [H.IsTriangulated] [F.IsTriangulated] [F.mapArrow.EssSurj] [CategoryTheory.NatTrans.CommShift e.hom ℤ] :
                  G.IsTriangulated
                  source
                  def CategoryTheory.Triangulated.Octahedron.map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] :
                  CategoryTheory.Triangulated.Octahedron ⋯ ⋯ ⋯ ⋯

                  The image of an octahedron by a triangulated functor.

                  Equations
                  • h.map F = { m₁ := F.map h.m₁, m₃ := F.map h.m₃, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯, comm₄ := ⋯, mem := ⋯ }
                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.Triangulated.Octahedron.map_m₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] :
                    (h.map F).m₁ = F.map h.m₁
                    source
                    @[simp]
                    theorem CategoryTheory.Triangulated.Octahedron.map_m₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁₂ : C} {Z₂₃ : C} {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} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] :
                    (h.map F).m₃ = F.map h.m₃
                    source
                    theorem CategoryTheory.isTriangulated_of_essSurj_mapComposableArrows_two {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] [(F.mapComposableArrows 2).EssSurj] [CategoryTheory.IsTriangulated C] :
                    CategoryTheory.IsTriangulated D

                    If F : C ⥤ D is a triangulated functor from a triangulated category, then D is also triangulated if tuples of composables arrows in D can be lifted to C.