The singularity category

The singularity category of an abelian category C is the Verdier quotient

D_sg(C) = Dᵇ(C) / Perf(C)

of the bounded derived category by its perfect objects. Here Perf(C) is the thick subcategory generated by the projective objects of C, viewed as complexes concentrated in degree zero: the smallest triangulated subcategory closed under retracts that contains them, ObjectProperty.triangEnvelope. Every bounded complex of projective objects is perfect (TauCeti.DerivedCategory.Bounded.perfect_Qh_obj_quotient_obj). When C has enough projectives, the perfect objects are exactly those represented by bounded complexes of projectives; that converse is not proved here. The quotient is the localization at the morphisms whose cone is perfect (ObjectProperty.trW), with the triangulated structure of Triangulated.Localization.

For a left noetherian ring A, the finitely generated left A-modules form the abelian category FGModuleCat A, and ModuleCat.SingularityCategory A is Buchweitz's singularity category Dᵇ(mod-A) / Kᵇ(proj-A). Right modules are left modules over Aᵐᵒᵖ.

Main definitions

• TauCeti.DerivedCategory.Bounded.perfect: the thick subcategory of Dᵇ(C) generated by the projective objects of C in degree zero.
• TauCeti.SingularityCategory: the Verdier quotient Dᵇ(C) / Perf(C), with its quotient functor TauCeti.SingularityCategory.Q, a triangulated localization.
• TauCeti.ModuleCat.SingularityCategory: the singularity category of a left noetherian ring.

Main results

• TauCeti.DerivedCategory.Bounded.perfect_Qh_obj_quotient_obj: a bounded complex of projective objects is perfect.
• TauCeti.DerivedCategory.Bounded.perfect_singleFunctor_obj: a projective object placed in any degree is perfect.
• TauCeti.DerivedCategory.Bounded.perfect_le_inverseImage_ι: a thick subcategory of the derived category containing the projective objects in degree zero contains the perfect objects.
• TauCeti.DerivedCategory.Bounded.perfect_trW_of_distinguished: a morphism whose image in the derived category has a perfect cone is in (perfect C).trW.
• TauCeti.SingularityCategory.isZero_Q_obj_of_perfect: perfect objects vanish in the singularity category; in particular so do the projective objects of C.
• TauCeti.SingularityCategory.nonempty_iso_Q_obj_shift_of_shortExact: a short exact sequence 0 ⟶ X ⟶ P ⟶ Y ⟶ 0 with P projective gives Y ≅ X[1] in the singularity category.
• TauCeti.SingularityCategory.nonempty_iso_Q_obj_singleFunctor_cycles: the cycles Zᵐ of an acyclic complex of projectives placed in degree n are the cycles Zᵐ⁻ⁿ placed in degree zero.

References

• Ragnar-Olaf Buchweitz, Maximal Cohen–Macaulay Modules and Tate Cohomology, Section 1.2.
• Dmitri Orlov, Triangulated categories of singularities and D-branes in Landau–Ginzburg models, Section 1.

def TauCeti.DerivedCategory.Bounded.projectiveSingle (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.ObjectProperty (DerivedCategory.Bounded C)

The projective objects of C, as complexes concentrated in degree zero, up to isomorphism.

theorem TauCeti.DerivedCategory.Bounded.projectiveSingle_iff (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (X : DerivedCategory.Bounded C) : projectiveSingle C X ↔ ∃ (P : C), CategoryTheory.Projective P ∧ Nonempty (X ≅ (singleFunctor C 0).obj P)

The objects of projectiveSingle C are the projective objects of C in degree zero, up to isomorphism.

instance TauCeti.DerivedCategory.Bounded.instNonemptyBoundedProjectiveSingle (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (projectiveSingle C).Nonempty

def TauCeti.DerivedCategory.Bounded.perfect (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.ObjectProperty (DerivedCategory.Bounded C)

The perfect objects of the bounded derived category: the thick subcategory generated by the projective objects of C in degree zero.

theorem TauCeti.DerivedCategory.Bounded.perfect_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : perfect C = (projectiveSingle C).triangEnvelope

The perfect objects are the thick closure of the projective objects in degree zero.

instance TauCeti.DerivedCategory.Bounded.instIsTriangulatedBoundedPerfect (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (perfect C).IsTriangulated

instance TauCeti.DerivedCategory.Bounded.instIsStableUnderRetractsBoundedPerfect (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (perfect C).IsStableUnderRetracts

theorem TauCeti.DerivedCategory.Bounded.perfect_singleFunctor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) {P : C} (hP : CategoryTheory.Projective P) : perfect C ((singleFunctor C n).obj P)

A projective object of C placed in any degree is perfect.

theorem TauCeti.DerivedCategory.Bounded.perfect_le_inverseImage_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (Q : CategoryTheory.ObjectProperty (DerivedCategory C)) [Q.IsClosedUnderIsomorphisms] [Q.IsTriangulated] [Q.IsStableUnderRetracts] (hQ : ∀ (P : C), CategoryTheory.Projective P → Q ((DerivedCategory.singleFunctor C 0).obj P)) : perfect C ≤ Q.inverseImage DerivedCategory.Bounded.ι

Perfect objects lie in every thick subcategory containing the projectives: a triangulated subcategory of the derived category which is stable under retracts and contains the projective objects placed in degree zero contains the perfect objects of the bounded derived category.

theorem TauCeti.DerivedCategory.Bounded.perfect_trW_of_distinguished {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {A B Z : DerivedCategory.Bounded C} (f : A ⟶ B) (g : DerivedCategory.Bounded.ι.obj B ⟶ DerivedCategory.Bounded.ι.obj Z) (h : DerivedCategory.Bounded.ι.obj Z ⟶ DerivedCategory.Bounded.ι.obj A⟦1⟧) (hT : CategoryTheory.Pretriangulated.Triangle.mk (DerivedCategory.Bounded.ι.map f) g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (hZ : perfect C Z) : (perfect C).trW f

A morphism of the bounded derived category whose image in the derived category is the first morphism of a distinguished triangle with perfect third vertex has a perfect cone.

theorem TauCeti.DerivedCategory.Bounded.perfect_Qh_obj_quotient_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (K : CochainComplex.Bounded C) (hK : ∀ (n : ℤ), CategoryTheory.Projective (K.obj.X n)) : perfect C ((Qh C).obj ((HomotopyCategory.Bounded.quotient C).obj K))

A bounded complex of projective objects is perfect.

@[reducible, inline]

abbrev TauCeti.SingularityCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : Type (max u v)

The singularity category Dᵇ(C) / Perf(C) of an abelian category: the Verdier quotient of the bounded derived category by the thick subcategory generated by the projective objects.

noncomputable def TauCeti.SingularityCategory.Q (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Functor (DerivedCategory.Bounded C) (SingularityCategory C)

The Verdier quotient functor Dᵇ(C) ⥤ D_sg(C).

theorem TauCeti.SingularityCategory.Q_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : Q C = (DerivedCategory.Bounded.perfect C).trW.Q

The quotient functor is the localization functor of (perfect C).trW.

instance TauCeti.SingularityCategory.instIsLocalizationBoundedQTrWPerfect (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (Q C).IsLocalization (DerivedCategory.Bounded.perfect C).trW

@[instance_reducible]

noncomputable instance TauCeti.SingularityCategory.instPreadditive (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Preadditive (SingularityCategory C)

instance TauCeti.SingularityCategory.instAdditiveBoundedQ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (Q C).Additive

instance TauCeti.SingularityCategory.instHasZeroObject (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Limits.HasZeroObject (SingularityCategory C)

@[instance_reducible]

noncomputable instance TauCeti.SingularityCategory.instHasShiftInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.HasShift (SingularityCategory C) ℤ

@[instance_reducible]

noncomputable instance TauCeti.SingularityCategory.instCommShiftBoundedQInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (Q C).CommShift ℤ

instance TauCeti.SingularityCategory.instAdditiveShiftFunctorInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : (CategoryTheory.shiftFunctor (SingularityCategory C) n).Additive

@[instance_reducible]

noncomputable instance TauCeti.SingularityCategory.instPretriangulated (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.Pretriangulated (SingularityCategory C)

instance TauCeti.SingularityCategory.instIsTriangulatedBoundedQ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (Q C).IsTriangulated

instance TauCeti.SingularityCategory.instIsTriangulated (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : CategoryTheory.IsTriangulated (SingularityCategory C)

theorem TauCeti.SingularityCategory.isZero_Q_obj_of_perfect {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {X : DerivedCategory.Bounded C} (hX : DerivedCategory.Bounded.perfect C X) : CategoryTheory.Limits.IsZero ((Q C).obj X)

Perfect objects vanish in the singularity category.

theorem TauCeti.SingularityCategory.isZero_Q_obj_singleFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {P : C} (hP : CategoryTheory.Projective P) : CategoryTheory.Limits.IsZero ((Q C).obj ((DerivedCategory.Bounded.singleFunctor C 0).obj P))

A projective object of C, in degree zero, vanishes in the singularity category.

theorem TauCeti.SingularityCategory.nonempty_iso_Q_obj_shift_of_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (hP : CategoryTheory.Projective S.X₂) : Nonempty ((Q C).obj ((DerivedCategory.Bounded.singleFunctor C 0).obj S.X₃) ≅ (Q C).obj ((DerivedCategory.Bounded.singleFunctor C 0).obj S.X₁)⟦1⟧)

In the singularity category, a short exact sequence 0 ⟶ X ⟶ P ⟶ Y ⟶ 0 with P projective identifies Y with the shift X[1], since the projective object P vanishes.

theorem TauCeti.SingularityCategory.nonempty_iso_Q_obj_cycles_shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {P : CochainComplex C ℤ} (hproj : ∀ (m : ℤ), CategoryTheory.Projective (P.X m)) (hacyclic : HomologicalComplex.Acyclic P) (k m : ℤ) : Nonempty ((Q C).obj ((DerivedCategory.Bounded.singleFunctor C 0).obj (HomologicalComplex.cycles P m))⟦k⟧ ≅ (Q C).obj ((DerivedCategory.Bounded.singleFunctor C 0).obj (HomologicalComplex.cycles P (m + k))))

In the singularity category, the cycles of an acyclic complex of projectives placed in degree zero satisfy Zᵐ⁺ᵏ ≅ Zᵐ[k] for every integer k.

theorem TauCeti.SingularityCategory.nonempty_iso_Q_obj_singleFunctor_cycles {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {P : CochainComplex C ℤ} (hproj : ∀ (m : ℤ), CategoryTheory.Projective (P.X m)) (hacyclic : HomologicalComplex.Acyclic P) (n m : ℤ) : Nonempty ((Q C).obj ((DerivedCategory.Bounded.singleFunctor C n).obj (HomologicalComplex.cycles P m)) ≅ (Q C).obj ((DerivedCategory.Bounded.singleFunctor C 0).obj (HomologicalComplex.cycles P (m - n))))

Cycles of an acyclic complex of projectives in every degree: in the singularity category, the cycles Zᵐ placed in degree n are isomorphic to the cycles Zᵐ⁻ⁿ placed in degree zero.

@[reducible, inline]

abbrev TauCeti.ModuleCat.SingularityCategory (A : Type u) [Ring A] [IsNoetherianRing A] [HasDerivedCategory (FGModuleCat A)] : Type (u + 1)

The singularity category of a left noetherian ring A, Dᵇ(mod-A) / Kᵇ(proj-A), for the abelian category of finitely generated left A-modules. Use Aᵐᵒᵖ for right modules.