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
@[simp]
theorem CategoryTheory.Functor.mapTriangle_map_hom₃ {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 ℤ] (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_3, u_1} C] [CategoryTheory.Category.{u_4, 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_3, u_1} C] [CategoryTheory.Category.{u_4, 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_3, u_1} C] [CategoryTheory.Category.{u_4, 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
def CategoryTheory.Functor.mapTriangle {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 ℤ] (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
    instance CategoryTheory.Functor.instFaithfulTriangleMapTriangle {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 ℤ] (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_3, u_1} C] [CategoryTheory.Category.{u_4, 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
    @[simp]
    theorem CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₁ {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 ℤ] (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_3, u_1} C] [CategoryTheory.Category.{u_4, 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_3, u_1} C] [CategoryTheory.Category.{u_4, 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_3, u_1} C] [CategoryTheory.Category.{u_4, 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_3, u_1} C] [CategoryTheory.Category.{u_4, 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_3, u_1} C] [CategoryTheory.Category.{u_4, 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 def CategoryTheory.Functor.mapTriangleCommShiftIso {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 ℤ] (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
      noncomputable instance CategoryTheory.Functor.instCommShiftTriangleMapTriangleInt {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 ℤ] (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
      @[simp]
      theorem CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₁ {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 ℤ] (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_inv_app_hom₂ {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 ℤ] (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_3, u_1} C] [CategoryTheory.Category.{u_4, 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_3, u_1} C] [CategoryTheory.Category.{u_4, 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_3, u_1} C] [CategoryTheory.Category.{u_4, 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_3, u_1} C] [CategoryTheory.Category.{u_4, 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
      def CategoryTheory.Functor.mapTriangleRotateIso {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 ℤ] (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
        class CategoryTheory.Functor.IsTriangulated {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 ℤ] (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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, 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] [self : F.IsTriangulated] (T : CategoryTheory.Pretriangulated.Triangle C) :
          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_3, u_1} C] [CategoryTheory.Category.{u_4, 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 CategoryTheory.Functor.IsTriangulated.instPreservesZeroMorphisms {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 ℤ] (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
          • ⋯ = ⋯