Projective coefficients for complete resolutions

A totally acyclic complex remains exact after applying Hom(-, Q) for any projective coefficient module Q. Consequently every map from its cycles to Q extends to the containing term. These extensions are the input for lifting maps between complete resolutions and for identifying finite projectives as relative injectives among Gorenstein-projective modules.

The dual exactness in CochainComplex.IsTotallyAcyclic tests only the regular module. A projective module Q is a retract of a free module Q →₀ A, and since the terms of the complex are finitely generated, a map from a term to Q →₀ A lands in the functions supported on a finite set (LinearMap.exists_finset_support_subset), a finite power of the regular module. No self-injectivity or commutativity assumption is needed. Taking the coefficient ring to be Rᵐᵒᵖ gives the statements for right R-modules.

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.

The free retraction is Mathlib's Module.projective_def'.

theorem CochainComplex.IsTotallyAcyclic.exact_hom_projective {A : Type u} [Ring A] {P : CochainComplex (ModuleCat A) ℤ} (hP : P.IsTotallyAcyclic) {Q : Type w} [AddCommGroup Q] [Module A Q] [Module.Projective A Q] (i j k : ℤ) (hij : i + 1 = j) (hjk : j + 1 = k) : Function.Exact (fun (f : ↑(P.X k) →ₗ[A] Q) => f ∘ₗ ModuleCat.Hom.hom (P.d j k)) fun (f : ↑(P.X j) →ₗ[A] Q) => f ∘ₗ ModuleCat.Hom.hom (P.d i j)

Applying Hom(-, Q) to a totally acyclic complex is exact for every projective coefficient module Q, even over a noncommutative ring.

theorem CochainComplex.IsTotallyAcyclic.exists_extend_iCycles {A : Type u} [Ring A] {P : CochainComplex (ModuleCat A) ℤ} (hP : P.IsTotallyAcyclic) {Q : Type w} [AddCommGroup Q] [Module A Q] [Module.Projective A Q] (n : ℤ) (f : ↑(HomologicalComplex.cycles P n) →ₗ[A] Q) : ∃ (g : ↑(P.X n) →ₗ[A] Q), g ∘ₗ ModuleCat.Hom.hom (HomologicalComplex.iCycles P n) = f

Every map from the cycles of a totally acyclic complex to a projective module extends to the containing term, with independent term and coefficient universes.

theorem CochainComplex.IsTotallyAcyclic.comp_iCycles_eq_iff {A : Type u} [Ring A] {P : CochainComplex (ModuleCat A) ℤ} (hP : P.IsTotallyAcyclic) {Q : Type w} [AddCommGroup Q] [Module A Q] [Module.Projective A Q] (n : ℤ) (f g : ↑(P.X n) →ₗ[A] Q) : f ∘ₗ ModuleCat.Hom.hom (HomologicalComplex.iCycles P n) = g ∘ₗ ModuleCat.Hom.hom (HomologicalComplex.iCycles P n) ↔ ∃ (h : ↑(P.X (n + 1)) →ₗ[A] Q), h ∘ₗ ModuleCat.Hom.hom (P.d n (n + 1)) = f - g

Two maps to a projective module have the same restriction to cycles exactly when their difference factors through the next differential. Thus cycle extensions are unique modulo coboundaries in the coefficient Hom complex.