Ext out of syzygies into objects of finite injective dimension

Let X be a k-th syzygy relative to a class of projective objects of an abelian category, so that there is an exact sequence 0 ⟶ X ⟶ Q₁ ⟶ ⋯ ⟶ Q_k with projective Qᵢ (CategoryTheory.ObjectProperty.IsSyzygy). Dimension shifting along the k short exact sequences gives Ext^{n+1}(X, Y) ≅ Ext^{n+k+1}(X', Y) for the last cokernel X'. So if Y has injective dimension at most d, then Ext^{n+1}(X, Y) = 0 as soon as n + k ≥ d; in particular a d-th syzygy has no higher extensions into Y.

Main results

• CategoryTheory.ObjectProperty.IsSyzygy.ext_eq_zero: Ext^{n+1}(X, Y) = 0 for a k-th syzygy X and Y of injective dimension at most d ≤ n + k.
• CategoryTheory.ObjectProperty.IsSyzygy.ext_eq_zero_of_hasInjectiveDimensionLE: a d-th syzygy has no higher extensions into an object of injective dimension at most d.

theorem CategoryTheory.ObjectProperty.IsSyzygy.ext_eq_zero {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {P : ObjectProperty C} (hP : ∀ (Q : C), P Q → Projective Q) {k : ℕ} {X : C} (hX : P.IsSyzygy k X) {Y : C} {d : ℕ} [HasInjectiveDimensionLE Y d] {n : ℕ} (hn : d ≤ n + k) (e : Abelian.Ext X Y (n + 1)) : e = 0

Ext out of a syzygy: if X is a k-th syzygy relative to projective objects and Y has injective dimension at most d, then Ext^{n+1}(X, Y) = 0 whenever d ≤ n + k.

theorem CategoryTheory.ObjectProperty.IsSyzygy.ext_eq_zero_of_hasInjectiveDimensionLE {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {P : ObjectProperty C} (hP : ∀ (Q : C), P Q → Projective Q) {d : ℕ} {X : C} (hX : P.IsSyzygy d X) (Y : C) [HasInjectiveDimensionLE Y d] (n : ℕ) (e : Abelian.Ext X Y (n + 1)) : e = 0

A d-th syzygy has no higher extensions into an object of injective dimension at most d.