Documentation

Mathlib.CategoryTheory.Localization.Triangulated

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 #

source
🔶 coverage
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.

Instances
    source
    🔸 coverage
    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.

    Instances For
      source
      📐 coverage
      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
      source
      📐 coverage
      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
      source
      📐 coverage
      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
      source
      📐 coverage
      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₃ ((shiftFunctor D 1).map a) = CategoryStruct.comp c T₂.mor₃
      source
      📐 coverage
      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 ⟶ (shiftFunctor D 1).obj X), Pretriangulated.Triangle.mk f g h ∈ L.essImageDistTriang
      source
      📐 coverage
      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₃ ((shiftFunctor D 1).map a) = CategoryStruct.comp c T₂.mor₃
      source
      🔸 coverage
      @[implicit_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.

      Instances For
        source
        📐 coverage
        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
        source
        📐 coverage
        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
        source
        📐 coverage
        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
        source
        🔸 coverage
        @[implicit_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
        source
        📐 coverage
        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
        source
        📐 coverage
        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
        source
        🔸 coverage
        @[implicit_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'
        source
        📐 coverage
        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'
        source
        📐 coverage
        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