Extensions of Gorenstein-projective objects

In an abelian category C, the Gorenstein-projective objects are closed under extensions: the middle term of a short exact sequence with Gorenstein-projective outer terms is Gorenstein-projective.

The proof reuses the horseshoe lemma for complete resolutions in an exact category (TauCeti.ExactStructure.CompleteResolution.horseshoe). It is applied to the extension-closed full subcategory of the objects X with Ext¹(X, Q) = 0 for every projective Q (CategoryTheory.ObjectProperty.extLeftOrthogonal), with the exact structure inherited from C. There the projective objects of C are projective-injective, so a totally acyclic complex of projectives is a complete resolution in this exact category; and the middle resolution produced by the horseshoe has projective terms, since they split as biproducts of the terms of the outer ones. Conversely a splice of short exact sequences with projective middle terms and Ext¹(-, Q)-orthogonal ends is a totally acyclic complex of projectives (CochainComplex.isTotallyAcyclicProjective_splice).

Main results

• CochainComplex.IsTotallyAcyclicProjective.extLeftOrthogonal_cycles: the cycles of a totally acyclic complex of projectives have no higher extensions by projectives.
• CochainComplex.isTotallyAcyclicProjective_splice: a splice of short exact sequences with projective middle terms and ends without extensions by projectives is totally acyclic.
• CategoryTheory.isGorensteinProjective_X₂_of_shortExact: Gorenstein-projective objects are closed under extensions.

References

• Edgar E. Enochs and Overtoun M. G. Jenda, Relative Homological Algebra, de Gruyter Expositions in Mathematics 30 (2000), Theorem 10.2.8.

theorem CochainComplex.isTotallyAcyclicProjective_splice {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (S : ℤ → CategoryTheory.ShortComplex C) (e : (n : ℤ) → (S n).X₃ ≅ (S (n + 1)).X₁) (hS : ∀ (n : ℤ), (S n).ShortExact) (hproj : ∀ (n : ℤ), CategoryTheory.Projective (S n).X₂) (hext : ∀ (n : ℤ) (Q : C) [CategoryTheory.Projective Q] (x : CategoryTheory.Abelian.Ext (S n).X₃ Q 1), x = 0) : (splice S e).IsTotallyAcyclicProjective

Splices of orthogonal short exact sequences are totally acyclic: splicing short exact sequences Sⁿ with projective middle terms, whose end terms have no extensions by projective objects, gives a totally acyclic complex of projectives.

theorem CochainComplex.IsTotallyAcyclicProjective.extLeftOrthogonal_cycles {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {P : CochainComplex C ℤ} (hP : P.IsTotallyAcyclicProjective) (k : ℤ) (i : ℕ) : (CategoryTheory.isProjective C).extLeftOrthogonal (i + 1) (HomologicalComplex.cycles P k)

The cycles of a totally acyclic complex of projectives lie in the Ext-left-orthogonal of the projective objects in every positive degree.

theorem CategoryTheory.isGorensteinProjective_X₂_of_shortExact {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) (h₁ : isGorensteinProjective C S.X₁) (h₃ : isGorensteinProjective C S.X₃) : isGorensteinProjective C S.X₂

Gorenstein-projective objects are closed under extensions: the middle term of a short exact sequence whose outer terms are Gorenstein-projective is Gorenstein-projective.

theorem CategoryTheory.isGorensteinProjective_isExtensionClosed {C : Type u} [Category.{v, u} C] [Abelian C] : (TauCeti.ExactStructure.abelian C).IsExtensionClosed (isGorensteinProjective C)

Gorenstein-projective objects are extension closed for the abelian exact structure.

instance CategoryTheory.instIsClosedUnderBinaryProductsIsGorensteinProjective {C : Type u} [Category.{v, u} C] [Abelian C] : (isGorensteinProjective C).IsClosedUnderBinaryProducts