Abelian categories with enough projectives have projective resolutions #

When C is abelian projective.d f and f are exact. Hence, starting from an epimorphism P ⟶ X, where P is projective, we can apply projective.d repeatedly to obtain a projective resolution of X.

source

theorem category_theory.exact_d_f {C : Type u} [category_theory.category C] [category_theory.enough_projectives C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :

category_theory.exact (category_theory.projective.d f) f

When C is abelian, projective.d f and f are exact.

Our goal is to define ProjectiveResolution.of Z : ProjectiveResolution Z. The 0-th object in this resolution will just be projective.over Z, i.e. an arbitrarily chosen projective object with a map to Z. After that, we build the n+1-st object as projective.syzygies applied to the previously constructed morphism, and the map to the n-th object as projective.d.

source

@[simp]

theorem category_theory.ProjectiveResolution.of_complex_d {C : Type u} [category_theory.category C] [category_theory.abelian C] [category_theory.enough_projectives C] (Z : C) (i j : ℕ) :

source

noncomputable def category_theory.ProjectiveResolution.of_complex {C : Type u} [category_theory.category C] [category_theory.abelian C] [category_theory.enough_projectives C] (Z : C) :

chain_complex C ℕ

Auxiliary definition for ProjectiveResolution.of.

Equations

category_theory.ProjectiveResolution.of_complex Z = chain_complex.mk' (category_theory.projective.over Z) (category_theory.projective.syzygies (category_theory.projective.π Z)) (category_theory.projective.d (category_theory.projective.π Z)) (λ (_x : Σ (X₀ X₁ : C), X₁ ⟶ X₀), category_theory.ProjectiveResolution.of_complex._match_1 _x)
category_theory.ProjectiveResolution.of_complex._match_1 ⟨X, ⟨Y, f⟩⟩ = ⟨category_theory.projective.syzygies f _, ⟨category_theory.projective.d f _, _⟩⟩

source

@[simp]

theorem category_theory.ProjectiveResolution.of_complex_X {C : Type u} [category_theory.category C] [category_theory.abelian C] [category_theory.enough_projectives C] (Z : C) (n : ℕ) :

source

@[irreducible]

noncomputable def category_theory.ProjectiveResolution.of {C : Type u} [category_theory.category C] [category_theory.abelian C] [category_theory.enough_projectives C] (Z : C) :

category_theory.ProjectiveResolution Z

In any abelian category with enough projectives, ProjectiveResolution.of Z constructs a projective resolution of the object Z.

Equations

category_theory.ProjectiveResolution.of Z = {complex := category_theory.ProjectiveResolution.of_complex Z, π := (category_theory.ProjectiveResolution.of_complex Z).mk_hom ((chain_complex.single₀ C).obj Z) (category_theory.projective.π Z) 0 _ (λ (n : ℕ) (_x : Σ' (f : (category_theory.ProjectiveResolution.of_complex Z).X n ⟶ ((chain_complex.single₀ C).obj Z).X n) (f' : (category_theory.ProjectiveResolution.of_complex Z).X (n + 1) ⟶ ((chain_complex.single₀ C).obj Z).X (n + 1)), f' ≫ ((chain_complex.single₀ C).obj Z).d (n + 1) n = (category_theory.ProjectiveResolution.of_complex Z).d (n + 1) n ≫ f), ⟨0, _⟩), projective := _, exact₀ := _, exact := _, epi := _}

source

@[protected, instance]

def category_theory.ProjectiveResolution.category_theory.has_projective_resolution {C : Type u} [category_theory.category C] [category_theory.abelian C] [category_theory.enough_projectives C] (Z : C) :

category_theory.has_projective_resolution Z

source

@[protected, instance]

def category_theory.ProjectiveResolution.category_theory.has_projective_resolutions {C : Type u} [category_theory.category C] [category_theory.abelian C] [category_theory.enough_projectives C] :

category_theory.has_projective_resolutions C