Abelian categories with enough projectives have projective resolutions

Main results

When the underlying category is abelian:

• CategoryTheory.ProjectiveResolution.lift: Given P : ProjectiveResolution X and Q : ProjectiveResolution Y, any morphism X ⟶ Y admits a lifting to a chain map P.complex ⟶ Q.complex. It is a lifting in the sense that P.ι intertwines the lift and the original morphism, see CategoryTheory.ProjectiveResolution.lift_commutes.

• CategoryTheory.ProjectiveResolution.liftHomotopy: Any two such descents are homotopic.

• CategoryTheory.ProjectiveResolution.homotopyEquiv: Any two projective resolutions of the same object are homotopy equivalent.

• CategoryTheory.projectiveResolutions: If every object admits a projective resolution, we can construct a functor projectiveResolutions C : C ⥤ HomotopyCategory C (ComplexShape.down ℕ).

• CategoryTheory.exact_d_f: Projective.d f and f are exact.

• CategoryTheory.ProjectiveResolution.of: Hence, starting from an epimorphism P ⟶ X, where P is projective, we can apply Projective.d repeatedly to obtain a projective resolution of X.

noncomputable def CategoryTheory.ProjectiveResolution.liftFZero {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y) (Q : ProjectiveResolution Z) : P.complex.X 0 ⟶ Q.complex.X 0

Auxiliary construction for lift.

theorem CategoryTheory.ProjectiveResolution.exact₀ {C : Type u} [Category.{v, u} C] [Abelian C] {Z : C} (P : ProjectiveResolution Z) : { X₁ := P.complex.X 1, X₂ := P.complex.X 0, X₃ := ((ChainComplex.single₀ C).obj Z).X 0, f := P.complex.d 1 0, g := P.π.f 0, zero := ⋯ }.Exact

noncomputable def CategoryTheory.ProjectiveResolution.liftFOne {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y) (Q : ProjectiveResolution Z) : P.complex.X 1 ⟶ Q.complex.X 1

Auxiliary construction for lift.

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftFOne_zero_comm {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y) (Q : ProjectiveResolution Z) : CategoryStruct.comp (liftFOne f P Q) (Q.complex.d 1 0) = CategoryStruct.comp (P.complex.d 1 0) (liftFZero f P Q)

noncomputable def CategoryTheory.ProjectiveResolution.liftFSucc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (P : ProjectiveResolution Y) (Q : ProjectiveResolution Z) (n : ℕ) (g : P.complex.X n ⟶ Q.complex.X n) (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 1)) (w : CategoryStruct.comp g' (Q.complex.d (n + 1) n) = CategoryStruct.comp (P.complex.d (n + 1) n) g) : (g'' : P.complex.X (n + 2) ⟶ Q.complex.X (n + 2)) ×' CategoryStruct.comp g'' (Q.complex.d (n + 2) (n + 1)) = CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g'

Auxiliary construction for lift.

noncomputable def CategoryTheory.ProjectiveResolution.lift {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y) (Q : ProjectiveResolution Z) : P.complex ⟶ Q.complex

A morphism in C lift to a chain map between projective resolutions.

@[simp]

theorem CategoryTheory.ProjectiveResolution.lift_commutes {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y) (Q : ProjectiveResolution Z) : CategoryStruct.comp (lift f P Q) Q.π = CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)

The resolution maps intertwine the lift of a morphism and that morphism.

@[simp]

theorem CategoryTheory.ProjectiveResolution.lift_commutes_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y) (Q : ProjectiveResolution Z) {Z✝ : ChainComplex C ℕ} (h : (ChainComplex.single₀ C).obj Z ⟶ Z✝) : CategoryStruct.comp (lift f P Q) (CategoryStruct.comp Q.π h) = CategoryStruct.comp P.π (CategoryStruct.comp ((ChainComplex.single₀ C).map f) h)

@[simp]

theorem CategoryTheory.ProjectiveResolution.lift_commutes_zero {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y) (Q : ProjectiveResolution Z) : CategoryStruct.comp ((lift f P Q).f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f

@[simp]

theorem CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y) (Q : ProjectiveResolution Z) {Z✝ : C} (h : ((ChainComplex.single₀ C).obj Z).X 0 ⟶ Z✝) : CategoryStruct.comp ((lift f P Q).f 0) (CategoryStruct.comp (Q.π.f 0) h) = CategoryStruct.comp (P.π.f 0) (CategoryStruct.comp f h)

noncomputable def CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp f Q.π = 0) : P.complex.X 0 ⟶ Q.complex.X 1

An auxiliary definition for liftHomotopyZero.

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp f Q.π = 0) : CategoryStruct.comp (liftHomotopyZeroZero f comm) (Q.complex.d 1 0) = f.f 0

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp f Q.π = 0) {Z✝ : C} (h : Q.complex.X 0 ⟶ Z✝) : CategoryStruct.comp (liftHomotopyZeroZero f comm) (CategoryStruct.comp (Q.complex.d 1 0) h) = CategoryStruct.comp (f.f 0) h

noncomputable def CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp f Q.π = 0) : P.complex.X 1 ⟶ Q.complex.X 2

An auxiliary definition for liftHomotopyZero.

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp f Q.π = 0) : CategoryStruct.comp (liftHomotopyZeroOne f comm) (Q.complex.d 2 1) = f.f 1 - CategoryStruct.comp (P.complex.d 1 0) (liftHomotopyZeroZero f comm)

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp f Q.π = 0) {Z✝ : C} (h : Q.complex.X 1 ⟶ Z✝) : CategoryStruct.comp (liftHomotopyZeroOne f comm) (CategoryStruct.comp (Q.complex.d 2 1) h) = CategoryStruct.comp (f.f 1 - CategoryStruct.comp (P.complex.d 1 0) (liftHomotopyZeroZero f comm)) h

noncomputable def CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (n : ℕ) (g : P.complex.X n ⟶ Q.complex.X (n + 1)) (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) (w : f.f (n + 1) = CategoryStruct.comp (P.complex.d (n + 1) n) g + CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1))) : P.complex.X (n + 2) ⟶ Q.complex.X (n + 3)

An auxiliary definition for liftHomotopyZero.

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc_comp {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (n : ℕ) (g : P.complex.X n ⟶ Q.complex.X (n + 1)) (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) (w : f.f (n + 1) = CategoryStruct.comp (P.complex.d (n + 1) n) g + CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1))) : CategoryStruct.comp (liftHomotopyZeroSucc f n g g' w) (Q.complex.d (n + 3) (n + 2)) = f.f (n + 2) - CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g'

@[simp]

theorem CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc_comp_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (n : ℕ) (g : P.complex.X n ⟶ Q.complex.X (n + 1)) (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) (w : f.f (n + 1) = CategoryStruct.comp (P.complex.d (n + 1) n) g + CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1))) {Z✝ : C} (h : Q.complex.X (n + 2) ⟶ Z✝) : CategoryStruct.comp (liftHomotopyZeroSucc f n g g' w) (CategoryStruct.comp (Q.complex.d (n + 3) (n + 2)) h) = CategoryStruct.comp (f.f (n + 2) - CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g') h

noncomputable def CategoryTheory.ProjectiveResolution.liftHomotopyZero {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp f Q.π = 0) : Homotopy f 0

Any lift of the zero morphism is homotopic to zero.

noncomputable def CategoryTheory.ProjectiveResolution.liftHomotopy {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (f : Y ⟶ Z) {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z} (g h : P.complex ⟶ Q.complex) (g_comm : CategoryStruct.comp g Q.π = CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)) (h_comm : CategoryStruct.comp h Q.π = CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)) : Homotopy g h

Two lifts of the same morphism are homotopic.

noncomputable def CategoryTheory.ProjectiveResolution.liftIdHomotopy {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (P : ProjectiveResolution X) : Homotopy (lift (CategoryStruct.id X) P P) (CategoryStruct.id P.complex)

The lift of the identity morphism is homotopic to the identity chain map.

noncomputable def CategoryTheory.ProjectiveResolution.liftCompHomotopy {C : Type u} [Category.{v, u} C] [Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (R : ProjectiveResolution Z) : Homotopy (lift (CategoryStruct.comp f g) P R) (CategoryStruct.comp (lift f P Q) (lift g Q R))

The lift of a composition is homotopic to the composition of the lifts.

noncomputable def CategoryTheory.ProjectiveResolution.homotopyEquiv {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (P Q : ProjectiveResolution X) : HomotopyEquiv P.complex Q.complex

Any two projective resolutions are homotopy equivalent.

@[simp]

theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (P Q : ProjectiveResolution X) : CategoryStruct.comp (P.homotopyEquiv Q).hom Q.π = P.π

@[simp]

theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (P Q : ProjectiveResolution X) {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : (ChainComplex.single₀ C).obj X ⟶ Z) : CategoryStruct.comp (P.homotopyEquiv Q).hom (CategoryStruct.comp Q.π h) = CategoryStruct.comp P.π h

@[simp]

theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (P Q : ProjectiveResolution X) : CategoryStruct.comp (P.homotopyEquiv Q).inv P.π = Q.π

@[simp]

theorem CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (P Q : ProjectiveResolution X) {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : (ChainComplex.single₀ C).obj X ⟶ Z) : CategoryStruct.comp (P.homotopyEquiv Q).inv (CategoryStruct.comp P.π h) = CategoryStruct.comp Q.π h

@[reducible, inline]

noncomputable abbrev CategoryTheory.projectiveResolution {C : Type u} [Category.{v, u} C] (Z : C) [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] [HasProjectiveResolution Z] : ProjectiveResolution Z

An arbitrarily chosen projective resolution of an object.

noncomputable def CategoryTheory.projectiveResolutions (C : Type u) [Category.{v, u} C] [Abelian C] [HasProjectiveResolutions C] : Functor C (HomotopyCategory C (ComplexShape.down ℕ))

Taking projective resolutions is functorial, if considered with target the homotopy category (ℕ-indexed chain complexes and chain maps up to homotopy).

noncomputable def CategoryTheory.ProjectiveResolution.iso {C : Type u} [Category.{v, u} C] [Abelian C] [HasProjectiveResolutions C] {X : C} (P : ProjectiveResolution X) : (projectiveResolutions C).obj X ≅ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj P.complex

If P : ProjectiveResolution X, then the chosen (projectiveResolutions C).obj X is isomorphic (in the homotopy category) to P.complex.

theorem CategoryTheory.ProjectiveResolution.iso_inv_naturality {C : Type u} [Category.{v, u} C] [Abelian C] [HasProjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) : CategoryStruct.comp P.iso.inv ((projectiveResolutions C).map f) = CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) Q.iso.inv

theorem CategoryTheory.ProjectiveResolution.iso_inv_naturality_assoc {C : Type u} [Category.{v, u} C] [Abelian C] [HasProjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) {Z : HomotopyCategory C (ComplexShape.down ℕ)} (h : (projectiveResolutions C).obj Y ⟶ Z) : CategoryStruct.comp P.iso.inv (CategoryStruct.comp ((projectiveResolutions C).map f) h) = CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) (CategoryStruct.comp Q.iso.inv h)

theorem CategoryTheory.ProjectiveResolution.iso_hom_naturality {C : Type u} [Category.{v, u} C] [Abelian C] [HasProjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) : CategoryStruct.comp ((projectiveResolutions C).map f) Q.iso.hom = CategoryStruct.comp P.iso.hom ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ)

theorem CategoryTheory.ProjectiveResolution.iso_hom_naturality_assoc {C : Type u} [Category.{v, u} C] [Abelian C] [HasProjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) {Z : HomotopyCategory C (ComplexShape.down ℕ)} (h : (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj Q.complex ⟶ Z) : CategoryStruct.comp ((projectiveResolutions C).map f) (CategoryStruct.comp Q.iso.hom h) = CategoryStruct.comp P.iso.hom (CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) h)

theorem CategoryTheory.exact_d_f {C : Type u} [Category.{v, u} C] [Abelian C] [EnoughProjectives C] {X Y : C} (f : X ⟶ Y) : { X₁ := Projective.syzygies f, X₂ := X, X₃ := Y, f := Projective.d f, g := f, zero := ⋯ }.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 from the n-th object as Projective.d.

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

Auxiliary definition for ProjectiveResolution.of.

theorem CategoryTheory.ProjectiveResolution.ofComplex_d_1_0 {C : Type u} [Category.{v, u} C] [Abelian C] [EnoughProjectives C] (Z : C) : (ofComplex Z).d 1 0 = Projective.d (Projective.π Z)

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

instance CategoryTheory.ProjectiveResolution.instProjectiveXNatOfComplex {C : Type u} [Category.{v, u} C] [Abelian C] [EnoughProjectives C] (Z : C) (n : ℕ) : Projective ((ofComplex Z).X n)

@[irreducible]

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

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

theorem CategoryTheory.ProjectiveResolution.of_def {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] [EnoughProjectives C] (Z : C) : of Z = { complex := ofComplex Z, projective := ⋯, hasHomology := ⋯, π := ((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩, quasiIso := ⋯ }

@[instance 100]

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

@[instance 100]

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