The additive category of Gorenstein-projective modules

The direct sum of two complete resolutions is again a complete resolution. Consequently, Gorenstein-projective modules contain the zero module and are closed under binary biproducts. Their full subcategory of modules is therefore additive; this is the ambient category on which the inherited exact structure and the Frobenius structure will be constructed.

Main declarations

• TauCeti.IsGorensteinProjective.biprod: binary biproducts preserve Gorenstein-projectivity.
• TauCeti.GorensteinProjectiveModuleCat: the additive full subcategory of Gorenstein-projective modules.

References

• Ragnar-Olaf Buchweitz, Maximal Cohen–Macaulay Modules and Tate Cohomology, Mathematical Surveys and Monographs 262, American Mathematical Society (2021), Section 4.

theorem TauCeti.isGorensteinProjective_of_isZero {A : Type u} [Ring A] {M : ModuleCat A} (hM : CategoryTheory.Limits.IsZero M) : IsGorensteinProjective A M

Every zero module is Gorenstein-projective.

theorem TauCeti.IsGorensteinProjective.biprod {A : Type u} [Ring A] {M N : ModuleCat A} (hM : IsGorensteinProjective A M) (hN : IsGorensteinProjective A N) : IsGorensteinProjective A (M ⊞ N)

A binary biproduct of Gorenstein-projective modules is Gorenstein-projective.

instance TauCeti.instContainsZeroModuleCatIsGorensteinProjective {A : Type u} [Ring A] : (IsGorensteinProjective A).ContainsZero

instance TauCeti.instIsClosedUnderBinaryProductsModuleCatIsGorensteinProjective {A : Type u} [Ring A] : (IsGorensteinProjective A).IsClosedUnderBinaryProducts

@[reducible, inline]

abbrev TauCeti.GorensteinProjectiveModuleCat (A : Type u) [Ring A] : Type (max u (v + 1))

The additive category of finitely generated Gorenstein-projective A-modules.