# mathlibdocumentation

category_theory.abelian.projective

# 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.

theorem category_theory.exact_d_f {C : Type u} {X Y : C} (f : X Y) :

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.

@[simp]
theorem category_theory.ProjectiveResolution.of_complex_d {C : Type u} (Z : C) (i j : ) :
= dite (i = j + 1) (λ (h : i = j + 1), (category_theory.ProjectiveResolution.of_complex._match_1 .fst (category_theory.ProjectiveResolution.of_complex._match_1 .snd.fst _ (λ (t : Σ' (X₀ X₁ X₂ : C) (d₀ : X₁ X₀) (d₁ : X₂ X₁), d₁ d₀ = 0), category_theory.ProjectiveResolution.of_complex._match_1 t.snd.fst, t.snd.snd.fst, t.snd.snd.snd.snd.fst⟩) j).d₀) (λ (h : ¬i = j + 1), 0)

Auxiliary definition for ProjectiveResolution.of.

Equations
• = (λ (_x : Σ (X₀ X₁ : C), X₁ X₀), category_theory.ProjectiveResolution.of_complex._match_1 _x)
• category_theory.ProjectiveResolution.of_complex._match_1 X, Y, f⟩ =
@[simp]
theorem category_theory.ProjectiveResolution.of_complex_X {C : Type u} (Z : C) (n : ) :
= (category_theory.ProjectiveResolution.of_complex._match_1 .fst (category_theory.ProjectiveResolution.of_complex._match_1 .snd.fst _ (λ (t : Σ' (X₀ X₁ X₂ : C) (d₀ : X₁ X₀) (d₁ : X₂ X₁), d₁ d₀ = 0), category_theory.ProjectiveResolution.of_complex._match_1 t.snd.fst, t.snd.snd.fst, t.snd.snd.snd.snd.fst⟩) n).X₀

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

Equations
@[instance]
@[instance]