Mathlib Changelog
v4
Changelog
About
Github
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