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) [CategoryTheory.Functor.CommShift F ℤ] :
∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Functor.mapTriangle F).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) [CategoryTheory.Functor.CommShift F ℤ] :
∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Functor.mapTriangle F).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) [CategoryTheory.Functor.CommShift F ℤ] :
∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Functor.mapTriangle F).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) [CategoryTheory.Functor.CommShift F ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) :
(CategoryTheory.Functor.mapTriangle F).obj T = CategoryTheory.Pretriangulated.Triangle.mk (F.map T.mor₁) (F.map T.mor₂) (CategoryTheory.CategoryStruct.comp (F.map T.mor₃) ((CategoryTheory.Functor.commShiftIso F 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) [CategoryTheory.Functor.CommShift F ℤ] :
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.instFaithfulTriangleTriangleCategoryTriangleTriangleCategoryMapTriangle {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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Faithful F] :
    CategoryTheory.Faithful (CategoryTheory.Functor.mapTriangle F)
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.Functor.instFullTriangleTriangleCategoryTriangleTriangleCategoryMapTriangle {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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Full F] [CategoryTheory.Faithful F] :
    CategoryTheory.Full (CategoryTheory.Functor.mapTriangle F)
    Equations
    • One or more equations did not get rendered due to their size.
    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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] (n : ℤ) (X : CategoryTheory.Pretriangulated.Triangle C) :
    ((CategoryTheory.Functor.mapTriangleCommShiftIso F n).hom.app X).hom₃ = (CategoryTheory.Functor.commShiftIso F 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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] (n : ℤ) (X : CategoryTheory.Pretriangulated.Triangle C) :
    ((CategoryTheory.Functor.mapTriangleCommShiftIso F n).inv.app X).hom₂ = (CategoryTheory.Functor.commShiftIso F 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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] (n : ℤ) (X : CategoryTheory.Pretriangulated.Triangle C) :
    ((CategoryTheory.Functor.mapTriangleCommShiftIso F n).hom.app X).hom₂ = (CategoryTheory.Functor.commShiftIso F 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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] (n : ℤ) (X : CategoryTheory.Pretriangulated.Triangle C) :
    ((CategoryTheory.Functor.mapTriangleCommShiftIso F n).inv.app X).hom₃ = (CategoryTheory.Functor.commShiftIso F 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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] (n : ℤ) (X : CategoryTheory.Pretriangulated.Triangle C) :
    ((CategoryTheory.Functor.mapTriangleCommShiftIso F n).hom.app X).hom₁ = (CategoryTheory.Functor.commShiftIso F 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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] (n : ℤ) (X : CategoryTheory.Pretriangulated.Triangle C) :
    ((CategoryTheory.Functor.mapTriangleCommShiftIso F n).inv.app X).hom₁ = (CategoryTheory.Functor.commShiftIso F n).inv.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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] (n : ℤ) :
    CategoryTheory.Functor.comp (CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n) (CategoryTheory.Functor.mapTriangle F) ≅ CategoryTheory.Functor.comp (CategoryTheory.Functor.mapTriangle F) (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.instCommShiftTriangleTriangleTriangleCategoryTriangleCategoryMapTriangleIntInstAddMonoidIntInstHasShiftTriangleIntTriangleCategoryInstAddMonoidIntInstHasShiftTriangleIntTriangleCategoryInstAddMonoidInt {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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor D n)] :
      CategoryTheory.Functor.CommShift (CategoryTheory.Functor.mapTriangle F) ℤ
      Equations
      • One or more equations did not get rendered due to their size.
      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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((CategoryTheory.Functor.mapTriangleRotateIso F).hom.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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((CategoryTheory.Functor.mapTriangleRotateIso F).hom.app X).hom₃ = (CategoryTheory.Functor.commShiftIso F 1).inv.app 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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((CategoryTheory.Functor.mapTriangleRotateIso F).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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((CategoryTheory.Functor.mapTriangleRotateIso F).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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((CategoryTheory.Functor.mapTriangleRotateIso F).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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] (X : CategoryTheory.Pretriangulated.Triangle C) :
      ((CategoryTheory.Functor.mapTriangleRotateIso F).inv.app X).hom₃ = (CategoryTheory.Functor.commShiftIso F 1).hom.app 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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Functor.Additive F] :
      CategoryTheory.Functor.comp (CategoryTheory.Functor.mapTriangle F) (CategoryTheory.Pretriangulated.rotate D) ≅ CategoryTheory.Functor.comp (CategoryTheory.Pretriangulated.rotate C) (CategoryTheory.Functor.mapTriangle F)

      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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor D n)] [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, (CategoryTheory.Functor.mapTriangle F).obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
        Instances
          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) [CategoryTheory.Functor.CommShift F ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C n)] [∀ (n : ℤ), CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor D n)] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [CategoryTheory.Functor.IsTriangulated F] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) :
          (CategoryTheory.Functor.mapTriangle F).obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles