Presentations from complete resolutions

A totally acyclic cochain complex P supplies, in every degree n, a short exact sequence

0 ⟶ Zⁿ(P) ⟶ Pⁿ ⟶ Zⁿ⁺¹(P) ⟶ 0.

The middle term is finitely generated and projective, while both cycle terms are Gorenstein-projective. These sequences are the projective presentations and copresentations used to put the Frobenius exact structure on Gorenstein-projective modules.

Main declarations

• TauCeti.IsGorensteinProjective.exists_projectivePresentation: every Gorenstein-projective module has a projective presentation whose kernel is again Gorenstein-projective.
• TauCeti.IsGorensteinProjective.exists_projectiveCopresentation: every Gorenstein-projective module embeds in a finitely generated projective module with Gorenstein-projective cokernel.

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.exists_projectivePresentation {A : Type u} [Ring A] {M : ModuleCat A} (hM : IsGorensteinProjective A M) : ∃ (S : CategoryTheory.ShortComplex (ModuleCat A)), S.ShortExact ∧ Nonempty (S.X₃ ≅ M) ∧ Module.Finite A ↑S.X₂ ∧ CategoryTheory.Projective S.X₂ ∧ IsGorensteinProjective A S.X₁

A Gorenstein-projective module has a projective presentation with a finitely generated projective middle term and a Gorenstein-projective kernel.

theorem TauCeti.IsGorensteinProjective.exists_projectiveCopresentation {A : Type u} [Ring A] {M : ModuleCat A} (hM : IsGorensteinProjective A M) : ∃ (S : CategoryTheory.ShortComplex (ModuleCat A)), S.ShortExact ∧ Nonempty (S.X₁ ≅ M) ∧ Module.Finite A ↑S.X₂ ∧ CategoryTheory.Projective S.X₂ ∧ IsGorensteinProjective A S.X₃

A Gorenstein-projective module embeds in a finitely generated projective module with Gorenstein-projective cokernel.