Commit 2023-05-26 17:27 c9d630c0

View on Github →

feat: port CategoryTheory.Abelian.Projective (#4322)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

Created Mathlib/CategoryTheory/Abelian/Projective.lean

added theorem CategoryTheory.ProjectiveResolution.exact_ofComplex

added def CategoryTheory.ProjectiveResolution.ofComplex

added theorem CategoryTheory.ProjectiveResolution.ofComplex_sq_10_comm

added theorem CategoryTheory.exact_d_f

added def CategoryTheory.preservesFiniteColimitsPreadditiveCoyonedaObjOfProjective

added theorem CategoryTheory.projective_of_preservesFiniteColimits_preadditiveCoyonedaObj

added def HomologicalComplex.Hom.toSingle₀ProjectiveResolution