The Frobenius category of Gorenstein-projective modules

Finitely generated Gorenstein-projective modules inherit the exact structure of modules. This exact structure is Frobenius: complete resolutions give enough projectives and injectives, and both classes consist exactly of the finitely generated projective modules. Finite projectives are relatively injective because maps into them extend across short exact sequences with Gorenstein-projective quotient. Conversely, each relative projective or injective is a retract of the projective middle term of a complete-resolution presentation.

These results supply the Frobenius structure needed for the triangulated stable category of Gorenstein-projectives. No noetherian or self-injectivity hypothesis is needed. Modules here are left modules; apply the construction to Rᵐᵒᵖ for right R-modules. The module universe can be independent of the ring universe, provided the ring is small in it. In particular, taking both universes equal includes the regular module and all its finite free powers.

References

• Ragnar-Olaf Buchweitz, Maximal Cohen--Macaulay Modules and Tate Cohomology, Section 4.
• Edgar E. Enochs and Overtoun M. G. Jenda, Relative Homological Algebra, Section 10.2.

noncomputable def TauCeti.GorensteinProjectiveModuleCat.exactStructure (A : Type u) [Ring A] [Small.{v, u} A] : ExactStructure (GorensteinProjectiveModuleCat A)

The exact structure on finitely generated Gorenstein-projective modules induced by the canonical abelian exact structure on all modules.

@[simp]

theorem TauCeti.GorensteinProjectiveModuleCat.exactStructure_conflation_iff (A : Type u) [Ring A] [Small.{v, u} A] (S : CategoryTheory.ShortComplex (GorensteinProjectiveModuleCat A)) : (exactStructure A).Conflation S ↔ (S.map (IsGorensteinProjective A).ι).ShortExact

Conflations of Gorenstein-projectives are precisely the underlying short exact sequences of modules.

@[simp]

theorem TauCeti.GorensteinProjectiveModuleCat.exactStructure_isProjective_iff {A : Type u} [Ring A] [Small.{v, u} A] (X : GorensteinProjectiveModuleCat A) : (exactStructure A).isProjective X ↔ CategoryTheory.Projective X.obj

The relative projectives among Gorenstein-projectives are exactly the projective underlying modules, which are already finitely generated.

@[simp]

theorem TauCeti.GorensteinProjectiveModuleCat.exactStructure_isInjective_iff {A : Type u} [Ring A] [Small.{v, u} A] (X : GorensteinProjectiveModuleCat A) : (exactStructure A).isInjective X ↔ CategoryTheory.Projective X.obj

The relative injectives among Gorenstein-projectives are also exactly the projective underlying modules, not the injectives of the ambient module category.

theorem TauCeti.GorensteinProjectiveModuleCat.exactStructure_enoughProjectives {A : Type u} [Ring A] [Small.{v, u} A] : (exactStructure A).EnoughProjectives

Complete resolutions provide enough relative projectives in the inherited exact structure.

theorem TauCeti.GorensteinProjectiveModuleCat.exactStructure_enoughInjectives {A : Type u} [Ring A] [Small.{v, u} A] : (exactStructure A).EnoughInjectives

Complete resolutions provide enough relative injectives in the inherited exact structure, with projective underlying middle modules.

theorem TauCeti.GorensteinProjectiveModuleCat.exactStructure_isFrobenius {A : Type u} [Ring A] [Small.{v, u} A] : (exactStructure A).IsFrobenius

Finitely generated Gorenstein-projective modules, with the inherited exact structure, form a Frobenius exact category. The projective-injective objects are the finite projectives.