Extensions of Gorenstein-projective modules

Gorenstein-projective modules are closed under extensions. Given complete resolutions of the outer terms of a short exact sequence, the projective and copresentation horseshoe steps assemble them into a degreewise split short exact sequence of complete resolutions. The middle resolution is totally acyclic, so its degree-zero cycles identify with the middle module.

Thus finitely generated Gorenstein-projective modules inherit the canonical exact structure from modules. This is the first ingredient in making their exact category Frobenius. The ring and module universes are independent under the standard smallness hypothesis needed to iterate the positive horseshoe step.

Main results

• TauCeti.isGorensteinProjective_X₂_of_shortExact: the middle term of a short exact sequence of Gorenstein-projective modules is Gorenstein-projective.
• TauCeti.IsGorensteinProjective.isExtensionClosed: Gorenstein-projective modules are extension closed for the canonical abelian exact structure.

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.

theorem TauCeti.isGorensteinProjective_X₂_of_shortExact {A : Type u} [Ring A] [Small.{v, u} A] {S : CategoryTheory.ShortComplex (ModuleCat A)} (hS : S.ShortExact) (h₁ : IsGorensteinProjective A S.X₁) (h₃ : IsGorensteinProjective A S.X₃) : IsGorensteinProjective A S.X₂

The middle term of a short exact sequence of Gorenstein-projective modules is Gorenstein-projective.

theorem TauCeti.IsGorensteinProjective.isExtensionClosed {A : Type u} [Ring A] [Small.{v, u} A] : (ExactStructure.abelian (ModuleCat A)).IsExtensionClosed (IsGorensteinProjective A)

Gorenstein-projective modules are extension closed for the canonical exact structure on modules.