Commit 2023-05-25 15:08 e425f617

View on Github →

feat: port CategoryTheory.Abelian.RightDerived (#4284)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Abelian/RightDerived.lean

added theorem CategoryTheory.Abelian.Functor.exact_of_map_injectiveResolution

added theorem CategoryTheory.Abelian.Functor.preserves_exact_of_preservesFiniteLimits_of_mono

added def CategoryTheory.Abelian.Functor.rightDerivedZeroIsoSelf

added def CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfApp

added def CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppInv

added theorem CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppInv_comp

added def CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfAppIso

added theorem CategoryTheory.Abelian.Functor.rightDerivedZeroToSelfApp_comp_inv

added theorem CategoryTheory.Abelian.Functor.rightDerivedZeroToSelf_natural

added def CategoryTheory.Functor.rightDerived

added def CategoryTheory.Functor.rightDerivedObjInjectiveSucc

added def CategoryTheory.Functor.rightDerivedObjInjectiveZero

added def CategoryTheory.Functor.rightDerivedObjIso

added theorem CategoryTheory.Functor.rightDerived_map_eq

added def CategoryTheory.NatTrans.rightDerived

added theorem CategoryTheory.NatTrans.rightDerived_comp

added theorem CategoryTheory.NatTrans.rightDerived_eq

added theorem CategoryTheory.NatTrans.rightDerived_id