mathlib documentation

category_theory.triangulated.pretriangulated

Pretriangulated Categories #

This file contains the definition of pretriangulated categories and triangulated functors between them.

Implementation Notes #

We work under the assumption that pretriangulated categories are preadditive categories, but not necessarily additive categories, as is assumed in some sources.

TODO: generalise this to n-angulated categories as in https://arxiv.org/abs/1006.4592

@[class]

structure category_theory.triangulated.pretriangulated (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] :

Type (max u v)

distinguished_triangles : set (category_theory.triangulated.triangle C)
isomorphic_distinguished : ∀ (T₁ : category_theory.triangulated.triangle C), (T₁ ∈ dist_triang C) → ∀ (T₂ : category_theory.triangulated.triangle C), (T₂ ≅ T₁) → (T₂ ∈ dist_triang C)
contractible_distinguished : ∀ (X : C), category_theory.triangulated.contractible_triangle C X ∈ dist_triang C
distinguished_cocone_triangle : ∀ (X Y : C) (f : X ⟶ Y), ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ (category_theory.shift_functor C 1).obj X), category_theory.triangulated.triangle.mk C f g h ∈ dist_triang C
rotate_distinguished_triangle : ∀ (T : category_theory.triangulated.triangle C), (T ∈ dist_triang C) ↔ T.rotate ∈ dist_triang C
complete_distinguished_triangle_morphism : ∀ (T₁ T₂ : category_theory.triangulated.triangle C), (T₁ ∈ dist_triang C) → (T₂ ∈ dist_triang C) → ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂), T₁.mor₁ ≫ b = a ≫ T₂.mor₁ → (∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (category_theory.shift_functor C 1).map a = c ≫ T₂.mor₃)

A preadditive category C with an additive shift, and a class of "distinguished triangles" relative to that shift is called pretriangulated if the following hold:

Any triangle that is isomorphic to a distinguished triangle is also distinguished.
Any triangle of the form (X,X,0,id,0,0) is distinguished.
For any morphism f : X ⟶ Y there exists a distinguished triangle of the form (X,Y,Z,f,g,h).
The triangle (X,Y,Z,f,g,h) is distinguished if and only if (Y,Z,X⟦1⟧,g,h,-f⟦1⟧) is.

Given a diagram:

      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
  │       │                │
  │a      │b               │a⟦1⟧'
  V       V                V
  X' ───> Y' ───> Z' ───> X'⟦1⟧
      f'      g'      h'

where the left square commutes, and whose rows are distinguished triangles, there exists a morphism c : Z ⟶ Z' such that (a,b,c) is a triangle morphism.

See https://stacks.math.columbia.edu/tag/0145

Instances for category_theory.triangulated.pretriangulated

category_theory.triangulated.pretriangulated.has_sizeof_inst

theorem category_theory.triangulated.pretriangulated.rot_of_dist_triangle (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] [category_theory.triangulated.pretriangulated C] (T : category_theory.triangulated.triangle C) (H : T ∈ dist_triang C) :

T.rotate ∈ dist_triang C

Given any distinguished triangle T, then we know T.rotate is also distinguished.

theorem category_theory.triangulated.pretriangulated.inv_rot_of_dist_triangle (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] [category_theory.triangulated.pretriangulated C] (T : category_theory.triangulated.triangle C) (H : T ∈ dist_triang C) :

T.inv_rotate ∈ dist_triang C

Given any distinguished triangle T, then we know T.inv_rotate is also distinguished.

theorem category_theory.triangulated.pretriangulated.comp_dist_triangle_mor_zero₁₂ (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] [category_theory.triangulated.pretriangulated C] (T : category_theory.triangulated.triangle C) (H : T ∈ dist_triang C) :

T.mor₁ ≫ T.mor₂ = 0

Given any distinguished triangle

      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧

the composition f ≫ g = 0. See https://stacks.math.columbia.edu/tag/0146

theorem category_theory.triangulated.pretriangulated.comp_dist_triangle_mor_zero₂₃ (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] [category_theory.triangulated.pretriangulated C] (T : category_theory.triangulated.triangle C) (H : T ∈ dist_triang C) :

T.mor₂ ≫ T.mor₃ = 0

Given any distinguished triangle

      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧

the composition g ≫ h = 0. See https://stacks.math.columbia.edu/tag/0146

theorem category_theory.triangulated.pretriangulated.comp_dist_triangle_mor_zero₃₁ (C : Type u) [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] [category_theory.triangulated.pretriangulated C] (T : category_theory.triangulated.triangle C) (H : T ∈ dist_triang C) :

T.mor₃ ≫ (category_theory.shift_equiv C 1).functor.map T.mor₁ = 0

Given any distinguished triangle

      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧

the composition h ≫ f⟦1⟧ = 0. See https://stacks.math.columbia.edu/tag/0146

structure category_theory.triangulated.pretriangulated.triangulated_functor_struct (C : Type u₁) [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (D : Type u₂) [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] :

Type (max u₁ u₂ v₁ v₂)

to_functor : C ⥤ D
comm_shift : category_theory.shift_functor C 1 ⋙ self.to_functor ≅ self.to_functor ⋙ category_theory.shift_functor D 1

The underlying structure of a triangulated functor between pretriangulated categories C and D is a functor F : C ⥤ D together with given functorial isomorphisms ξ X : F(X⟦1⟧) ⟶ F(X)⟦1⟧.

Instances for category_theory.triangulated.pretriangulated.triangulated_functor_struct

category_theory.triangulated.pretriangulated.triangulated_functor_struct.has_sizeof_inst
category_theory.triangulated.pretriangulated.triangulated_functor_struct.inhabited

def category_theory.triangulated.pretriangulated.triangulated_functor_struct.id (C : Type u₁) [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] :

category_theory.triangulated.pretriangulated.triangulated_functor_struct C C

The identity triangulated_functor_struct.

Equations

category_theory.triangulated.pretriangulated.triangulated_functor_struct.id C = {to_functor := {obj := λ (X : C), X, map := λ (_x _x_1 : C) (f : _x ⟶ _x_1), f, map_id' := _, map_comp' := _}, comm_shift := category_theory.iso.refl (category_theory.shift_functor C 1 ⋙ {obj := λ (X : C), X, map := λ (_x _x_1 : C) (f : _x ⟶ _x_1), f, map_id' := _, map_comp' := _})}

@[protected, instance]

def category_theory.triangulated.pretriangulated.triangulated_functor_struct.inhabited (C : Type u₁) [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] :

inhabited (category_theory.triangulated.pretriangulated.triangulated_functor_struct C C)

Equations

category_theory.triangulated.pretriangulated.triangulated_functor_struct.inhabited C = {default := category_theory.triangulated.pretriangulated.triangulated_functor_struct.id C _}

@[simp]

theorem category_theory.triangulated.pretriangulated.triangulated_functor_struct.map_triangle_map_hom₂ {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] (F : category_theory.triangulated.pretriangulated.triangulated_functor_struct C D) (S T : category_theory.triangulated.triangle C) (f : S ⟶ T) :

(F.map_triangle.map f).hom₂ = F.to_functor.map f.hom₂

def category_theory.triangulated.pretriangulated.triangulated_functor_struct.map_triangle {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] (F : category_theory.triangulated.pretriangulated.triangulated_functor_struct C D) :

category_theory.triangulated.triangle C ⥤ category_theory.triangulated.triangle D

Given a triangulated_functor_struct we can define a functor from triangles of C to triangles of D.

Equations

F.map_triangle = {obj := λ (T : category_theory.triangulated.triangle C), category_theory.triangulated.triangle.mk D (F.to_functor.map T.mor₁) (F.to_functor.map T.mor₂) (F.to_functor.map T.mor₃ ≫ F.comm_shift.hom.app T.obj₁), map := λ (S T : category_theory.triangulated.triangle C) (f : S ⟶ T), {hom₁ := F.to_functor.map f.hom₁, hom₂ := F.to_functor.map f.hom₂, hom₃ := F.to_functor.map f.hom₃, comm₁' := _, comm₂' := _, comm₃' := _}, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.triangulated.pretriangulated.triangulated_functor_struct.map_triangle_map_hom₁ {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] (F : category_theory.triangulated.pretriangulated.triangulated_functor_struct C D) (S T : category_theory.triangulated.triangle C) (f : S ⟶ T) :

(F.map_triangle.map f).hom₁ = F.to_functor.map f.hom₁

@[simp]

theorem category_theory.triangulated.pretriangulated.triangulated_functor_struct.map_triangle_map_hom₃ {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] (F : category_theory.triangulated.pretriangulated.triangulated_functor_struct C D) (S T : category_theory.triangulated.triangle C) (f : S ⟶ T) :

(F.map_triangle.map f).hom₃ = F.to_functor.map f.hom₃

@[simp]

theorem category_theory.triangulated.pretriangulated.triangulated_functor_struct.map_triangle_obj {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] (F : category_theory.triangulated.pretriangulated.triangulated_functor_struct C D) (T : category_theory.triangulated.triangle C) :

F.map_triangle.obj T = category_theory.triangulated.triangle.mk D (F.to_functor.map T.mor₁) (F.to_functor.map T.mor₂) (F.to_functor.map T.mor₃ ≫ F.comm_shift.hom.app T.obj₁)

structure category_theory.triangulated.pretriangulated.triangulated_functor (C : Type u₁) [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] (D : Type u₂) [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] [category_theory.triangulated.pretriangulated C] [category_theory.triangulated.pretriangulated D] :

Type (max u₁ u₂ v₁ v₂)

to_triangulated_functor_struct : category_theory.triangulated.pretriangulated.triangulated_functor_struct C D
map_distinguished' : ∀ (T : category_theory.triangulated.triangle C), (T ∈ dist_triang C) → (self.to_triangulated_functor_struct.map_triangle.obj T ∈ dist_triang D)

A triangulated functor between pretriangulated categories C and D is a functor F : C ⥤ D together with given functorial isomorphisms ξ X : F(X⟦1⟧) ⟶ F(X)⟦1⟧ such that for every distinguished triangle (X,Y,Z,f,g,h) of C, the triangle (F(X), F(Y), F(Z), F(f), F(g), F(h) ≫ (ξ X)) is a distinguished triangle of D. See https://stacks.math.columbia.edu/tag/014V

Instances for category_theory.triangulated.pretriangulated.triangulated_functor

category_theory.triangulated.pretriangulated.triangulated_functor.has_sizeof_inst
category_theory.triangulated.pretriangulated.triangulated_functor.inhabited

@[protected, instance]

def category_theory.triangulated.pretriangulated.triangulated_functor.inhabited (C : Type u₁) [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] [category_theory.triangulated.pretriangulated C] :

inhabited (category_theory.triangulated.pretriangulated.triangulated_functor C C)

Equations

category_theory.triangulated.pretriangulated.triangulated_functor.inhabited C = {default := {to_triangulated_functor_struct := {to_functor := {obj := λ (X : C), X, map := λ (_x _x_1 : C) (f : _x ⟶ _x_1), f, map_id' := _, map_comp' := _}, comm_shift := category_theory.iso.refl (category_theory.shift_functor C 1 ⋙ {obj := λ (X : C), X, map := λ (_x _x_1 : C) (f : _x ⟶ _x_1), f, map_id' := _, map_comp' := _})}, map_distinguished' := _}}

@[simp]

theorem category_theory.triangulated.pretriangulated.triangulated_functor.map_triangle_map_hom₁ {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] [category_theory.triangulated.pretriangulated C] [category_theory.triangulated.pretriangulated D] (F : category_theory.triangulated.pretriangulated.triangulated_functor C D) (S T : category_theory.triangulated.triangle C) (f : S ⟶ T) :

(F.map_triangle.map f).hom₁ = F.to_triangulated_functor_struct.to_functor.map f.hom₁

@[simp]

theorem category_theory.triangulated.pretriangulated.triangulated_functor.map_triangle_obj_mor₁ {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] [category_theory.triangulated.pretriangulated C] [category_theory.triangulated.pretriangulated D] (F : category_theory.triangulated.pretriangulated.triangulated_functor C D) (T : category_theory.triangulated.triangle C) :

(F.map_triangle.obj T).mor₁ = F.to_triangulated_functor_struct.to_functor.map T.mor₁

def category_theory.triangulated.pretriangulated.triangulated_functor.map_triangle {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] [category_theory.triangulated.pretriangulated C] [category_theory.triangulated.pretriangulated D] (F : category_theory.triangulated.pretriangulated.triangulated_functor C D) :

category_theory.triangulated.triangle C ⥤ category_theory.triangulated.triangle D

Given a triangulated_functor we can define a functor from triangles of C to triangles of D.

Equations

F.map_triangle = F.to_triangulated_functor_struct.map_triangle

@[simp]

theorem category_theory.triangulated.pretriangulated.triangulated_functor.map_triangle_obj_mor₂ {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] [category_theory.triangulated.pretriangulated C] [category_theory.triangulated.pretriangulated D] (F : category_theory.triangulated.pretriangulated.triangulated_functor C D) (T : category_theory.triangulated.triangle C) :

(F.map_triangle.obj T).mor₂ = F.to_triangulated_functor_struct.to_functor.map T.mor₂

@[simp]

theorem category_theory.triangulated.pretriangulated.triangulated_functor.map_triangle_obj_mor₃ {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] [category_theory.triangulated.pretriangulated C] [category_theory.triangulated.pretriangulated D] (F : category_theory.triangulated.pretriangulated.triangulated_functor C D) (T : category_theory.triangulated.triangle C) :

(F.map_triangle.obj T).mor₃ = F.to_triangulated_functor_struct.to_functor.map T.mor₃ ≫ F.to_triangulated_functor_struct.comm_shift.hom.app T.obj₁

@[simp]

theorem category_theory.triangulated.pretriangulated.triangulated_functor.map_triangle_map_hom₂ {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] [category_theory.triangulated.pretriangulated C] [category_theory.triangulated.pretriangulated D] (F : category_theory.triangulated.pretriangulated.triangulated_functor C D) (S T : category_theory.triangulated.triangle C) (f : S ⟶ T) :

(F.map_triangle.map f).hom₂ = F.to_triangulated_functor_struct.to_functor.map f.hom₂

@[simp]

theorem category_theory.triangulated.pretriangulated.triangulated_functor.map_triangle_map_hom₃ {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] [category_theory.triangulated.pretriangulated C] [category_theory.triangulated.pretriangulated D] (F : category_theory.triangulated.pretriangulated.triangulated_functor C D) (S T : category_theory.triangulated.triangle C) (f : S ⟶ T) :

(F.map_triangle.map f).hom₃ = F.to_triangulated_functor_struct.to_functor.map f.hom₃

@[simp]

theorem category_theory.triangulated.pretriangulated.triangulated_functor.map_triangle_obj_obj₃ {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] [category_theory.triangulated.pretriangulated C] [category_theory.triangulated.pretriangulated D] (F : category_theory.triangulated.pretriangulated.triangulated_functor C D) (T : category_theory.triangulated.triangle C) :

(F.map_triangle.obj T).obj₃ = F.to_triangulated_functor_struct.to_functor.obj T.obj₃

@[simp]

theorem category_theory.triangulated.pretriangulated.triangulated_functor.map_triangle_obj_obj₂ {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] [category_theory.triangulated.pretriangulated C] [category_theory.triangulated.pretriangulated D] (F : category_theory.triangulated.pretriangulated.triangulated_functor C D) (T : category_theory.triangulated.triangle C) :

(F.map_triangle.obj T).obj₂ = F.to_triangulated_functor_struct.to_functor.obj T.obj₂

@[simp]

theorem category_theory.triangulated.pretriangulated.triangulated_functor.map_triangle_obj_obj₁ {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] [category_theory.triangulated.pretriangulated C] [category_theory.triangulated.pretriangulated D] (F : category_theory.triangulated.pretriangulated.triangulated_functor C D) (T : category_theory.triangulated.triangle C) :

(F.map_triangle.obj T).obj₁ = F.to_triangulated_functor_struct.to_functor.obj T.obj₁

theorem category_theory.triangulated.pretriangulated.triangulated_functor.map_distinguished {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.has_shift C ℤ] [category_theory.preadditive C] [∀ (n : ℤ), (category_theory.shift_functor C n).additive] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_zero_object D] [category_theory.has_shift D ℤ] [category_theory.preadditive D] [∀ (n : ℤ), (category_theory.shift_functor D n).additive] [category_theory.triangulated.pretriangulated C] [category_theory.triangulated.pretriangulated D] (F : category_theory.triangulated.pretriangulated.triangulated_functor C D) (T : category_theory.triangulated.triangle C) (h : T ∈ dist_triang C) :

F.map_triangle.obj T ∈ dist_triang D

Given a triangulated_functor and a distinguished triangle T of C, then the triangle it maps onto in D is also distinguished.