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}
[Category.{u_3, u_1} C]
[HasShift C ℤ]
[Preadditive C]
[Limits.HasZeroObject C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
(W : MorphismProperty C)
extends W.IsCompatibleWithShift ℤ :
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.
- 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₃ ((shiftFunctor C 1).map a) = CategoryStruct.comp c T₂.mor₃
Instances
def
CategoryTheory.Functor.essImageDistTriang
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, 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 ℤ]
:
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
Instances For
theorem
CategoryTheory.Functor.essImageDistTriang_mem_of_iso
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, 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)
:
theorem
CategoryTheory.Functor.contractible_mem_essImageDistTriang
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, 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)
:
theorem
CategoryTheory.Functor.rotate_essImageDistTriang
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, 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)
:
theorem
CategoryTheory.Functor.complete_distinguished_essImageDistTriang_morphism
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, 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₃
theorem
CategoryTheory.Triangulated.Localization.distinguished_cocone_triangle
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, 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
theorem
CategoryTheory.Triangulated.Localization.complete_distinguished_triangle_morphism
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, 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₃
def
CategoryTheory.Triangulated.Localization.pretriangulated
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, 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]
:
The pretriangulated structure on the localized category.
Equations
Instances For
instance
CategoryTheory.Triangulated.Localization.isTriangulated_functor
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, 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]
:
theorem
CategoryTheory.Triangulated.Localization.isTriangulated
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, 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]
:
instance
CategoryTheory.Triangulated.Localization.instAdditiveLocalizationShiftFunctorInt
{C : Type u_1}
[Category.{u_3, 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
noncomputable instance
CategoryTheory.Triangulated.Localization.instPretriangulatedLocalization
{C : Type u_1}
[Category.{u_3, u_1} C]
[HasShift C ℤ]
[Preadditive C]
[Limits.HasZeroObject C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
(W : MorphismProperty C)
[W.HasLeftCalculusOfFractions]
[W.IsCompatibleWithTriangulation]
:
Equations
instance
CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization
{C : Type u_1}
[Category.{u_3, 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]
:
instance
CategoryTheory.Triangulated.Localization.instAdditiveLocalization'ShiftFunctorInt
{C : Type u_1}
[Category.{u_4, 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 : ℤ)
:
noncomputable instance
CategoryTheory.Triangulated.Localization.instPretriangulatedLocalization'
{C : Type u_1}
[Category.{u_3, 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]
:
Equations
instance
CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization'
{C : Type u_1}
[Category.{u_3, 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]
:
theorem
CategoryTheory.Functor.distTriang_iff
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, 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)
: