Gorenstein-projective objects in the singularity category

Let C be an abelian category, G a Gorenstein-projective object of C and Y any object of C. The map Hom_C(G, Y) ⟶ Hom_{D_sg(C)}(G, Y) induced by the singularity category D_sg(C) = Dᵇ(C) / Perf(C) is surjective, and its kernel consists of the morphisms factoring through a projective object. Hence the functor from the stable category of Gorenstein-projective objects to the singularity category is fully faithful (X.-W. Chen).

Let P be a complete resolution of G = Z⁰, with cycles Zᵐ. The short exact sequences 0 ⟶ Zᵐ ⟶ Pᵐ ⟶ Zᵐ⁺¹ ⟶ 0 give morphisms Zᵐ⁺¹[-m-1] ⟶ Zᵐ[-m] in the bounded derived category whose cones Pᵐ[-m] are perfect, and their composites δₘ : Zᵐ[-m] ⟶ G. Every morphism from G to a perfect object K is killed by δₘ for m large, since Hom(Zᵐ[-m], K) = 0 for m large: this holds for K a projective object in degree zero because the cycles have no higher extensions by projectives, and passes to the thick subcategory generated by these objects. By the calculus of fractions of the Verdier quotient, every morphism G ⟶ Y of D_sg(C) then comes from a morphism Zᵐ[-m] ⟶ Y, and every morphism G ⟶ Y vanishing in D_sg(C) is killed by some δₘ. Finally Ext^{>0}(Pᵐ, Y) = 0 lets morphisms Zᵐ[-m] ⟶ Y extend along δₘ, and lets the vanishing of δₘ ≫ f descend to δ₁ ≫ f = 0, which says that f factors through G ⟶ P⁰.

Main definitions

• CategoryTheory.GorensteinProjective.toSingularityCategory: the functor from the stable category of Gorenstein-projective objects to the singularity category.

Main results

• TauCeti.SingularityCategory.map_surjective_of_isGorensteinProjective: for G Gorenstein-projective, every morphism G ⟶ Y of the singularity category comes from C.
• TauCeti.SingularityCategory.map_eq_zero_iff_of_isGorensteinProjective: a morphism G ⟶ Y of C vanishes in the singularity category if and only if it factors through a projective object.
• CategoryTheory.GorensteinProjective.fullyFaithfulToSingularityCategory: Chen's theorem, the functor from the stable category of Gorenstein-projective objects to the singularity category is fully faithful.
• TauCeti.SingularityCategory.exists_iso_Q_obj_singleFunctor_of_isGorensteinProjective: a Gorenstein-projective object placed in any degree is isomorphic in the singularity category to a cycle of its complete resolution placed in degree zero (TauCeti.SingularityCategory.nonempty_iso_Q_obj_singleFunctor_cycles), so CategoryTheory.GorensteinProjective.mem_essImage_toSingularityCategory: it lies in the essential image of Chen's functor.

References

• Xiao-Wu Chen, Relative singularity categories and Gorenstein-projective modules, Math. Nachr. 284 (2011), 199–212.
• Ragnar-Olaf Buchweitz, Maximal Cohen–Macaulay Modules and Tate Cohomology, Mathematical Surveys and Monographs 262, American Mathematical Society (2021), Section 4.4.

theorem TauCeti.SingularityCategory.map_surjective_of_isGorensteinProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {G : C} (hG : CategoryTheory.isGorensteinProjective C G) (Y : C) : Function.Surjective fun (f : G ⟶ Y) => (Q C).map ((DerivedCategory.Bounded.singleFunctor C 0).map f)

Morphisms out of a Gorenstein-projective object in the singularity category. For G Gorenstein-projective and Y any object of an abelian category C, every morphism from G to Y in the singularity category comes from a morphism G ⟶ Y of C.

theorem TauCeti.SingularityCategory.map_eq_zero_iff_of_isGorensteinProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {G Y : C} (hG : CategoryTheory.isGorensteinProjective C G) (f : G ⟶ Y) : (Q C).map ((DerivedCategory.Bounded.singleFunctor C 0).map f) = 0 ↔ (CategoryTheory.isProjective C).FactorsThrough f

The kernel on a Gorenstein-projective object. For G Gorenstein-projective and Y any object of an abelian category C, a morphism G ⟶ Y vanishes in the singularity category if and only if it factors through a projective object.

theorem TauCeti.SingularityCategory.exists_iso_Q_obj_singleFunctor_of_isGorensteinProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {G : C} (hG : CategoryTheory.isGorensteinProjective C G) (n : ℤ) : ∃ (G' : C), CategoryTheory.isGorensteinProjective C G' ∧ Nonempty ((Q C).obj ((DerivedCategory.Bounded.singleFunctor C n).obj G) ≅ (Q C).obj ((DerivedCategory.Bounded.singleFunctor C 0).obj G'))

Gorenstein-projective objects in every degree: in the singularity category, a Gorenstein-projective object placed in any degree is isomorphic to a Gorenstein-projective object placed in degree zero, namely a cycle of its complete resolution.

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

The functor from Gorenstein-projective objects to the singularity category, placing an object in degree zero.

instance CategoryTheory.GorensteinProjective.instAdditiveSingularityCategoryToSingularityCategoryFunctor (C : Type u) [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] : (toSingularityCategoryFunctor C).Additive

@[simp]

theorem CategoryTheory.GorensteinProjective.toSingularityCategoryFunctor_obj {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] (X : GorensteinProjective C) : (toSingularityCategoryFunctor C).obj X = (TauCeti.SingularityCategory.Q C).obj ((TauCeti.DerivedCategory.Bounded.singleFunctor C 0).obj X.obj)

The functor toSingularityCategoryFunctor places an object in degree zero.

@[simp]

theorem CategoryTheory.GorensteinProjective.toSingularityCategoryFunctor_map {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {X Y : GorensteinProjective C} (f : X ⟶ Y) : (toSingularityCategoryFunctor C).map f = (TauCeti.SingularityCategory.Q C).map ((TauCeti.DerivedCategory.Bounded.singleFunctor C 0).map f.hom)

The functor toSingularityCategoryFunctor places a morphism in degree zero.

noncomputable def CategoryTheory.GorensteinProjective.toSingularityCategory (C : Type u) [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] : Functor (exactStructure C).ProjectiveStableCategory (TauCeti.SingularityCategory C)

Chen's functor from the stable category of Gorenstein-projective objects to the singularity category, induced by placing an object in degree zero. It is well defined because projective objects vanish in the singularity category.

instance CategoryTheory.GorensteinProjective.instAdditiveProjectiveStableCategoryExactStructureSingularityCategoryToSingularityCategory (C : Type u) [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] : (toSingularityCategory C).Additive

theorem CategoryTheory.GorensteinProjective.projectiveStableFunctor_comp_toSingularityCategory (C : Type u) [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] : (exactStructure C).projectiveStableFunctor.comp (toSingularityCategory C) = toSingularityCategoryFunctor C

Chen's functor restricts to placing objects in degree zero along the quotient functor.

@[simp]

theorem CategoryTheory.GorensteinProjective.toSingularityCategory_obj_projectiveStableFunctor_obj {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] (X : GorensteinProjective C) : (toSingularityCategory C).obj ((exactStructure C).projectiveStableFunctor.obj X) = (TauCeti.SingularityCategory.Q C).obj ((TauCeti.DerivedCategory.Bounded.singleFunctor C 0).obj X.obj)

Chen's functor sends the class of an object to that object placed in degree zero.

@[simp]

theorem CategoryTheory.GorensteinProjective.toSingularityCategory_map_projectiveStableFunctor_map {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {X Y : GorensteinProjective C} (f : X ⟶ Y) : (toSingularityCategory C).map ((exactStructure C).projectiveStableFunctor.map f) = (TauCeti.SingularityCategory.Q C).map ((TauCeti.DerivedCategory.Bounded.singleFunctor C 0).map f.hom)

Chen's functor sends the class of a morphism f of Gorenstein-projective objects to f placed in degree zero.

instance CategoryTheory.GorensteinProjective.instFullProjectiveStableCategoryExactStructureSingularityCategoryToSingularityCategory (C : Type u) [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] : (toSingularityCategory C).Full

Chen's theorem, fullness: every morphism of the singularity category between Gorenstein-projective objects comes from a morphism of C.

instance CategoryTheory.GorensteinProjective.instFaithfulProjectiveStableCategoryExactStructureSingularityCategoryToSingularityCategory (C : Type u) [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] : (toSingularityCategory C).Faithful

Chen's theorem, faithfulness: a morphism of Gorenstein-projective objects vanishing in the singularity category factors through a projective object.

noncomputable def CategoryTheory.GorensteinProjective.fullyFaithfulToSingularityCategory (C : Type u) [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] : (toSingularityCategory C).FullyFaithful

Chen's theorem: the functor from the stable category of Gorenstein-projective objects of an abelian category to its singularity category is fully faithful.

theorem CategoryTheory.GorensteinProjective.mem_essImage_toSingularityCategory {C : Type u} [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] {G : C} (hG : isGorensteinProjective C G) (n : ℤ) : (toSingularityCategory C).essImage ((TauCeti.SingularityCategory.Q C).obj ((TauCeti.DerivedCategory.Bounded.singleFunctor C n).obj G))

A Gorenstein-projective object placed in any degree lies in the essential image of Chen's functor (TauCeti.SingularityCategory.exists_iso_Q_obj_singleFunctor_of_isGorensteinProjective).