Verdier localizations: kernels and comparison functors

Let C be a pretriangulated category and P a class of objects. Mathlib's Verdier localization inverts the class P.trW of morphisms whose cone satisfies P. This file records the elementary facts relating P to the localization and to triangle functors, and the comparison functors between two Verdier localizations.

The statements about P.trW itself hold for arbitrary P in a pretriangulated C:

• A triangle functor F inverts P.trW exactly when it sends every object of P to zero.
• The zero objects of a pretriangulated category form a thick triangulated subcategory, so the objects killed by a triangle functor do as well.
• For P ≤ Q the identity functor is a localizer morphism from P.trW to Q.trW.

Mathlib only constructs the triangulated structure on the localization at P.trW (through the calculus of fractions and the compatibility with the triangulation) when C is triangulated and P is a triangulated subcategory. Under these hypotheses the statements above have the following consequences for Verdier quotients:

• Together with the localization universal property, the first statement says that the Verdier quotient by P is the universal triangulated category in which the objects of P vanish.
• An object becomes zero in the Verdier quotient by a thick triangulated subcategory P exactly when it belongs to P.
• If moreover Q is triangulated, then for P ≤ Q the localizer morphism induces a comparison triangle functor between the Verdier quotients by P and by Q (CategoryTheory.LocalizerMorphism.isTriangulated_localizedFunctor), compatible with the two localization functors up to natural isomorphism.
• Approximation. Let δᵢ : Xᵢ ⟶ X₀ be morphisms such that every morphism from X₀ to an object of P is killed by some δᵢ. Then every morphism L X₀ ⟶ L Y of the Verdier quotient becomes, after precomposition with some L δᵢ, the image of a morphism Xᵢ ⟶ Y, and every morphism X₀ ⟶ Y vanishing in the Verdier quotient is killed by some δᵢ. Both follow from the calculus of fractions: the denominator of a fraction out of X₀ has its cone in P.

Main definitions

• CategoryTheory.ObjectProperty.trWLocalizerMorphismOfLE: the identity functor, as a localizer morphism from P.trW to Q.trW when P ≤ Q.

Main results

• CategoryTheory.ObjectProperty.trW_isInvertedBy_iff: a triangle functor inverts P.trW if and only if it kills P.
• CategoryTheory.ObjectProperty.TrWLocalization.isZero_obj_iff: the kernel of the Verdier localization at a thick triangulated subcategory P is P.
• CategoryTheory.ObjectProperty.TrWLocalization.exists_map_comp_eq_map and CategoryTheory.ObjectProperty.TrWLocalization.exists_comp_eq_zero_of_map_eq_zero: morphisms out of an object approximated by morphisms δᵢ as above, and their kernel.

References

• J.-L. Verdier, Des catégories dérivées des catégories abéliennes, Astérisque 239 (1996), Chapitre II, §2.
• A. Neeman, Triangulated categories, Annals of Mathematics Studies 148, Princeton University Press (2001), Chapter 2.

instance CategoryTheory.ObjectProperty.instIsTriangulatedIsZero_tauCeti {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : ObjectProperty.IsTriangulated Limits.IsZero

The zero objects of a pretriangulated category form a triangulated subcategory.

theorem CategoryTheory.ObjectProperty.trW_isInvertedBy_iff {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {E : Type u_2} [Category.{v_2, u_2} E] [Limits.HasZeroObject E] [Preadditive E] [HasShift E ℤ] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated E] (F : Functor C E) [F.CommShift ℤ] [F.IsTriangulated] : P.trW.IsInvertedBy F ↔ ∀ (X : C), P X → Limits.IsZero (F.obj X)

A triangle functor inverts the morphisms whose cone lies in P if and only if it sends every object of P to a zero object. When C is triangulated and P is a triangulated subcategory, so that the localization at P.trW is triangulated, this together with the localization universal property identifies the triangle functors that factor through the Verdier quotient by P.

theorem CategoryTheory.ObjectProperty.TrWLocalization.isZero_obj {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {D : Type u_2} [Category.{v_2, u_2} D] (L : Functor C D) [L.IsLocalization P.trW] [Limits.HasZeroMorphisms D] [L.PreservesZeroMorphisms] {X : C} (hX : P X) : Limits.IsZero (L.obj X)

An object of P becomes zero in the Verdier localization at P.

theorem CategoryTheory.ObjectProperty.TrWLocalization.isZero_obj_iff {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {D : Type u_2} [Category.{v_2, u_2} D] (L : Functor C D) [L.IsLocalization P.trW] [Limits.HasZeroMorphisms D] [L.PreservesZeroMorphisms] [IsTriangulated C] [P.IsTriangulated] [P.IsStableUnderRetracts] (X : C) : Limits.IsZero (L.obj X) ↔ P X

The kernel of the Verdier localization. If P is a thick triangulated subcategory of a triangulated category, an object becomes zero in the Verdier localization at P if and only if it belongs to P.

theorem CategoryTheory.ObjectProperty.TrWLocalization.exists_map_comp_eq_map {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {D : Type u_2} [Category.{v_2, u_2} D] (L : Functor C D) [L.IsLocalization P.trW] [IsTriangulated C] [P.IsTriangulated] {ι : Type u_3} {X : ι → C} {X₀ : C} (δ : (i : ι) → X i ⟶ X₀) (H : ∀ (K : C), P K → ∀ (a : X₀ ⟶ K), ∃ (i : ι), CategoryStruct.comp (δ i) a = 0) {Y : C} (g : L.obj X₀ ⟶ L.obj Y) : ∃ (i : ι) (h : X i ⟶ Y), CategoryStruct.comp (L.map (δ i)) g = L.map h

Morphisms out of an approximated object. Let δᵢ : Xᵢ ⟶ X₀ be morphisms such that every morphism from X₀ to an object of P is killed by some δᵢ. Then every morphism L X₀ ⟶ L Y in the Verdier localization becomes, after precomposition with some L δᵢ, the image of a morphism Xᵢ ⟶ Y.

theorem CategoryTheory.ObjectProperty.TrWLocalization.exists_comp_eq_zero_of_map_eq_zero {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {D : Type u_2} [Category.{v_2, u_2} D] (L : Functor C D) [L.IsLocalization P.trW] [Limits.HasZeroMorphisms D] [L.PreservesZeroMorphisms] [IsTriangulated C] [P.IsTriangulated] {ι : Type u_3} {X : ι → C} {X₀ : C} (δ : (i : ι) → X i ⟶ X₀) (H : ∀ (K : C), P K → ∀ (a : X₀ ⟶ K), ∃ (i : ι), CategoryStruct.comp (δ i) a = 0) {Y : C} (f : X₀ ⟶ Y) (hf : L.map f = 0) : ∃ (i : ι), CategoryStruct.comp (δ i) f = 0

The kernel on an approximated object. Let δᵢ : Xᵢ ⟶ X₀ be morphisms such that every morphism from X₀ to an object of P is killed by some δᵢ. A morphism f : X₀ ⟶ Y that vanishes in the Verdier localization is killed by some δᵢ.

def CategoryTheory.ObjectProperty.trWLocalizerMorphismOfLE {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P Q : ObjectProperty C} (h : P ≤ Q) : LocalizerMorphism P.trW Q.trW

For P ≤ Q, the identity functor of C, as a morphism of localizers from the morphisms with cone in P to the morphisms with cone in Q. It induces a comparison functor between any localizations at P.trW and Q.trW; when C is triangulated and P, Q are triangulated subcategories, this is the comparison triangle functor between the Verdier quotients.

@[simp]

theorem CategoryTheory.ObjectProperty.trWLocalizerMorphismOfLE_functor {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P Q : ObjectProperty C} (h : P ≤ Q) : (trWLocalizerMorphismOfLE h).functor = Functor.id C

The localizer morphism trWLocalizerMorphismOfLE h is given by the identity functor.

@[instance_reducible]

instance CategoryTheory.ObjectProperty.instCommShiftFunctorTrWTrWLocalizerMorphismOfLEInt {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P Q : ObjectProperty C} (h : P ≤ Q) : (trWLocalizerMorphismOfLE h).functor.CommShift ℤ

The identity functor underlying trWLocalizerMorphismOfLE h commutes with the shift.

instance CategoryTheory.ObjectProperty.instIsTriangulatedFunctorTrWTrWLocalizerMorphismOfLE {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P Q : ObjectProperty C} (h : P ≤ Q) : (trWLocalizerMorphismOfLE h).functor.IsTriangulated

The identity functor underlying trWLocalizerMorphismOfLE h is a triangle functor.