Localizing subcategories

Let C be a pretriangulated category. If A and B are triangulated subcategories of C, we define predicates (typeclasses IsVerdierRightLocalizing and IsVerdierLeftLocalizing) saying that A is right B-localizing (or left B-localizing). When B is closed under isomorphisms, we show that this implies that the functor from the Verdier quotient A/(A ⊓ B) to C/B is fully faithful.

References

• Jean-Louis Verdier, Des catégories dérivées des catégories abéliennes, Proposition 2.3.5, Chapitre II

class CategoryTheory.ObjectProperty.IsVerdierRightLocalizing {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) : Prop

If A and B are triangulated subcategories of a (pre)triangulated category C (with B closed under isomorphisms), we say that A is right B-localizing if any morphism X ⟶ Y with X in B and Y in A factors through an object that is in A and B. Note that the definition does not use the (pre)triangulated structure: see isVerdierRightLocalizing_iff for a characterization which relies on it.

• fac {X Y : C} (f : X ⟶ Y) (hX : B X) (hY : A Y) : ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ CategoryStruct.comp a b = f

class CategoryTheory.ObjectProperty.IsVerdierLeftLocalizing {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) : Prop

If A and B are triangulated subcategories of a (pre)triangulated category C (with B closed under isomorphisms), we say that A is left B-localizing if any morphism X ⟶ Y with X in A and Y in B factors through an object that is in A and B. Note that the definition does not use the (pre)triangulated structure: see isVerdierLeftLocalizing_iff for a characterization which relies on it.

• fac {X Y : C} (f : X ⟶ Y) (hX : A X) (hY : B Y) : ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ CategoryStruct.comp a b = f

instance CategoryTheory.ObjectProperty.instIsVerdierRightLocalizingOppositeOpOfIsVerdierLeftLocalizing {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) [A.IsVerdierLeftLocalizing B] : A.op.IsVerdierRightLocalizing B.op

instance CategoryTheory.ObjectProperty.instIsVerdierRightLocalizingUnopOfIsVerdierLeftLocalizingOpposite {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty Cᵒᵖ) [A.IsVerdierLeftLocalizing B] : A.unop.IsVerdierRightLocalizing B.unop

instance CategoryTheory.ObjectProperty.instIsVerdierLeftLocalizingOppositeOpOfIsVerdierRightLocalizing {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) [A.IsVerdierRightLocalizing B] : A.op.IsVerdierLeftLocalizing B.op

instance CategoryTheory.ObjectProperty.instIsVerdierLeftLocalizingUnopOfIsVerdierRightLocalizingOpposite {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty Cᵒᵖ) [A.IsVerdierRightLocalizing B] : A.unop.IsVerdierLeftLocalizing B.unop

theorem CategoryTheory.ObjectProperty.isVerdierLeftLocalizing_op_iff {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) : A.op.IsVerdierLeftLocalizing B.op ↔ A.IsVerdierRightLocalizing B

theorem CategoryTheory.ObjectProperty.isVerdierRightLocalizing_op_iff {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) : A.op.IsVerdierRightLocalizing B.op ↔ A.IsVerdierLeftLocalizing B

theorem CategoryTheory.ObjectProperty.isVerdierRightLocalizing_iff {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : A.IsVerdierRightLocalizing B ↔ ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ CategoryStruct.comp s b = s'

theorem CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.fac' {C : Type u_1} [Category.{v_1, u_1} C] {A B : ObjectProperty C} [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierRightLocalizing B] {X Y : C} (s : X ⟶ Y) (hX : A X) (hs : B.trW s) : ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ CategoryStruct.comp s b = s'

theorem CategoryTheory.ObjectProperty.isVerdierLeftLocalizing_iff {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : A.IsVerdierLeftLocalizing B ↔ ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A Y → B.trW s → ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ CategoryStruct.comp a s = s'

theorem CategoryTheory.ObjectProperty.IsVerdierLeftLocalizing.fac' {C : Type u_1} [Category.{v_1, u_1} C] {A B : ObjectProperty C} [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierLeftLocalizing B] {X Y : C} (s : X ⟶ Y) (hY : A Y) (hs : B.trW s) : ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ CategoryStruct.comp a s = s'

@[implicit_reducible]

def CategoryTheory.ObjectProperty.triangulatedLocalizerMorphism {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [A.IsTriangulated] : LocalizerMorphism (B.inverseImage A.ι).trW B.trW

If A is a triangulated subcategory of a pretriangulated category C, and B : ObjectProperty C, this is the inclusion functor A.ι : A.FullSubcategory ⥤ C, considered as a localizer morphism, where C is equipped with the property of morphisms B.trW and A.FullSubcategory with the property of morphisms (B.inverseImage A.ι).trW.

Equations

• A.triangulatedLocalizerMorphism B = { functor := A.ι, map := ⋯ }

@[implicit_reducible]

instance CategoryTheory.ObjectProperty.instCommShiftFullSubcategoryFunctorTrWInverseImageιTriangulatedLocalizerMorphismInt {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [A.IsTriangulated] : (A.triangulatedLocalizerMorphism B).functor.CommShift ℤ

Equations

• A.instCommShiftFullSubcategoryFunctorTrWInverseImageιTriangulatedLocalizerMorphismInt B = A.commShiftι

instance CategoryTheory.ObjectProperty.instIsTriangulatedFullSubcategoryFunctorTrWInverseImageιTriangulatedLocalizerMorphism {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [A.IsTriangulated] : (A.triangulatedLocalizerMorphism B).functor.IsTriangulated

theorem CategoryTheory.ObjectProperty.trW_inverseImage_ι_iff {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [A.IsTriangulated] {X Y : A.FullSubcategory} (f : X ⟶ Y) : (B.inverseImage A.ι).trW f ↔ (A ⊓ B).trW f.hom

theorem CategoryTheory.ObjectProperty.inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : (B.op.inverseImage A.op.ι).trW.inverseImage A.opEquivalence.inverse = (B.inverseImage A.ι).op.trW

instance CategoryTheory.ObjectProperty.instFullLocalizedFunctorFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphism {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} D₁] [Category.{v_4, u_4} D₂] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierRightLocalizing B] (L₁ : Functor A.FullSubcategory D₁) (L₂ : Functor C D₂) [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Full

instance CategoryTheory.ObjectProperty.instAdditiveLocalizedFunctorFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphism {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} D₁] [Category.{v_4, u_4} D₂] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] (L₁ : Functor A.FullSubcategory D₁) (L₂ : Functor C D₂) [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] [Preadditive D₁] [Preadditive D₂] [L₁.Additive] [L₂.Additive] : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Additive

instance CategoryTheory.ObjectProperty.instFaithfulLocalizedFunctorFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphism {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} D₁] [Category.{v_4, u_4} D₂] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierRightLocalizing B] (L₁ : Functor A.FullSubcategory D₁) (L₂ : Functor C D₂) [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful

instance CategoryTheory.ObjectProperty.instIsLocalizedFullyFaithfulFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphismOfIsVerdierRightLocalizing {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierRightLocalizing B] : (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful

instance CategoryTheory.ObjectProperty.instIsLocalizedFullyFaithfulFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphismOfIsVerdierLeftLocalizing {C : Type u_1} [Category.{v_1, u_1} C] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierLeftLocalizing B] : (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful

instance CategoryTheory.ObjectProperty.instAdditiveLocalizedFunctorFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphismOfIsVerdierLeftLocalizing {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} D₁] [Category.{v_4, u_4} D₂] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] (L₁ : Functor A.FullSubcategory D₁) (L₂ : Functor C D₂) [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] [A.IsVerdierLeftLocalizing B] [Preadditive D₁] [Preadditive D₂] [L₁.Additive] [L₂.Additive] : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Additive

noncomputable def CategoryTheory.ObjectProperty.IsVerdierLeftLocalizing.fullyFaithful {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} D₁] [Category.{v_4, u_4} D₂] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierLeftLocalizing B] {L₁ : Functor A.FullSubcategory D₁} {L₂ : Functor C D₂} {F : Functor D₁ D₂} [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] (e : L₁.comp F ≅ A.ι.comp L₂) : F.FullyFaithful

If A is a left B-localizing triangulated subcategory in the sense of Verdier, then the induced functor between the localizations with respect to (B.inverseImage A.ι).trW and B.trW is fully faithful.

Equations

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

noncomputable def CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.fullyFaithful {C : Type u_1} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} D₁] [Category.{v_4, u_4} D₂] (A B : ObjectProperty C) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierRightLocalizing B] {L₁ : Functor A.FullSubcategory D₁} {L₂ : Functor C D₂} {F : Functor D₁ D₂} [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW] (e : L₁.comp F ≅ A.ι.comp L₂) : F.FullyFaithful

If A is a right B-localizing triangulated subcategory in the sense of Verdier, then the induced functor between the localizations with respect to (B.inverseImage A.ι).trW and B.trW is fully faithful.

Equations

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