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

class CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (W : 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 (shiftFunctor C a) = W
• compatible_with_triangulation (T₁ T₂ : Pretriangulated.Triangle C) : T₁ ∈ Pretriangulated.distinguishedTriangles → T₂ ∈ Pretriangulated.distinguishedTriangles → ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂), W a → W b → CategoryStruct.comp T₁.mor₁ b = CategoryStruct.comp a T₂.mor₁ → ∃ (c : T₁.obj₃ ⟶ T₂.obj₃) (_ : W c), CategoryStruct.comp T₁.mor₂ c = CategoryStruct.comp b T₂.mor₂ ∧ CategoryStruct.comp T₁.mor₃ (a⟦1⟧') = CategoryStruct.comp c T₂.mor₃

def CategoryTheory.Functor.essImageDistTriang {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HasShift D ℤ] [L.CommShift ℤ] : Set (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

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

theorem CategoryTheory.Functor.essImageDistTriang_mem_of_iso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HasShift D ℤ] [L.CommShift ℤ] {T₁ T₂ : 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} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HasShift D ℤ] [L.CommShift ℤ] [L.EssSurj] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms D] [L.PreservesZeroMorphisms] (X : D) : Pretriangulated.contractibleTriangle X ∈ L.essImageDistTriang

theorem CategoryTheory.Functor.rotate_essImageDistTriang {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HasShift D ℤ] [L.CommShift ℤ] [Preadditive D] [L.Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] (T : 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} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HasShift D ℤ] [L.CommShift ℤ] (H : ∀ (T₁' T₂' : Pretriangulated.Triangle C), T₁' ∈ Pretriangulated.distinguishedTriangles → T₂' ∈ Pretriangulated.distinguishedTriangles → ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂), CategoryStruct.comp (L.map T₁'.mor₁) b = CategoryStruct.comp a (L.map T₂'.mor₁) → ∃ (φ : L.mapTriangle.obj T₁' ⟶ L.mapTriangle.obj T₂'), φ.hom₁ = a ∧ φ.hom₂ = b) (T₁ T₂ : Pretriangulated.Triangle D) (hT₁ : T₁ ∈ L.essImageDistTriang) (hT₂ : T₂ ∈ L.essImageDistTriang) (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (fac : CategoryStruct.comp T₁.mor₁ b = CategoryStruct.comp a T₂.mor₁) : ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), CategoryStruct.comp T₁.mor₂ c = CategoryStruct.comp b T₂.mor₂ ∧ CategoryStruct.comp T₁.mor₃ (a⟦1⟧') = CategoryStruct.comp c T₂.mor₃

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

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

@[instance_reducible]

def CategoryTheory.Triangulated.Localization.pretriangulated {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HasShift D ℤ] [L.CommShift ℤ] (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] [Limits.HasZeroObject D] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [L.Additive] : 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} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (L : Functor C D) [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [HasShift D ℤ] [L.CommShift ℤ] (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] [Limits.HasZeroObject D] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [L.Additive] : L.IsTriangulated

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

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

@[instance_reducible]

noncomputable instance CategoryTheory.Triangulated.Localization.instPretriangulatedLocalization {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (W : MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] : 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} [Category.{v_1, u_1} C] [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (W : MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] [IsTriangulated C] : IsTriangulated W.Localization

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

@[instance_reducible]

noncomputable instance CategoryTheory.Triangulated.Localization.instPretriangulatedLocalization' {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (W : MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] [W.HasLocalization] : 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} [Category.{v_1, u_1} C] [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (W : MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] [W.HasLocalization] [IsTriangulated C] : IsTriangulated W.Localization'

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