Localization of triangulated categories

If L : C ⥤ D is a localization functor for a class of morphisms W that is compatible with the triangulation on the category C and admits a left calculus of fractions, it is shown in this file that D can be equipped with a pretriangulated category structure, and that it is triangulated.

References

• [Jean-Louis Verdier, Des catégories dérivées des catégories abéliennes][verdier1996]

class CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (W : CategoryTheory.MorphismProperty C) extends W.IsCompatibleWithShift ℤ : Prop

Given W is a class of morphisms in a pretriangulated category C, this is the condition that W is compatible with the triangulation on C.

• condition : ∀ (a : ℤ), W.inverseImage (CategoryTheory.shiftFunctor C a) = W
• compatible_with_triangulation : ∀ (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C), T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂), W a → W b → CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ → ∃ (c : T₁.obj₃ ⟶ T₂.obj₃) (_ : W c), CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧ CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃

def CategoryTheory.Functor.essImageDistTriang {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] : Set (CategoryTheory.Pretriangulated.Triangle D)

Given a functor C ⥤ D from a pretriangulated category, this is the set of triangles in D that are in the essential image of distinguished triangles of C.

Equations

• L.essImageDistTriang T = ∃ (T' : CategoryTheory.Pretriangulated.Triangle C) (x : T ≅ L.mapTriangle.obj T'), T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

theorem CategoryTheory.Functor.essImageDistTriang_mem_of_iso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle D} (e : T₂ ≅ T₁) (h : T₁ ∈ L.essImageDistTriang) : T₂ ∈ L.essImageDistTriang

theorem CategoryTheory.Functor.contractible_mem_essImageDistTriang {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] [L.EssSurj] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] [L.PreservesZeroMorphisms] (X : D) : CategoryTheory.Pretriangulated.contractibleTriangle X ∈ L.essImageDistTriang

theorem CategoryTheory.Functor.rotate_essImageDistTriang {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] [CategoryTheory.Preadditive D] [L.Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] (T : CategoryTheory.Pretriangulated.Triangle D) : T ∈ L.essImageDistTriang ↔ T.rotate ∈ L.essImageDistTriang

theorem CategoryTheory.Functor.complete_distinguished_essImageDistTriang_morphism {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] (H : ∀ (T₁' T₂' : CategoryTheory.Pretriangulated.Triangle C), T₁' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → T₂' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂), CategoryTheory.CategoryStruct.comp (L.map T₁'.mor₁) b = CategoryTheory.CategoryStruct.comp a (L.map T₂'.mor₁) → ∃ (φ : L.mapTriangle.obj T₁' ⟶ L.mapTriangle.obj T₂'), φ.hom₁ = a ∧ φ.hom₂ = b) (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle D) (hT₁ : T₁ ∈ L.essImageDistTriang) (hT₂ : T₂ ∈ L.essImageDistTriang) (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (fac : CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁) : ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧ CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor D 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃

theorem CategoryTheory.Triangulated.Localization.distinguished_cocone_triangle {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : D} (f : X ⟶ Y) : ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor D 1).obj X), CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ L.essImageDistTriang

theorem CategoryTheory.Triangulated.Localization.complete_distinguished_triangle_morphism {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle D) (hT₁ : T₁ ∈ L.essImageDistTriang) (hT₂ : T₂ ∈ L.essImageDistTriang) (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (fac : CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁) : ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧ CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor D 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃

def CategoryTheory.Triangulated.Localization.pretriangulated {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [L.Additive] : CategoryTheory.Pretriangulated D

The pretriangulated structure on the localized category.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Triangulated.Localization.isTriangulated_functor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [L.Additive] : L.IsTriangulated

Equations

• ⋯ = ⋯

theorem CategoryTheory.Triangulated.Localization.isTriangulated {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [L.IsTriangulated] [CategoryTheory.IsTriangulated C] : CategoryTheory.IsTriangulated D

instance CategoryTheory.Triangulated.Localization.instAdditiveLocalizationShiftFunctorInt {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] (n : ℤ) : (CategoryTheory.shiftFunctor W.Localization n).Additive

Equations

• ⋯ = ⋯

instance CategoryTheory.Triangulated.Localization.instPretriangulatedLocalization {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] : CategoryTheory.Pretriangulated W.Localization

Equations

• CategoryTheory.Triangulated.Localization.instPretriangulatedLocalization W = CategoryTheory.Triangulated.Localization.pretriangulated W.Q W

instance CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] [CategoryTheory.IsTriangulated C] : CategoryTheory.IsTriangulated W.Localization

Equations

• ⋯ = ⋯

instance CategoryTheory.Triangulated.Localization.instAdditiveLocalization'ShiftFunctorInt {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] [W.HasLocalization] (n : ℤ) : (CategoryTheory.shiftFunctor W.Localization' n).Additive

Equations

• ⋯ = ⋯

instance CategoryTheory.Triangulated.Localization.instPretriangulatedLocalization' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] [W.HasLocalization] : CategoryTheory.Pretriangulated W.Localization'

Equations

• CategoryTheory.Triangulated.Localization.instPretriangulatedLocalization' W = CategoryTheory.Triangulated.Localization.pretriangulated W.Q' W

instance CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] [W.HasLocalization] [CategoryTheory.IsTriangulated C] : CategoryTheory.IsTriangulated W.Localization'

Equations

• ⋯ = ⋯

theorem CategoryTheory.Functor.distTriang_iff {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [L.mapArrow.EssSurj] [L.IsTriangulated] (T : CategoryTheory.Pretriangulated.Triangle D) : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ T ∈ L.essImageDistTriang