Syzygies relative to a property of objects

Let P be a property of objects of a category with zero morphisms, such as being a finitely generated projective module. An object X is a k-th syzygy relative to P when there is an exact sequence 0 ⟶ X ⟶ Q₁ ⟶ ⋯ ⟶ Q_k with every Qᵢ satisfying P. It is defined by recursion on k: every object is a 0-th syzygy, and X is a (k + 1)-st syzygy when it is the first term of a short exact sequence 0 ⟶ X ⟶ Q ⟶ X' ⟶ 0 with P Q and X' a k-th syzygy. Splicing these short exact sequences gives the long exact sequence, ending in an epimorphism onto the last cokernel; so for the projective objects of an abelian category, the k-th syzygies are the objects of the form Ωᵏ N.

Main definitions

• CategoryTheory.ObjectProperty.IsSyzygy P k: the k-th syzygies relative to P.

Main results

• CategoryTheory.ObjectProperty.isSyzygy_succ_iff: the recursive description.
• CategoryTheory.ObjectProperty.IsSyzygy.of_succ: a (k + 1)-st syzygy is a k-th syzygy.
• CategoryTheory.ObjectProperty.IsSyzygy.map: functors preserving short exact sequences preserve syzygies.
• The k-th syzygies are closed under isomorphisms.

References

• M. Auslander, M. Bridger, Stable module theory, Mem. Amer. Math. Soc. 94 (1969), §2.

def CategoryTheory.ObjectProperty.IsSyzygy {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : ℕ → ObjectProperty C

k-th syzygies relative to P: every object is a 0-th syzygy, and X is a (k + 1)-st syzygy when there is a short exact sequence 0 ⟶ X ⟶ Q ⟶ X' ⟶ 0 with P Q and X' a k-th syzygy.

@[simp]

theorem CategoryTheory.ObjectProperty.isSyzygy_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) (X : C) : P.IsSyzygy 0 X

Every object is a 0-th syzygy.

theorem CategoryTheory.ObjectProperty.isSyzygy_succ_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) (k : ℕ) (X : C) : P.IsSyzygy (k + 1) X ↔ ∃ (S : ShortComplex C), S.ShortExact ∧ Nonempty (X ≅ S.X₁) ∧ P S.X₂ ∧ P.IsSyzygy k S.X₃

X is a (k + 1)-st syzygy exactly when it is the first term of a short exact sequence whose middle term satisfies P and whose last term is a k-th syzygy.

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsIsSyzygy {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) (k : ℕ) : (P.IsSyzygy k).IsClosedUnderIsomorphisms

theorem CategoryTheory.ObjectProperty.IsSyzygy.of_succ {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} {k : ℕ} {X : C} (h : P.IsSyzygy (k + 1) X) : P.IsSyzygy k X

A (k + 1)-st syzygy is a k-th syzygy.

theorem CategoryTheory.ObjectProperty.IsSyzygy.of_le {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} {k l : ℕ} (hlk : l ≤ k) {X : C} (h : P.IsSyzygy k X) : P.IsSyzygy l X

A k-th syzygy is an l-th syzygy for every l ≤ k.

theorem CategoryTheory.ObjectProperty.IsSyzygy.map {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} {D : Type u_1} [Category.{v_1, u_1} D] [Limits.HasZeroMorphisms D] {P' : ObjectProperty D} (F : Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) (hP : ∀ (Q : C), P Q → P' (F.obj Q)) {k : ℕ} {X : C} (h : P.IsSyzygy k X) : P'.IsSyzygy k (F.obj X)

Syzygies are preserved by functors that preserve short exact sequences and send objects of P to objects of P'.