noncomputable def ext_well_defined {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {M A : C} (P Q : CategoryTheory.ProjectiveResolution M) (n : ℕ) : CochainComplex.HomComplex.CohomologyClass P.cochainComplex ((CochainComplex.singleFunctor C 0).obj A) ↑n ≃+ CochainComplex.HomComplex.CohomologyClass Q.cochainComplex ((CochainComplex.singleFunctor C 0).obj A) ↑n