CategoryTheory.ProjectiveResolution.lift_commutes

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

This theorem, named `CategoryTheory.ProjectiveResolution.lift_commutes`, asserts that in an Abelian category `C`, for any two objects `Y` and `Z` in `C` and a morphism `f` from `Y` to `Z`, together with projective resolutions `P` of `Y` and `Q` of `Z`, the composition of the lift of `f` with respect to `P` and `Q` followed by the projection of `Q` is the same as the composition of the projection of `P` and the image of `f` under the functor that creates a chain complex supported in degree zero. This is a statement about the commutativity of a certain diagram in the category of chain complexes.

More concisely: In an Abelian category, for any morphism `f` between objects `Y` and `Z`, and given projective resolutions `P` of `Y` and `Q` of `Z`, the diagram commutes, i.e., (lift of `f` with respect to `P` and `Q`) ∘ projection of `Q` = projection of `P` ∘ `f` (as chain complexes in degree 0).