The positive horseshoe step for complete resolutions

A map into a projective module extends across a monomorphism whose cokernel is Gorenstein-projective. Consequently, copresentations of the ends of a short exact sequence can be combined into a copresentation of its middle term, with middle module the direct sum of the prescribed copresenting modules. Only the left copresenting module must be projective. The cokernel is an extension of the two prescribed cokernels.

This is the positive-degree step of the complete horseshoe construction. Unlike an injective horseshoe, it does not require projective modules to be injective among all modules. Only the original quotient is assumed Gorenstein-projective. Iteration of this step, together with the projective horseshoe in negative degrees, constructs extensions of complete resolutions. The results here do not yet assert that Gorenstein-projective modules are extension closed.

The prescribed horseshoe allows independent ring and module universes. The iteratable specialization requires the ring to be small in the module universe, so categorical projectivity implies module projectivity. Taking A = Rᵐᵒᵖ gives right modules. No noetherian or self-injectivity hypothesis is needed.

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 pushout and Noether argument is dual to ExactStructure.exists_conflation_biprod_of_conflation_of_projective. It replaces ambient injectivity by the splitting theorem IsGorensteinProjective.nonempty_splitting_of_projective.

theorem TauCeti.IsGorensteinProjective.exists_copresentation_horseshoe {A : Type u} [Ring A] {S : CategoryTheory.ShortComplex (ModuleCat A)} (hN : IsGorensteinProjective A S.X₃) (hS : S.ShortExact) {PX KX PZ KZ : ModuleCat A} {iX : S.X₁ ⟶ PX} {pX : PX ⟶ KX} {hX : CategoryTheory.CategoryStruct.comp iX pX = 0} (hTX : { X₁ := S.X₁, X₂ := PX, X₃ := KX, f := iX, g := pX, zero := hX }.ShortExact) {iZ : S.X₃ ⟶ PZ} {pZ : PZ ⟶ KZ} {hZ : CategoryTheory.CategoryStruct.comp iZ pZ = 0} (hTZ : { X₁ := S.X₃, X₂ := PZ, X₃ := KZ, f := iZ, g := pZ, zero := hZ }.ShortExact) [Module.Projective A ↑PX] : ∃ (K : ModuleCat A) (i : S.X₂ ⟶ PX ⊞ PZ) (p : PX ⊞ PZ ⟶ K) (hip : CategoryTheory.CategoryStruct.comp i p = 0) (a : KX ⟶ K) (b : K ⟶ KZ) (hab : CategoryTheory.CategoryStruct.comp a b = 0), { X₁ := S.X₂, X₂ := PX ⊞ PZ, X₃ := K, f := i, g := p, zero := hip }.ShortExact ∧ { X₁ := KX, X₂ := K, X₃ := KZ, f := a, g := b, zero := hab }.ShortExact ∧ CategoryTheory.CategoryStruct.comp S.f i = CategoryTheory.CategoryStruct.comp iX CategoryTheory.Limits.biprod.inl ∧ CategoryTheory.CategoryStruct.comp i CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp S.g iZ ∧ CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl p = CategoryTheory.CategoryStruct.comp pX a ∧ CategoryTheory.CategoryStruct.comp p b = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd pZ

The positive horseshoe step. Copresentations of the two ends of a short exact sequence with Gorenstein-projective quotient combine to a copresentation of the middle term. The left copresenting module is projective; no injectivity or projectivity is required of the right copresenting module. The new cokernel is an extension of the prescribed cokernels, and all four squares of the horseshoe commute.

theorem TauCeti.IsGorensteinProjective.exists_projectiveCopresentation_of_shortExact {A : Type u} [Ring A] [Small.{v, u} A] {S : CategoryTheory.ShortComplex (ModuleCat A)} (hL : IsGorensteinProjective A S.X₁) (hN : IsGorensteinProjective A S.X₃) (hS : S.ShortExact) : ∃ (T : CategoryTheory.ShortComplex (ModuleCat A)) (U : CategoryTheory.ShortComplex (ModuleCat A)), T.ShortExact ∧ Nonempty (T.X₁ ≅ S.X₂) ∧ Module.Finite A ↑T.X₂ ∧ CategoryTheory.Projective T.X₂ ∧ U.ShortExact ∧ Nonempty (U.X₂ ≅ T.X₃) ∧ IsGorensteinProjective A U.X₁ ∧ IsGorensteinProjective A U.X₃

An extension of Gorenstein-projective modules embeds in a finite projective module, with cokernel again an extension of Gorenstein-projective modules. The ring must be small in the module universe. This is an iteratable positive horseshoe step, not yet a claim that the middle term or its cokernel is Gorenstein-projective.