Gorenstein-projective objects have no higher extensions by projectives

Let C be an abelian category and G a Gorenstein-projective object of C. Then Ext^{n+1}(G, Q) = 0 for every projective object Q of C.

A complete resolution P of G is acyclic, so its cycles fit into short exact sequences 0 ⟶ Zⁱ ⟶ Pⁱ ⟶ Zⁱ⁺¹ ⟶ 0 (HomologicalComplex.shortExact_mk_iCycles_toCycles). Since the middle terms are projective, the long exact sequence of Ext(-, Q) shifts dimension: Ext^{n+1}(Zⁱ⁺¹, Q) is a quotient of Ext^n(Zⁱ, Q). In degree 1, the obstruction is a morphism Zⁱ ⟶ Q which does not extend to Pⁱ, and every such morphism extends because P is totally acyclic.

Main results

• CochainComplex.IsTotallyAcyclicProjective.exists_comp_iCycles_eq: a morphism from the cycles of a totally acyclic complex of projectives to a projective object extends to the term.
• CategoryTheory.isGorensteinProjective.ext_eq_zero: Ext^{n+1}(G, Q) = 0 for G Gorenstein-projective and Q projective.

theorem CochainComplex.IsTotallyAcyclicProjective.exists_comp_iCycles_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CochainComplex C ℤ} (hP : P.IsTotallyAcyclicProjective) (n : ℤ) {Q : C} [CategoryTheory.Projective Q] (φ : HomologicalComplex.cycles P n ⟶ Q) : ∃ (g : P.X n ⟶ Q), CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles P n) g = φ

Morphisms from cycles to projectives extend: a morphism from the cycles of a totally acyclic complex of projectives to a projective object extends to the term containing them.

theorem CochainComplex.IsTotallyAcyclicProjective.ext_cycles_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CochainComplex C ℤ} (hP : P.IsTotallyAcyclicProjective) [CategoryTheory.HasExt C] (Q : C) [CategoryTheory.Projective Q] (n : ℕ) (m : ℤ) (e : CategoryTheory.Abelian.Ext (HomologicalComplex.cycles P m) Q (n + 1)) : e = 0

The cycles of a totally acyclic complex of projectives have no higher extensions by projective objects.

theorem CategoryTheory.isGorensteinProjective.ext_eq_zero {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {G : C} (hG : isGorensteinProjective C G) (Q : C) [Projective Q] {n : ℕ} (e : Abelian.Ext G Q (n + 1)) : e = 0

Gorenstein-projective objects have no higher extensions by projectives: Ext^{n+1}(G, Q) = 0 for a Gorenstein-projective object G and a projective object Q.