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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.Exact (CategoryTheory.Projective.d f) f

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

def CategoryTheory.preservesFiniteColimitsPreadditiveCoyonedaObjOfProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) [hP : CategoryTheory.Projective P] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj (Opposite.op P))

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

theorem CategoryTheory.projective_of_preservesFiniteColimits_preadditiveCoyonedaObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) [hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj (Opposite.op P))] : CategoryTheory.Projective P

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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) (n : ℕ) : HomologicalComplex.X (CategoryTheory.ProjectiveResolution.ofComplex Z) n = (ChainComplex.mkAux (CategoryTheory.Projective.over Z) (CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z)) (CategoryTheory.Projective.syzygies (CategoryTheory.Projective.d (CategoryTheory.Projective.π Z))) (CategoryTheory.Projective.d (CategoryTheory.Projective.π Z)) (CategoryTheory.Projective.d (CategoryTheory.Projective.d (CategoryTheory.Projective.π Z))) (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Projective.syzygies { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd, snd := { fst := CategoryTheory.Projective.d { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd, snd := (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.d { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd) { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd = 0) } }.snd.fst { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) (i : ℕ) (j : ℕ) : HomologicalComplex.d (CategoryTheory.ProjectiveResolution.ofComplex Z) i j = if h : i = j + 1 then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (ChainComplex.mkAux (CategoryTheory.Projective.over Z) (CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z)) (CategoryTheory.Projective.syzygies (CategoryTheory.Projective.d (CategoryTheory.Projective.π Z))) (CategoryTheory.Projective.d (CategoryTheory.Projective.π Z)) (CategoryTheory.Projective.d (CategoryTheory.Projective.d (CategoryTheory.Projective.π Z))) (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Projective.syzygies { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd, snd := { fst := CategoryTheory.Projective.d { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd, snd := (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.d { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd) { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd = 0) } }.snd.fst { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.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.Projective.over Z) (CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z)) (CategoryTheory.Projective.syzygies (CategoryTheory.Projective.d (CategoryTheory.Projective.π Z))) (CategoryTheory.Projective.d (CategoryTheory.Projective.π Z)) (CategoryTheory.Projective.d (CategoryTheory.Projective.d (CategoryTheory.Projective.π Z))) (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Projective.syzygies { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd, snd := { fst := CategoryTheory.Projective.d { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd, snd := (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.d { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd) { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd = 0) } }.snd.fst { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.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.Projective.over Z) (CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z)) (CategoryTheory.Projective.syzygies (CategoryTheory.Projective.d (CategoryTheory.Projective.π Z))) (CategoryTheory.Projective.d (CategoryTheory.Projective.π Z)) (CategoryTheory.Projective.d (CategoryTheory.Projective.d (CategoryTheory.Projective.π Z))) (_ : CategoryTheory.CategoryStruct.comp { fst := CategoryTheory.Projective.syzygies { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd, snd := { fst := CategoryTheory.Projective.d { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd, snd := (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.d { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd) { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.2.snd = 0) } }.snd.fst { fst := CategoryTheory.Projective.over Z, snd := { fst := CategoryTheory.Projective.syzygies (CategoryTheory.Projective.π Z), snd := CategoryTheory.Projective.d (CategoryTheory.Projective.π Z) } }.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

def CategoryTheory.ProjectiveResolution.ofComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) : ChainComplex C ℕ

Auxiliary definition for ProjectiveResolution.of.

theorem CategoryTheory.ProjectiveResolution.ofComplex_sq_10_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) : CategoryTheory.CategoryStruct.comp 0 (HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) 1 0) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d (CategoryTheory.ProjectiveResolution.ofComplex Z) 1 0) (CategoryTheory.Projective.π Z)

theorem CategoryTheory.ProjectiveResolution.exact_ofComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) (n : ℕ) : CategoryTheory.Exact (HomologicalComplex.d (CategoryTheory.ProjectiveResolution.ofComplex Z) (n + 2) (n + 1)) (HomologicalComplex.d (CategoryTheory.ProjectiveResolution.ofComplex Z) (n + 1) n)

theorem CategoryTheory.ProjectiveResolution.of_def {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) : CategoryTheory.ProjectiveResolution.of Z = CategoryTheory.ProjectiveResolution.mk (CategoryTheory.ProjectiveResolution.ofComplex Z) (ChainComplex.mkHom (CategoryTheory.ProjectiveResolution.ofComplex Z) ((ChainComplex.single₀ C).obj Z) (CategoryTheory.Projective.π Z) 0 (_ : CategoryTheory.CategoryStruct.comp 0 (HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) 1 0) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d (CategoryTheory.ProjectiveResolution.ofComplex Z) 1 0) (CategoryTheory.Projective.π Z)) fun n x => { fst := 0, snd := (_ : CategoryTheory.CategoryStruct.comp 0 (HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d (CategoryTheory.ProjectiveResolution.ofComplex Z) (n + 2) (n + 1)) x.snd.fst) }) (_ : CategoryTheory.Exact (HomologicalComplex.d (CategoryTheory.ProjectiveResolution.ofComplex Z) 1 0) (HomologicalComplex.Hom.f (ChainComplex.mkHom (CategoryTheory.ProjectiveResolution.ofComplex Z) ((ChainComplex.single₀ C).obj Z) (CategoryTheory.Projective.π Z) 0 (_ : CategoryTheory.CategoryStruct.comp 0 (HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) 1 0) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d (CategoryTheory.ProjectiveResolution.ofComplex Z) 1 0) (CategoryTheory.Projective.π Z)) fun n x => { fst := 0, snd := (_ : CategoryTheory.CategoryStruct.comp 0 (HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d (CategoryTheory.ProjectiveResolution.ofComplex Z) (n + 2) (n + 1)) x.snd.fst) }) 0)) (_ : ∀ (n : ℕ), CategoryTheory.Exact (HomologicalComplex.d (CategoryTheory.ProjectiveResolution.ofComplex Z) (n + 2) (n + 1)) (HomologicalComplex.d (CategoryTheory.ProjectiveResolution.ofComplex Z) (n + 1) n))

@[irreducible]

def CategoryTheory.ProjectiveResolution.of {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) : CategoryTheory.ProjectiveResolution Z

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

instance CategoryTheory.ProjectiveResolution.instHasProjectiveResolutionHasZeroObjectPreadditiveHasZeroMorphismsToPreadditiveHasEqualizersHasImages_of_hasStrongEpiMonoFactorisationsInstHasStrongEpiMonoFactorisations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (Z : C) : CategoryTheory.HasProjectiveResolution Z

instance CategoryTheory.ProjectiveResolution.instHasProjectiveResolutionsHasZeroObjectPreadditiveHasZeroMorphismsToPreadditiveHasEqualizersHasImages_of_hasStrongEpiMonoFactorisationsInstHasStrongEpiMonoFactorisations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] : CategoryTheory.HasProjectiveResolutions C

def HomologicalComplex.Hom.toSingle₀ProjectiveResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : ChainComplex C ℕ} {Y : C} (f : X ⟶ (ChainComplex.single₀ C).obj Y) [QuasiIso f] (H : ∀ (n : ℕ), CategoryTheory.Projective (HomologicalComplex.X X n)) : CategoryTheory.ProjectiveResolution Y

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.