Gorenstein-projective modules as Gorenstein-projective objects of mod-A

Let A be a left noetherian ring, so that the finitely generated A-modules form an abelian category FGModuleCat A. The module notion of total acyclicity (CochainComplex.IsTotallyAcyclic: finitely generated projective terms, acyclic, and Hom_A(P, A) acyclic) agrees with total acyclicity in the abelian category FGModuleCat A (CochainComplex.IsTotallyAcyclicProjective: projective terms, acyclic, and Hom(P, Q) acyclic for every projective object Q). Testing the regular module suffices because finitely generated projective modules are retracts of finite free modules (CochainComplex.IsTotallyAcyclic.exact_hom_projective). Consequently a finitely generated module is Gorenstein-projective in the module sense (TauCeti.IsGorensteinProjective) if and only if it is a Gorenstein-projective object of FGModuleCat A (CategoryTheory.isGorensteinProjective).

So the abelian-category theory applies to the finitely generated Gorenstein-projective modules over a noetherian ring. Right modules over R are the case A = Rᵐᵒᵖ.

Main results

• CochainComplex.isTotallyAcyclicProjective_iff_isTotallyAcyclic: a cochain complex of finitely generated modules is totally acyclic in FGModuleCat A if and only if its underlying complex of modules is totally acyclic in the module sense.
• FGModuleCat.isGorensteinProjective_iff: a finitely generated module is a Gorenstein-projective object of FGModuleCat A if and only if it is a Gorenstein-projective module.

theorem CochainComplex.isTotallyAcyclicProjective_iff_isTotallyAcyclic {A : Type u} [Ring A] [IsNoetherianRing A] [Small.{v, u} A] (P : CochainComplex (FGModuleCat A) ℤ) : P.IsTotallyAcyclicProjective ↔ IsTotallyAcyclic (((CategoryTheory.forget₂ (FGModuleCat A) (ModuleCat A)).mapHomologicalComplex (ComplexShape.up ℤ)).obj P)

Total acyclicity in mod-A is total acyclicity of modules: a cochain complex of finitely generated modules over a left noetherian ring is totally acyclic in the abelian category FGModuleCat A if and only if its underlying complex of modules is totally acyclic.

theorem FGModuleCat.isGorensteinProjective_iff {A : Type u} [Ring A] [IsNoetherianRing A] [Small.{v, u} A] (M : FGModuleCat A) : CategoryTheory.isGorensteinProjective (FGModuleCat A) M ↔ TauCeti.IsGorensteinProjective A M.obj

Gorenstein-projective modules are the Gorenstein-projective objects of mod-A: over a left noetherian ring, a finitely generated module is a Gorenstein-projective object of the abelian category FGModuleCat A if and only if it is a Gorenstein-projective module.