# Documentation

Mathlib.CategoryTheory.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 CategoryTheory.exact_d_f {C : Type u} {X : C} {Y : C} (f : X Y) :

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

The preadditive Co-Yoneda functor on P preserves colimits if P is projective.

Instances For

An object is projective if its preadditive Co-Yoneda functor preserves finite colimits.

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 CategoryTheory.ProjectiveResolution.ofComplex_X {C : Type u} (Z : C) (n : ) :
= (ChainComplex.mkAux () () () () () (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Projective.syzygies { fst := , snd := }.2.snd, snd := { fst := CategoryTheory.Projective.d { fst := , snd := }.2.snd, snd := (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.d { fst := , snd := }.2.snd) { fst := , snd := }.2.snd = 0) } }.snd.fst { fst := , snd := }.snd.snd = 0) (fun t => { fst := CategoryTheory.Projective.syzygies t.snd.snd.snd.snd.fst, snd := { fst := CategoryTheory.Projective.d t.snd.snd.snd.snd.fst, snd := (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.d t.snd.snd.snd.snd.fst) t.snd.snd.snd.snd.fst = 0) } }) n).X₀
@[simp]
theorem CategoryTheory.ProjectiveResolution.ofComplex_d {C : Type u} (Z : C) (i : ) (j : ) :
= if h : i = j + 1 then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (ChainComplex.mkAux () () () () () (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Projective.syzygies { fst := , snd := }.2.snd, snd := { fst := CategoryTheory.Projective.d { fst := , snd := }.2.snd, snd := (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.d { fst := , snd := { fst := , snd := } }.2.snd) { fst := , snd := { fst := , snd := } }.2.snd = 0) } }.snd.fst { fst := , snd := }.snd.snd = 0) (fun t => { fst := CategoryTheory.Projective.syzygies t.snd.snd.snd.snd.fst, snd := { fst := CategoryTheory.Projective.d t.snd.snd.snd.snd.fst, snd := (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.d t.snd.snd.snd.snd.fst) t.snd.snd.snd.snd.fst = 0) } }) i).X₀ = (ChainComplex.mkAux () () () () () (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Projective.syzygies { fst := , snd := }.2.snd, snd := { fst := CategoryTheory.Projective.d { fst := , snd := }.2.snd, snd := (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.d { fst := , snd := { fst := , snd := } }.2.snd) { fst := , snd := { fst := , snd := } }.2.snd = 0) } }.snd.fst { fst := , snd := }.snd.snd = 0) (fun t => { fst := CategoryTheory.Projective.syzygies t.snd.snd.snd.snd.fst, snd := { fst := CategoryTheory.Projective.d t.snd.snd.snd.snd.fst, snd := (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.d t.snd.snd.snd.snd.fst) t.snd.snd.snd.snd.fst = 0) } }) (j + 1)).X₀)) (ChainComplex.mkAux () () () () () (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Projective.syzygies { fst := , snd := }.2.snd, snd := { fst := CategoryTheory.Projective.d { fst := , snd := }.2.snd, snd := (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.d { fst := , snd := }.2.snd) { fst := , snd := }.2.snd = 0) } }.snd.fst { fst := , snd := }.snd.snd = 0) (fun t => { fst := CategoryTheory.Projective.syzygies t.snd.snd.snd.snd.fst, snd := { fst := CategoryTheory.Projective.d t.snd.snd.snd.snd.fst, snd := (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.d t.snd.snd.snd.snd.fst) t.snd.snd.snd.snd.fst = 0) } }) j).d₀ else 0

Auxiliary definition for ProjectiveResolution.of.

Instances For
theorem CategoryTheory.ProjectiveResolution.of_def {C : Type u_1} [] (Z : C) :
= CategoryTheory.ProjectiveResolution.mk () (ChainComplex.mkHom () (().obj Z) () 0 (_ : CategoryTheory.CategoryStruct.comp 0 (HomologicalComplex.d (().obj Z) 1 0) = ) fun n x => { fst := 0, snd := (_ : CategoryTheory.CategoryStruct.comp 0 (HomologicalComplex.d (().obj Z) (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d () (n + 2) (n + 1)) x.snd.fst) }) (_ : CategoryTheory.Exact () (HomologicalComplex.Hom.f (ChainComplex.mkHom () (().obj Z) () 0 (_ : CategoryTheory.CategoryStruct.comp 0 (HomologicalComplex.d (().obj Z) 1 0) = CategoryTheory.CategoryStruct.comp () ()) fun n x => { fst := 0, snd := (_ : CategoryTheory.CategoryStruct.comp 0 (HomologicalComplex.d (().obj Z) (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d () (n + 2) (n + 1)) x.snd.fst) }) 0)) (_ : ∀ (n : ), CategoryTheory.Exact (HomologicalComplex.d () (n + 2) (n + 1)) ())
@[irreducible]

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

Instances For
def HomologicalComplex.Hom.toSingle₀ProjectiveResolution {C : Type u} {X : } {Y : C} (f : X ().obj Y) [] (H : ∀ (n : ), ) :

If X is a chain complex of projective objects and we have a quasi-isomorphism f : X ⟶ Y[0], then X is a projective resolution of Y.

Instances For