Extensions of totally acyclic complexes

Total acyclicity is preserved by a short exact sequence of complexes which splits in every degree. The splitting makes the middle terms finite projective. It also makes the dual sequence exact, while the ordinary long exact homology sequence gives acyclicity of the middle complex.

This is the homological part of the complete horseshoe argument: once an extension of Gorenstein-projective modules has been lifted to a degreewise split sequence of complete resolutions, its middle resolution is again complete.

Main result

• CochainComplex.IsTotallyAcyclic.of_degreewise_split: the middle complex in a degreewise split extension of totally acyclic complexes is totally acyclic.
• CochainComplex.IsTotallyAcyclic.isExtensionClosed: totally acyclic complexes form an extension-closed property for the componentwise split exact structure.

References

• Ragnar-Olaf Buchweitz, Maximal Cohen--Macaulay Modules and Tate Cohomology, Mathematical Surveys and Monographs 262, American Mathematical Society (2021), Section 4.
• Charles A. Weibel, An Introduction to Homological Algebra, Lemma 2.2.8.

theorem CochainComplex.IsTotallyAcyclic.of_degreewise_split {A : Type u} [Ring A] {S : CategoryTheory.ShortComplex (CochainComplex (ModuleCat A) ℤ)} (h₁ : S.X₁.IsTotallyAcyclic) (h₃ : S.X₃.IsTotallyAcyclic) (s : (n : ℤ) → { X₁ := S.X₁.X n, X₂ := S.X₂.X n, X₃ := S.X₃.X n, f := S.f.f n, g := S.g.f n, zero := ⋯ }.Splitting) : S.X₂.IsTotallyAcyclic

The middle complex in a degreewise split extension of totally acyclic complexes is totally acyclic. The chosen splittings need not commute with the differentials.

theorem CochainComplex.IsTotallyAcyclic.isExtensionClosed {A : Type u} [Ring A] : ((TauCeti.ExactStructure.split (ModuleCat A)).homologicalComplex (ComplexShape.up ℤ)).IsExtensionClosed fun (P : HomologicalComplex (ModuleCat A) (ComplexShape.up ℤ)) => IsTotallyAcyclic P

Totally acyclic complexes are extension closed for the componentwise split exact structure on cochain complexes.