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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] :
Functor (Pretriangulated.Triangle C) (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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] {X✝ Y✝ : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] {X✝ Y✝ : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] (T : Pretriangulated.Triangle C) :
    F.mapTriangle.obj T = Pretriangulated.Triangle.mk (F.map T.mor₁) (F.map T.mor₂) (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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] {X✝ Y✝ : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [F.Faithful] :
    F.mapTriangle.Faithful
    source
    instance CategoryTheory.Functor.instFullTriangleMapTriangleOfFaithful {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [F.Full] [F.Faithful] :
    F.mapTriangle.Full
    source
    noncomputable def CategoryTheory.Functor.mapTriangleCommShiftIso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) :
    (Pretriangulated.Triangle.shiftFunctor C n).comp F.mapTriangle ≅ F.mapTriangle.comp (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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) (X : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) (X : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) (X : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) (X : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) (X : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (n : ℤ) (X : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] :
      F.mapTriangle.CommShift ℤ
      Equations
      source
      def CategoryTheory.Functor.mapTriangleRotateIso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] :
      F.mapTriangle.comp (Pretriangulated.rotate D) ≅ (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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) :
        (F.mapTriangleRotateIso.hom.app X).hom₁ = CategoryStruct.id (F.obj X.obj₂)
        source
        @[simp]
        theorem CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₁ {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) :
        (F.mapTriangleRotateIso.inv.app X).hom₁ = CategoryStruct.id (F.obj X.obj₂)
        source
        @[simp]
        theorem CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₂ {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) :
        (F.mapTriangleRotateIso.hom.app X).hom₂ = CategoryStruct.id (F.obj X.obj₃)
        source
        @[simp]
        theorem CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₂ {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) :
        (F.mapTriangleRotateIso.inv.app X).hom₂ = CategoryStruct.id (F.obj X.obj₃)
        source
        noncomputable def CategoryTheory.Functor.mapTriangleInvRotateIso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] :
        F.mapTriangle.comp (Pretriangulated.invRotate D) ≅ (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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) :
          (F.mapTriangleInvRotateIso.inv.app X).hom₃ = CategoryStruct.id (F.obj X.obj₂)
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₁ {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) :
          (F.mapTriangleInvRotateIso.hom.app X).hom₂ = CategoryStruct.id (F.obj X.obj₁)
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₂ {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) :
          (F.mapTriangleInvRotateIso.inv.app X).hom₂ = CategoryStruct.id (F.obj X.obj₁)
          source
          @[simp]
          theorem CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₁ {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Preadditive C] [Preadditive D] [F.Additive] (X : Pretriangulated.Triangle C) :
          (F.mapTriangleInvRotateIso.hom.app X).hom₃ = CategoryStruct.id (F.obj X.obj₂)
          source
          def CategoryTheory.Functor.mapTriangleIdIso (C : Type u_1) [Category.{u_4, u_1} C] [HasShift C ℤ] :
          (Functor.id C).mapTriangle ≅ Functor.id (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) [Category.{u_4, u_1} C] [HasShift C ℤ] (X : Pretriangulated.Triangle C) :
            ((mapTriangleIdIso C).inv.app X).hom₂ = CategoryStruct.id X.obj₂
            source
            @[simp]
            theorem CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₃ (C : Type u_1) [Category.{u_4, u_1} C] [HasShift C ℤ] (X : Pretriangulated.Triangle C) :
            ((mapTriangleIdIso C).inv.app X).hom₃ = CategoryStruct.id X.obj₃
            source
            @[simp]
            theorem CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₂ (C : Type u_1) [Category.{u_4, u_1} C] [HasShift C ℤ] (X : Pretriangulated.Triangle C) :
            ((mapTriangleIdIso C).hom.app X).hom₂ = CategoryStruct.id X.obj₂
            source
            @[simp]
            theorem CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₁ (C : Type u_1) [Category.{u_4, u_1} C] [HasShift C ℤ] (X : Pretriangulated.Triangle C) :
            ((mapTriangleIdIso C).hom.app X).hom₁ = CategoryStruct.id X.obj₁
            source
            @[simp]
            theorem CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₁ (C : Type u_1) [Category.{u_4, u_1} C] [HasShift C ℤ] (X : Pretriangulated.Triangle C) :
            ((mapTriangleIdIso C).inv.app X).hom₁ = CategoryStruct.id X.obj₁
            source
            @[simp]
            theorem CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₃ (C : Type u_1) [Category.{u_4, u_1} C] [HasShift C ℤ] (X : Pretriangulated.Triangle C) :
            ((mapTriangleIdIso C).hom.app X).hom₃ = CategoryStruct.id X.obj₃
            source
            def CategoryTheory.Functor.mapTriangleCompIso {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] (X : Pretriangulated.Triangle C) :
              ((F.mapTriangleCompIso G).hom.app X).hom₃ = 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] (X : Pretriangulated.Triangle C) :
              ((F.mapTriangleCompIso G).inv.app X).hom₂ = 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] (X : Pretriangulated.Triangle C) :
              ((F.mapTriangleCompIso G).inv.app X).hom₁ = 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] (X : Pretriangulated.Triangle C) :
              ((F.mapTriangleCompIso G).hom.app X).hom₁ = 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] (X : Pretriangulated.Triangle C) :
              ((F.mapTriangleCompIso G).hom.app X).hom₂ = 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] (X : Pretriangulated.Triangle C) :
              ((F.mapTriangleCompIso G).inv.app X).hom₃ = CategoryStruct.id (G.obj (F.obj X.obj₃))
              source
              def CategoryTheory.Functor.mapTriangleIso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] (X : Pretriangulated.Triangle C) :
                ((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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] (X : Pretriangulated.Triangle C) :
                ((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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] (X : Pretriangulated.Triangle C) :
                ((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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] (X : Pretriangulated.Triangle C) :
                ((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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] (X : Pretriangulated.Triangle C) :
                ((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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] (X : Pretriangulated.Triangle C) :
                ((mapTriangleIso e).inv.app X).hom₃ = e.inv.app X.obj₃
                source
                class CategoryTheory.Functor.IsTriangulated {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] :
                Prop

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

                Instances
                  source
                  theorem CategoryTheory.Functor.map_distinguished {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] [F.IsTriangulated] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) :
                  F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
                  source
                  @[instance 100]
                  instance CategoryTheory.Functor.IsTriangulated.instPreservesZeroMorphisms {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] [F.IsTriangulated] :
                  F.PreservesZeroMorphisms
                  source
                  instance CategoryTheory.Functor.IsTriangulated.instPreservesLimitsOfShapeDiscreteWalkingPair {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] [F.IsTriangulated] :
                  Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
                  source
                  @[instance 100]
                  instance CategoryTheory.Functor.IsTriangulated.instAdditive {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] [F.IsTriangulated] :
                  F.Additive
                  source
                  instance CategoryTheory.Functor.IsTriangulated.instId {C : Type u_1} [Category.{u_4, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] :
                  (Functor.id C).IsTriangulated
                  source
                  instance CategoryTheory.Functor.IsTriangulated.instComp {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroObject E] [Preadditive C] [Preadditive D] [Preadditive E] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated C] [Pretriangulated D] [Pretriangulated E] [F.IsTriangulated] [G.IsTriangulated] :
                  (F.comp G).IsTriangulated
                  source
                  theorem CategoryTheory.Functor.isTriangulated_of_iso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [NatTrans.CommShift e.hom ℤ] [F₁.IsTriangulated] :
                  F₂.IsTriangulated
                  source
                  theorem CategoryTheory.Functor.isTriangulated_iff_of_iso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [HasShift C ℤ] [HasShift D ℤ] (F : Functor C D) [F.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] [F.IsTriangulated] [F.mapArrow.EssSurj] (T : Pretriangulated.Triangle D) (hT : T ∈ Pretriangulated.distinguishedTriangles) :
                  ∃ (T' : Pretriangulated.Triangle C) (_ : T' ∈ 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} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] (F : Functor C D) [F.CommShift ℤ] (G : Functor D E) [G.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroObject E] [Preadditive C] [Preadditive D] [Preadditive E] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated C] [Pretriangulated D] [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} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} E] [HasShift C ℤ] [HasShift D ℤ] [HasShift E ℤ] {F : Functor C D} [F.CommShift ℤ] {G : Functor D E} [G.CommShift ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasZeroObject E] [Preadditive C] [Preadditive D] [Preadditive E] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated C] [Pretriangulated D] [Pretriangulated E] {H : Functor C E} (e : F.comp G ≅ H) [H.CommShift ℤ] [H.IsTriangulated] [F.IsTriangulated] [F.mapArrow.EssSurj] [NatTrans.CommShift e.hom ℤ] :
                  G.IsTriangulated
                  source
                  def CategoryTheory.Triangulated.Octahedron.map {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] :
                  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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) (F : 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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁} {h₁₂ : Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂} {h₂₃ : Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁} {h₁₃ : Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles} (h : Octahedron comm h₁₂ h₂₃ h₁₃) (F : 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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [HasShift C ℤ] [HasShift D ℤ] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Preadditive C] [Preadditive D] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] [(F.mapComposableArrows 2).EssSurj] [IsTriangulated C] :
                    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.