theorem proposition_23_57 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {M N : C} (f : M ⟶ N) (P : CategoryTheory.ProjectiveResolution M) (Q : CategoryTheory.ProjectiveResolution N) : (∃ (α : P.complex ⟶ Q.complex), CategoryTheory.CategoryStruct.comp α Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)) ∧ ∀ (g h : P.complex ⟶ Q.complex), CategoryTheory.CategoryStruct.comp g Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f) → CategoryTheory.CategoryStruct.comp h Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f) → Nonempty (Homotopy g h)

theorem proposition_23_57_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {M N : C} (f : M ⟶ N) (I : CategoryTheory.InjectiveResolution M) (J : CategoryTheory.InjectiveResolution N) : (∃ (α : I.cocomplex ⟶ J.cocomplex), CategoryTheory.CategoryStruct.comp I.ι α = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) J.ι) ∧ ∀ (g h : I.cocomplex ⟶ J.cocomplex), CategoryTheory.CategoryStruct.comp I.ι g = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) J.ι → CategoryTheory.CategoryStruct.comp I.ι h = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) J.ι → Nonempty (Homotopy g h)

theorem resolution_comparison_unique_up_to_homotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {M N : C} (f : M ⟶ N) (P : CategoryTheory.ProjectiveResolution M) (Q : CategoryTheory.ProjectiveResolution N) (I : CategoryTheory.InjectiveResolution M) (J : CategoryTheory.InjectiveResolution N) : ((∃ (α : P.complex ⟶ Q.complex), CategoryTheory.CategoryStruct.comp α Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)) ∧ ∀ (g h : P.complex ⟶ Q.complex), CategoryTheory.CategoryStruct.comp g Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f) → CategoryTheory.CategoryStruct.comp h Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f) → Nonempty (Homotopy g h)) ∧ (∃ (α : I.cocomplex ⟶ J.cocomplex), CategoryTheory.CategoryStruct.comp I.ι α = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) J.ι) ∧ ∀ (g h : I.cocomplex ⟶ J.cocomplex), CategoryTheory.CategoryStruct.comp I.ι g = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) J.ι → CategoryTheory.CategoryStruct.comp I.ι h = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) J.ι → Nonempty (Homotopy g h)