Commit 2023-05-30 07:31 0e56a9ea

View on Github →

feat: port CategoryTheory.Abelian.LeftDerived (#4477)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Abelian/LeftDerived.lean

added theorem CategoryTheory.Abelian.Functor.exact_of_map_ProjectiveResolution

added def CategoryTheory.Abelian.Functor.leftDerivedZeroIsoSelf

added def CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfApp

added def CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfAppInv

added theorem CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfAppInv_comp

added def CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfAppIso

added theorem CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfApp_comp_inv

added theorem CategoryTheory.Abelian.Functor.leftDerived_zero_to_self_natural

added theorem CategoryTheory.Abelian.Functor.preserves_exact_of_PreservesFiniteColimits_of_epi